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

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

Finite-q homogenization-error control above the minimal scale

This file begins the Section 5.7 corollary converting the localized minimal-scale J estimate into finite-q control of \mathcal E_{r,\infty,q}. The first lemma is the deterministic geometric summation step: after each weighted scale response term is bounded by a summable geometric row, the finite-q homogenization error is bounded by the corresponding q-root.

theorem HCPolySupport.Book.Ch05.Section57.constantFullBlockMatrix_scalarMatrix_eq_diagonal {d : ℕ} {σ : ℝ} (hσ : 0 < σ) : Ch02.constantFullBlockMatrix (scalarMatrix σ) = Matrix.diagonal fun (α : BlockCoord d) => match α with | Sum.inl val => σ | Sum.inr val => σ⁻¹

For a scalar reference coefficient, the Chapter 2 full block matrix is the diagonal matrix with entries σ and σ⁻¹.

theorem HCPolySupport.Book.Ch05.Section57.constantFullBlockMatrixSqrt_scalarMatrix_eq_scalarFullBlockSqrt {d : ℕ} {σ : ℝ} (hσ : 0 < σ) : Ch02.constantFullBlockMatrixSqrt (scalarMatrix σ) = Matrix.diagonal (Section56.scalarFullBlockSqrtDiag σ σ)

The Chapter 2 square-root normalizer agrees with the Section 5.7 scalar normalizer for a scalar reference coefficient.

theorem HCPolySupport.Book.Ch05.Section57.ringInverse_scalarFullBlockSqrtDiag_eq_scalarFullBlockInvSqrtDiag {d : ℕ} {σ : ℝ} (hσ : 0 < σ) : Ring.inverse (Section56.scalarFullBlockSqrtDiag σ σ) = Ch04.scalarFullBlockInvSqrtDiag σ σ

Coordinatewise inverse of the scalar square-root diagonal used in Section 5.7.

theorem HCPolySupport.Book.Ch05.Section57.constantFullBlockMatrixInvSqrt_scalarMatrix_eq_scalarFullBlockInvSqrt {d : ℕ} {σ : ℝ} (hσ : 0 < σ) : Ch02.constantFullBlockMatrixInvSqrt (scalarMatrix σ) = Matrix.diagonal (Ch04.scalarFullBlockInvSqrtDiag σ σ)

The Chapter 2 inverse square-root normalizer agrees with the Section 5.7 scalar inverse normalizer for a scalar reference coefficient.

theorem HCPolySupport.Book.Ch05.Section57.limitNormalizedJProbeSum_le_four_normalizedProbeSum_of_aelocallyUniformlyEllipticField {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) (Q : TriadicCube d) : limitNormalizedJProbeSum hP hStruct Q a ≤ 4 * limitNormalizedJNormalizedProbeSum hP hStruct Q a

Pointwise version of the finite-basis normalization step for sampled coefficient fields.

theorem HCPolySupport.Book.Ch05.Section57.BlockResponseMax_scalarMatrix_le_limitNormalizedJNormalizedProbeSum {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) (Q : TriadicCube d) : Ch02.normalizedBlockResponseMax Q (Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha) (scalarMatrix (barSigmaLimit hP hStruct)) ≤ 4 * ↑(Fintype.card (BlockCoord d)) * limitNormalizedJNormalizedProbeSum hP hStruct Q a

One-cube bridge from the Chapter 2 normalized block-response maximum to the Section 5.7 finite normalized probe sum.

theorem HCPolySupport.Book.Ch05.Section57.limitNormalizedJNormalizedProbeSum_le_localizedLimitNormalizedJNormalizedProbeSumMax {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {m n : ℕ} {R : TriadicCube d} (hR : R ∈ descendantsAtScale (originCube d ↑m) ↑n) (a : RegCoeffField d) : limitNormalizedJNormalizedProbeSum hP hStruct R a ≤ localizedLimitNormalizedJNormalizedProbeSumMax hP hStruct m n a

A descendant's normalized finite-probe sum is bounded by the localized maximum over all descendants at the same scale.

theorem HCPolySupport.Book.Ch05.Section57.maxDescendantNormalizedBlockResponse_cube_scalarMatrix_le_NormalizedProbeJMax {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) : Ch02.maxDescendantNormalizedBlockResponseAtScale (originCube d ↑m) (↑n) (Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField a ha) (scalarMatrix (barSigmaLimit hP hStruct)) ≤ 4 * ↑(Fintype.card (BlockCoord d)) * ↑(Fintype.card (NormalizedProbeIndex d)) * localizedNormalizedProbeJMax hP hStruct m n a

Localized bridge from the Chapter 2 descendant response maximum to the Section 5.7 finite normalized-probe maximum.

theorem HCPolySupport.Book.Ch05.Section57.weighted_localizedNormalizedProbeJMax_le_of_forall_probe {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {m n : ℕ} (a : RegCoeffField d) {W R : ℝ} (hW : 0 < W) (hprobe : ∀ (i : NormalizedProbeIndex d), W * localizedLimitNormalizedJMax hP hStruct m n (normalizedProbeVec i) a ≤ R) : W * localizedNormalizedProbeJMax hP hStruct m n a ≤ R

If every normalized finite probe satisfies a weighted localized estimate, then the finite-probe maximum satisfies the same weighted estimate.

theorem HCPolySupport.Book.Ch05.Section57.limitNormalizedBlockJObservable_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) (Q : TriadicCube d) (e : FullBlockVec d) (a : RegCoeffField d) : 0 ≤ limitNormalizedBlockJObservable hP hStruct Q e a

The limiting-normalized block response is nonnegative.

theorem HCPolySupport.Book.Ch05.Section57.localizedLimitNormalizedJMax_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {m n : ℕ} (hnm : n ≤ m) (e : FullBlockVec d) (a : RegCoeffField d) : 0 ≤ localizedLimitNormalizedJMax hP hStruct m n e a

Localized limiting-normalized maxima are nonnegative.

theorem HCPolySupport.Book.Ch05.Section57.localizedNormalizedProbeJMax_nonneg {d : ℕ} [NeZero d] {P : Ch04.RestrictionCoeffLaw d} (hP : Ch04.RestrictionLawCarrier P) (hStruct : Ch04.RestrictionStructuralLaw P) {m n : ℕ} (hnm : n ≤ m) (a : RegCoeffField d) : 0 ≤ localizedNormalizedProbeJMax hP hStruct m n a

The finite normalized-probe maximum is nonnegative.

theorem HCPolySupport.Book.Ch05.Section57.scaleResponseAtScale_originCube_nat_le_sqrt_const_mul_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) : 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)) * localizedNormalizedProbeJMax hP hStruct m n a)

Natural-scale response control from the localized finite normalized-probe maximum.

theorem HCPolySupport.Book.Ch05.Section57.homogenizationErrorFinite_infinity_le_rpow_of_weighted_geometric_bound {d : ℕ} (Q : TriadicCube d) {n : ℤ} (hn : n ≤ Q.scale) (a : Ch02.TriadicCoeffFamily d) (a0 : Mat d) {r delta q B : ℝ} (hrq : 0 ≤ r * q) (hdeltaq : 0 < delta * q) (hq : 0 < q) (hB : 0 ≤ B) (hterm : ∀ (l : ℕ), Ch02.geometricWeight r q l * (Ch02.scaleResponseAtScale Q (n - ↑l) Ch02.MultiscaleExponent.infinity a a0).rpow q ≤ Ch02.geometricWeight delta q l * B) : Ch02.HomogenizationErrorFinite Q n r Ch02.MultiscaleExponent.infinity q a a0 ≤ B.rpow (1 / q)

A deterministic finite-q summation principle for the Chapter 2 homogenization error.

The hypothesis hterm is exactly the pointwise weighted scale-row estimate which comes from the localized J minimal-scale bound after choosing delta = r - tau / 2. The conclusion is the finite-q \ell^q norm bound in the definition of HomogenizationErrorFinite.

theorem HCPolySupport.Book.Ch05.Section57.weighted_scaleResponse_term_le_of_scaleResponse_le {d : ℕ} (Q : TriadicCube d) {n : ℤ} (hn : n ≤ Q.scale) (a : Ch02.TriadicCoeffFamily d) (a0 : Mat d) {r tau delta q A R : ℝ} {l : ℕ} (hdelta : delta = r - tau / 2) (hrq : 0 ≤ r * q) (hdeltaq : 0 < delta * q) (hq : 0 < q) (hA : 0 ≤ A) (hR : 0 ≤ R) (hscale : Ch02.scaleResponseAtScale Q (n - ↑l) Ch02.MultiscaleExponent.infinity a a0 ≤ A * Real.rpow 3 (tau / 2 * ↑l) * R) : Ch02.geometricWeight r q l * (Ch02.scaleResponseAtScale Q (n - ↑l) Ch02.MultiscaleExponent.infinity a a0).rpow q ≤ Ch02.geometricWeight delta q l * (Ch02.geometricDiscount r q * (Ch02.geometricDiscount delta q)⁻¹ * A.rpow q * R.rpow q)

Convert a pointwise response bound with discount tau / 2 into the weighted geometric row bound used by homogenizationErrorFinite_infinity_le_rpow_of_weighted_geometric_bound.

This is the deterministic algebra behind the phrase "give up some t to get finite q": if delta = r - tau / 2 is positive, the extra 3^{tau l / 2} from taking the square root of a J-bound is absorbed by the r-geometric weight.

theorem HCPolySupport.Book.Ch05.Section57.homogenizationErrorFinite_infinity_le_of_scaleResponse_le {d : ℕ} (Q : TriadicCube d) {n : ℤ} (hn : n ≤ Q.scale) (a : Ch02.TriadicCoeffFamily d) (a0 : Mat d) {r tau delta q A R : ℝ} (hdelta : delta = r - tau / 2) (hrq : 0 ≤ r * q) (hdeltaq : 0 < delta * q) (hq : 0 < q) (hA : 0 ≤ A) (hR : 0 ≤ R) (hscale : ∀ (l : ℕ), Ch02.scaleResponseAtScale Q (n - ↑l) Ch02.MultiscaleExponent.infinity a a0 ≤ A * Real.rpow 3 (tau / 2 * ↑l) * R) : Ch02.HomogenizationErrorFinite Q n r Ch02.MultiscaleExponent.infinity q a a0 ≤ (Ch02.geometricDiscount r q * (Ch02.geometricDiscount delta q)⁻¹ * A.rpow q * R.rpow q).rpow (1 / q)

Finite-q deterministic \mathcal E control from a scale-by-scale response estimate.

This is the packaged geometric summation step used by the Section 5.7 minimal-scale corollary. The constant is explicit: it is only the ratio of the two geometric normalizations, multiplied by the q-power of the scale-response prefactor.

theorem HCPolySupport.Book.Ch05.Section57.scaleResponseAtScale_infinity_le_of_maxDescendant_le_sq {d : ℕ} (Q : TriadicCube d) {k : ℤ} (_hk : k ≤ Q.scale) (a : Ch02.TriadicCoeffFamily d) (a0 : Mat d) {B : ℝ} (hB : 0 ≤ B) (hmax : Ch02.maxDescendantNormalizedBlockResponseAtScale Q k a a0 ≤ B ^ 2) : Ch02.scaleResponseAtScale Q k Ch02.MultiscaleExponent.infinity a a0 ≤ B

Square-root form of the p = infinity scale response: a bound on the underlying descendant maximum by B^2 gives a bound on the scale response by B.