High-contrast homogenization: Provider.Response.DiagonalWeakNormRecentDecomposition

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

Decomposition of a recent scale

The centered parent state is split through the child optimizer. The first piece is the coarse-block comparison term; the second is the averaged optimizer-difference term controlled by its exact energy.

theorem HCPolySupport.HighContrast.Response.blockCellAverage_recent_difference {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k t) (a : CoeffSpace d) (p r : Vec d) : (blockCellAverage (adaptedCellAt q k w) fun (x : Vec d) => diagonalWeakChildState hq k w a p r x - diagonalWeakState hq t a p r x) = blockCellAverage (adaptedCellAt q k w) (diagonalWeakChildState hq k w a p r) - blockCellAverage (adaptedCellAt q k w) (diagonalWeakState hq t a p r)

Averaging the recent child/parent state difference is the difference of their cell averages.

theorem HCPolySupport.HighContrast.Response.diagonalWeak_recent_scale_decomposition_le {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {S m : Mat d} (hsymm : matTranspose S = S) (hsq : S * S = m) (hm : Matrix.PosDef m) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {rho delta : ℝ} (hrho : 0 < rho) (hdelta1 : delta ≤ 1) {a : CoeffSpace d} (p r : Vec d) (hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤) (hgood : (diagonalWeakMaximum rho q t E a).toReal ≤ delta) : (blockAvsumL2 (alignedIndex q k t) fun (w : Fin d → ℤ) => blockMatVecMul (Book.Ch02.blockDiag S S⁻¹) (blockCellAverage (adaptedCellAt q k w) (diagonalWeakState hq t a p r) - blockCellAverage (adaptedCell q t) (diagonalWeakState hq t a p r))) ≤ diagonalWeakMetricFactor m E * diagonalWeakLoadMinus E p r * diagonalWeakCellDefect q k t E a + 4 * diagonalWeakMetricFactor m E * diagonalWeakLoadMinus E p r * 3 ^ (rho * (↑t - ↑k) / 2) * √(blockSize (diagonalWeakAverageDefect q k t E a) (Book.Ch02.blockIdentity d))

The centered parent contribution at one recent scale is the sum of the cell-defect and averaged-defect bounds.

The released split level

noncomputable def HCPolySupport.HighContrast.Response.recentConstantAtLevel (delta : ℝ) : ℝ

The recent-scale coefficient at a released split level.

Equations

• HCPolySupport.HighContrast.Response.recentConstantAtLevel delta = √2 * (1 + √delta)

theorem HCPolySupport.HighContrast.Response.one_le_recentConstantAtLevel (delta : ℝ) : 1 ≤ recentConstantAtLevel delta

theorem HCPolySupport.HighContrast.Response.zero_le_recentConstantAtLevel (delta : ℝ) : 0 ≤ recentConstantAtLevel delta

theorem HCPolySupport.HighContrast.Response.diagonalWeak_recent_scale_decomposition_at_level_le {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) {k t : ℤ} (hkt : k ≤ t) {S m : Mat d} (hsymm : matTranspose S = S) (hsq : S * S = m) (hm : Matrix.PosDef m) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {rho delta : ℝ} (hrho : 0 < rho) {a : CoeffSpace d} (p r : Vec d) (hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤) (hgood : (diagonalWeakMaximum rho q t E a).toReal ≤ delta) : (blockAvsumL2 (alignedIndex q k t) fun (w : Fin d → ℤ) => blockMatVecMul (Book.Ch02.blockDiag S S⁻¹) (blockCellAverage (adaptedCellAt q k w) (diagonalWeakState hq t a p r) - blockCellAverage (adaptedCell q t) (diagonalWeakState hq t a p r))) ≤ diagonalWeakMetricFactor m E * diagonalWeakLoadMinus E p r * diagonalWeakCellDefect q k t E a + recentConstantAtLevel delta * diagonalWeakMetricFactor m E * diagonalWeakLoadMinus E p r * 3 ^ (rho * (↑t - ↑k) / 2) * √(blockSize (diagonalWeakAverageDefect q k t E a) (Book.Ch02.blockIdentity d))

The centered parent contribution at one recent scale, at a released split level.