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

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

Step 3 — the drift advance and synchronized propagation

Group F of the printed proof (p.fixed.geometry.one.grid.propagation): the determinant-drift advance and conjunct 6, e.fixed.geometry.synchronized.propagation.

Part of the proof of HCPoly/Entry/Statements/OneGridPropagation.lean. Conventions of the 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 module HCPoly/Entry/OneGridPropagation.lean; this group's stronger internal algebraic and history lemmas omit an unused source-scale 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.

The declaration text of this file is copied unchanged; only this header, the imports and the namespace frame are new.

Group F. Step 3 — the drift advance and the synchronized propagation

(p.fixed.geometry.one.grid.propagation)

theorem HCPolySupport.HighContrast.Multiscale.determinantDrift_advance (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) : MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ∀ (metric : Mat d), Matrix.PosDef metric → ∀ (m L : ℤ), ↑jStar ≤ m → 1 ≤ L → determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar (m + L) ≤ 3 ^ (-((1 - γ) / 8) * ↑L) * Real.exp (detIncrement P (Geometry.explicitRoundedGrid jStar metric) m (m + L)) * determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar m + Real.exp (detIncrement P (Geometry.explicitRoundedGrid jStar metric) m (m + L)) - 1

e.fixed.geometry.drift.advance at the actual stochastic use site: the helper determinantDrift_advance_of_posDef_antitone composed with Annealed.adaptedMean_posDef and Annealed.adaptedMean_antitone. It needs only m ≥ j_*, so it also serves the diagonal case of Step 5.

theorem HCPolySupport.HighContrast.Multiscale.synchronized_propagation (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) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar (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 + determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar m) + C * (Real.exp (↑(bigQ d γ) * synchCharge P (Geometry.explicitRoundedGrid jStar metric) (↑h) m) - 1)

Conjunct 6, e.fixed.geometry.synchronized.propagation (p.fixed.geometry.one.grid.propagation): the drift advance at L = h gives D_{q,j_*}(m+h) ≤ ⅛e^{QΔ̂^q_h(m)}D_{q,j_*}(m) + C(e^{QΔ̂^q_h(m)}-1), which is added to the profile contraction.