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

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

ℝ≥0∞ bridge for the overlap Besov pieces

The overlap Besov seminorms are real-valued (eLpNorm-.toReal style); the comparison estimates run in ℝ≥0∞. This file performs the ofReal/toReal crossing once: each real Besov piece is rewritten as (or bounded by) its ℝ≥0∞ counterpart here, and the proof files never touch toReal again.

Bridge lemmas toward the Gagliardo side are stated as junk-value-safe inequalities (≤), which hold without integrability hypotheses; equalities hold under MemLp and are provided where needed.

theorem HCPolySupport.Gagliardo.ofReal_oscillation_rpow_le {d : ℕ} (S : TriadicCube d) (p : ENNReal) (u : Vec d → ℝ) : ENNReal.ofReal (cubeBesovOverlapOscillation S p u ^ p.toReal) ≤ MeasureTheory.eLpNorm (fun (x : Vec d) => u x - ScalarOverlap.cubeAverage S u) p (ScalarOverlap.normalizedCubeMeasure S) ^ p.toReal

BR4 (junk-safe): the p-th power of the overlap oscillation, pushed to ℝ≥0∞, is at most the corresponding eLpNorm power. No integrability hypothesis: if the eLpNorm is infinite the right side is ∞.

theorem HCPolySupport.Gagliardo.ofReal_depthAverage_eq {d : ℕ} (Q : TriadicCube d) (j : ℕ) (p : ENNReal) (u : Vec d → ℝ) : ENNReal.ofReal (cubeBesovOverlapDepthAverage Q p u j) = (↑(ScalarOverlap.centersAtDepth Q j).card)⁻¹ * ∑ S ∈ ScalarOverlap.centersAtDepth Q j, ENNReal.ofReal (cubeBesovOverlapOscillation S p u ^ p.toReal)

BR3: the depth average crosses to ℝ≥0∞ as an explicit averaged sum.

theorem HCPolySupport.Gagliardo.ofReal_depthSeminorm_rpow_eq {d : ℕ} (Q : TriadicCube d) (s : ℝ) {p : ENNReal} (hp0 : p ≠ 0) (hpt : p ≠ ⊤) (u : Vec d → ℝ) (j : ℕ) : ENNReal.ofReal (cubeBesovOverlapDepthSeminorm Q s p u j ^ p.toReal) = ENNReal.ofReal (cubeBesovOverlapDepthWeight Q s j ^ p.toReal) * ENNReal.ofReal (cubeBesovOverlapDepthAverage Q p u j)

BR2: the depth seminorm's p-th power crosses to ℝ≥0∞ as weight-power times depth average.

theorem HCPolySupport.Gagliardo.ofReal_partialSeminorm_rpow_eq {d : ℕ} (Q : TriadicCube d) (s : ℝ) {p : ENNReal} (hp0 : p ≠ 0) (hpt : p ≠ ⊤) (N : ℕ) (u : Vec d → ℝ) : ENNReal.ofReal (cubeBesovOverlapPartialSeminorm Q s p p N u ^ p.toReal) = ∑ j ∈ Finset.range (N + 1), ENNReal.ofReal (cubeBesovOverlapDepthSeminorm Q s p u j ^ p.toReal)

BR1: the partial seminorm's p-th power crosses to ℝ≥0∞ as the sum of the depth-seminorm powers (diagonal case q = p).