Documentation

LeanPool.HighContrastHomogenization.Entry.Multiscale.Initial.Propagation

High-contrast homogenization: Entry.Multiscale.Initial.Propagation #

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

Initialization: the one-grid propagation statement at the Euclidean grid #

The one-grid propagation statement HCPolySupport.HighContrast.Entry.fixed_geometry_one_grid_propagation_full (HCPoly/Entry/OneGridPropagation.lean, p.fixed.geometry.one.grid.propagation) is specialized to the Euclidean grid metric = 1, where Geometry.explicitRoundedGrid jStar 1 = 1: its conjuncts 5, 6 and 7 become the carried-history majorization, the synchronized propagation step and the synchronized multiplicity budget used in Steps 2 and 3 of p.initial.fixed.grid.scale.

E. Steps 2–3 — logarithmic decrement and the hitting index #

(p.initial.fixed.grid.scale). The one-grid propagation statement enters through one_grid_propagation_input, which repeats the exact type of HCPolySupport.HighContrast.Entry.fixed_geometry_one_grid_propagation_full (HCPoly/Entry/Statements/OneGridPropagation.lean, byte for byte) and is discharged by one direct application of the statement proved in HCPoly/Entry/OneGridPropagation.lean.

source
theorem HCPolySupport.HighContrast.Multiscale.one_grid_propagation_input (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 → history P γ (Geometry.explicitRoundedGrid jStar metric) jStar m ≤ C * profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m ∧ (n + ↑h ≤ m → profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n (m + ↑h) ≤ 1 / 8 * 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)) ∧ (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)) ∧ (m = 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)) ∧ fluctuationHistory P γ (Geometry.explicitRoundedGrid jStar metric) jStar m + meanHistory P γ (Geometry.explicitRoundedGrid jStar metric) (↑jStar) m + determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar m ≤ C * (profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m + determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar m) ∧ (n + ↑h ≤ m → profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n (m + ↑h) + determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar (m + ↑h) ≤ 1 / 8 * Real.exp (↑(bigQ d γ) * synchCharge P (Geometry.explicitRoundedGrid jStar metric) (↑h) m) * (profile P γ (Geometry.explicitRoundedGrid jStar metric) jStar n m + determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar m) + C * (Real.exp (↑(bigQ d γ) * synchCharge P (Geometry.explicitRoundedGrid jStar metric) (↑h) m) - 1)) ∧ (∀ (m₀ : ℤ), ↑jStar + ↑h ≤ m₀ → ∀ (Ksteps : ℕ), 1 ≤ Ksteps → ∑ k ∈ Finset.range Ksteps, synchCharge P (Geometry.explicitRoundedGrid jStar metric) (↑h) (m₀ + ↑k * ↑h) ≤ ↑h * detIncrement P (Geometry.explicitRoundedGrid jStar metric) (m₀ + 1 - ↑h) (m₀ + ↑Ksteps * ↑h)) ∧ (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))

Exact bridge to the one-grid propagation statement.

source
theorem HCPolySupport.HighContrast.Multiscale.carried_history_majorization_one (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) :
∃ (Csrc : ℝ), 0 < Csrc ∧ ∃ (C : ℝ), 0 < C ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (n m : ℤ), ↑jStar ≤ n → n ≤ m → fluctuationHistory P γ 1 jStar m + meanHistory P γ 1 (↑jStar) m + determinantDrift P γ 1 jStar m ≤ C * (profile P γ 1 jStar n m + determinantDrift P γ 1 jStar m)

E1. e.fixed.geometry.carried.majorization on the Euclidean grid (the one-grid statement's conjunct 5 at metric = 1, h = 2Q, L = 1).

source
theorem HCPolySupport.HighContrast.Multiscale.synchronized_propagation_one (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) :
∃ (Csrc : ℝ), 0 < Csrc ∧ ∃ (C : ℝ), 0 < C ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (h : ℕ), 2 * bigQ d γ ≤ h → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (n m : ℤ), ↑jStar ≤ n → n + ↑h ≤ m → profile P γ 1 jStar n (m + ↑h) + determinantDrift P γ 1 jStar (m + ↑h) ≤ 1 / 8 * Real.exp (↑(bigQ d γ) * synchCharge P 1 (↑h) m) * (profile P γ 1 jStar n m + determinantDrift P γ 1 jStar m) + C * (Real.exp (↑(bigQ d γ) * synchCharge P 1 (↑h) m) - 1)

E2. e.fixed.geometry.synchronized.propagation on the Euclidean grid (the one-grid statement's conjunct 6 at metric = 1).

source
theorem HCPolySupport.HighContrast.Multiscale.synchronized_multiplicity_one (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) :
∃ (Csrc : ℝ), 0 < Csrc ∧ ∀ (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (Src : CoeffSpace d → ℝ), MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K Src → ∀ (h : ℕ), 2 * bigQ d γ ≤ h → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ⌈Csrc * Real.logb 3 (2 * K)⌉ ≤ ↑jStar → ∀ (m₀ : ℤ), ↑jStar + ↑h ≤ m₀ → ∀ (Ksteps : ℕ), 1 ≤ Ksteps → ∑ k ∈ Finset.range Ksteps, synchCharge P 1 (↑h) (m₀ + ↑k * ↑h) ≤ ↑h * detIncrement P 1 (m₀ + 1 - ↑h) (m₀ + ↑Ksteps * ↑h)

E3. e.fixed.geometry.synchronized.multiplicity on the Euclidean grid (the one-grid statement's conjunct 7 at metric = 1).