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

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

Step 5 — startup, the absorbed drift and the drift-carrying span

Group H of the printed proof (p.fixed.geometry.one.grid.propagation), second part: conjuncts 4 and 8, e.fixed.geometry.profile.startup and e.fixed.geometry.fixed.span.propagation, with the absorbed drift advance between them.

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 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_startup (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 → profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n (n + L) ≤ C * ↑L * (history P γ (Geometry.explicitRoundedGrid jStar metric) jStar n + Real.exp (↑(bigQ d γ) * detIncrement P (Geometry.explicitRoundedGrid jStar metric) n (n + L)) - 1)

Conjunct 4, e.fixed.geometry.profile.startup (p.fixed.geometry.one.grid.propagation display e.fixed.geometry.profile.startup).

theorem HCPolySupport.HighContrast.Multiscale.determinantDrift_advance_absorbed (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 → ∀ (L : ℤ), 1 ≤ L → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ∀ (metric : Mat d), Matrix.PosDef metric → ∀ (m : ℤ), ↑jStar ≤ m → determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar m ≤ 1 → determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar (m + L) ≤ determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar m + 2 * (Real.exp (detIncrement P (Geometry.explicitRoundedGrid jStar metric) m (m + L)) - 1)

The absorbed drift advance (p.fixed.geometry.one.grid.propagation): when D_{q,j_*}(m) ≤ 1, applying e^x a ≤ a + e^x - 1 to e.fixed.geometry.drift.advance gives coefficient one on the drift and the printed 2 on the remainder.

theorem HCPolySupport.HighContrast.Multiscale.fixed_span_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 → ∀ (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 ≤ m → m = n ∨ n + ↑h ≤ m → profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m + determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar m ≤ 1 → profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n (m + L) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar (m + L) ≤ C * ↑L * (profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m + determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar m + Real.exp (↑(bigQ d γ) * detIncrement P (Geometry.explicitRoundedGrid jStar metric) m (m + L)) - 1)

Conjunct 8, e.fixed.geometry.fixed.span.propagation: add the absorbed drift advance to the fixed-span estimate when m ≥ n+h, and to the startup estimate when m = n using 𝒫_q(n;n) = ℋ_q(n); then e^{Δ^q_{m,m+L}} - 1 ≤ e^{QΔ^q_{m,m+L}} - 1.