Documentation

LeanPool.HighContrastHomogenization.Support.Internal.Ch02.SubadditivityScaling

Coarse-graining support: Support.Internal.Ch02.SubadditivityScaling #

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

source
noncomputable def HCPolySupport.Internal.Ch02.BookCh02.coeffOnOfIsEllipticFieldOn {d : ℕ} (U : Book.Ch02.Domain d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U.carrier a) :
Book.Ch02.CoeffOn U

Turn an old pointwise elliptic field on a Book domain into a public CoeffOn. This is only an internal bridge from old proof engines to the a.e.-native public surface.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.Internal.Ch02.BookCh02.responseSubadditivityAndScalingTheory {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) :
    Book.Ch02.ResponseSubadditivityAndScalingTheory U a