Documentation

LeanPool.HighContrastHomogenization.Provider.Initialization.Boundary

High-contrast homogenization: Provider.Initialization.Boundary #

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

Lower bounds for the source boundary constant #

The witness eccentricity is a matrix condition number and is at least one. The geometric-series factor is also at least one for 0 ≤ g < 1; hence the printed boundary constant is at least one as soon as its dimensional factor is.

source
theorem HCPolySupport.HighContrast.Initialization.one_le_witnessEccentricity {d : ℕ} [Nonempty (Fin d)] {mu : Mat d} (hmu : Matrix.PosDef mu) :
1 ≤ witnessEccentricity mu

The eccentricity of a positive witness is at least one in positive dimension.

source
theorem HCPolySupport.HighContrast.Initialization.one_le_zetaG {g : ℝ} (hg : g ∈ Set.Ico 0 1) :
1 ≤ zetaG g

The geometric series factor is at least one for the source exponent range.

source
theorem HCPolySupport.HighContrast.Initialization.one_le_boundaryConst {d : ℕ} [Nonempty (Fin d)] {Cd g : ℝ} (hCd : 1 ≤ Cd) (hg : g ∈ Set.Ico 0 1) {mu : Mat d} (hmu : Matrix.PosDef mu) :
1 ≤ boundaryConst Cd g mu

The exact boundary-constant lower bound in the initialization anchor.