BallDirichletPoincare #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Explicit Dirichlet Poincaré inequality on Euclidean balls #
The ball datum is extended by zero to the equal-radius sup ball, realized as an axis cube. This is the ball-specific bridge required by the zeroth-order energy comparison.
theorem
Algsuperdiff.StochasticProcess.Common.Regularity.Ported.normalizedL2On_euclideanBall_le_vectorGradient
{d : ℕ}
[NeZero d]
(z : HCPolySupport.Vec d)
{r : ℝ}
(hr : 0 < r)
(rho : HCPolySupport.H10Function (HCPolySupport.euclideanBall z r))
:
Section4.Support.normalizedL2On (HCPolySupport.euclideanBall z r) rho.toFun ≤ unitCubeDirichletPoincareExplicit d * (2 * r) * ↑d * vectorNormalizedL2On (HCPolySupport.euclideanBall z r) rho.grad
Normalized Dirichlet Poincaré on a Euclidean ball, with an explicit dimension-only constant inherited from the unit axis cube.