Coarse-graining support: Support.Book.Ch05.Theorems.Section57.HomogenizationErrorFiniteQ

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

Finite-q homogenization-error control

This file continues the Section 5.7 conversion from the localized quenched J estimate to finite-q homogenization-error bounds. The lemmas below are the deterministic square-root step: a weighted J estimate at one scale gives the corresponding p = infinity scale-response estimate with half the discount exponent.

theorem HCPolySupport.Book.Ch05.Section57.sqrt_mul_le_sqrt_mul_rpow_half_of_weighted_le {C Y R τ L : ℝ} (hC : 0 ≤ C) (hR : 0 ≤ R) (hweighted : Real.rpow 3 (-τ * L) * Y ≤ R ^ 2) : √(C * Y) ≤ √C * Real.rpow 3 (τ / 2 * L) * R

If 3^{-τL} Y is bounded by R², then the square-root response gains the factor 3^{τL/2}.

theorem HCPolySupport.Book.Ch05.Section57.scaleResponseAtScale_originCube_nat_le_rpow_of_weighted_localizedNormalizedProbeJMax {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 : ℕ} (hnm : n ≤ m) {τ R : ℝ} (hR : 0 ≤ R) (hweighted : Real.rpow 3 (-τ * ↑(m - n)) * localizedNormalizedProbeJMax hP hStruct m n a ≤ R ^ 2) : Ch02.scaleResponseAtScale (originCube d ↑m) (↑n) 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)) * R

One-scale response control from the localized finite-probe maximum, after using the weighted Section 5.7 estimate.

theorem HCPolySupport.Book.Ch05.Section57.scaleResponseAtScale_originCube_nat_le_rpow_of_weighted_localizedUnitJMax {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 : ℕ} (hnm : n ≤ m) {τ R : ℝ} (hR : 0 ≤ R) (hunit : ∀ (e : FullBlockVec d), e ⬝ᵥ e ≤ 1 → Real.rpow 3 (-τ * ↑(m - n)) * localizedLimitNormalizedJMax hP hStruct m n e a ≤ R ^ 2) : Ch02.scaleResponseAtScale (originCube d ↑m) (↑n) 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)) * R

The same one-scale response control, using the unit-vector form supplied by the minimal-scale theorem.

theorem HCPolySupport.Book.Ch05.Section57.scaleResponseAtScale_originCube_nat_sub_le_rpow_of_weighted_localizedUnitJMax {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) {τ R : ℝ} (hR : 0 ≤ R) (hunit : ∀ (e : FullBlockVec d), e ⬝ᵥ e ≤ 1 → Real.rpow 3 (-τ * ↑(m - (n - l))) * localizedLimitNormalizedJMax hP hStruct m (n - l) e a ≤ R ^ 2) : 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))) * R

Natural lower-scale version of scaleResponseAtScale_originCube_nat_le_rpow_of_weighted_localizedUnitJMax. This is the form used in the finite-q row summation: the l-th term in \mathcal E(Q,n) samples the scale n-l.

theorem HCPolySupport.Book.Ch05.Section57.scaleResponseAtScale_originCube_nat_sub_le_of_minimalScaleUnitJ {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) (hunit : ∀ (e : FullBlockVec d), e ⬝ᵥ e ≤ 1 → Real.rpow 3 (-τ * ↑(m - (n - l))) * localizedLimitNormalizedJMax hP hStruct m (n - l) e 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) ^ (-α))

One natural lower-scale response estimate obtained by inserting the minimal-scale envelope and taking a square root.

theorem HCPolySupport.Book.Ch05.Section57.finset_sum_nat_scaleResponse_terms_le_of_minimalScaleUnitJ {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 : ℕ} (hnm : n ≤ m) {r τ δ q X α : ℝ} (hδ : δ = r - τ / 2) (hrq : 0 ≤ r * q) (hδq : 0 < δ * q) (hq : 0 < q) (hX : 0 < X) (hunit : ∀ l ≤ n, ∀ (e : FullBlockVec d), e ⬝ᵥ e ≤ 1 → Real.rpow 3 (-τ * ↑(m - (n - l))) * localizedLimitNormalizedJMax hP hStruct m (n - l) e a ≤ (3 ^ m / X) ^ (-α)) : have Cresp := √(4 * ↑(Fintype.card (BlockCoord d)) * ↑(Fintype.card (NormalizedProbeIndex d))); have A := Cresp * Real.rpow 3 (τ / 2 * ↑(m - n)); have R := √((3 ^ m / X) ^ (-α)); ∑ l ∈ Finset.range (n + 1), Ch02.geometricWeight r q l * (Ch02.scaleResponseAtScale (originCube d ↑m) (↑n - ↑l) Ch02.MultiscaleExponent.infinity (Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha) (scalarMatrix (barSigmaLimit hP hStruct))).rpow q ≤ Ch02.geometricDiscount r q * (Ch02.geometricDiscount δ q)⁻¹ * A.rpow q * R.rpow q

Natural-scale finite-row summation from the minimal-scale J estimate.

This controls the part of the finite-q homogenization-error series with l ≤ n, i.e. the scales which are still nonnegative. The closed \mathcal E corollary absorbs the lower scales into the same minimal-scale envelope before exposing a theorem statement.