HomCGFinalGagliardo

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

C^{0,α}(□) ⊂ W^{s′,q}(□) at s′ < α, with the exact cube scaling

What this file supplies

The measurement named two "absent analytic inputs" for the order-loss route. MINING CORRECTION: the first one is not absent — the Provider.Regularity.lintegral_enorm_sub_rpow_neg_le_of_subset_ball (HolderGagliardoRadial.lean) is already the β-Riesz ball integral at general β ∈ (0,d) in the ambient sup metric,

  ∫_{B(x,R)} |x-y|^{-β} dy ≤ C_rad(d,β) · R^{d} · R^{-β},

with C_rad(d,β) = 3^{β} 2^{d} (1-3^{β-d})^{-1}. A search of CoarseGraining and Mathlib by name finds only CoarseGraining's β = 1 instance; the general statement was proved in this repository's own Theorem C tree. Nothing is re-derived here.

What IS new here is the transfer of that estimate to CoarseGraining's fractional carriers, whose kernel differs from the Theorem C tree's:

• Gagliardo.gagliardoKernel s 2 uses the ambient dist, at p = 2, and the Hölder exponent is pinned to 1/2 in normalizedGagliardoESeminormOn_le_of_holderHalf;
• cubeEuclideanWspKernel s′ q uses euclideanDist and HilbertVec.ofVec, at a general finite exponent q.

cubeEuclideanWspESeminorm_le_of_holder is the general (α, s′, q) statement at CoarseGraining's carrier, and cubeEuclideanWspFullENorm_le_of_holder assembles it with the L^q half into the full norm CoarseGraining's smooth dual pairs against.

The exponent arithmetic (machine-checked below)

With t = |x-y| (sup metric) and E = euclideanDist x y ≥ t,

  ‖cubeEuclideanWspKernel s′ q φ (x,y)‖ = E^{-(s′+d/q)} · |φ(x)-φ(y)|_eucl
                                        ≤ t^{-(s′+d/q)} · d · K · t^{α}
                                        = (d K) · t^{α - s′ - d/q},

so the q-th power is (dK)^q · t^{-β} with

  β  =  d - (α - s′) q  ∈ (0, d)      ↔      0 < (α - s′) q < d.

The ball estimate then gives R^{d}R^{-β} = R^{(α-s′)q}, and the q-th root restores the single factor R^{α-s′}. On □_m, R = 3^{m}, so the seminorm half carries exactly 3^{m(α-s′)}; the L^q half carries 3^{-s′m} from cubeEuclideanWspScalePowerWeight, which is 3^{m(α-s′)} · 3^{-αm}, i.e. the same factor times the Hölder gauge's own 3^{-αm} weight. Hence the ONE factor 3^{m(α-s′)} in front of wsInftyGauge □_m α Ksup KHol, as the measurement predicted.

The Euclidean/sup comparison is taken at CoarseGraining's own constant d (euclideanNorm_le_dimension_mul_norm), not √d; nothing downstream is sensitive to which.

1. The Gagliardo singularity exponent of a C^{0,α} field at (s′, q)

def Algsuperdiff.Section4.Provider.Homogenization.cgGagliardoBeta (d : ℕ) (alpha s' q : ℝ) : ℝ

β(d, α, s′, q) = d - (α - s′)·q: the singularity exponent of the W^{s′,q} Gagliardo integrand of a C^{0,α} field.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.cgGagliardoBeta d alpha s' q = ↑d - (alpha - s') * q

theorem Algsuperdiff.Section4.Provider.Homogenization.cgGagliardoBeta_lt {d : ℕ} {alpha s' q : ℝ} (h : 0 < (alpha - s') * q) : cgGagliardoBeta d alpha s' q < ↑d

theorem Algsuperdiff.Section4.Provider.Homogenization.cgGagliardoBeta_pos {d : ℕ} {alpha s' q : ℝ} (h : (alpha - s') * q < ↑d) : 0 < cgGagliardoBeta d alpha s' q

2. The finite exponent as a real

theorem Algsuperdiff.Section4.Provider.Homogenization.one_lt_finiteLpExponent_toReal (q : HCPolySupport.FiniteLpExponent) : 1 < q.exponent.toReal

1 < p.exponent.toReal for a FiniteLpExponent.

3. The pointwise majorant on CoarseGraining's fractional kernel

4. The seminorm half

theorem Algsuperdiff.Section4.Provider.Homogenization.cubeEuclideanWspESeminorm_le_of_holder {d : ℕ} {Q : HCPolySupport.TriadicCube d} {s' : ↑HCPolySupport.FractionalOrder} {q : HCPolySupport.FiniteLpExponent} {phi : HCPolySupport.Vec d → HCPolySupport.Vec d} {alpha K : ℝ} (hK : 0 ≤ K) (hlo : 0 < (alpha - ↑s') * q.exponent.toReal) (hhi : (alpha - ↑s') * q.exponent.toReal < ↑d) (hg : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet Q) alpha K phi) : HCPolySupport.cubeEuclideanWspESeminorm Q s' q phi ≤ ENNReal.ofReal (↑d * K * Regularity.radialKernelConst d (cgGagliardoBeta d alpha (↑s') q.exponent.toReal) ^ q.exponent.toReal⁻¹ * HCPolySupport.cubeScaleFactor Q ^ (alpha - ↑s'))

[φ]_{W^{s′,q}(□)} ≤ d · K · C_rad(d,β)^{1/q} · L^{α-s′}.

The C^{0,α} ↪ W^{s′,q} embedding at CoarseGraining's carrier, on a triadic cube, with L = cubeScaleFactor □ the side length. The order loss α - s′ > 0 is what makes the Gagliardo integral converge; the range guard is 0 < (α - s′)·q < d, i.e. β ∈ (0,d).