Coarse-graining support: Support.Sobolev.Fractional.JensenStep

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Jensen/averaging step for the Gagliardo seminorm on overlap cubes

This file proves the per-cube Jensen step (U1): for an overlap cube S, the p-th power of the L^p(μ) oscillation of u around its cube average is controlled by the doubled L^p difference integral, where μ = ScalarOverlap.normalizedCubeMeasure S is the probability normalization of volume on the enlarged cube of S.

The proof is the standard one: the deviation from the average is the average of differences (probability measure), the enorm of a Bochner integral is at most the lintegral of enorms, and L^1(μ) ↪ L^p(μ) on a probability measure (Jensen/Hölder).

theorem HCPolySupport.Gagliardo.eLpNorm_sub_average_rpow_le_double_lintegral {d : ℕ} (S : TriadicCube d) {p : ENNReal} (hp : 1 ≤ p) (hpt : p ≠ ⊤) {u : Vec d → ℝ} (hu : MeasureTheory.MemLp u p (ScalarOverlap.normalizedCubeMeasure S)) : MeasureTheory.eLpNorm (fun (x : Vec d) => u x - ScalarOverlap.cubeAverage S u) p (ScalarOverlap.normalizedCubeMeasure S) ^ p.toReal ≤ ∫⁻ (x : Vec d), ∫⁻ (y : Vec d), ‖u x - u y‖ₑ ^ p.toReal ∂ScalarOverlap.normalizedCubeMeasure S ∂ScalarOverlap.normalizedCubeMeasure S

U1 (Jensen per cube): the p-th power of the L^p oscillation around the cube average is at most the doubled L^p difference integral, for a probability normalization and 1 ≤ p < ∞.