High-contrast homogenization: Provider.Regularity.CorrectorOriginCubeFields

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Corrector fields on integer-scale origin cubes

Projective local gradients restrict canonically to every integer-scale centered cube. This module packages corrector gradients, full gradients, coefficient flux defects, local weak norms, and summable error tails without choosing pointwise representatives.

Restriction to integer-scale origin cubes

noncomputable def HCPolySupport.HighContrast.originCubeL2RestrictLinear {d : ℕ} {n m : ℤ} (hnm : n ≤ m) : ↥(HilbertVectorL2 (openCubeSet (originCube d m))) →ₗ[ℝ] ↥(HilbertVectorL2 (openCubeSet (originCube d n)))

The real linear restriction map for Hilbert-vector L² classes from the scale-m origin cube to the scale-n origin cube, for n ≤ m.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.originCubeL2RestrictLinear_norm_le {d : ℕ} {n m : ℤ} (hnm : n ≤ m) (g : ↥(HilbertVectorL2 (openCubeSet (originCube d m)))) : ‖(originCubeL2RestrictLinear hnm) g‖ ≤ ‖g‖

noncomputable def HCPolySupport.HighContrast.originCubeL2Restrict {d : ℕ} {n m : ℤ} (hnm : n ≤ m) : ↥(HilbertVectorL2 (openCubeSet (originCube d m))) →L[ℝ] ↥(HilbertVectorL2 (openCubeSet (originCube d n)))

Restriction of a Hilbert-vector L² class between nested centered integer-scale origin cubes.

Equations

• HCPolySupport.HighContrast.originCubeL2Restrict hnm = (HCPolySupport.HighContrast.originCubeL2RestrictLinear hnm).mkContinuous 1 ⋯

theorem HCPolySupport.HighContrast.originCubeL2Restrict_coeFn_ae {d : ℕ} {n m : ℤ} (hnm : n ≤ m) (g : ↥(HilbertVectorL2 (openCubeSet (originCube d m)))) : ↑↑((originCubeL2Restrict hnm) g) =ᵐ[volumeMeasureOn (openCubeSet (originCube d n))] ↑↑g

Integer-cube restriction agrees almost everywhere with the original local representative.

@[simp]

theorem HCPolySupport.HighContrast.originCubeL2Restrict_refl {d : ℕ} {n : ℤ} : originCubeL2Restrict ⋯ = ContinuousLinearMap.id ℝ ↥(HilbertVectorL2 (openCubeSet (originCube d n)))

Restriction from an origin cube to itself is the identity.

def HCPolySupport.HighContrast.originCubeCoverGeneration (n : ℤ) : ℕ

The canonical natural exhaustion index covering an integer scale.

Equations

• HCPolySupport.HighContrast.originCubeCoverGeneration n = n.toNat

theorem HCPolySupport.HighContrast.le_originCubeCoverGeneration (n : ℤ) : n ≤ ↑(originCubeCoverGeneration n)

Every integer scale is below its canonical natural cover.

noncomputable def HCPolySupport.HighContrast.LocalGradientCarrier.originCubeComponent {d : ℕ} (G : ↥(LocalGradientCarrier d)) (n : ℤ) : ↥(HilbertVectorL2 (openCubeSet (originCube d n)))

The component of a projective local gradient on an arbitrary integer-scale origin cube.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.LocalGradientCarrier.originCubeComponent_eq_restrict_component {d : ℕ} (G : ↥(LocalGradientCarrier d)) {n : ℤ} (q : ℕ) (hnq : n ≤ ↑q) : originCubeComponent G n = (originCubeL2Restrict hnq) (component G q)

Restricting from any natural exhaustion component covering the target gives the canonical integer component.

@[simp]

theorem HCPolySupport.HighContrast.LocalGradientCarrier.originCubeComponent_natCast {d : ℕ} (G : ↥(LocalGradientCarrier d)) (n : ℕ) : originCubeComponent G ↑n = component G n

On natural scales the integer component is the original projective component.

Quotient-safe local weak norms

theorem HCPolySupport.HighContrast.dualPairing_eq_of_ae_eq_on {d : ℕ} {U : Set (Vec d)} {F G : Vec d → Vec d} (hFG : F =ᵐ[volumeMeasureOn U] G) (psi : Vec d → Vec d) : dualPairing U F psi = dualPairing U G psi

The fail-closed dual pairing depends only on the local a.e. class of its first field.

theorem HCPolySupport.HighContrast.negOneNorm_eq_of_ae_eq_on {d : ℕ} {U : Set (Vec d)} {F G : Vec d → Vec d} (hFG : F =ᵐ[volumeMeasureOn U] G) : negOneNorm U F = negOneNorm U G

The normalized H⁻¹ dual norm depends only on the local a.e. class.

noncomputable def HCPolySupport.HighContrast.localNegOneNorm {d : ℕ} (U : Set (Vec d)) (F : ↥(HilbertVectorL2 U)) : ENNReal

The normalized negative first-order Sobolev norm of a local L² class.

Equations

• HCPolySupport.HighContrast.localNegOneNorm U F = HCPolySupport.HighContrast.negOneNorm U fun (x : HCPolySupport.Vec d) => (↑↑F x).toVec

theorem HCPolySupport.HighContrast.localNegOneNorm_toHilbertVectorL2OfVecField {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : MemVectorL2 U f) : localNegOneNorm U (toHilbertVectorL2OfVecField hf) = negOneNorm U f

The local negative first-order Sobolev norm reads the represented raw field.

Corrector gradients and flux defects

theorem HCPolySupport.HighContrast.memVectorL2_const_originCube {d : ℕ} (e : Vec d) (n : ℤ) : MemVectorL2 (openCubeSet (originCube d n)) fun (x : Vec d) => e

noncomputable def HCPolySupport.HighContrast.correctorGradientOnOriginCube {d : ℕ} (Phi : Vec d → NormalizedLocalH1Carrier d) (e : Vec d) (n : ℤ) : ↥(HilbertVectorL2 (openCubeSet (originCube d n)))

The local corrector-gradient class at an integer scale.

Equations

• HCPolySupport.HighContrast.correctorGradientOnOriginCube Phi e n = HCPolySupport.HighContrast.LocalGradientCarrier.originCubeComponent (Phi e).gradient n

noncomputable def HCPolySupport.HighContrast.constantGradientOnOriginCube {d : ℕ} (e : Vec d) (n : ℤ) : ↥(HilbertVectorL2 (openCubeSet (originCube d n)))

The constant slope as a local Hilbert-vector L² class.

Equations

• HCPolySupport.HighContrast.constantGradientOnOriginCube e n = HCPolySupport.toHilbertVectorL2OfVecField ⋯

noncomputable def HCPolySupport.HighContrast.correctorFullGradientOnOriginCube {d : ℕ} (Phi : Vec d → NormalizedLocalH1Carrier d) (e : Vec d) (n : ℤ) : ↥(HilbertVectorL2 (openCubeSet (originCube d n)))

The full local gradient e + ∇φ_e.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.correctorFullGradientOnOriginCube_eq_of_gradient_eq {d : ℕ} (Phi : Vec d → NormalizedLocalH1Carrier d) (e : Vec d) (n : ℤ) {g : Vec d → Vec d} (hg : MemVectorL2 (openCubeSet (originCube d n)) g) (hgrad : correctorGradientOnOriginCube Phi e n = toHilbertVectorL2OfVecField hg) : correctorFullGradientOnOriginCube Phi e n = toHilbertVectorL2OfVecField ⋯

A raw representative of the corrector gradient gives the literal full gradient class.

noncomputable def HCPolySupport.HighContrast.scalarIdentityCorrectorFluxDefectOnOriginCube {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (Phi : Vec d → NormalizedLocalH1Carrier d) (e : Vec d) (n : ℤ) : ↥(HilbertVectorL2 (openCubeSet (originCube d n)))

The scalar-identity coefficient flux defect a(e + ∇φ_e) - e as a local a.e. class.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.scalarIdentityCorrectorFluxDefectOnOriginCube_toVec_ae {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (Phi : Vec d → NormalizedLocalH1Carrier d) (e : Vec d) (n : ℤ) {g : Vec d → Vec d} (hg : MemVectorL2 (openCubeSet (originCube d n)) g) (hgrad : correctorGradientOnOriginCube Phi e n = toHilbertVectorL2OfVecField hg) : (fun (x : Vec d) => (↑↑(scalarIdentityCorrectorFluxDefectOnOriginCube a Phi e n) x).toVec) =ᵐ[volumeMeasureOn (openCubeSet (originCube d n))] fun (x : Vec d) => matVecMul (Book.Ch03.publicCoeffField (originCube d n) a x) (e + g x) - e

The flux-defect class has the literal raw coefficient-field representative whenever the corrector gradient does.

theorem HCPolySupport.HighContrast.publicCoeffField_originCube_ae_eq_of_le {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) : Book.Ch03.publicCoeffField (originCube d m) a =ᵐ[volumeMeasureOn (openCubeSet (originCube d n))] Book.Ch03.publicCoeffField (originCube d n) a

Compatible public coefficient fields agree almost everywhere on every smaller centered origin cube.

Infinite weak-error tails