ForcingLp #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Local normalized L² control from the source L^p datum #
theorem
Algsuperdiff.StochasticProcess.Common.Regularity.Ported.memVectorL2_of_memVectorLpOn_of_subset
{d : ℕ}
{U W : Set (HCPolySupport.Vec d)}
{p : ℝ}
{f : HCPolySupport.Vec d → HCPolySupport.Vec d}
[MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict W)]
(hp2 : 2 ≤ p)
(hWU : W ⊆ U)
(hf : MemVectorLpOn U p f)
:
Restriction and finite-measure exponent lowering from the source carrier to the quadratic weak-test carrier.
noncomputable def
Algsuperdiff.StochasticProcess.Common.Regularity.Ported.normalizedVolumeOn
{d : ℕ}
(W : Set (HCPolySupport.Vec d))
:
Volume restricted to a set and scaled by the inverse of its volume.
Equations
Instances For
theorem
Algsuperdiff.StochasticProcess.Common.Regularity.Ported.vectorNormalizedL2On_le_volume_rpow_mul_vectorLpSizeOn
{d : ℕ}
{U W : Set (HCPolySupport.Vec d)}
{p : ℝ}
{f : HCPolySupport.Vec d → HCPolySupport.Vec d}
(hp0 : 0 < p)
(hp2 : 2 ≤ p)
(hWU : W ⊆ U)
(hW : 0 < (MeasureTheory.volume W).toReal)
(hf : MemVectorLpOn U p f)
:
Finite-measure Hölder embedding in exactly the normalized vector carrier. The volume factor is explicit and therefore can be evaluated geometrically on balls without hiding exponent dependence in a constant.