Documentation

LeanPool.HighContrastHomogenization.Support.Sobolev.Foundations.PoincareW1p.SmoothCase

Coarse-graining support: Support.Sobolev.Foundations.PoincareW1p.SmoothCase #

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

source
noncomputable def HCPolySupport.W1pFunction.smoothPoincareLpBase {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) :
ℝ

The geometric base of the smooth Lᵖ Poincare bound, formed from the domain volume, a chosen coordinate bound, the dimension, and the unit-ball volume.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def HCPolySupport.W1pFunction.smoothPoincareLpConst {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) :
    ℝ

    One plus the absolute value of the geometric base for the smooth Lᵖ Poincare bound.

    Equations
    Instances For
      source
      theorem HCPolySupport.W1pFunction.smoothPoincareLpConst_nonneg {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) :
      0 ≤ smoothPoincareLpConst hU
      source
      theorem HCPolySupport.W1pFunction.subAverageLpSeminorm_le_smoothPoincareLpConst_mul_gradientCoordLpSeminormSum_ofContDiff {d : ℕ} {U : Set (Vec d)} [NeZero d] [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hU : IsOpenBoundedConvexDomain U) {q : ℝ} (hq : 1 < q) {f : Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hvol : 0 < (MeasureTheory.volume U).toReal) :
      have u := ofContDiffOnIsOpenBoundedConvexDomain hU ⋯; u.subAverageLpSeminorm ≤ smoothPoincareLpConst hU * u.gradientCoordLpSeminormSum