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

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

Constants for the fractional Sobolev versus Besov comparison

Every numeric fact used by the W^{s,p} versus B^s_{p,p} equivalence is proved here, once, with explicit hypotheses. The proof files consume these lemmas with exact; no positivity/nlinarith grinding happens outside this file.

Uniformity ledger (each bound is uniform in s ∈ (0,1) and p ∈ [1,∞), so the final equivalence constant depends on the dimension only):

• geometric tails have ratio at most 3⁻¹, hence sum at most 3/2 ≤ 2;
• the kernel-insertion prefactor 3^{d/p+s} is at most 3^{d+1};
• the triangle-splitting factor (2^{p-1})^{1/p} is at most 2.

theorem HCPolySupport.Gagliardo.tsum_pow_le_two_of_le_third {c : ENNReal} (hc : c ≤ 3⁻¹) : ∑' (n : ℕ), c ^ n ≤ 2

Geometric series with ratio at most 3⁻¹ sums to at most 2 in ℝ≥0∞.

theorem HCPolySupport.Gagliardo.sum_range_pow_le_two_of_le_third {c : ENNReal} (hc : c ≤ 3⁻¹) (N : ℕ) : ∑ n ∈ Finset.range N, c ^ n ≤ 2

Finite geometric sums with ratio at most 3⁻¹ are at most 2 in ℝ≥0∞.

theorem HCPolySupport.Gagliardo.rpow_three_kernel_exponent_le {d : ℕ} {s pr : ℝ} (hs : s < 1) (hp : 1 ≤ pr) : 3 ^ (↑d / pr + s) ≤ 3 ^ (↑d + 1)

The kernel-insertion prefactor collapses to a dimensional constant: 3^{d/p + s} ≤ 3^{d+1} for s < 1 ≤ p, in ℝ≥0∞.

theorem HCPolySupport.Gagliardo.rpow_two_sub_one_div_le_two {pr : ℝ} (hp : 1 ≤ pr) : 2 ^ ((pr - 1) * (1 / pr)) ≤ 2

Triangle-splitting cost after the p-th root: (2^{p-1})^{1/p} ≤ 2 for p ≥ 1, phrased in ℝ≥0∞.

theorem HCPolySupport.Gagliardo.rpow_three_le_rpow_three {a b : ℝ} (h : a ≤ b) : 3 ^ a ≤ 3 ^ b

Monotone collapse for powers of three with bounded exponent, ℝ≥0∞ form.

theorem HCPolySupport.Gagliardo.rpow_three_ne_zero (x : ℝ) : 3 ^ x ≠ 0

3^x is positive (nonzero) in ℝ≥0∞.

theorem HCPolySupport.Gagliardo.rpow_three_ne_top (x : ℝ) : 3 ^ x ≠ ⊤

3^x is finite in ℝ≥0∞.