Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.RowSupply.ResponseAttainabilityPricing

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.RowSupply.ResponseAttainabilityPricing

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

Response times attainability pricing on ruled observation cubes #

The Dirichlet flux right-hand side contains the outer-exponent-one response at the regularity order. A strict exponent gap converts it to the outer-exponent-two response at a lower order. The result is a product of that response and the Dirichlet energy price, exactly matching the two factors in the deterministic homogenization estimate.

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

The geometric-series loss in the conversion from an outer-exponent-two response at order b to an outer-exponent-one response at the strictly larger order r.

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