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

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

Span Fluctuation Seeds

The seeds of the span construction and the fluctuation bounds along it: the seed moments of the span-2Q induction, the exponential bound e^{QΔ} - 1 ≤ C 𝒫 on the seed window, and the span-2Q recurrence with its additivity splittings and induction over the new generations. These are Group G of the printed proof of p.fixed.geometry.one.grid.propagation, and the second part serves e.fixed.geometry.new.fluctuations.

Step 4 — the seeds of the span-2Q induction

Group G of the printed proof (p.fixed.geometry.one.grid.propagation), first part: the seed moments of the span-2Q induction and the bound e^{QΔ} - 1 ≤ C 𝒫 on the seed window.

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 module 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 G. Step 4 — an arbitrary advance (p.fixed.geometry.one.grid.propagation)

theorem HCPolySupport.HighContrast.Multiscale.moment_seed_le_profile (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 → ∀ (r : ℤ), m + 1 - 2 * ↑(bigQ d γ) ≤ r → r ≤ m → Real.exp (↑(bigQ d γ) * detIncrement P (Geometry.explicitRoundedGrid jStar metric) r m) * ∫ (a : CoeffSpace d), absSchattenNorm (↑(bigQ d γ)) (normalizedFluctuationSelf P (Geometry.explicitRoundedGrid jStar metric) r a) ^ bigQ d γ ∂P ≤ C * profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m

The seed moments of the span-2Q induction (p.fixed.geometry.one.grid.propagation): for m+1-2Q ≤ r ≤ m one has r ≥ n+1 and m-r < 2Q, so the scale-r term of 𝒫_q(m;n) controls e^{QΔ^q_{r,m}}E[|V^q_r|_{S_Q}^Q].

theorem HCPolySupport.HighContrast.Multiscale.exp_logDetLoss_sub_one_le_profile (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 → profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m ≤ 1 → ∀ (r : ℤ), m + 1 - 2 * ↑(bigQ d γ) ≤ r → r < m → Real.exp (↑(bigQ d γ) * detIncrement P (Geometry.explicitRoundedGrid jStar metric) r m) - 1 ≤ C * profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m

e^{QΔ^q_{r,m}} - 1 ≤ C 𝒫_q(m;n) for r < m in the seed window (p.fixed.geometry.one.grid.propagation), from Δ^q_{r,m} ≤ tr(P^q_{r,m} - I_{2d}), the comparison of e^{Qt}-1 with (1+t)^Q-1 and the scale-r term of ℋ^mean_q(m;n). The premise 𝒫_q(m;n) ≤ 1 is the printed one.

Step 4 — the new fluctuations of an arbitrary advance

Group G of the printed proof (p.fixed.geometry.one.grid.propagation), second part: e.fixed.geometry.new.fluctuations, the span-2Q fluctuation estimate.

Part of the proof of the declaration in HCPoly/Entry/Statements/OneGridPropagation.lean. Conventions: 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; the stronger internal algebraic and history lemmas omit an unused threshold, and the 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_fluctuations_span_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 → ∀ (L : ℤ), 1 ≤ L → ∀ (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 ≤ 1 → ∑ s ∈ Finset.Icc (m + 1) (m + L), 3 ^ (-((1 - γ) / 4) * (↑(m + L) - ↑s)) * Real.exp (↑(bigQ d γ) * detIncrement P (Geometry.explicitRoundedGrid jStar metric) s (m + L)) * ∫ (a : CoeffSpace d), absSchattenNorm (↑(bigQ d γ)) (normalizedFluctuationSelf P (Geometry.explicitRoundedGrid jStar metric) s a) ^ bigQ d γ ∂P ≤ C * ↑L * (profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m + Real.exp (↑(bigQ d γ) * detIncrement P (Geometry.explicitRoundedGrid jStar metric) m (m + L)) - 1)

e.fixed.geometry.new.fluctuations (p.fixed.geometry.one.grid.propagation): the span-2Q recurrence, the additivity splittings, and the induction in s over the new generations.