HolderL2Interpolation #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Square integrability from continuity and a Hölder bound #
A continuous function with a finite Hölder bound on a bounded cube has a
uniform pointwise bound there, hence belongs to L² on the cube.
References #
- ABK26, the localized error and regularity quantities of Section 5.1.
Square integrability #
theorem
Algsuperdiff.Section5.Support.memLp_two_of_continuousOn_of_holder
{d : ℕ}
{y : HCPolySupport.Vec d}
{n : ℤ}
{K : ℝ}
(hK : 0 ≤ K)
{f : HCPolySupport.Vec d → ℝ}
(hcont : ContinuousOn f (cubeSetAt y n))
(hf : Section4.Support.HolderSeminormBoundOn (cubeSetAt y n) (1 / 2) K f)
:
MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (cubeSetAt y n))