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

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

Step 5 — the diagonal profile and the initial moments

Group H of the printed proof (p.fixed.geometry.one.grid.propagation), first part: 𝒫_q(n;n) = ℋ_q(n), the diagonal moment comparison, and the new fluctuation terms of the initial advance.

Part of the proof of the statement in 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 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.

Group H. Step 5 — the initial advance and the drift assembly

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

theorem HCPolySupport.HighContrast.Multiscale.profile_diagonal_eq_history (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 → ∀ (n : ℤ), profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n n = history P γ (Geometry.explicitRoundedGrid jStar metric) jStar n

𝒫_q(n;n) = ℋ_q(n) at the actual geometry (near e.scale.selection.complete.profile): the diagonal identity Multiscale.profile_self_of_posDef with its positive-definiteness discharged.

theorem HCPolySupport.HighContrast.Multiscale.moment_diagonal_le_fluctuationHistory (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 → ∀ (n : ℤ), ↑jStar ≤ n → ∫ (a : CoeffSpace d), absSchattenNorm (↑(bigQ d γ)) (normalizedFluctuationSelf P (Geometry.explicitRoundedGrid jStar metric) n a) ^ bigQ d γ ∂P ≤ 2 * ↑d * fluctuationHistory P γ (Geometry.explicitRoundedGrid jStar metric) jStar n

E[|V^q_n|_{S_Q}^Q] ≤ 2d·ℋ^fluc_q(n) (p.fixed.geometry.one.grid.propagation): comparison of the Schatten and operator norms at the diagonal generation, where the printed supremum of the fluctuation history is taken at j = n and the lattice point 0.

theorem HCPolySupport.HighContrast.Multiscale.startup_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 → ∀ (L : ℤ), 1 ≤ L → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (metric : Mat d), Matrix.PosDef metric → ∀ (n : ℤ), ↑jStar ≤ n → history P γ (Geometry.explicitRoundedGrid jStar metric) jStar n ≤ 1 → ∑ j ∈ Finset.Icc (n + 1) (n + L), 3 ^ (-((1 - γ) / 4) * (↑(n + L) - ↑j)) * Real.exp (↑(bigQ d γ) * detIncrement P (Geometry.explicitRoundedGrid jStar metric) j (n + L)) * ∫ (a : CoeffSpace d), absSchattenNorm (↑(bigQ d γ)) (normalizedFluctuationSelf P (Geometry.explicitRoundedGrid jStar metric) j a) ^ bigQ d γ ∂P ≤ C * ↑L * (history P γ (Geometry.explicitRoundedGrid jStar metric) jStar n + Real.exp (↑(bigQ d γ) * detIncrement P (Geometry.explicitRoundedGrid jStar metric) n (n + L)) - 1)

The new fluctuation terms of the initial advance (p.fixed.geometry.one.grid.propagation): apply the powered recurrence with span r at the base generation n, seed with E[|V^q_n|_{S_Q}^Q] ≤ 2d ℋ_q(n), use e^x a ≤ a + e^x - 1 at a = ℋ_q(n) ≤ 1, and sum. The constant is uniform in 1 ≤ r ≤ L.