High-contrast homogenization: Entry.OneGridPropagation

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

One-grid propagation

The type repeats the statement of HCPoly/Entry/Statements/OneGridPropagation.lean (p.fixed.geometry.one.grid.propagation): same binders, same binder kinds and order, same eight guarded conjuncts, the source-lower-scale premise where the statement has it, and no additional hypothesis. This source-facing statement carries the source lower scale exactly; the internal algebraic and history lemmas it assembles (in HCPoly/Entry/Multiscale/OneGrid/) include stronger statements that omit an unused source-scale threshold, and the generic integration helpers among them take finiteness, integrability or measurability inputs that are proved at their own use sites, not extra premises of this proposition.

The eight conjuncts are proved in HCPoly/Entry/Multiscale/OneGrid/, one printed step per file; this file only assembles them under one Csrc and one C = C(d,γ) chosen before the law, the geometry, h, L and j_*, as the statement requires.

theorem HCPolySupport.HighContrast.Entry.fixed_geometry_one_grid_propagation_full (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))

The eight-conclusion form of p.fixed.geometry.one.grid.propagation: the four printed conclusions (i)–(iv) of the proposition together with the four estimates that the paper proves on the way (e.fixed.geometry.profile.contraction, e.fixed.geometry.profile.fixed.span, e.fixed.geometry.profile.startup, e.fixed.geometry.carried.majorization), all under one C_src and one C = C(d,γ). The proposition's own statement projects out of this one.

Assembled from the eight conjunct proofs by taking one Csrc and one C above all of theirs. The proposition's own C is a single C(d,γ); the printed proof's "C may change from line to line" is realized by the per-conjunct existentials, never by a constant that sees the law, the geometry, h, L or j_*.

theorem HCPolySupport.HighContrast.Entry.fixedGeometryPropagation (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) + 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 = 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)) ∧ ∀ (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)

The statement proved for p.fixed.geometry.one.grid.propagation: the four printed conclusions (i)–(iv), projected out of fixed_geometry_one_grid_propagation_full, whose eight conclusions list them as the first, sixth, eighth and seventh. The statement repeats the statement HCPolySupport.HighContrast.fixed_geometry_one_grid_propagation (HCPoly/Entry/Statements/OneGridPropagation.lean) byte for byte.