Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch05.Theorems.Section57.HomogenizationErrorMinimalScale

Coarse-graining support: Support.Book.Ch05.Theorems.Section57.HomogenizationErrorMinimalScale #

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Minimal-scale finite-q homogenization-error assembly #

This file contains the deterministic bridge used in the Section 5.7 corollary: pointwise localized J control and pointwise unit-ellipticity control imply a single collapsed bound on \mathcal E_{r,\infty,q}.

source
theorem HCPolySupport.Book.Ch05.Section57.homogenizationErrorOnOriginCube_le_of_minimalScaleUnitJ_and_unitEllipticity {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) {a : RegCoeffField d} (ha : Ch04.AELocallyUniformlyEllipticField a) {m : ℕ} {r τ δ q X α : ℝ} (hδ : δ = r - τ / 2) (hτ : 0 < τ) (hrq : 0 ≤ r * q) (hδq : 0 < δ * q) (hq : 0 < q) (hUpper : hΓ.params.sUpper < τ / 2) (hLower : hΓ.params.sLower < τ / 2) (hX : 0 < X) (hJ : ∀ (e : FullBlockVec d), e ⬝ᵥ e ≤ 1 → ∀ {n : ℕ}, X ≤ 3 ^ m → n < m → Real.rpow 3 (-τ * ↑(m - n)) * localizedLimitNormalizedJMax hP hStruct m n e a ≤ (3 ^ m / X) ^ (-α)) (hUnit : localizedLimitWeightedUnitEllipticitySup hP hStruct hΓ.params m a ≤ (Real.rpow 3 (τ / 2 * ↑m) * √((3 ^ m / X) ^ (-α))) ^ 2) (hScale : X ≤ 3 ^ m) :
have Cresp := √(4 * ↑(Fintype.card (BlockCoord d)) * ↑(Fintype.card (NormalizedProbeIndex d))); have Cneg := (Ch02.geometricDiscount (τ / 2) 1)⁻¹ * (2 * √(↑(Fintype.card (BlockCoord d)) ^ 2)); have A := max Cresp Cneg * Real.rpow 3 (τ / 2); Ch02.HomogenizationErrorOnCube (originCube d ↑m) r Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite q) (Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha) (scalarMatrix (barSigmaLimit hP hStruct)) ≤ (Ch02.geometricDiscount r q * (Ch02.geometricDiscount δ q)⁻¹).rpow (1 / q) * A * √((3 ^ m / X) ^ (-α))

Whole-cube finite-q homogenization-error control from one random scale which controls both the positive-scale J rows and the negative-scale unit-ellipticity rows.

source
theorem HCPolySupport.Book.Ch05.Section57.scaleResponseAtScale_originCube_nat_sub_le_of_minimalScaleProbeJ {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) {a : RegCoeffField d} (ha : Ch04.AELocallyUniformlyEllipticField a) {m n l : ℕ} (hln : l ≤ n) (hnm : n ≤ m) {τ X α : ℝ} (hX : 0 < X) (hprobe : Real.rpow 3 (-τ * ↑(m - (n - l))) * localizedNormalizedProbeJMax hP hStruct m (n - l) a ≤ (3 ^ m / X) ^ (-α)) :
Ch02.scaleResponseAtScale (originCube d ↑m) (↑n - ↑l) Ch02.MultiscaleExponent.infinity (Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha) (scalarMatrix (barSigmaLimit hP hStruct)) ≤ √(4 * ↑(Fintype.card (BlockCoord d)) * ↑(Fintype.card (NormalizedProbeIndex d))) * Real.rpow 3 (τ / 2 * ↑(m - (n - l))) * √((3 ^ m / X) ^ (-α))

Natural lower-scale response estimate obtained from the finite normalized probe maximum and the minimal-scale envelope.

source
theorem HCPolySupport.Book.Ch05.Section57.homogenizationErrorOnOriginCube_le_of_positiveScaleResponses_and_unitEllipticity {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) {a : RegCoeffField d} (ha : Ch04.AELocallyUniformlyEllipticField a) {m : ℕ} {r τ δ q X α : ℝ} (hδ : δ = r - τ / 2) (hτ : 0 < τ) (hrq : 0 ≤ r * q) (hδq : 0 < δ * q) (hq : 0 < q) (hUpper : hΓ.params.sUpper < τ / 2) (hLower : hΓ.params.sLower < τ / 2) (hX : 0 < X) (hPos : ∀ {l : ℕ}, 1 ≤ l → l ≤ m → Ch02.scaleResponseAtScale (originCube d ↑m) (↑m - ↑l) Ch02.MultiscaleExponent.infinity (Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha) (scalarMatrix (barSigmaLimit hP hStruct)) ≤ √(4 * ↑(Fintype.card (BlockCoord d)) * ↑(Fintype.card (NormalizedProbeIndex d))) * Real.rpow 3 (τ / 2 * ↑l) * √((3 ^ m / X) ^ (-α))) (hUnit : localizedLimitWeightedUnitEllipticitySup hP hStruct hΓ.params m a ≤ (Real.rpow 3 (τ / 2 * ↑m) * √((3 ^ m / X) ^ (-α))) ^ 2) :
have Cresp := √(4 * ↑(Fintype.card (BlockCoord d)) * ↑(Fintype.card (NormalizedProbeIndex d))); have Cneg := (Ch02.geometricDiscount (τ / 2) 1)⁻¹ * (2 * √(↑(Fintype.card (BlockCoord d)) ^ 2)); have A := max Cresp Cneg * Real.rpow 3 (τ / 2); Ch02.HomogenizationErrorOnCube (originCube d ↑m) r Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite q) (Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha) (scalarMatrix (barSigmaLimit hP hStruct)) ≤ (Ch02.geometricDiscount r q * (Ch02.geometricDiscount δ q)⁻¹).rpow (1 / q) * A * √((3 ^ m / X) ^ (-α))

Whole-cube finite-q homogenization-error control from positive-scale response rows and the negative-scale unit-ellipticity envelope.

source
theorem HCPolySupport.Book.Ch05.Section57.homogenizationErrorOnOriginCube_le_of_minimalScaleProbeJ_and_unitEllipticity {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) {a : RegCoeffField d} (ha : Ch04.AELocallyUniformlyEllipticField a) {m : ℕ} {r τ δ q X α : ℝ} (hδ : δ = r - τ / 2) (hτ : 0 < τ) (hrq : 0 ≤ r * q) (hδq : 0 < δ * q) (hq : 0 < q) (hUpper : hΓ.params.sUpper < τ / 2) (hLower : hΓ.params.sLower < τ / 2) (hX : 0 < X) (hProbe : ∀ {n : ℕ}, X ≤ 3 ^ m → n < m → Real.rpow 3 (-τ * ↑(m - n)) * localizedNormalizedProbeJMax hP hStruct m n a ≤ (3 ^ m / X) ^ (-α)) (hUnit : localizedLimitWeightedUnitEllipticitySup hP hStruct hΓ.params m a ≤ (Real.rpow 3 (τ / 2 * ↑m) * √((3 ^ m / X) ^ (-α))) ^ 2) (hScale : X ≤ 3 ^ m) :
have Cresp := √(4 * ↑(Fintype.card (BlockCoord d)) * ↑(Fintype.card (NormalizedProbeIndex d))); have Cneg := (Ch02.geometricDiscount (τ / 2) 1)⁻¹ * (2 * √(↑(Fintype.card (BlockCoord d)) ^ 2)); have A := max Cresp Cneg * Real.rpow 3 (τ / 2); Ch02.HomogenizationErrorOnCube (originCube d ↑m) r Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite q) (Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha) (scalarMatrix (barSigmaLimit hP hStruct)) ≤ (Ch02.geometricDiscount r q * (Ch02.geometricDiscount δ q)⁻¹).rpow (1 / q) * A * √((3 ^ m / X) ^ (-α))

Whole-cube finite-q homogenization-error control from one random scale which controls the positive finite-probe J rows and the negative-scale unit-ellipticity rows.

source
theorem HCPolySupport.Book.Ch05.Section57.homogenizationErrorOnOriginCube_le_of_two_minimalScales_probeJ {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) {a : RegCoeffField d} (ha : Ch04.AELocallyUniformlyEllipticField a) {m : ℕ} {r τ δ q XJ XU α : ℝ} (hδ : δ = r - τ / 2) (hτ : 0 < τ) (hrq : 0 ≤ r * q) (hδq : 0 < δ * q) (hq : 0 < q) (hUpper : hΓ.params.sUpper < τ / 2) (hLower : hΓ.params.sLower < τ / 2) (hα : 0 ≤ α) (hXJ : 0 < XJ) (hXU : 0 < XU) (hProbe : ∀ {n : ℕ}, XJ ≤ 3 ^ m → n < m → Real.rpow 3 (-τ * ↑(m - n)) * localizedNormalizedProbeJMax hP hStruct m n a ≤ (3 ^ m / XJ) ^ (-α)) (hUnit : localizedLimitWeightedUnitEllipticitySup hP hStruct hΓ.params m a ≤ (Real.rpow 3 (τ / 2 * ↑m) * √((3 ^ m / XU) ^ (-α))) ^ 2) (hScale : max XJ XU ≤ 3 ^ m) :
have X := max XJ XU; have Cresp := √(4 * ↑(Fintype.card (BlockCoord d)) * ↑(Fintype.card (NormalizedProbeIndex d))); have Cneg := (Ch02.geometricDiscount (τ / 2) 1)⁻¹ * (2 * √(↑(Fintype.card (BlockCoord d)) ^ 2)); have A := max Cresp Cneg * Real.rpow 3 (τ / 2); Ch02.HomogenizationErrorOnCube (originCube d ↑m) r Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite q) (Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha) (scalarMatrix (barSigmaLimit hP hStruct)) ≤ (Ch02.geometricDiscount r q * (Ch02.geometricDiscount δ q)⁻¹).rpow (1 / q) * A * √((3 ^ m / X) ^ (-α))

Same deterministic assembly with separate pointwise scales for the finite probe J rows and the unit-ellipticity rows. The exposed bound uses the single collapsed scale max XJ XU.

source
theorem HCPolySupport.Book.Ch05.Section57.homogenizationErrorOnOriginCube_le_of_two_minimalScales {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (hΓ : GammaSigmaCoarseGrainedEllipticity P hP hStruct) {a : RegCoeffField d} (ha : Ch04.AELocallyUniformlyEllipticField a) {m : ℕ} {r τ δ q XJ XU α : ℝ} (hδ : δ = r - τ / 2) (hτ : 0 < τ) (hrq : 0 ≤ r * q) (hδq : 0 < δ * q) (hq : 0 < q) (hUpper : hΓ.params.sUpper < τ / 2) (hLower : hΓ.params.sLower < τ / 2) (hα : 0 ≤ α) (hXJ : 0 < XJ) (hXU : 0 < XU) (hJ : ∀ (e : FullBlockVec d), e ⬝ᵥ e ≤ 1 → ∀ {n : ℕ}, XJ ≤ 3 ^ m → n < m → Real.rpow 3 (-τ * ↑(m - n)) * localizedLimitNormalizedJMax hP hStruct m n e a ≤ (3 ^ m / XJ) ^ (-α)) (hUnit : localizedLimitWeightedUnitEllipticitySup hP hStruct hΓ.params m a ≤ (Real.rpow 3 (τ / 2 * ↑m) * √((3 ^ m / XU) ^ (-α))) ^ 2) (hScale : max XJ XU ≤ 3 ^ m) :
have X := max XJ XU; have Cresp := √(4 * ↑(Fintype.card (BlockCoord d)) * ↑(Fintype.card (NormalizedProbeIndex d))); have Cneg := (Ch02.geometricDiscount (τ / 2) 1)⁻¹ * (2 * √(↑(Fintype.card (BlockCoord d)) ^ 2)); have A := max Cresp Cneg * Real.rpow 3 (τ / 2); Ch02.HomogenizationErrorOnCube (originCube d ↑m) r Ch02.MultiscaleExponent.infinity (Ch02.MultiscaleExponent.finite q) (Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha) (scalarMatrix (barSigmaLimit hP hStruct)) ≤ (Ch02.geometricDiscount r q * (Ch02.geometricDiscount δ q)⁻¹).rpow (1 / q) * A * √((3 ^ m / X) ^ (-α))

Same deterministic assembly with separate pointwise scales for the J rows and the unit-ellipticity rows. The exposed bound uses the single collapsed scale max XJ XU.