Documentation

LeanPool.HighContrastHomogenization.Provider.Response.DiagonalWeakNormMaximum

High-contrast homogenization: Provider.Response.DiagonalWeakNormMaximum #

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

The all-scale response maximum #

This file turns the extended-real maximum of the diagonal weak estimate into pointwise real bounds whenever that maximum is finite. The extended-real carrier retains the divergent branch rather than assigning it a favourable real value.

source
theorem HCPolySupport.HighContrast.Response.blockSize_le_one_add_blockExcess {d : ℕ} {A E : BlockMat d} (hA : IsSymmetricBlockMat A) (hApsd : Matrix.PosSemidef (toFullBlockMat A)) (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) :
blockSize A E ≤ 1 + blockExcess A E

A positive response has size at most one plus its excess above the reference block.

source
theorem HCPolySupport.HighContrast.Response.blockExcess_nonneg {d : ℕ} {A E : BlockMat d} (hA : IsSymmetricBlockMat A) (hApsd : Matrix.PosSemidef (toFullBlockMat A)) (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) :
0 ≤ blockExcess A E

The excess of a positive response is nonnegative.

source
theorem HCPolySupport.HighContrast.Response.sqrt_blockSize_le_one_add_sqrt_blockExcess {d : ℕ} {A E : BlockMat d} (hA : IsSymmetricBlockMat A) (hApsd : Matrix.PosSemidef (toFullBlockMat A)) (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) :
√(blockSize A E) ≤ 1 + √(blockExcess A E)

Taking square roots in the size--excess comparison leaves the convenient majorant 1 + √excess.

source
theorem HCPolySupport.HighContrast.Response.weighted_excess_le_diagonalWeakMaximum_toReal {d : ℕ} {rho : ℝ} {q : Mat d} (hq : Matrix.PosDef q) {t k : ℤ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {a : CoeffSpace d} (hkt : k ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k t) (hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤) :
3 ^ (-rho * (↑t - ↑k)) * blockExcess (adaptedResponse q k w a) E ≤ (diagonalWeakMaximum rho q t E a).toReal

On the finite branch, every weighted cell excess is bounded by the real value of the extended maximum.

source
theorem HCPolySupport.HighContrast.Response.blockExcess_le_mul_rpow_of_weighted_le {rho B : ℝ} {t k : ℤ} {e : ℝ} (hweighted : 3 ^ (-rho * (↑t - ↑k)) * e ≤ B) :
e ≤ B * 3 ^ (rho * (↑t - ↑k))

Removing the maximum's weight costs the reciprocal geometric factor.

source
theorem HCPolySupport.HighContrast.Response.sqrt_blockExcess_le_sqrt_mul_rpow_of_weighted_le {rho B : ℝ} {t k : ℤ} {e : ℝ} (hB : 0 ≤ B) (hweighted : 3 ^ (-rho * (↑t - ↑k)) * e ≤ B) :
√e ≤ √B * 3 ^ (rho * (↑t - ↑k) / 2)

The square root of a cell excess inherits half of the maximum's geometric weight.

source
theorem HCPolySupport.HighContrast.Response.sqrt_blockSize_adaptedResponse_le_of_maximum_finite {d : ℕ} {rho : ℝ} {q : Mat d} (hq : Matrix.PosDef q) {t k : ℤ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) {a : CoeffSpace d} (hkt : k ≤ t) {w : Fin d → ℤ} (hw : w ∈ alignedIndex q k t) (hfinite : diagonalWeakMaximum rho q t E a ≠ ⊤) :
√(blockSize (adaptedResponse q k w a) E) ≤ 1 + √(diagonalWeakMaximum rho q t E a).toReal * 3 ^ (rho * (↑t - ↑k) / 2)

A finite all-scale maximum controls the square root of every normalized response block.