High-contrast homogenization: Provider.Regularity.CorrectorLocalLimit

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

Normalized local limits of finite-volume corrector parts

Finite-volume H¹ functions are normalized by subtracting their average on the fixed unit cube. A componentwise Cauchy hypothesis on their normalized local gradients then produces a unique projective local value-gradient limit. The limit contains only compatible almost-everywhere L² classes.

instance HCPolySupport.HighContrast.localGradientCubeFiniteMeasure (d n : ℕ) : MeasureTheory.IsFiniteMeasure (volumeMeasureOn (localGradientCube d n))

Projective scalar-value classes

@[reducible, inline]

noncomputable abbrev HCPolySupport.HighContrast.LocalValueL2 (d n : ℕ) : AddSubgroup (Vec d →ₘ[volumeMeasureOn (localGradientCube d n)] ℝ)

Scalar L² values on one member of the centered cube exhaustion.

Equations

• HCPolySupport.HighContrast.LocalValueL2 d n = HCPolySupport.ScalarL2 (HCPolySupport.HighContrast.localGradientCube d n)

noncomputable def HCPolySupport.HighContrast.localValueRestrictLinear {d m n : ℕ} (hmn : m ≤ n) : ↥(LocalValueL2 d n) →ₗ[ℝ] ↥(LocalValueL2 d m)

The linear restriction of scalar L² classes from the larger local cube to the smaller one.

Equations

• HCPolySupport.HighContrast.localValueRestrictLinear hmn = { toFun := fun (f : ↥(HCPolySupport.HighContrast.LocalValueL2 d n)) => MeasureTheory.MemLp.toLp ↑↑f ⋯, map_add' := ⋯, map_smul' := ⋯ }

theorem HCPolySupport.HighContrast.localValueRestrictLinear_norm_le {d m n : ℕ} (hmn : m ≤ n) (f : ↥(LocalValueL2 d n)) : ‖(localValueRestrictLinear hmn) f‖ ≤ ‖f‖

noncomputable def HCPolySupport.HighContrast.localValueRestrict {d m n : ℕ} (hmn : m ≤ n) : ↥(LocalValueL2 d n) →L[ℝ] ↥(LocalValueL2 d m)

Restriction of a scalar L² class to a smaller exhaustion cube.

Equations

• HCPolySupport.HighContrast.localValueRestrict hmn = (HCPolySupport.HighContrast.localValueRestrictLinear hmn).mkContinuous 1 ⋯

theorem HCPolySupport.HighContrast.localValueRestrict_coeFn_ae {d m n : ℕ} (hmn : m ≤ n) (f : ↥(LocalValueL2 d n)) : ↑↑((localValueRestrict hmn) f) =ᵐ[volumeMeasureOn (localGradientCube d m)] ↑↑f

Restriction agrees almost everywhere with the same scalar representative.

theorem HCPolySupport.HighContrast.norm_localValueRestrict_le {d m n : ℕ} (hmn : m ≤ n) (f : ↥(LocalValueL2 d n)) : ‖(localValueRestrict hmn) f‖ ≤ ‖f‖

Scalar restriction does not increase the L² norm.

noncomputable def HCPolySupport.HighContrast.localValueProjectiveSubmodule (d : ℕ) : Submodule ℝ ((n : ℕ) → ↥(LocalValueL2 d n))

Compatible scalar local classes form the projective value submodule.

Equations

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

@[reducible, inline]

noncomputable abbrev HCPolySupport.HighContrast.LocalValueCarrier (d : ℕ) : Submodule ℝ ((n : ℕ) → ↥(LocalValueL2 d n))

The countable projective carrier for local scalar-value classes.

Equations

• HCPolySupport.HighContrast.LocalValueCarrier d = HCPolySupport.HighContrast.localValueProjectiveSubmodule d

def HCPolySupport.HighContrast.LocalValueCarrier.component {d : ℕ} (f : ↥(LocalValueCarrier d)) (n : ℕ) : ↥(LocalValueL2 d n)

The scalar L² class on one exhaustion cube.

Equations

• HCPolySupport.HighContrast.LocalValueCarrier.component f n = ↑f n

theorem HCPolySupport.HighContrast.LocalValueCarrier.restrict_component {d : ℕ} (f : ↥(LocalValueCarrier d)) {m n : ℕ} (hmn : m ≤ n) : (localValueRestrict hmn) (component f n) = component f m

Projective scalar components agree under restriction.

theorem HCPolySupport.HighContrast.LocalValueCarrier.ext {d : ℕ} {f g : ↥(LocalValueCarrier d)} (h : ∀ (n : ℕ), component f n = component g n) : f = g

A projective scalar value is determined by its local components.

theorem HCPolySupport.HighContrast.LocalValueCarrier.ext_iff {d : ℕ} {f g : ↥(LocalValueCarrier d)} : f = g ↔ ∀ (n : ℕ), component f n = component g n

Fixed-unit normalization

def HCPolySupport.HighContrast.restrictLocalH1 {d m n : ℕ} (hmn : m ≤ n) (u : H1Function (localGradientCube d n)) : H1Function (localGradientCube d m)

Restriction of an H¹ function to a smaller exhaustion cube.

Equations

• HCPolySupport.HighContrast.restrictLocalH1 hmn u = u.restrict ⋯ ⋯

noncomputable def HCPolySupport.HighContrast.normalizeOnUnitCube {d n : ℕ} (u : H1Function (localGradientCube d n)) : H1Function (localGradientCube d n)

Normalize an H¹ function by subtracting its average on cube zero.

Equations

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

theorem HCPolySupport.HighContrast.restrictLocalH1_normalizeOnUnitCube_zero {d n : ℕ} (u : H1Function (localGradientCube d n)) : restrictLocalH1 ⋯ (normalizeOnUnitCube u) = (restrictLocalH1 ⋯ u).subAverage

Fixed-unit normalization restricts on cube zero to ordinary mean subtraction there.

theorem HCPolySupport.HighContrast.normalizeOnUnitCube_meanZero {d n : ℕ} (u : H1Function (localGradientCube d n)) : MeanZeroOn (localGradientCube d 0) (restrictLocalH1 ⋯ (normalizeOnUnitCube u)).toFun

Fixed-unit normalization has zero average on the fixed unit cube.

theorem HCPolySupport.HighContrast.normalizeOnUnitCube_grad {d n : ℕ} (u : H1Function (localGradientCube d n)) : (normalizeOnUnitCube u).grad = u.grad

Fixed-unit normalization leaves the weak gradient unchanged.

noncomputable def HCPolySupport.HighContrast.normalizedLocalH1 {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) (n k : ℕ) : H1Function (localGradientCube d n)

The normalized restriction of the (n+k)th finite-volume function to the nth exhaustion cube.

Equations

• HCPolySupport.HighContrast.normalizedLocalH1 u n k = HCPolySupport.HighContrast.restrictLocalH1 ⋯ (HCPolySupport.HighContrast.normalizeOnUnitCube (u (n + k)))

theorem HCPolySupport.HighContrast.normalizedLocalH1_meanZero {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) (n k : ℕ) : MeanZeroOn (localGradientCube d 0) (restrictLocalH1 ⋯ (normalizedLocalH1 u n k)).toFun

Every normalized local restriction has zero average on cube zero.

theorem HCPolySupport.HighContrast.restrictLocalH1_normalizedLocalH1 {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) {m n : ℕ} (hmn : m ≤ n) (k : ℕ) : restrictLocalH1 hmn (normalizedLocalH1 u n k) = normalizedLocalH1 u m (k + (n - m))

Restricting a normalized tail to a smaller cube is a shifted normalized tail of the smaller local sequence.

The fixed-anchor Poincare bridge

noncomputable def HCPolySupport.HighContrast.anchoredLocalPoincareConstant (d n : ℕ) : ℝ

A positive cube-dependent constant for Poincare with the additive gauge fixed by zero average on cube zero.

Equations

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

theorem HCPolySupport.HighContrast.anchoredLocalPoincareConstant_pos (d n : ℕ) : 0 < anchoredLocalPoincareConstant d n

The fixed-anchor Poincare constant is strictly positive.

theorem HCPolySupport.HighContrast.norm_toScalarL2_le_anchoredLocalPoincareConstant_mul_grad {d n : ℕ} (w : H1Function (localGradientCube d n)) (hmean : MeanZeroOn (localGradientCube d 0) (restrictLocalH1 ⋯ w).toFun) : ‖w.toScalarL2‖ ≤ anchoredLocalPoincareConstant d n * ‖w.gradToHilbertVectorL2‖

Poincare on an outer exhaustion cube, with its additive constant fixed by zero average on cube zero.

def HCPolySupport.HighContrast.NormalizedLocalGradientCauchy {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) : Prop

Normalized finite-volume gradients are Cauchy on every fixed exhaustion cube.

Equations

• HCPolySupport.HighContrast.NormalizedLocalGradientCauchy u = ∀ (n : ℕ), CauchySeq fun (k : ℕ) => (HCPolySupport.HighContrast.normalizedLocalH1 u n k).gradToHilbertVectorL2

theorem HCPolySupport.HighContrast.normalizedLocalValue_cauchy {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) (hgrad : NormalizedLocalGradientCauchy u) (n : ℕ) : CauchySeq fun (k : ℕ) => (normalizedLocalH1 u n k).toScalarL2

The fixed-anchor Poincare estimate upgrades local gradient Cauchy to local scalar-value Cauchy.

noncomputable def HCPolySupport.HighContrast.normalizedLocalPair {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) (n k : ℕ) : ↥(LocalValueL2 d n) × ↥(LocalGradientL2 d n)

The normalized local value-gradient pair on one fixed cube.

Equations

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

theorem HCPolySupport.HighContrast.normalizedLocalPair_cauchy {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) (hgrad : NormalizedLocalGradientCauchy u) (n : ℕ) : CauchySeq (normalizedLocalPair u n)

Normalized local value-gradient pairs are Cauchy under the explicit gradient Cauchy premise.

Projective local-limit assembly

noncomputable def HCPolySupport.HighContrast.normalizedLocalPairLimit {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) (hgrad : NormalizedLocalGradientCauchy u) (n : ℕ) : ↥(LocalValueL2 d n) × ↥(LocalGradientL2 d n)

The unique limit of the normalized value-gradient sequence on one fixed cube.

Equations

• HCPolySupport.HighContrast.normalizedLocalPairLimit u hgrad n = Classical.choose ⋯

theorem HCPolySupport.HighContrast.localValueRestrict_normalizedLocalPairLimit {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) (hgrad : NormalizedLocalGradientCauchy u) {m n : ℕ} (hmn : m ≤ n) : (localValueRestrict hmn) (normalizedLocalPairLimit u hgrad n).1 = (normalizedLocalPairLimit u hgrad m).1

theorem HCPolySupport.HighContrast.localGradientRestrict_normalizedLocalPairLimit {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) (hgrad : NormalizedLocalGradientCauchy u) {m n : ℕ} (hmn : m ≤ n) : (localGradientRestrict hmn) (normalizedLocalPairLimit u hgrad n).2 = (normalizedLocalPairLimit u hgrad m).2

noncomputable def HCPolySupport.HighContrast.normalizedLocalValueLimit {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) (hgrad : NormalizedLocalGradientCauchy u) : ↥(LocalValueCarrier d)

The compatible local L² value limits of the functions normalized by their unit-cube mean.

Equations

• HCPolySupport.HighContrast.normalizedLocalValueLimit u hgrad = ⟨fun (n : ℕ) => (HCPolySupport.HighContrast.normalizedLocalPairLimit u hgrad n).1, ⋯⟩

noncomputable def HCPolySupport.HighContrast.normalizedLocalGradientLimit {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) (hgrad : NormalizedLocalGradientCauchy u) : ↥(LocalGradientCarrier d)

The compatible local L² gradient limits of the normalized functions.

Equations

• HCPolySupport.HighContrast.normalizedLocalGradientLimit u hgrad = ⟨fun (n : ℕ) => (HCPolySupport.HighContrast.normalizedLocalPairLimit u hgrad n).2, ⋯⟩

structure HCPolySupport.HighContrast.NormalizedLocalH1Carrier (d : ℕ) : Type

A normalized local H¹ carrier consists only of compatible local L² value and gradient classes, the closed weak-gradient relation on each cube, and the fixed-unit zero-average condition.

• value : ↥(LocalValueCarrier d)

  The compatible scalar L² classes on the nested local cubes.

• gradient : ↥(LocalGradientCarrier d)

  The compatible gradient L² classes paired with the local values in the closed H¹ graph.

• graph (n : ℕ) : (LocalValueCarrier.component self.value n, LocalGradientCarrier.component self.gradient n) ∈ h1GraphClosedSubmodule
• unitMeanZero : scalarIntegralCLM (LocalValueCarrier.component self.value 0) = 0

def HCPolySupport.HighContrast.NormalizedLocalH1Carrier.valueComponent {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℕ) : ↥(LocalValueL2 d n)

The scalar local component on the nth cube.

Equations

• z.valueComponent n = HCPolySupport.HighContrast.LocalValueCarrier.component z.value n

def HCPolySupport.HighContrast.NormalizedLocalH1Carrier.gradientComponent {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℕ) : ↥(LocalGradientL2 d n)

The weak-gradient local component on the nth cube.

Equations

• z.gradientComponent n = HCPolySupport.HighContrast.LocalGradientCarrier.component z.gradient n

theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.ext {d : ℕ} {z w : NormalizedLocalH1Carrier d} (hvalue : ∀ (n : ℕ), z.valueComponent n = w.valueComponent n) (hgradient : ∀ (n : ℕ), z.gradientComponent n = w.gradientComponent n) : z = w

Normalized local carriers are determined by their value and gradient components.

theorem HCPolySupport.HighContrast.NormalizedLocalH1Carrier.ext_iff {d : ℕ} {z w : NormalizedLocalH1Carrier d} : z = w ↔ (∀ (n : ℕ), z.valueComponent n = w.valueComponent n) ∧ ∀ (n : ℕ), z.gradientComponent n = w.gradientComponent n

theorem HCPolySupport.HighContrast.normalizedLocalPairLimit_mem_h1Graph {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) (hgrad : NormalizedLocalGradientCauchy u) (n : ℕ) : normalizedLocalPairLimit u hgrad n ∈ h1GraphClosedSubmodule

theorem HCPolySupport.HighContrast.normalizedLocalPairLimit_unitMeanZero {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) (hgrad : NormalizedLocalGradientCauchy u) : scalarIntegralCLM (normalizedLocalPairLimit u hgrad 0).1 = 0

noncomputable def HCPolySupport.HighContrast.assembledNormalizedLocalH1Carrier {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) (hgrad : NormalizedLocalGradientCauchy u) : NormalizedLocalH1Carrier d

Assemble the compatible local value and gradient limits with zero integral on the unit cube.

Equations

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

def HCPolySupport.HighContrast.IsNormalizedLocalLimit {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) (z : NormalizedLocalH1Carrier d) : Prop

Literal characterization of a normalized local limit: convergence of the value-gradient pair on every fixed exhaustion cube.

Equations

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

theorem HCPolySupport.HighContrast.existsUnique_normalizedLocalLimit {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) (hgrad : NormalizedLocalGradientCauchy u) : ∃! z : NormalizedLocalH1Carrier d, IsNormalizedLocalLimit u z

Under the explicit local gradient-Cauchy premise, the normalized local limit exists and is unique.

noncomputable def HCPolySupport.HighContrast.normalizedCorrectorLocalLimit {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) (hgrad : NormalizedLocalGradientCauchy u) : NormalizedLocalH1Carrier d

The normalized projective local limit selected from its unique characterization.

Equations

• HCPolySupport.HighContrast.normalizedCorrectorLocalLimit u hgrad = Classical.choose ⋯

theorem HCPolySupport.HighContrast.normalizedCorrectorLocalLimit_isLimit {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) (hgrad : NormalizedLocalGradientCauchy u) : IsNormalizedLocalLimit u (normalizedCorrectorLocalLimit u hgrad)

The selected local limit satisfies the literal componentwise characterization.

theorem HCPolySupport.HighContrast.isNormalizedLocalLimit_iff_eq {d : ℕ} (u : (q : ℕ) → H1Function (localGradientCube d q)) (hgrad : NormalizedLocalGradientCauchy u) (z : NormalizedLocalH1Carrier d) : IsNormalizedLocalLimit u z ↔ z = normalizedCorrectorLocalLimit u hgrad

The literal convergence characterization identifies exactly the selected normalized local limit.