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

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

Besov-to-Gagliardo comparison: the partial overlap Besov seminorm is

controlled by the fractional Sobolev seminorm

Main result (ofReal_partialSeminorm_rpow_le_gagliardo): for every depth truncation N, the p-th power of the diagonal overlap Besov partial seminorm is at most 2 * 3^d times the p-th power of the volume-normalized Gagliardo seminorm. The constant is purely dimensional.

Proof skeleton: the ℝ≥0∞ bridge (ENNRealBridge) rewrites the partial seminorm power as a sum of depth pieces; Jensen (JensenStep) bounds each per-cube oscillation by a doubled difference integral; the depth coefficient collapses (scale bookkeeping + the 3^{dj} center count); the per-pair backwards geometric tail (TailSummation) and the bounded-overlap count (OverlapIntegral) convert the depth sum into the Gagliardo kernel integral (AssemblyPieces).

theorem HCPolySupport.Gagliardo.measurable_pair_diff_enorm_rpow {d : ℕ} {u : Vec d → ℝ} (humeas : Measurable u) (pr : ℝ) : Measurable fun (z : Vec d × Vec d) => ‖u z.1 - u z.2‖ₑ ^ pr

Measurability of the pairwise difference enorm power.

theorem HCPolySupport.Gagliardo.lintegral_indicator_one_mul {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {A : Set α} (hA : MeasurableSet A) (G : α → ENNReal) : ∫⁻ (z : α), A.indicator (fun (x : α) => 1) z * G z ∂μ = ∫⁻ (z : α) in A, G z ∂μ

Multiplying by a 0/1 indicator inside a lintegral restricts the domain.

theorem HCPolySupport.Gagliardo.double_lintegral_normalized_eq {d : ℕ} (S : TriadicCube d) {pr : ℝ} {u : Vec d → ℝ} (humeas : Measurable u) : ∫⁻ (x : Vec d), ∫⁻ (y : Vec d), ‖u x - u y‖ₑ ^ pr ∂ScalarOverlap.normalizedCubeMeasure S ∂ScalarOverlap.normalizedCubeMeasure S = ENNReal.ofReal (ScalarOverlap.cubeVolume S)⁻¹ * (ENNReal.ofReal (ScalarOverlap.cubeVolume S)⁻¹ * ∫⁻ (z : Vec d × Vec d) in ScalarOverlap.cubeSet S ×ˢ ScalarOverlap.cubeSet S, ‖u z.1 - u z.2‖ₑ ^ pr ∂MeasureTheory.volume.prod MeasureTheory.volume)

Unnormalization: the doubled lintegral against the normalized enlarged-cube measure is the volume-normalized product set-lintegral.

theorem HCPolySupport.Gagliardo.ofReal_oscillation_rpow_le_setProd {d : ℕ} (S : TriadicCube d) {p : ENNReal} (hp : 1 ≤ p) (hpt : p ≠ ⊤) {u : Vec d → ℝ} (humeas : Measurable u) (hu : MeasureTheory.MemLp u p (ScalarOverlap.normalizedCubeMeasure S)) : ENNReal.ofReal (cubeBesovOverlapOscillation S p u ^ p.toReal) ≤ ENNReal.ofReal (ScalarOverlap.cubeVolume S)⁻¹ * (ENNReal.ofReal (ScalarOverlap.cubeVolume S)⁻¹ * ∫⁻ (z : Vec d × Vec d) in ScalarOverlap.cubeSet S ×ˢ ScalarOverlap.cubeSet S, ‖u z.1 - u z.2‖ₑ ^ p.toReal ∂MeasureTheory.volume.prod MeasureTheory.volume)

Per-center bound (U1 + U2): the p-th power of the overlap oscillation is controlled by the volume-normalized product set-lintegral of differences.

theorem HCPolySupport.Gagliardo.depth_coeff_identity {cQ : ℝ} (hc : 0 < cQ) (d j : ℕ) (t : ℝ) : (cQ / 3 ^ j) ^ (-t) * ((3 ^ (d * j))⁻¹ * (((cQ / 3 ^ j) ^ d)⁻¹ * ((cQ / 3 ^ j) ^ d)⁻¹)) = (cQ ^ d)⁻¹ * (cQ / 3 ^ j) ^ (-(t + ↑d))

Real coefficient identity for one depth: weight power times the depth count inverse times the squared volume inverse collapses to the parent volume inverse times the kernel scale power.

theorem HCPolySupport.Gagliardo.depth_coefficient_le {d : ℕ} (Q : TriadicCube d) (j : ℕ) (s pr : ℝ) : ENNReal.ofReal (cubeBesovOverlapDepthWeight Q s j ^ pr) * ((↑(ScalarOverlap.centersAtDepth Q j).card)⁻¹ * (ENNReal.ofReal ((cubeScaleFactor Q / 3 ^ j) ^ d)⁻¹ * ENNReal.ofReal ((cubeScaleFactor Q / 3 ^ j) ^ d)⁻¹)) ≤ ENNReal.ofReal (cubeVolume Q)⁻¹ * ENNReal.ofReal ((cubeScaleFactor Q / 3 ^ j) ^ (-(s * pr + ↑d)))

Depth coefficient bound: weight power times center-count inverse times the squared per-cube volume normalization is at most the parent volume inverse times the kernel scale power.

theorem HCPolySupport.Gagliardo.ofReal_depthSeminorm_rpow_le_sum {d : ℕ} (Q : TriadicCube d) {s : ℝ} {p : ENNReal} (hp : 1 ≤ p) (hpt : p ≠ ⊤) {u : Vec d → ℝ} (humeas : Measurable u) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (j : ℕ) : ENNReal.ofReal (cubeBesovOverlapDepthSeminorm Q s p u j ^ p.toReal) ≤ ENNReal.ofReal (cubeVolume Q)⁻¹ * (ENNReal.ofReal ((cubeScaleFactor Q / 3 ^ j) ^ (-(s * p.toReal + ↑d))) * ∑ S ∈ ScalarOverlap.centersAtDepth Q j, ∫⁻ (z : Vec d × Vec d) in ScalarOverlap.cubeSet S ×ˢ ScalarOverlap.cubeSet S, ‖u z.1 - u z.2‖ₑ ^ p.toReal ∂MeasureTheory.volume.prod MeasureTheory.volume)

Per-depth bound: the p-th power of one depth seminorm is controlled by the kernel-scale-weighted sum of product set-lintegrals over the centers.

theorem HCPolySupport.Gagliardo.sum_setLIntegral_eq_lintegral_count {d : ℕ} (Q : TriadicCube d) (j : ℕ) {F : Vec d × Vec d → ENNReal} (hF : Measurable F) : ∑ S ∈ ScalarOverlap.centersAtDepth Q j, ∫⁻ (z : Vec d × Vec d) in ScalarOverlap.cubeSet S ×ˢ ScalarOverlap.cubeSet S, F z ∂MeasureTheory.volume.prod MeasureTheory.volume = ∫⁻ (z : Vec d × Vec d), (∑ S ∈ ScalarOverlap.centersAtDepth Q j, (ScalarOverlap.cubeSet S ×ˢ ScalarOverlap.cubeSet S).indicator (fun (x : Vec d × Vec d) => 1) z) * F z ∂MeasureTheory.volume.prod MeasureTheory.volume

Sum of product set-lintegrals over the depth-j centers as one lintegral against the pointwise overlap count.

theorem HCPolySupport.Gagliardo.filtered_scale_sum_le {d : ℕ} (Q : TriadicCube d) {a : ℝ} (ha : 1 ≤ a) {D : ℝ} (hD : 0 < D) (N : ℕ) : ∑ j ∈ Finset.range (N + 1) with D ≤ cubeScaleFactor Q / 3 ^ j, ENNReal.ofReal ((cubeScaleFactor Q / 3 ^ j) ^ (-a)) ≤ 2 * ENNReal.ofReal (D ^ (-a))

Backwards geometric tail: over depths whose enlarged side dominates a fixed positive distance D, the kernel scale powers sum to at most 2 * D^(-a).

theorem HCPolySupport.Gagliardo.pointwise_pair_sum_le {d : ℕ} (Q : TriadicCube d) {a pr : ℝ} (ha : 1 ≤ a) (hpr : 0 < pr) (u : Vec d → ℝ) (N : ℕ) (z : Vec d × Vec d) : ∑ j ∈ Finset.range (N + 1), ENNReal.ofReal ((cubeScaleFactor Q / 3 ^ j) ^ (-a)) * ((∑ S ∈ ScalarOverlap.centersAtDepth Q j, (ScalarOverlap.cubeSet S ×ˢ ScalarOverlap.cubeSet S).indicator (fun (x : Vec d × Vec d) => 1) z) * ‖u z.1 - u z.2‖ₑ ^ pr) ≤ 2 * 3 ^ d * ((cubeSet Q ×ˢ cubeSet Q).indicator (fun (x : Vec d × Vec d) => 1) z * (ENNReal.ofReal (dist z.1 z.2 ^ (-a)) * ‖u z.1 - u z.2‖ₑ ^ pr))

Pointwise pair bound: for each pair z, the depth sum of kernel-scale powers times overlap counts times the difference power is controlled by the distance power on the parent product cube, with constant 2 * 3^d.

theorem HCPolySupport.Gagliardo.ofReal_partialSeminorm_rpow_le_gagliardo {d : ℕ} [NeZero d] (Q : TriadicCube d) {s : ℝ} (hs : 0 ≤ s) {p : ENNReal} (hp : 1 ≤ p) (hpt : p ≠ ⊤) {u : Vec d → ℝ} (humeas : Measurable u) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (N : ℕ) : ENNReal.ofReal (cubeBesovOverlapPartialSeminorm Q s p p N u ^ p.toReal) ≤ 2 * 3 ^ d * cubeGagliardoESeminorm Q s p u ^ p.toReal

Besov-to-Gagliardo comparison (truncated form): the p-th power of the diagonal overlap Besov partial seminorm is at most 2 * 3^d times the p-th power of the volume-normalized Gagliardo seminorm, uniformly in the truncation depth N.

theorem HCPolySupport.Gagliardo.besovOverlapSeminormValueSet_bddAbove_of_gagliardo {d : ℕ} [NeZero d] (Q : TriadicCube d) {s : ℝ} (hs : 0 ≤ s) {p : ENNReal} (hp : 1 ≤ p) (hpt : p ≠ ⊤) {u : Vec d → ℝ} (humeas : Measurable u) (hu : MeasureTheory.MemLp u p (normalizedCubeMeasure Q)) (hfin : cubeGagliardoESeminorm Q s p u ≠ ⊤) : BddAbove (cubeBesovOverlapSeminormValueSet Q s p p u)

Corollary: when the Gagliardo seminorm is finite, the set of partial overlap Besov seminorm values is bounded above (uniformly in the depth).