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

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

Lower-scale response envelope

This file supplies the deterministic lower-scale input for the closed \mathcal E estimate. The results here keep the lower-scale contribution in the same algebraic envelope used by the main finite-q summation.

theorem HCPolySupport.Book.Ch05.Section57.weighted_negative_scaleResponse_le_scaleZero_ellipticity_roots {d : ℕ} [NeZero d] (m j : ℕ) {s σ : ℝ} (hs : 0 < s) (hσ : 0 < σ) (a : Ch02.TriadicCoeffFamily d) : let Q := originCube d ↑m; let D := descendantsAtScale Q 0; have hD := ⋯; Ch02.geometricWeight s 1 (j + m) * Ch02.scaleResponseAtScale Q (-↑j) Ch02.MultiscaleExponent.infinity a (scalarMatrix σ) ≤ √(↑(Fintype.card (BlockCoord d)) ^ 2) * (√σ⁻¹ * (Real.rpow 3 (-s * ↑m) * (D.sup' hD fun (U : TriadicCube d) => Ch02.LambdaSq U s (Ch02.MultiscaleExponent.finite 1) a).rpow (1 / 2)) + √σ * (Real.rpow 3 (-s * ↑m) * (D.sup' hD fun (U : TriadicCube d) => (Ch02.lambdaSq U s (Ch02.MultiscaleExponent.finite 1) a)⁻¹).rpow (1 / 2)))

A negative-scale response row is controlled by the scale-zero Ch2 ellipticity suprema, with the same weight as in the homogenization-error series.

theorem HCPolySupport.Book.Ch05.Section57.weighted_negative_scaleResponse_le_of_scaleZero_collapsed {d : ℕ} [NeZero d] (m j : ℕ) {s σ R : ℝ} (hs : 0 < s) (hσ : 0 < σ) (hR : 0 ≤ R) (a : Ch02.TriadicCoeffFamily d) (hupper : let Q := originCube d ↑m; let D := descendantsAtScale Q 0; have hD := ⋯; (σ⁻¹ * D.sup' hD fun (U : TriadicCube d) => Ch02.LambdaSq U s (Ch02.MultiscaleExponent.finite 1) a) ≤ (Real.rpow 3 (s * ↑m) * R) ^ 2) (hlower : let Q := originCube d ↑m; let D := descendantsAtScale Q 0; have hD := ⋯; (σ * D.sup' hD fun (U : TriadicCube d) => (Ch02.lambdaSq U s (Ch02.MultiscaleExponent.finite 1) a)⁻¹) ≤ (Real.rpow 3 (s * ↑m) * R) ^ 2) : Ch02.geometricWeight s 1 (j + m) * Ch02.scaleResponseAtScale (originCube d ↑m) (-↑j) Ch02.MultiscaleExponent.infinity a (scalarMatrix σ) ≤ 2 * √(↑(Fintype.card (BlockCoord d)) ^ 2) * R

If the scale-zero ellipticity suprema are already in the collapsed minimal-scale envelope, then every negative response row is in the same weighted envelope.

theorem HCPolySupport.Book.Ch05.Section57.negative_scaleResponse_le_of_weighted_envelope {d : ℕ} (m j : ℕ) {s σ A R : ℝ} (hs : 0 < s) (hA : 0 ≤ A) (hR : 0 ≤ R) (a : Ch02.TriadicCoeffFamily d) (hweighted : Ch02.geometricWeight s 1 (j + m) * Ch02.scaleResponseAtScale (originCube d ↑m) (-↑j) Ch02.MultiscaleExponent.infinity a (scalarMatrix σ) ≤ A * R) : Ch02.scaleResponseAtScale (originCube d ↑m) (-↑j) Ch02.MultiscaleExponent.infinity a (scalarMatrix σ) ≤ (Ch02.geometricDiscount s 1)⁻¹ * A * Real.rpow 3 (s * ↑(j + m)) * R

Weighted negative-scale response control gives the unweighted algebraic scale envelope, paying only the fixed geometric-discount constant.