High-contrast homogenization: Setup.Moments

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

Moment and history carriers for the fixed-grid estimates

The objects the fixed-grid section builds on a doubled block matrix and on the adapted geometry: the Schatten norm |H|_{S_Q} and the mixed norm ‖H‖_{L^Q(S_Q)}, the scalar sizes |F^{-1/2}HF^{-1/2}| and |(F^{-1/2}(H-F)F^{-1/2})_+|, the gain functions Φ_Q and 𝔥_Q, the adapted moment carriers A_j^q(z), E_j^q, v_j^q, Δ_{j,T}^q, P_{j,T}^q, the portable histories 𝓗_q^cen, 𝓗_q^nl, 𝓗_q and the profile 𝒫_q(T;b), the synchronized charge, and the linear drift.

Three encoding conventions are used throughout and are recorded here.

Scalar sizes are Loewner. For a symmetric H and a positive F the number |F^{-1/2}HF^{-1/2}| is the least t ≥ 0 with -tF ≤ H ≤ tF, and the size of the positive part of F^{-1/2}(H-F)F^{-1/2} is the least t ≥ 0 with H ≤ (1+t)F. Both are written in that form, as the intrinsic contrast and the scalar bound of the setup layer are; no matrix square root enters a scalar size. The reference text never defines the matrix positive part; the Loewner form is the reading forced by its two uses, that the positive part of a symmetric matrix is its spectral positive part.

Schatten sizes are spectral. The Schatten norm has no Loewner form, so |H|_{S_Q} = (tr((H²)^{Q/2}))^{1/Q} is written with the continuous functional calculus of the nonnegative symmetric matrix H², at an arbitrary real Q ≥ 1, and the normalization F^{-1/2}HF^{-1/2} is the literal conjugation by the positive semidefinite square root of F⁻¹ that the setup layer has already characterized as the unique such root.

Failing closed. Every quantity whose finiteness is a hypothesis or a conclusion of the reference text — the mixed norms, the histories, the profiles, the suprema over infinite cell families — is valued in ℝ≥0∞. An unbounded supremum or a divergent moment is then ∞ rather than a real junk value, and the reference text's convention that the supremum of an empty family of nonnegative quantities is zero is the lattice's own.

Doubled block arithmetic

def HCPolySupport.HighContrast.blockSub {d : ℕ} (A B : BlockMat d) : BlockMat d

The difference of two doubled block matrices.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.blockSharp {d : ℕ} (H : BlockMat d) : BlockMat d

The sharp involution H^♯ = R H^{-1} R of a positive block, the conjugation by the reflection being the block reflection of the ambient layer. At the reference block this is 𝐄_* = (R𝐄R)^{-1}, and 𝐄_*^{-1} = R𝐄R is blockReflect 𝐄 (the dual of the coarse block).

Equations

• HCPolySupport.HighContrast.blockSharp H = HCPolySupport.blockReflect (HCPolySupport.Book.Ch02.blockMatInv H)

noncomputable def HCPolySupport.HighContrast.blockLogDet {d : ℕ} (H : BlockMat d) : ℝ

The log-determinant of a doubled block matrix.

Equations

• HCPolySupport.HighContrast.blockLogDet H = Real.log (Matrix.det (HCPolySupport.toFullBlockMat H))

def HCPolySupport.HighContrast.blockTrace {d : ℕ} (H : BlockMat d) : ℝ

The trace of a doubled block matrix.

Equations

• HCPolySupport.HighContrast.blockTrace H = Matrix.trace (HCPolySupport.toFullBlockMat H)

noncomputable def HCPolySupport.HighContrast.normalizedBlock {d : ℕ} (H F : BlockMat d) : BlockMat d

The normalized block F^{-1/2} H F^{-1/2}, the square root being the positive semidefinite square root of F⁻¹.

Equations

• One or more equations did not get rendered due to their size.

Scalar sizes: the Loewner encodings of |F^{-1/2} · F^{-1/2}|

noncomputable def HCPolySupport.HighContrast.blockSize {d : ℕ} (H F : BlockMat d) : ℝ

|F^{-1/2} H F^{-1/2}| for a symmetric H and a positive F: the least t ≥ 0 with -tF ≤ H ≤ tF. On a positive H the lower constraint is vacuous. At H = 𝐄 this is the normalization Λ(F;𝐄) of the source-control subsection; at F = 𝐄_* and H = 𝐄 it is κ_𝐄.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.blockExcess {d : ℕ} (H F : BlockMat d) : ℝ

|(F^{-1/2}(H - F)F^{-1/2})_+|, the size of the positive part of the F-normalized excess: the least t ≥ 0 with H ≤ (1+t)F.

Equations

• HCPolySupport.HighContrast.blockExcess H F = sInf {t : ℝ | 0 ≤ t ∧ HCPolySupport.BlockMatLoewnerLE H (HCPolySupport.HighContrast.blockScale (1 + t) F)}

The Schatten norm and the mixed norm

noncomputable def HCPolySupport.HighContrast.schattenNorm {d : ℕ} (Q : ℝ) (H : BlockMat d) : ℝ

The Schatten norm |H|_{S_Q} = (tr((H²)^{Q/2}))^{1/Q} of a symmetric doubled block matrix, the power of the nonnegative symmetric matrix H² being taken by the continuous functional calculus.

Equations

• HCPolySupport.HighContrast.schattenNorm Q H = (cfc (fun (x : ℝ) => x ^ (Q / 2)) (HCPolySupport.toFullBlockMat H * HCPolySupport.toFullBlockMat H)).trace ^ Q⁻¹

noncomputable def HCPolySupport.HighContrast.schattenSize {d : ℕ} (Q : ℝ) (H F : BlockMat d) : ℝ

The Schatten norm |F^{-1/2} H F^{-1/2}|_{S_Q} of the F-normalized matrix.

Equations

• HCPolySupport.HighContrast.schattenSize Q H F = HCPolySupport.HighContrast.schattenNorm Q (HCPolySupport.HighContrast.normalizedBlock H F)

noncomputable def HCPolySupport.HighContrast.lqSchattenSize {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (Q : ℝ) (A : CoeffSpace d → BlockMat d) (F : BlockMat d) : ENNReal

The mixed norm ‖F^{-1/2} H F^{-1/2}‖_{L^Q(S_Q)} = (E[|·|_{S_Q}^Q])^{1/Q} of a random doubled block matrix normalized by a deterministic positive F.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.lqNorm {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (Q : ℝ) (X : CoeffSpace d → ℝ) : ENNReal

The L^Q norm of a real random variable.

Equations

• HCPolySupport.HighContrast.lqNorm P Q X = MeasureTheory.eLpNorm X (ENNReal.ofReal Q) P

The gain functions

noncomputable def HCPolySupport.HighContrast.gainPhi (Q x : ℝ) : ℝ

Φ_Q(x) = e^{(1-1/Q)x}(e^x-1)^{1/Q} + (e^x-1), for x ≥ 0.

Equations

• HCPolySupport.HighContrast.gainPhi Q x = Real.exp ((1 - Q⁻¹) * x) * (Real.exp x - 1) ^ Q⁻¹ + (Real.exp x - 1)

noncomputable def HCPolySupport.HighContrast.frakH {d : ℕ} (Q : ℝ) (Pm : BlockMat d) : ℝ

𝔥_Q(P) = (1 + tr(P - I))^Q - 1, for P ≥ I.

Equations

• HCPolySupport.HighContrast.frakH Q Pm = (1 + (HCPolySupport.HighContrast.blockTrace Pm - 2 * ↑d)) ^ Q - 1

The adapted moment carriers

noncomputable def HCPolySupport.HighContrast.adaptedCellCenter {d : ℕ} (q : Mat d) (r : ℤ) (w : Fin d → ℤ) : Vec d

The center 3^r q w of the aligned adapted cell z + ⋄_r^q, z ∈ 3^r 𝕃_q (the adapted cubes of a rounded geometry).

Equations

• HCPolySupport.HighContrast.adaptedCellCenter q r w = 3 ^ r • HCPolySupport.matVecMul q fun (i : Fin d) => ↑(w i)

noncomputable def HCPolySupport.HighContrast.adaptedResponse {d : ℕ} (q : Mat d) (r : ℤ) (w : Fin d → ℤ) (a : CoeffSpace d) : BlockMat d

The adapted response A_r^q(z) = 𝐀(z + ⋄_r^q) at the aligned center z = 3^r q w.

Equations

• HCPolySupport.HighContrast.adaptedResponse q r w a = HCPolySupport.HighContrast.coarseBlock (HCPolySupport.HighContrast.adaptedCellAt q r w) a

noncomputable def HCPolySupport.HighContrast.adaptedMean {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q : Mat d) (r : ℤ) : BlockMat d

The adapted mean E_r^q = E[A_r^q(0)].

Equations

• HCPolySupport.HighContrast.adaptedMean P q r = HCPolySupport.HighContrast.annealedBlock P (HCPolySupport.HighContrast.adaptedCell q r)

def HCPolySupport.HighContrast.HasFiniteAdaptedMean {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q : Mat d) (r : ℤ) : Prop

Finiteness of the adapted mean: the coarse response over the adapted cell is integrable, so E_r^q is the expectation it names.

Equations

• HCPolySupport.HighContrast.HasFiniteAdaptedMean P q r = HCPolySupport.HighContrast.HasIntegrableCoarseBlock P (HCPolySupport.HighContrast.adaptedCell q r)

noncomputable def HCPolySupport.HighContrast.centeredMoment {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (Q : ℝ) (q : Mat d) (r : ℤ) : ENNReal

The centered normalized moment v_r^q = ‖(E_r^q)^{-1/2}(A_r^q(0) - E_r^q)(E_r^q)^{-1/2}‖_{L^Q(S_Q)}.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.detIncrement {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q : Mat d) (j T : ℤ) : ℝ

The determinant increment Δ_{j,T}^q = log det E_j^q - log det E_T^q.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.relMean {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q : Mat d) (j T : ℤ) : BlockMat d

The relative mean P_{j,T}^q = (E_T^q)^{-1/2}E_j^q(E_T^q)^{-1/2}.

Equations

• HCPolySupport.HighContrast.relMean P q j T = HCPolySupport.HighContrast.normalizedBlock (HCPolySupport.HighContrast.adaptedMean P q j) (HCPolySupport.HighContrast.adaptedMean P q T)

noncomputable def HCPolySupport.HighContrast.synchCharge {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (q : Mat d) (h T : ℤ) : ℝ

The synchronized charge Δ̂_h^q(T) = Σ_{j=T+1}^{T+h} Δ_{j-h,j}^q.

Equations

• HCPolySupport.HighContrast.synchCharge P q h T = ∑ j ∈ Finset.Icc (T + 1) (T + h), HCPolySupport.HighContrast.detIncrement P q (j - h) j

The portable histories and the profile

noncomputable def HCPolySupport.HighContrast.centeredHistory {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (Q rhoMax : ℝ) (q : Mat d) (jStar b : ℤ) : ENNReal

The centered history 𝓗_q^cen(b) (e.scale.selection.fluctuation.history).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.nonlinearHistory {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (Q a : ℝ) (q : Mat d) (jStar b : ℤ) : ENNReal

The nonlinear history 𝓗_q^nl(b) (02, after e.scale.selection.fluctuation.history).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.portableHistory {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (Q a rhoMax : ℝ) (q : Mat d) (jStar b : ℤ) : ENNReal

The complete history 𝓗_q(b) = 𝓗_q^cen(b) + 𝓗_q^nl(b).

Equations

• HCPolySupport.HighContrast.portableHistory P Q a rhoMax q jStar b = HCPolySupport.HighContrast.centeredHistory P Q rhoMax q jStar b + HCPolySupport.HighContrast.nonlinearHistory P Q a q jStar b

noncomputable def HCPolySupport.HighContrast.portableProfile {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (Q a rhoMax : ℝ) (q : Mat d) (jStar b T : ℤ) : ENNReal

The portable profile 𝒫_q(T;b) (e.scale.selection.complete.profile).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.linearDrift {d : ℕ} (P : MeasureTheory.Measure (CoeffSpace d)) (rhoDr : ℝ) (q : Mat d) (b T : ℤ) : ℝ

The linear drift 𝒟_{q,b}^{ρ_dr}(T), the determinant drift e.scale.selection.determinant.drift at a general drift exponent.

Equations

• One or more equations did not get rendered due to their size.

The contraction parameters

noncomputable def HCPolySupport.HighContrast.lambdaCen (d : ℕ) (Q a Crec : ℝ) (h : ℤ) : ℝ

The centered contraction factor λ_cen = 3^{-ha} + 2^{Q-1}C_rec^Q 3^{-hQd/2} (02, in p.fixed.geometry.one.grid.propagation).

Equations

• HCPolySupport.HighContrast.lambdaCen d Q a Crec h = 3 ^ (-↑h * a) + 2 ^ (Q - 1) * Crec ^ Q * 3 ^ (-↑h * Q * ↑d / 2)

noncomputable def HCPolySupport.HighContrast.lambdaPort (d : ℕ) (Q a Crec : ℝ) (h : ℤ) : ℝ

The portable contraction factor λ_port = max{3^{-ha} + 2^{Q-1}C_rec^Q3^{-hQd/2}, 3^{-ha}} (02, in p.fixed.geometry.one.grid.propagation).

Equations

• HCPolySupport.HighContrast.lambdaPort d Q a Crec h = max (HCPolySupport.HighContrast.lambdaCen d Q a Crec h) (3 ^ (-↑h * a))

theorem HCPolySupport.HighContrast.adaptedCellAt_eq_adaptedCellTranslate {d : ℕ} (q : Mat d) (r : ℤ) (w : Fin d → ℤ) : adaptedCellAt q r w = adaptedCellTranslate q r (adaptedCellCenter q r w)

An aligned adapted cell is the translate of the centered adapted cell by its own center.