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

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

Gagliardo-to-Besov direction of the fractional comparison

This file proves the lower comparison: the p-th power of the fractional Sobolev (Gagliardo) seminorm of u on a triadic cube Q is controlled, up to a dimensional constant, by the supremum of the p-th powers of the finite-depth overlapping Besov seminorms.

The proof decomposes the off-diagonal product cube into triadic distance shells, captures each shell pair inside an overlapping center cube at the matching depth (G3, exists_centersAtDepth_pair_mem), splits the difference through the cube average (triangle inequality plus L^p bookkeeping), and resums the shells into the depth seminorms.

noncomputable def HCPolySupport.Gagliardo.gagliardoBesovLowerConstant (d : ℕ) : ENNReal

Constant for the Gagliardo-to-Besov direction; depends only on d.

Accounting (everything is measured per pr := p.toReal ≥ 1-th power):

• 2 ^ pr * 2 ≤ 4 ^ pr from the triangle split through the cube average (two symmetric one-variable slots);
• 9 ^ (s·pr + d) ≤ 9 ^ pr * (9 ^ d) ^ pr from comparing the shell radius c_Q / 3 ^ (n+1) with the depth side length c_Q / 3 ^ j, n ≤ j + 1 (using s ≤ 1);
• 3 ^ d ≤ (3 ^ d) ^ pr from the overlapping center count card ≤ (3 ^ d) ^ (j + 1) against the depth volume 3 ^ (j d);
• a final flat factor 2 ≤ 2 ^ pr from the shell-to-depth reindexing j = n - 1.

Total: (2 * (4 * 9 * 9 ^ d * 3 ^ d)) ^ pr = (2 ^ 3 * 3 ^ (3 d + 2)) ^ pr.

Equations

• HCPolySupport.Gagliardo.gagliardoBesovLowerConstant d = 2 ^ 3 * 3 ^ (3 * d + 2)

theorem HCPolySupport.Gagliardo.dist_le_cubeScaleFactor_of_mem_cubeSet {d : ℕ} {Q : TriadicCube d} {x y : Vec d} (hx : x ∈ cubeSet Q) (hy : y ∈ cubeSet Q) : dist x y ≤ cubeScaleFactor Q

Diameter bound for the small triadic cube: two points of cubeSet Q are at sup-distance at most the side length cubeScaleFactor Q.

def HCPolySupport.Gagliardo.shellSet {d : ℕ} (Q : TriadicCube d) (n : ℕ) : Set (Vec d × Vec d)

Triadic distance shell adapted to the cube Q: pairs at distance in (c_Q / 3 ^ (n+1), c_Q / 3 ^ n].

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.Gagliardo.measurableSet_shellSet {d : ℕ} (Q : TriadicCube d) (n : ℕ) : MeasurableSet (shellSet Q n)

theorem HCPolySupport.Gagliardo.exists_mem_shellSet {d : ℕ} {Q : TriadicCube d} {z : Vec d × Vec d} (hz1 : z.1 ∈ cubeSet Q) (hz2 : z.2 ∈ cubeSet Q) (hne : z.1 ≠ z.2) : ∃ (n : ℕ), z ∈ shellSet Q n

Every off-diagonal pair of Q lies in some shell.

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

Gagliardo-to-Besov comparison. The p-th power of the fractional Sobolev seminorm on a triadic cube is controlled by the supremum of the p-th powers of the finite-depth overlapping Besov seminorms, with a constant depending only on the dimension.