Documentation

LeanPool.HighContrastHomogenization.Provider.Response.PreYoungPartialConstants

High-contrast homogenization: Provider.Response.PreYoungPartialConstants #

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

Common coefficients for the pre-Young estimate #

The weak-product and boundary-row estimates have distinct dimensional coefficients. Their maximum is the component coefficient supplied to the algebraic pre-Young closure.

source
noncomputable def HCPolySupport.HighContrast.Response.preYoungDivCurlCoefficient (d : ℕ) :
ℝ

The coefficient in the annealed weak-product estimate.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.HighContrast.Response.preYoungRowCoefficient (d : ℕ) :
    ℝ

    The coefficient left after summing the boundary-row scale weights.

    Equations
    Instances For
      source
      noncomputable def HCPolySupport.HighContrast.Response.preYoungComponentCoefficient (d : ℕ) :
      ℝ

      A common coefficient for the weak-product and boundary-row terms.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem HCPolySupport.HighContrast.Response.preYoungRowCoefficient_nonneg (d : ℕ) :
        0 ≤ preYoungRowCoefficient d
        source
        theorem HCPolySupport.HighContrast.Response.preYoungRowCoefficient_le_component (d : ℕ) :
        preYoungRowCoefficient d ≤ preYoungComponentCoefficient d
        source
        theorem HCPolySupport.HighContrast.Response.preYoungDivCurlCoefficient_le_component (d : ℕ) :
        preYoungDivCurlCoefficient d ≤ preYoungComponentCoefficient d
        source
        theorem HCPolySupport.HighContrast.Response.preYoungComponentCoefficient_nonneg (d : ℕ) :
        0 ≤ preYoungComponentCoefficient d