BallPoincare #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Poincare readout on local sup-balls #
theorem
Algsuperdiff.StochasticProcess.Common.Regularity.Ported.normalizedL2On_axisCube_sub_average_le_vectorGradient
{d : ℕ}
(z : HCPolySupport.Vec d)
{L : ℝ}
(hL : 0 < L)
(u : HCPolySupport.H1Function (HCPolySupport.axisCube z L))
:
(Section4.Support.normalizedL2On (HCPolySupport.axisCube z L) fun (x : HCPolySupport.Vec d) =>
u.toFun x - HCPolySupport.volumeAverage (HCPolySupport.axisCube z L) u.toFun) ≤ HCPolySupport.unitMeanZeroPoincareConst d * L * ↑d * vectorNormalizedL2On (HCPolySupport.axisCube z L) u.grad
Normalized mean-zero Poincare on an arbitrary positive axis cube, with the gradient already aggregated in the Euclidean vector carrier.
theorem
Algsuperdiff.StochasticProcess.Common.Regularity.Ported.normalizedL2On_metricBall_sub_average_le_vectorGradient
{d : ℕ}
(x : HCPolySupport.Vec d)
{r : ℝ}
(hr : 0 < r)
(u : HCPolySupport.H1Function (Metric.ball x r))
:
(Section4.Support.normalizedL2On (Metric.ball x r) fun (y : HCPolySupport.Vec d) =>
u.toFun y - HCPolySupport.volumeAverage (Metric.ball x r) u.toFun) ≤ HCPolySupport.unitMeanZeroPoincareConst d * (2 * r) * ↑d * vectorNormalizedL2On (Metric.ball x r) u.grad
The same Poincare row on the open sup-ball realization.