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

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

Exponent And Loss Arithmetic

This module proves the exponent arithmetic of the one-grid propagation and the algebra of the log-determinant loss it is applied to. It establishes the numeric facts about Q = 𝒬(d,γ) and the contraction, span and averaging coefficients, the elementary exponential inequalities and the geometric profile weights; and it proves additivity of the log-determinant loss, its comparison with the synchronized loss, and the synchronized multiplicity bound. It serves p.fixed.geometry.one.grid.propagation.

Printed exponent and coefficient arithmetic

Group A of the printed proof (p.fixed.geometry.one.grid.propagation): the numeric facts about Q = 𝒬(d,γ), the contraction, span and averaging coefficients, the elementary exponential inequalities and the geometric profile weights.

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 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 A. The printed exponent and coefficient arithmetic

(p.fixed.geometry.one.grid.propagation)

theorem HCPolySupport.HighContrast.Multiscale.bigQ_twelve_le (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : 12 ≤ bigQ d γ

Q ≥ 12 for d ≥ 2 and γ ∈ [0,1) (p.fixed.geometry.one.grid.propagation).

theorem HCPolySupport.HighContrast.Multiscale.one_sub_gamma_mul_span_ge (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (h : ℕ) (hh : 2 * bigQ d γ ≤ h) : 8 * (↑d + 1) ≤ (1 - γ) * ↑h

(1-γ)h ≥ 2(1-γ)Q ≥ 8(d+1) for every natural h ≥ 2Q (p.fixed.geometry.one.grid.propagation).

theorem HCPolySupport.HighContrast.Multiscale.three_rpow_neg_eighth_span_lt (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (h : ℕ) (hh : 2 * bigQ d γ ≤ h) : 3 ^ (-((1 - γ) / 8) * ↑h) < 1 / 8

3^{-⅛(1-γ)h} ≤ 3^{-3} < 1/8 for every natural h ≥ 2Q (p.fixed.geometry.one.grid.propagation). This is the drift half of the contraction.

theorem HCPolySupport.HighContrast.Multiscale.two_bigQ_mul_three_rpow_le_third (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : 2 * ↑(bigQ d γ) * 3 ^ (-↑d * (↑(bigQ d γ) - 1)) ≤ 1 / 3

2Q·3^{-d(Q-1)} ≤ 1/3 (p.fixed.geometry.one.grid.propagation).

theorem HCPolySupport.HighContrast.Multiscale.contraction_coefficient_lt (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (h : ℕ) (hh : 2 * bigQ d γ ≤ h) : 3 ^ (-((1 - γ) / 4) * ↑h) + 2 ^ (bigQ d γ - 1) * (3 ^ d * ↑(bigQ d γ)) ^ bigQ d γ * 3 ^ (-(↑(bigQ d γ) * ↑d / 2) * ↑h) < 1 / 8

The printed contraction coefficient 3^{-¼(1-γ)h} + 2^{Q-1}(3^dQ)^Q 3^{-Qdh/2} ≤ 3^{-6} + ½·3^{-12} < 1/8, for every natural h ≥ 2Q (p.fixed.geometry.one.grid.propagation).

theorem HCPolySupport.HighContrast.Multiscale.span_coefficient_le (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : 2 ^ (bigQ d γ - 1) * (3 ^ d * ↑(bigQ d γ)) ^ bigQ d γ * 3 ^ (-↑d * ↑(bigQ d γ) ^ 2) ≤ 1 / 8

The span-2Q coefficient 2^{Q-1}(3^dQ)^Q 3^{-dQ²} ≤ 1/8 used in Step 4, where the recurrence is applied with the fixed span 2Q so that the constants do not depend on the possibly larger h (p.fixed.geometry.one.grid.propagation).

theorem HCPolySupport.HighContrast.Multiscale.averaging_coefficient_le (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) : ↑(bigQ d γ) * 3 ^ (↑d / 2) * (1 + (2 * ↑d) ^ (↑(bigQ d γ))⁻¹) ≤ 3 ^ d * ↑(bigQ d γ)

Q·3^{d/2}(1 + (2d)^{1/Q}) ≤ 3^d Q for d ≥ 2, Q ≥ 2 (p.fixed.geometry.one.grid.propagation): the step that turns the recurrence's printed prefactor into the contraction's.

theorem HCPolySupport.HighContrast.Multiscale.exp_pred_mul_sub_one_le (N : ℕ) (hN : 1 ≤ N) (t : ℝ) (ht : 0 ≤ t) : Real.exp ((↑N - 1) * t) * (Real.exp t - 1) ≤ Real.exp (↑N * t) - 1

e^{(N-1)t}(e^t - 1) ≤ e^{Nt} - 1 for t ≥ 0 (p.fixed.geometry.one.grid.propagation).

theorem HCPolySupport.HighContrast.Multiscale.exp_mul_le_add_exp_sub_one (x a : ℝ) (hx : 0 ≤ x) (_ha : 0 ≤ a) (ha1 : a ≤ 1) : Real.exp x * a ≤ a + Real.exp x - 1

e^x a ≤ a + e^x - 1 for 0 ≤ a ≤ 1 and x ≥ 0 (p.fixed.geometry.one.grid.propagation).

theorem HCPolySupport.HighContrast.Multiscale.profile_geometric_weight_sum_le (γ : ℝ) (hγ : γ ∈ Set.Ico 0 1) (a b : ℤ) : ∑ j ∈ Finset.Ico a b, 3 ^ (-((1 - γ) / 4) * (↑b - 1 - ↑j)) ≤ (1 - 3 ^ (-((1 - γ) / 4)))⁻¹

The geometric tail of the profile weights is bounded by a constant depending only on γ (p.fixed.geometry.one.grid.propagation, "the geometric sum is bounded by C").

Log-determinant loss algebra and the multiplicity bound

Group B of the printed proof (p.fixed.geometry.one.grid.propagation): additivity of the log-determinant loss, its comparison with the synchronized loss, and conjunct 7, e.fixed.geometry.synchronized.multiplicity.

Part of the proof of 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 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 B. Log-determinant loss algebra and the multiplicity bound

(p.fixed.geometry.one.grid.propagation)

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

Δ^q_{j-h,m+h} ≤ Δ̂^q_h(m) for m < j ≤ m+h (p.fixed.geometry.one.grid.propagation). Taking j = m+h gives the Δ^q_{m,m+h} ≤ Δ̂^q_h(m) used in Step 3.

theorem HCPolySupport.HighContrast.Multiscale.synchronized_multiplicity (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 → ∀ (h : ℕ), 2 * bigQ d γ ≤ h → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ∀ (metric : Mat d), Matrix.PosDef metric → ∀ (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)

Conjunct 7, e.fixed.geometry.synchronized.multiplicity (p.fixed.geometry.one.grid.propagation): expand the synchronized losses into adjacent increments, observe that the smallest index is at least j_* and that each increment occurs at most h times.