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

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

Step 4 — propagation over a fixed span

Group G of the printed proof (p.fixed.geometry.one.grid.propagation), third part: the old and new terms of 𝒫_q(m+L;n) and conjunct 3, e.fixed.geometry.profile.fixed.span.

Part of the proof of the statement 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 statement in 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_old_terms_advance_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 → ∀ (L : ℤ), 1 ≤ L → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ∀ (metric : Mat d), Matrix.PosDef metric → ∀ (n m : ℤ), ↑jStar ≤ n → n ≤ m → profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m ≤ 1 → 3 ^ (-((1 - γ) / 4) * (↑(m + L) - ↑n)) * (1 + meanPenalty (bigQ d γ) (relMean P (Geometry.explicitRoundedGrid jStar metric) n (m + L))) * history P γ (Geometry.explicitRoundedGrid jStar metric) jStar n + ∑ j ∈ Finset.Ico n m, 3 ^ (-((1 - γ) / 4) * (↑(m + L) - 1 - ↑j)) * meanPenalty (bigQ d γ) (relMean P (Geometry.explicitRoundedGrid jStar metric) j (m + L)) + ∑ j ∈ Finset.Icc (n + 1) m, 3 ^ (-((1 - γ) / 4) * (↑(m + L) - ↑j)) * Real.exp (↑(bigQ d γ) * detIncrement P (Geometry.explicitRoundedGrid jStar metric) j (m + L)) * ∫ (a : CoeffSpace d), absSchattenNorm (↑(bigQ d γ)) (normalizedFluctuationSelf P (Geometry.explicitRoundedGrid jStar metric) j a) ^ bigQ d γ ∂P ≤ profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m + C * (Real.exp (↑(bigQ d γ) * detIncrement P (Geometry.explicitRoundedGrid jStar metric) m (m + L)) - 1)

The generations up to m in 𝒫_q(m+L;n) (p.fixed.geometry.one.grid.propagation): the initial-history term, the old fluctuation sum and the mean-history contribution all pick up the factor 3^{-¼(1-γ)L}e^{QΔ^q_{m,m+L}}, and 𝒫_q(m;n) ≤ 1 converts that into an additive remainder.

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

The new mean terms of an arbitrary advance (p.fixed.geometry.one.grid.propagation): L indices, weights at most one, each penalty at most e^{QΔ^q_{m,m+L}} - 1.

theorem HCPolySupport.HighContrast.Multiscale.profile_fixed_span (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 → profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n (m + L) ≤ 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)

Conjunct 3, e.fixed.geometry.profile.fixed.span (p.fixed.geometry.one.grid.propagation).