HolderGagliardoEmbedding

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

C^{0,1/2}(A) ↪ H^s(A) for s < 1/2, on an arbitrary window

Nothing here imports that file, nothing here claims the anchor, and nothing here is a frozen statement.

The target

This module proves the window-free content of it — the Hölder-into- Gagliardo embedding at a general fractional index with the honest constant — and StepFourSeminormComparisons instantiates it at the Step-3 windows.

  |g(x) - g(y)| ≤ K |x-y|^{1/2}  on A ,   A ⊆ B(x,R) for every x ∈ A ,
  0 < s < 1/2 ,  1 ≤ d
      ⟹  [g]_{H^s(A)} ≤ K · ( C_rad(d, d+2s-1) · R^{d} · R^{-(d+2s-1)} )^{1/2} .

Since R^{d}·R^{-(d+2s-1)} = R^{1-2s}, the right side is K·C(d,s)·R^{1/2-s}; at s = 1/4 this is the manuscript's 3^{j/4} once R := 3^j.

The volume normalization is inert

The manuscript's [·]_{H^s(A)} averages in the first slot only. Bounding the inner integral uniformly over the first slot and integrating against a probability measure returns the bound with no volume factor at all: the estimate below is normalization-free, which is why the printed C carries no |U_j|.

References

• ABK26, t.regularity Step 4.
• ABK26, ([·]_{W^{s,p}}), ([·]_{C^{0,α}} and the p = ∞ identification).

1. The Gagliardo exponent of a C^{0,1/2} field

def Algsuperdiff.Section4.Provider.Regularity.holderGagliardoBeta (d : ℕ) (s : ℝ) : ℝ

β(d,s) = d + 2s - 1: the singularity exponent of the Gagliardo integrand of a C^{0,1/2} field at fractional index s.

Equations

• Algsuperdiff.Section4.Provider.Regularity.holderGagliardoBeta d s = ↑d + 2 * s - 1

theorem Algsuperdiff.Section4.Provider.Regularity.holderGagliardoBeta_pos {d : ℕ} {s : ℝ} (hd : 1 ≤ d) (hs0 : 0 < s) : 0 < holderGagliardoBeta d s

theorem Algsuperdiff.Section4.Provider.Regularity.holderGagliardoBeta_lt {d : ℕ} {s : ℝ} (hs : s < 1 / 2) : holderGagliardoBeta d s < ↑d

2. The pointwise majorant on the Gagliardo kernel

3. The embedding

theorem Algsuperdiff.Section4.Provider.Regularity.normalizedGagliardoESeminormOn_le_of_holderHalf {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {A : Set (HCPolySupport.Vec d)} {g : HCPolySupport.Vec d → E} {K R s : ℝ} (hd : 1 ≤ d) (hAmeas : MeasurableSet A) (hA0 : MeasureTheory.volume A ≠ 0) (hAtop : MeasureTheory.volume A ≠ ⊤) (hball : ∀ x ∈ A, A ⊆ Metric.ball x R) (hR : 0 < R) (hs0 : 0 < s) (hs : s < 1 / 2) (hK : 0 ≤ K) (hg : Support.HolderSeminormBoundOn A (1 / 2) K g) : Support.normalizedGagliardoESeminormOn A s g ≤ ENNReal.ofReal (K * √(radialKernelConst d (holderGagliardoBeta d s) * (R ^ d * R ^ (-holderGagliardoBeta d s))))

If g obeys the Hölder-1/2 bound K on A, if A has sup-diameter at most R (in the form A ⊆ B(x,R) for every x ∈ A), and if 0 < s < 1/2, then the volume-normalized Gagliardo seminorm of g on A is at most K · (C_rad(d,β) · R^d · R^{-β})^{1/2} with β = d + 2s - 1, i.e. K · C(d,s) · R^{1/2-s}.