High-contrast homogenization: Entry.Multiscale.DriftAdvance

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

Drift Advance

The identities of the diagonal profile and the finite-sum algebra of the determinant drift they advance. At equal generations the profile is the printed prefactor times the history, and it equals the history once the terminal mean is positive definite; the drift algebra splits the printed determinant drift at an intermediate generation, telescopes the log-determinant loss, and bounds one synchronized step of the drift by the terminal loss increment. These deterministic finite-sum facts are the drift-advance input to p.fixed.geometry.one.grid.propagation.

Diagonal profile identities

This file contains only the deterministic finite-sum and normalization algebra needed at the diagonal m = n. The positivity assumption is kept exactly where the total normalization needs it.

theorem HCPolySupport.HighContrast.Multiscale.matSqrt_inv_posDef_full {ι : Type u_1} [Fintype ι] [DecidableEq ι] {m : Matrix ι ι ℝ} (hm : m.PosDef) : (matSqrt m⁻¹).PosDef

The inverse square root is positive definite on every finite real matrix carrier.

theorem HCPolySupport.HighContrast.Multiscale.normalizedBlock_self_of_posDef {d : ℕ} (F : BlockMat d) (hF : Matrix.PosDef (toFullBlockMat F)) : normalizedBlock F F = Book.Ch02.blockIdentity d

Normalizing a positive definite block by itself gives the doubled identity.

theorem HCPolySupport.HighContrast.Multiscale.meanPenalty_identity {d : ℕ} (Q : ℕ) : meanPenalty Q (Book.Ch02.blockIdentity d) = 0

The mean penalty of the identity is zero, for every natural moment including 0.

theorem HCPolySupport.HighContrast.Multiscale.profile_self_eq_factor_mul_history {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (q : Mat d) (jStar : ℕ) (n : ℤ) : profile P γ q jStar n n = (1 + meanPenalty (bigQ d γ) (relMean P q n n)) * history P γ q jStar n

At the diagonal, the profile is exactly the printed prefactor times the history.

theorem HCPolySupport.HighContrast.Multiscale.profile_self_of_posDef {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (q : Mat d) (jStar : ℕ) (n : ℤ) (hF : Matrix.PosDef (toFullBlockMat (adaptedMean P q n))) : profile P γ q jStar n n = history P γ q jStar n

With a positive terminal mean, the diagonal normalized mean is the identity.

Determinant drift algebra

Spectral trace/determinant bounds, positive matrix normalization, and the finite-sum algebra for the printed determinant drift. The matrix-family hypotheses are deterministic support inputs; their annealed proofs are the mean order of p.fixed.geometry.parent.child.recurrence.

theorem HCPolySupport.HighContrast.Multiscale.determinantDrift_split {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (q : Mat d) (jStar : ℕ) (m L : ℤ) (hm : ↑jStar ≤ m) (hL : 0 ≤ L) : determinantDrift P γ q jStar (m + L) = ∑ j ∈ Finset.Icc (↑jStar + 1) m, 3 ^ (-((1 - γ) / 8) * (↑(m + L) - ↑j)) * blockTrace (blockSub (relMean P q (j - 1) (m + L)) (relMean P q j (m + L))) + ∑ j ∈ Finset.Icc (m + 1) (m + L), 3 ^ (-((1 - γ) / 8) * (↑(m + L) - ↑j)) * blockTrace (blockSub (relMean P q (j - 1) (m + L)) (relMean P q j (m + L)))

Split the printed drift sum at an intermediate generation m.

theorem HCPolySupport.HighContrast.Multiscale.det_matSqrt_sq {ι : Type u_1} [Fintype ι] [DecidableEq ι] {m : Matrix ι ι ℝ} (hm : m.PosSemidef) : (matSqrt m).det ^ 2 = m.det

The determinant of the positive square root has the expected square.

theorem HCPolySupport.HighContrast.Multiscale.det_normalized_eq_div {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F G : Matrix ι ι ℝ) (hG : G.PosDef) : (matSqrt G⁻¹ * F * matSqrt G⁻¹).det = F.det / G.det

The normalized determinant is the quotient of full determinants.

theorem HCPolySupport.HighContrast.Multiscale.det_normalizedBlock_eq_exp {d : ℕ} (F G : BlockMat d) (hF : Matrix.PosDef (toFullBlockMat F)) (hG : Matrix.PosDef (toFullBlockMat G)) : Matrix.det (toFullBlockMat (normalizedBlock F G)) = Real.exp (blockLogDet F - blockLogDet G)

Full log determinants give the normalization factor with coefficient one.

theorem HCPolySupport.HighContrast.Multiscale.normalized_trace_sub_one_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {F G : Matrix ι ι ℝ} (hF : F.PosDef) (hG : G.PosDef) (hGF : G ≤ F) : (matSqrt G⁻¹ * F * matSqrt G⁻¹ - 1).trace ≤ F.det / G.det - 1

The conjugated trace/determinant bound on a positive definite pair.

theorem HCPolySupport.HighContrast.Multiscale.normalizedMean_trace_sub_identity_le {d : ℕ} (F G : BlockMat d) (hF : Matrix.PosDef (toFullBlockMat F)) (hG : Matrix.PosDef (toFullBlockMat G)) (hGF : BlockMatLoewnerLE G F) : blockTrace (blockSub (normalizedBlock F G) (Book.Ch02.blockIdentity d)) ≤ Real.exp (blockLogDet F - blockLogDet G) - 1

The printed trace increment bound for normalized full blocks.

theorem HCPolySupport.HighContrast.Multiscale.matrix_le_det_smul_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {P : Matrix ι ι ℝ} (hP : P.IsHermitian) (hIP : 1 ≤ P) : P ≤ P.det • 1

Every eigenvalue is bounded by the determinant when all eigenvalues are at least one.

theorem HCPolySupport.HighContrast.Multiscale.normalized_increment_trace_le {d : ℕ} (F G H : BlockMat d) (hF : Matrix.PosDef (toFullBlockMat F)) (hG : Matrix.PosDef (toFullBlockMat G)) (hH : Matrix.PosSemidef (toFullBlockMat H)) (hGF : BlockMatLoewnerLE G F) : blockTrace (normalizedBlock H G) ≤ Real.exp (blockLogDet F - blockLogDet G) * blockTrace (normalizedBlock H F)

Changing normalization of a positive increment costs at most the full determinant ratio. The argument uses spectral order, inverse order and cyclic trace, without commutativity.

theorem HCPolySupport.HighContrast.Multiscale.blockLogDet_normalizedMean_eq_loss {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q : Mat d) (j k : ℤ) (hj : Matrix.PosDef (toFullBlockMat (adaptedMean P q j))) (hk : Matrix.PosDef (toFullBlockMat (adaptedMean P q k))) : blockLogDet (relMean P q j k) = detIncrement P q j k

The logarithm of the normalized mean is exactly the loss increment.

theorem HCPolySupport.HighContrast.Multiscale.logDetLoss_add {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q : Mat d) (i j k : ℤ) : detIncrement P q i j + detIncrement P q j k = detIncrement P q i k

The full log-determinant loss telescopes without analytic premises.

theorem HCPolySupport.HighContrast.Multiscale.determinantDrift_advance_of_posDef_antitone {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (γ : ℝ) (hγ : γ ≤ 1) (q : Mat d) (jStar : ℕ) (m L : ℤ) (hm : ↑jStar ≤ m) (hL : 1 ≤ L) (hpos : ∀ j ∈ Set.Icc (↑jStar) (m + L), Matrix.PosDef (toFullBlockMat (adaptedMean P q j))) (horder : ∀ j ∈ Set.Icc (↑jStar + 1) (m + L), BlockMatLoewnerLE (adaptedMean P q j) (adaptedMean P q (j - 1))) : determinantDrift P γ q jStar (m + L) ≤ 3 ^ (-((1 - γ) / 8) * ↑L) * Real.exp (detIncrement P q m (m + L)) * determinantDrift P γ q jStar m + Real.exp (detIncrement P q m (m + L)) - 1

The printed drift advance for a positive adjacent-decreasing mean family. These finite-dimensional hypotheses are the future outputs of annealed mean order; no integrability of the total real drift formula is required.