High-contrast homogenization: Entry.Multiscale.OneGrid.Contraction

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

Step 2 — profile contraction

Group E of the printed proof (p.fixed.geometry.one.grid.propagation), third part: the contraction reduction and conjunct 2, e.fixed.geometry.profile.contraction.

Part of the proof of the result stated in HCPoly/Entry/Statements/OneGridPropagation.lean. Conventions of this group: q = 𝒬(𝔪) is Geometry.explicitRoundedGrid jStar metric at every loss, history, profile and drift; metric (not m) names the positive matrix, because m, n, m₀ are generations; the source lower scale e.source.lower.scale is carried exactly by the source-facing file HCPoly/Entry/OneGridPropagation.lean; this group's stronger internal algebraic and history lemmas omit an unused threshold, and this group's generic integration helpers take finiteness, integrability or measurability inputs that are proved at their actual use sites, not extra premises of the printed proposition.

theorem HCPolySupport.HighContrast.Multiscale.profile_contraction_reduction (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∃ (C : ℝ), 0 < C ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (h : ℕ), 2 * bigQ d γ ≤ h → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (metric : Mat d), Matrix.PosDef metric → ∀ (n m : ℤ), ↑jStar ≤ n → n + ↑h ≤ m → profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n (m + ↑h) ≤ (3 ^ (-((1 - γ) / 4) * ↑h) + 2 ^ (bigQ d γ - 1) * (3 ^ d * ↑(bigQ d γ)) ^ bigQ d γ * 3 ^ (-(↑(bigQ d γ) * ↑d / 2) * ↑h)) * Real.exp (↑(bigQ d γ) * synchCharge P (Geometry.explicitRoundedGrid jStar metric) (↑h) m) * profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m + C * (Real.exp (↑(bigQ d γ) * synchCharge P (Geometry.explicitRoundedGrid jStar metric) (↑h) m) - 1)

The first inequality of e.fixed.geometry.profile.contraction.reduction (p.fixed.geometry.one.grid.propagation): add the new fluctuations, the mean terms and the transported initial-history term.

theorem HCPolySupport.HighContrast.Multiscale.profile_contraction (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (Csrc : ℝ), 0 < Csrc ∧ ∃ (C : ℝ), 0 < C ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (h : ℕ), 2 * bigQ d γ ≤ h → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (metric : Mat d), Matrix.PosDef metric → ∀ (n m : ℤ), ↑jStar ≤ n → n + ↑h ≤ m → profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n (m + ↑h) ≤ 1 / 8 * Real.exp (↑(bigQ d γ) * synchCharge P (Geometry.explicitRoundedGrid jStar metric) (↑h) m) * profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m + C * (Real.exp (↑(bigQ d γ) * synchCharge P (Geometry.explicitRoundedGrid jStar metric) (↑h) m) - 1)

Conjunct 2, e.fixed.geometry.profile.contraction (p.fixed.geometry.one.grid.propagation): the contraction constant is 1/8 for every natural h ≥ 2Q.