High-contrast homogenization: Provider.PortableHistory.CheckpointMoment

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

The centered moment at the checkpoint

The startup estimate of p.fixed.geometry.one.grid.propagation needs one comparison between the two ways a centered response is measured: the Schatten size v_b^q, which is a mixed norm of (E_b^q)^{-1/2}(A_b^q(0) - E_b^q)(E_b^q)^{-1/2}, and the scalar size, which is what the centered history 𝓗_q^{cen}(b) accumulates. The printed step is

(v_b^q)^Q ≤ 2d 𝓗_q^{cen}(b),

"at scale b the operator norm is among the terms defining 𝓗_q^{cen}(b)".

Two facts produce it. First, the scalar size is the spectral norm of the normalized block. Its norm sandwich and the spectral Schatten estimate then bound the Schatten size by (2d)^{1/Q} times the scalar size. Second, the term of the supremum defining 𝓗_q^{cen}(b) at the scale j = b and the lattice index w = 0 is exactly the scalar size of the centered response of the cell ⋄_b^q, with geometric weight 3^0 = 1, and its center — the origin — lies in ⋄_b^q.

The scalar size against the Schatten size

theorem HCPolySupport.HighContrast.PortableHistory.zero_le_blockSize {d : ℕ} {X F : BlockMat d} (hX : IsSymmetricBlockMat X) (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) : 0 ≤ blockSize X F

The scalar size of a symmetric block against a positive block is nonnegative.

theorem HCPolySupport.HighContrast.PortableHistory.schattenSize_le_blockSize {d : ℕ} {X F : BlockMat d} (hX : IsSymmetricBlockMat X) (hF : IsSymmetricBlockMat F) (hFpd : Book.Ch02.BlockPosDef F) {Q : ℝ} (hQ : 0 < Q) : schattenSize Q X F ≤ (2 * ↑d) ^ Q⁻¹ * blockSize X F

The Schatten size costs at most (2d)^{1/Q} against the scalar size. The scalar size is the spectral norm of the normalized block, whose norm sandwich bounds its Schatten size by the dimensional factor.

The checkpoint term of the centered history

theorem HCPolySupport.HighContrast.PortableHistory.adaptedCellAt_zero {d : ℕ} (q : Mat d) (k : ℤ) : adaptedCellAt q k 0 = adaptedCell q k

The aligned adapted cell at the zero lattice index is the centered adapted cell.

theorem HCPolySupport.HighContrast.PortableHistory.ofReal_blockSize_le_centeredSup {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {q : Mat d} (hq : Matrix.PosDef q) {rhoMax : ℝ} {jStar b : ℤ} (hb : jStar ≤ b) (a : CoeffSpace d) : ENNReal.ofReal (blockSize (blockSub (coarseBlock (adaptedCell q b) a) (adaptedMean P q b)) (adaptedMean P q b)) ≤ ⨆ (j : ℤ), ⨆ (_ : jStar ≤ j), ⨆ (_ : j ≤ b), ⨆ (w : Fin d → ℤ), ⨆ (_ : adaptedCellCenter q j w ∈ adaptedCell q b), ENNReal.ofReal (3 ^ (-rhoMax * (↑b - ↑j)) * blockSize (blockSub (adaptedResponse q j w a) (adaptedMean P q j)) (adaptedMean P q b))

The centered response of the cell ⋄_b^q is one of the terms of the supremum defining 𝓗_q^{cen}(b).

The checkpoint display