FractionalPoincare

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

The mean-zero fractional Poincaré inequality, at the Section-4 carriers

This module is a carrier-level utility for the Section 4 estimates.

The estimate

For a set W of positive finite volume, sup-diameter at most D, and any f integrable on W,

  ‖f - ⨍_W f‖_{L²(W)}  ≤  D^{s + d/2} · |W|^{-1/2} · [f]_{H^s(W)} ,

with [·]_{H^s(W)} the manuscript's volume-normalized Gagliardo seminorm Support.normalizedGagliardoESeminormOn and ‖·‖_{L²(W)} its ℝ≥0∞ reading eLpNorm · 2 (Support.normalizedVolumeMeasureOn W) — the exact left-hand-side carrier of the frozen Section-4 harmonic surface.

The constant is s-uniform: no factor degenerates as s ↑ 1 or s ↓ 0, and on the development's windows it collapses to a dimensional numeral (see FractionalPoincareWindow). No Sobolev embedding, no compactness and no inner product enter: the ambient Vec d = Fin d → ℝ carries the supremum norm and the proof uses only Jensen and the volume ratio.

The three moves

1. Jensen (eLpNorm_sub_integral_le_eLpNorm_prod). Against the probability measure μ = ⨍_W, f x - ⨍_W f = ∫_y (f x - f y) dμ(y), so ‖f x - ⨍_W f‖ₑ ≤ ‖f x - f ·‖_{L¹(μ)} ≤ ‖f x - f ·‖_{L²(μ)} (eLpNorm_le_eLpNorm_of_exponent_le, valid because μ is a probability measure). Squaring and integrating in x, then Tonelli, gives ‖f - ⨍_W f‖_{L²(μ)} ≤ ‖f ·₁ - f ·₂‖_{L²(μ⊗μ)}.
2. The kernel (norm_sub_le_rpow_mul_norm_gagliardoKernel). Pointwise on W × W, ‖f x - f y‖ = |x-y|^{s+d/2}·‖K(x,y)‖ ≤ D^{s+d/2}·‖K(x,y)‖ with K CoarseGraining's Gagliardo.gagliardoKernel s 2 f; the diagonal is the trivial case 0 ≤ 0.
3. The normalization (normalizedGagliardoMeasureOn_eq_smul_prod). The manuscript's Gagliardo measure is normalized in x and plain volume in y, i.e. ν = |W| · (μ ⊗ μ); the single factor |W|^{-1/2} is exactly that asymmetry, and it is what cancels the D^d half of D^{s+d/2}.

References

• ABK26, e.excess.def (the L² carrier); the normalized fractional seminorm.
• Algsuperdiff/Section4/Support/Dirichlet.lean (normalizedVolumeMeasureOn, normalizedGagliardoESeminormOn).

1. The p = 2 eLpNorm as a lintegral

2. Jensen against a probability measure

theorem Algsuperdiff.Section4.Provider.Regularity.enorm_sub_integral_rpow_two_le {α : Type u_1} [MeasurableSpace α] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] {f : α → E} (hf : MeasureTheory.Integrable f μ) (x : α) : ‖f x - ∫ (y : α), f y ∂μ‖ₑ ^ 2 ≤ ∫⁻ (y : α), ‖f x - f y‖ₑ ^ 2 ∂μ

The pointwise Jensen step. Against a probability measure the deviation of f x from the mean is controlled in L² by the two-point differences.

theorem Algsuperdiff.Section4.Provider.Regularity.eLpNorm_sub_integral_le_eLpNorm_prod {α : Type u_1} [MeasurableSpace α] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] {f : α → E} (hf : MeasureTheory.Integrable f μ) : MeasureTheory.eLpNorm (fun (x : α) => f x - ∫ (y : α), f y ∂μ) 2 μ ≤ MeasureTheory.eLpNorm (fun (z : α × α) => f z.1 - f z.2) 2 (μ.prod μ)

Jensen at the L² level. The mean-subtracted L²(μ) norm is at most the L²(μ ⊗ μ) norm of the two-point difference field.

3. The pointwise kernel bound

theorem Algsuperdiff.Section4.Provider.Regularity.norm_sub_le_rpow_mul_norm_gagliardoKernel {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {s D : ℝ} (hs : 0 ≤ s) (f : HCPolySupport.Vec d → E) {x y : HCPolySupport.Vec d} (hxy : dist x y ≤ D) : ‖f x - f y‖ ≤ D ^ (s + ↑d / 2) * ‖HCPolySupport.Gagliardo.gagliardoKernel s 2 f (x, y)‖

The kernel bound. On a set of sup-diameter at most D the raw increment is D^{s+d/2} times CoarseGraining's difference-quotient kernel.

4. The window measures

theorem Algsuperdiff.Section4.Provider.Regularity.isProbabilityMeasure_normalizedVolumeMeasureOn {d : ℕ} {W : Set (HCPolySupport.Vec d)} (hWpos : 0 < MeasureTheory.volume W) (hWtop : MeasureTheory.volume W ≠ ⊤) : MeasureTheory.IsProbabilityMeasure (Support.normalizedVolumeMeasureOn W)

The volume-normalized measure of a window of positive finite volume is a probability measure.

theorem Algsuperdiff.Section4.Provider.Regularity.restrict_eq_smul_normalizedVolumeMeasureOn {d : ℕ} {W : Set (HCPolySupport.Vec d)} (hWpos : 0 < MeasureTheory.volume W) (hWtop : MeasureTheory.volume W ≠ ⊤) : MeasureTheory.volume.restrict W = MeasureTheory.volume W • Support.normalizedVolumeMeasureOn W

The restricted volume is |W| times the normalized volume.

theorem Algsuperdiff.Section4.Provider.Regularity.normalizedGagliardoMeasureOn_eq_smul_prod {d : ℕ} {W : Set (HCPolySupport.Vec d)} (hWpos : 0 < MeasureTheory.volume W) (hWtop : MeasureTheory.volume W ≠ ⊤) : Support.normalizedGagliardoMeasureOn W = MeasureTheory.volume W • (Support.normalizedVolumeMeasureOn W).prod (Support.normalizedVolumeMeasureOn W)

The asymmetry of the manuscript's Gagliardo normalization. It is |W| times the symmetric probability square.

5. The estimate

theorem Algsuperdiff.Section4.Provider.Regularity.eLpNorm_sub_integral_le_normalizedGagliardoESeminormOn {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {W : Set (HCPolySupport.Vec d)} {s D : ℝ} {f : HCPolySupport.Vec d → E} (hW : MeasurableSet W) (hWpos : 0 < MeasureTheory.volume W) (hWtop : MeasureTheory.volume W ≠ ⊤) (hs : 0 ≤ s) (hdiam : ∀ x ∈ W, ∀ y ∈ W, dist x y ≤ D) (hf : MeasureTheory.Integrable f (MeasureTheory.volume.restrict W)) : MeasureTheory.eLpNorm (fun (x : HCPolySupport.Vec d) => f x - ∫ (y : HCPolySupport.Vec d), f y ∂Support.normalizedVolumeMeasureOn W) 2 (Support.normalizedVolumeMeasureOn W) ≤ ENNReal.ofReal (D ^ (s + ↑d / 2) / √(MeasureTheory.volume W).toReal) * Support.normalizedGagliardoESeminormOn W s f

The mean-zero fractional Poincaré inequality.

For W of positive finite volume and sup-diameter at most D, and f integrable on W,

  ‖f - ⨍_W f‖_{L²(W)}  ≤  ( D^{s+d/2} / |W|^{1/2} ) · [f]_{H^s(W)} .

The constant is s-uniform: it is a single rpow of the diameter against the volume, with no (1-s)^{-1} or s^{-1} anywhere. Both sides are the frozen Section-4 surface's own carriers.

6. The development's average carriers

theorem Algsuperdiff.Section4.Provider.Regularity.integral_normalizedVolumeMeasureOn_eq_volumeAverageVec {d : ℕ} {W : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : MeasureTheory.Integrable f (MeasureTheory.volume.restrict W)) : ∫ (y : HCPolySupport.Vec d), f y ∂Support.normalizedVolumeMeasureOn W = HCPolySupport.volumeAverageVec W f

The abstract average against normalizedVolumeMeasureOn W is CoarseGraining's volumeAverageVec on vector fields integrable on W.