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

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

Assembly pieces for the Besov-to-Gagliardo direction

Three small bridges used by the final estimate:

• MemWsp-side restriction: global L^p membership on the parent cube restricts to every enlarged center cube (with the normalization change absorbed into a finite scalar);
• the kernel identification: the p-th enorm power of the Gagliardo kernel is exactly the distance power times the difference power (U4);
• the lintegral of the Gagliardo product measure as a normalized plain product integral.

theorem HCPolySupport.Gagliardo.memLp_overlap_of_memLp {d : ℕ} {Q : TriadicCube d} {p : ENNReal} {u : Vec d → ℝ} (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) {j : ℕ} {S : TriadicCube d} (hS : S ∈ ScalarOverlap.centersAtDepth Q j) : MeasureTheory.MemLp u p (ScalarOverlap.normalizedCubeMeasure S)

Restriction step: L^p membership for the parent's normalized measure implies membership for every center's normalized enlarged-cube measure.

theorem HCPolySupport.Gagliardo.enorm_gagliardoKernel_rpow {d : ℕ} (s : ℝ) {p : ENNReal} (hp0 : p ≠ 0) (hpt : p ≠ ⊤) (u : Vec d → ℝ) (z : Vec d × Vec d) : ‖gagliardoKernel s p u z‖ₑ ^ p.toReal = ENNReal.ofReal (dist z.1 z.2 ^ (-(s * p.toReal + ↑d))) * ‖u z.1 - u z.2‖ₑ ^ p.toReal

U4 (kernel identification): pointwise, the p-th enorm power of the Gagliardo kernel splits into the distance power times the difference power. Both sides vanish on the diagonal, so no case split is needed downstream.

theorem HCPolySupport.Gagliardo.lintegral_gagliardoCubeMeasure_eq {d : ℕ} (Q : TriadicCube d) (f : Vec d × Vec d → ENNReal) : ∫⁻ (z : Vec d × Vec d), f z ∂gagliardoCubeMeasure Q = ENNReal.ofReal (cubeVolume Q)⁻¹ * ∫⁻ (z : Vec d × Vec d) in cubeSet Q ×ˢ cubeSet Q, f z ∂MeasureTheory.volume.prod MeasureTheory.volume

The Gagliardo cube measure integrates as the volume-normalized plain product integral over Q ×ˢ Q.