Documentation

LeanPool.HighContrastHomogenization.Provider.Response.DivCurlCutoffCoefficient

High-contrast homogenization: Provider.Response.DivCurlCutoffCoefficient #

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

The div-curl coefficient at a cutoff of the cube's own scale #

The div-curl weak-norm coefficient depends on the cube through its side length and through the two bounds carried by the cutoff's gradient field: the sup norm of that field and a bound for its derivative. For a cutoff adapted to the cube these two bounds carry one and two negative powers of the side length respectively, so the side length cancels once and the coefficient inherits a single negative power of the side length with a dimension-only prefactor.

The prefactor is recorded here explicitly. The cutoff's own constant is kept abstract: for the canonical smooth product cutoff it necessarily grows with the dimension, so no numeral is available.

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

The dimension-only prefactor of the div-curl coefficient.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.Response.divCurlDimensionCoeff_nonneg (d : ℕ) :
    0 ≤ divCurlDimensionCoeff d

    The dimension-only prefactor is nonnegative.

    source
    theorem HCPolySupport.HighContrast.Response.divCurlWeakNormCoeff_originCube_le {d : ℕ} (t : ℤ) {B Bone Ccut : ℝ} (hBbound : B ≤ Ccut * 3 ^ (-2 * t)) (hBonebound : Bone ≤ Ccut * 3 ^ (-t)) :
    divCurlWeakNormCoeff (originCube d t) B Bone ≤ divCurlDimensionCoeff d * (Ccut * 3 ^ (-t))

    The div-curl coefficient at an adapted cutoff. With the cutoff's gradient field bounded by Ccut times the reciprocal side length and its derivative by Ccut times the square of the reciprocal side length, the coefficient is at most a dimension-only multiple of Ccut times the reciprocal side length.