Documentation

LeanPool.HighContrastHomogenization.Provider.Quenched.UnitRangeCellArithmetic

High-contrast homogenization: Provider.Quenched.UnitRangeCellArithmetic #

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

Constants for the one-cell renormalization estimate #

source
noncomputable def HCPolySupport.HighContrast.Quenched.unitRangeCellGain (d : ℕ) (g : ℝ) (E : BlockMat d) :
ℝ

The dimension, old exponent, and reference cost in the one-cell estimate.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.HighContrast.Quenched.unitRangeCellGain_pos {d : ℕ} [NeZero d] {g : ℝ} {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (hsharp : BlockMatLoewnerLE (blockSharp E) E) :
    0 < unitRangeCellGain d g E