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

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

Step 2 — the fluctuation and mean sums of a synchronized step

Group E of the printed proof (p.fixed.geometry.one.grid.propagation), second part: the new fluctuation terms of 𝒫_q(m+h;n), transport of the mean-history terms across a synchronized step, and the mean terms of the new block m ≤ j < m+h.

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 module HCPoly/Entry/OneGridPropagation.lean; this group's stronger internal algebraic and history lemmas omit an unused source 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.new_fluctuation_sum_le (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 → ∑ j ∈ Finset.Icc (m + 1) (m + ↑h), 3 ^ (-((1 - γ) / 4) * (↑(m + ↑h) - ↑j)) * Real.exp (↑(bigQ d γ) * detIncrement P (Geometry.explicitRoundedGrid jStar metric) j (m + ↑h)) * ∫ (a : CoeffSpace d), absSchattenNorm (↑(bigQ d γ)) (normalizedFluctuationSelf P (Geometry.explicitRoundedGrid jStar metric) j a) ^ bigQ d γ ∂P ≤ 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 new fluctuation terms of 𝒫_q(m+h;n) (p.fixed.geometry.one.grid.propagation): apply the powered recurrence at j-h ∈ [n+1,m], use additivity Δ^q_{j,m+h} + Δ^q_{j-h,j} = Δ^q_{j-h,m+h} ≤ Δ̂^q_h(m) and e^{QΔ^q_{j,m+h}}(e^{QΔ^q_{j-h,j}} - 1) ≤ e^{QΔ̂^q_h(m)} - 1, then sum.

theorem HCPolySupport.HighContrast.Multiscale.meanHistory_transport_le (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (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 → ∀ (metric : Mat d), Matrix.PosDef metric → ∀ (n m : ℤ), ↑jStar ≤ n → n + ↑h ≤ m → ∑ j ∈ Finset.Ico n m, 3 ^ (-((1 - γ) / 4) * (↑(m + ↑h) - 1 - ↑j)) * meanPenalty (bigQ d γ) (relMean P (Geometry.explicitRoundedGrid jStar metric) j (m + ↑h)) ≤ 3 ^ (-((1 - γ) / 4) * ↑h) * Real.exp (↑(bigQ d γ) * detIncrement P (Geometry.explicitRoundedGrid jStar metric) m (m + ↑h)) * meanHistory P γ (Geometry.explicitRoundedGrid jStar metric) n m + C * (Real.exp (↑(bigQ d γ) * detIncrement P (Geometry.explicitRoundedGrid jStar metric) m (m + ↑h)) - 1)

Transport of the mean-history terms across a synchronized step (p.fixed.geometry.one.grid.propagation).

theorem HCPolySupport.HighContrast.Multiscale.meanPenalty_upper_block_sum_le (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ∃ (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 → ∀ (metric : Mat d), Matrix.PosDef metric → ∀ (n m : ℤ), ↑jStar ≤ n → n + ↑h ≤ m → ∑ j ∈ Finset.Ico m (m + ↑h), 3 ^ (-((1 - γ) / 4) * (↑(m + ↑h) - 1 - ↑j)) * meanPenalty (bigQ d γ) (relMean P (Geometry.explicitRoundedGrid jStar metric) j (m + ↑h)) ≤ C * (Real.exp (↑(bigQ d γ) * synchCharge P (Geometry.explicitRoundedGrid jStar metric) (↑h) m) - 1)

The mean terms of the new block m ≤ j < m+h (p.fixed.geometry.one.grid.propagation): there the eigenvalues of P^q_{j,m+h} are at least one, so 1 + tr(P^q_{j,m+h} - I) ≤ det P^q_{j,m+h} = e^{Δ^q_{j,m+h}} ≤ e^{Δ̂^q_h(m)}.