Coarse-graining support: Support.Sobolev.Foundations.PoincareW1p.Dilation #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
noncomputable def
HCPolySupport.W1pMeanZeroFunction.unscale
{d : ℕ}
{U : Set (Vec d)}
{p : ENNReal}
{a : ℝ}
(ha : 0 < a)
(u : W1pMeanZeroFunction (a • U) p)
:
Pull a mean-zero W^{1,p}(a • U) witness back to a mean-zero witness on
U by positive dilation.
Equations
- HCPolySupport.W1pMeanZeroFunction.unscale ha u = { toW1pFunction := HCPolySupport.W1pFunction.unscale ha u.toW1pFunction, meanZero := ⋯ }
Instances For
@[simp]
theorem
HCPolySupport.W1pMeanZeroFunction.unscale_toW1pFunction
{d : ℕ}
{U : Set (Vec d)}
{p : ENNReal}
{a : ℝ}
(ha : 0 < a)
(u : W1pMeanZeroFunction (a • U) p)
:
theorem
HCPolySupport.W1pMeanZeroFunction.gradientCoordLpSeminormSum_unscale_eq
{d : ℕ}
{U : Set (Vec d)}
{p : ENNReal}
{a : ℝ}
(ha : 0 < a)
(hp_top : p ≠ ⊤)
(u : W1pMeanZeroFunction (a • U) p)
:
(unscale ha u).gradientCoordLpSeminormSum = a * W1pFunction.dilationLpFactor d p a⁻¹ * u.gradientCoordLpSeminormSum
The coordinate-sum gradient seminorm under positive dilation pullback.
noncomputable def
HCPolySupport.W1pPoincareEstimate.dilate
{d : ℕ}
{U : Set (Vec d)}
{p : ENNReal}
{a : ℝ}
(ha : 0 < a)
(hp_top : p ≠ ⊤)
(hC : W1pPoincareEstimate U p)
:
W1pPoincareEstimate (a • U) p
Transport a finite-p mean-zero Poincare estimate to a positive dilation
of its domain. The constant gains exactly one factor of the dilation scale.
Equations
- HCPolySupport.W1pPoincareEstimate.dilate ha hp_top hC = { constantValue := a * hC.constantValue, constant_nonneg := ⋯, bound := ⋯ }
Instances For
@[simp]
theorem
HCPolySupport.W1pPoincareEstimate.dilate_constant
{d : ℕ}
{U : Set (Vec d)}
{p : ENNReal}
{a : ℝ}
(ha : 0 < a)
(hp_top : p ≠ ⊤)
(hC : W1pPoincareEstimate U p)
: