Documentation

LeanPool.HighContrastHomogenization.Support.Deterministic.CoarsePoincare.Setup.Conversions

Coarse-graining support: Support.Deterministic.CoarsePoincare.Setup.Conversions #

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

Deterministic coarse-grained Poincare inequalities #

This file packages the first deterministic Chapter-3 q = 1 Poincare step.

At the current checkpoint we keep the one-cube energy estimate as an explicit hypothesis on descendant cube averages. This isolates the honest downstream multiscale summation argument while the fully note-faithful Chapter-2 energy-averaging interface is still being stabilized upstream.

source
def HCPolySupport.CubeAverageGradientEnergyControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (g : Vec d → Vec d) (energy : Vec d → ℝ) :
Prop

Descendant cube-average control for gradients by the local coarse σ_*^{-1} block and a scalar energy density.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def HCPolySupport.CubeAverageFluxEnergyControl {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (flux : Vec d → Vec d) (energy : Vec d → ℝ) :
    Prop

    Descendant cube-average control for fluxes by the local coarse b block and a scalar energy density.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem HCPolySupport.responseJ_le_plainUpperBound_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hEll : IsEllipticFieldOn lam Lam U a) (hvol : (MeasureTheory.volume U).toReal ≠ 0) (p q : Vec d) :
      ResponseJ U p q a ≤ lam⁻¹ * (Lam ^ 2 * vecNormSq p + vecNormSq q)
      source
      theorem HCPolySupport.matNorm_le_two_mul_card_mul_of_posSemidef_of_quadratic_le {d : ℕ} {A : Mat d} {C : ℝ} (hPos : Matrix.PosSemidef A) (hC : 0 ≤ C) (hquad : ∀ (x : Vec d), vecDot x (matVecMul A x) ≤ C * vecNormSq x) :
      matNorm A ≤ 2 * ↑(Fintype.card (Fin d)) * C