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

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

The trace inequality, the mean penalty and drift positivity

Group C of the printed proof (p.fixed.geometry.one.grid.propagation): the positive-semidefinite trace inequality, composition and advance of the mean penalty, its exponential bound, the loss/trace comparison, and nonnegativity of the determinant drift.

Part of the proof of the printed proposition p.fixed.geometry.one.grid.propagation, stated 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 HCPoly/Entry/OneGridPropagation.lean; this group's stronger internal algebraic and history lemmas omit an unused threshold on the source lower scale, 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 C. The printed trace inequality, the mean penalty and drift positivity

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

theorem HCPolySupport.HighContrast.Multiscale.trace_mul_le_trace_mul_trace {ι : Type u_1} [Fintype ι] {A B : Matrix ι ι ℝ} (hA : A.PosSemidef) (hB : B.PosSemidef) : (A * B).trace ≤ A.trace * B.trace

tr(AB) ≤ (tr A)(tr B) for positive semidefinite A, B: the positivity step behind the printed trace inequality (p.fixed.geometry.one.grid.propagation).

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

The printed composition of mean penalties across a change of normalization (p.fixed.geometry.one.grid.propagation): 1 + Ψ_Q(P^q_{j,m}) ≤ (1 + Ψ_Q(P^q_{n,m}))(1 + Ψ_Q(P^q_{j,n})).

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

The mean-penalty advance used in Steps 2 and 4 (p.fixed.geometry.one.grid.propagation): Ψ_Q(P^q_{j,k}) ≤ e^{QΔ^q_{m,k}}Ψ_Q(P^q_{j,m}) + e^{QΔ^q_{m,k}} - 1 for j ≤ m ≤ k.

theorem HCPolySupport.HighContrast.Multiscale.meanPenalty_normalizedMean_le_exp_sub_one (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 → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ∀ (metric : Mat d), Matrix.PosDef metric → ∀ (j k : ℤ), ↑jStar ≤ j → j ≤ k → meanPenalty (bigQ d γ) (relMean P (Geometry.explicitRoundedGrid jStar metric) j k) ≤ Real.exp (↑(bigQ d γ) * detIncrement P (Geometry.explicitRoundedGrid jStar metric) j k) - 1

Ψ_Q(P^q_{j,k}) ≤ e^{QΔ^q_{j,k}} - 1, the bound used for the generations above the base (p.fixed.geometry.one.grid.propagation).

theorem HCPolySupport.HighContrast.Multiscale.logDetLoss_le_blockTrace_normalizedMean (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 → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ∀ (metric : Mat d), Matrix.PosDef metric → ∀ (j k : ℤ), ↑jStar ≤ j → j ≤ k → detIncrement P (Geometry.explicitRoundedGrid jStar metric) j k ≤ blockTrace (blockSub (relMean P (Geometry.explicitRoundedGrid jStar metric) j k) (Book.Ch02.blockIdentity d))

Δ^q_{j,k} ≤ tr(P^q_{j,k} - I_{2d}) (p.fixed.geometry.one.grid.propagation), the step that converts a loss into a profile term in Step 4.

theorem HCPolySupport.HighContrast.Multiscale.determinantDrift_nonneg (d : ℕ) (hd : 2 ≤ d) (γ : ℝ) (P : MeasureTheory.Measure (CoeffSpace d)) (E : BlockMat d) (Ψ : ℝ → ℝ) (K : ℝ) (S : CoeffSpace d → ℝ) : MeasureTheory.IsProbabilityMeasure P → IsStationaryLaw P → IsUnitRangeLaw P → CoarseEllipticityDagger P γ E Ψ K S → ∀ (jStar : ℕ), 2 * d ≤ 3 ^ jStar → ∀ (metric : Mat d), Matrix.PosDef metric → ∀ (m : ℤ), 0 ≤ determinantDrift P γ (Geometry.explicitRoundedGrid jStar metric) jStar m

The determinant drift is nonnegative: each printed increment P^q_{j-1,m} - P^q_{j,m} is a normalized positive semidefinite increment, and the weights are positive.