Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.MultiscaleEllipticityExponentGap

High-contrast homogenization: Provider.Regularity.MultiscaleEllipticityExponentGap #

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

Exponent-gap control of multiscale ellipticity #

The outer-exponent-one ellipticity rows at order r are controlled by the outer-exponent-two rows at every smaller positive order b. The proof is the same weighted Cauchy--Schwarz argument as the response-error exponent bridge.

source
noncomputable def HCPolySupport.HighContrast.exponentGapFactor (b r : ℝ) :
ℝ

The square of the response-exponent gap factor between orders b < r. This is the whole loss incurred when a q = 1 quantity at order r is read off the q = 2 row at the strictly smaller order b; it is finite for every such pair, so no relation between r and 2 * b is ever needed.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem HCPolySupport.HighContrast.exponentGapFactor_pos {b r : ℝ} (hb : 0 < b) (hbr : b < r) :
    0 < exponentGapFactor b r

    The response-exponent gap factor is positive on every admissible pair.

    source
    theorem HCPolySupport.HighContrast.LambdaS_le_exponentGap_mul_LambdaSq_finite_two {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : Book.Ch02.TriadicCoeffFamily d) {b r : ℝ} (hb : 0 < b) (hbr : b < r) :
    Book.Ch02.LambdaS Q r a ≤ (Book.Ch02.geometricDiscount r 1 * (√(Book.Ch02.geometricDiscount (r - b) 2))⁻¹ * (√(Book.Ch02.geometricDiscount b 2))⁻¹) ^ 2 * Book.Ch02.LambdaSq Q b (Book.Ch02.MultiscaleExponent.finite 2) a

    The upper q = 1 ellipticity at order r is controlled by the upper q = 2 ellipticity at every smaller positive order b.

    source
    theorem HCPolySupport.HighContrast.lambdaS_inv_le_exponentGap_mul_lambdaSq_finite_two_inv {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : Book.Ch02.TriadicCoeffFamily d) {b r : ℝ} (hb : 0 < b) (hbr : b < r) :
    (Book.Ch02.lambdaS Q r a)⁻¹ ≤ (Book.Ch02.geometricDiscount r 1 * (√(Book.Ch02.geometricDiscount (r - b) 2))⁻¹ * (√(Book.Ch02.geometricDiscount b 2))⁻¹) ^ 2 * (Book.Ch02.lambdaSq Q b (Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹

    The inverse lower q = 1 ellipticity at order r is controlled by the inverse lower q = 2 ellipticity at every smaller positive order b.