BallForcing

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Dimension-only normalization of the source term on Euclidean balls

noncomputable def Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastUnitBallVolumePrice (d : ℕ) : ℝ

A dimension-only upper bound for the harmless unit-ball normalization.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.smallContrastUnitBallVolumePrice_nonneg (d : ℕ) : 0 ≤ smallContrastUnitBallVolumePrice d

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.unitBallVolume_rpow_neg_inv_le_price {d : ℕ} {p : ℝ} (hp : 1 ≤ p) : (MeasureTheory.volume (smallContrastUnitBall d)).toReal ^ (-1 / p) ≤ smallContrastUnitBallVolumePrice d

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.volume_euclideanBall_toReal_eq_unit_mul_pow {d : ℕ} [NeZero d] (z : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : (MeasureTheory.volume (HCPolySupport.euclideanBall z r)).toReal = (MeasureTheory.volume (smallContrastUnitBall d)).toReal * r ^ d

Exact scaling of Euclidean-ball volume from the unit ball.

theorem Algsuperdiff.StochasticProcess.Common.Regularity.Ported.vectorNormalizedL2On_euclideanBall_le_price_mul_rpow_mul_globalLp {d : ℕ} [NeZero d] {U : Set (HCPolySupport.Vec d)} (z : HCPolySupport.Vec d) {r p : ℝ} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hr : 0 < r) (hp : 2 ≤ p) (hball : HCPolySupport.euclideanBall z r ⊆ U) (hf : MemVectorLpOn U p f) : vectorNormalizedL2On (HCPolySupport.euclideanBall z r) f ≤ smallContrastUnitBallVolumePrice d * r ^ (-↑d / p) * vectorLpSizeOn U p f

The local normalized L² source row on a ball, with all dependence on its radius explicit and the remaining normalization depending only on d.