Integrability

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Local block energy: integrability workhorses

Two small IntegrableOn workhorses used throughout the test-identity expansion and the bulk/cutoff estimates. Every integrand appearing in the coupled weak-form expansion is either

• h · (F · G) with h ∈ L∞ and F, G ∈ L² (bulk / energy integrands), or
• u · (F · g) with u ∈ L², F ∈ L² and g ∈ L∞ (cutoff integrands).

Both are L¹ on the finite-measure cube; the two lemmas below package the Hölder/L∞ bookkeeping so the downstream files never touch it directly.

theorem HCPolySupport.integrableOn_memLpTop_mul_vecDot {d : ℕ} {U : Set (Vec d)} {h : Vec d → ℝ} {F G : Vec d → Vec d} (hh : MeasureTheory.MemLp h ⊤ (volumeMeasureOn U)) (hF : MemVectorL2 U F) (hG : MemVectorL2 U G) : MeasureTheory.IntegrableOn (fun (x : Vec d) => h x * vecDot (F x) (G x)) U MeasureTheory.volume

Bulk-type integrability. h · (F · G) is L¹ when h ∈ L∞ and F, G ∈ L².

theorem HCPolySupport.integrableOn_scalarL2_mul_vecDot_memLpTop {d : ℕ} {U : Set (Vec d)} {u : Vec d → ℝ} {F g : Vec d → Vec d} (hu : MemScalarL2 U u) (hF : MemVectorL2 U F) (hg : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => g x i) ⊤ (volumeMeasureOn U)) : MeasureTheory.IntegrableOn (fun (x : Vec d) => u x * vecDot (F x) (g x)) U MeasureTheory.volume

Cutoff-type integrability. u · (F · g) is L¹ when u, F ∈ L² and every coordinate of g lies in L∞.