FractionalPoincareWindow

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

The mean-zero fractional Poincaré inequality on the §4.3/§4.4 windows

The estimate

On the truncated window U_k = (x + □_k) ∩ □_m of a centre x ∈ □_m, at any scale k ≤ m and any 0 ≤ s,

  ‖f - ⨍_{U_k} f‖_{L²(U_k)}  ≤  2^{d/2} · 3^{ks} · [f]_{H^s(U_k)} .

At the anchor's own window k = n+3 and the development's range 0 ≤ s ≤ 1 this is the numeral 2^{d/2}·27·3^{ns} (…_anchorWindow_le): a dimensional, s-uniform constant. Nothing degenerates at either endpoint of the s range.

The two geometric inputs, both sharp

• the diameter — truncatedWindow_dist_le: U_k sits in a cube of side 3^k, so any two of its points are within 3^k in the ambient supremum metric. Exactly the side, no loss.
• the volume — volume_toReal_truncatedWindow_half_ge: every coordinate slice of U_k keeps at least half the small interval, so U_k contains an axis cube of side 3^k/2 and |U_k| ≥ (3^k/2)^d. This is the sharp lower bound; the inscribed-cube route already proved (volume_truncatedWindow_ge at (3^{k-1})^d, volume_toReal_truncatedWindow_bounds at (3^{k-2})^d) costs (3/2)^d resp. (9/2)^d more, which is why the corner is computed here instead. The corner is the coordinatewise clamp max(xᵢ - 3^k/2, -3^m/2).

Their combination is the only place the constant is produced: the general estimate's factor is D^{s+d/2}/|W|^{1/2}, and

  (3^k)^{s+d/2} / ((3^k/2)^d)^{1/2}  =  2^{d/2}·(3^k)^s .

References

• ABK26, (L²), (H^s).
• Algsuperdiff/Section4/Provider/Regularity/FractionalPoincare.lean.
• Algsuperdiff/Section4/Provider/ExcessDecay/BoundaryLaneWindows.lean (truncatedWindow).

1. The diameter of a truncated window

theorem Algsuperdiff.Section4.Provider.Regularity.truncatedWindow_dist_le {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {p q : HCPolySupport.Vec d} (hp : p ∈ ExcessDecay.truncatedWindow x m k) (hq : q ∈ ExcessDecay.truncatedWindow x m k) : dist p q ≤ 3 ^ k

Two points of U_k = (x+□_k) ∩ □_m are within 3^k in the ambient supremum metric.

2. The sharp volume lower bound

noncomputable def Algsuperdiff.Section4.Provider.Regularity.halfWindowCorner {d : ℕ} (x : HCPolySupport.Vec d) (m k : ℤ) : HCPolySupport.Vec d

The lower corner of the inscribed half-side axis cube: the coordinatewise clamp of xᵢ - 3^k/2 into □_m.

Equations

• Algsuperdiff.Section4.Provider.Regularity.halfWindowCorner x m k i = max (x i - 1 / 2 * 3 ^ k) (-(1 / 2) * 3 ^ m)

theorem Algsuperdiff.Section4.Provider.Regularity.axisCube_halfWindowCorner_subset_truncatedWindow {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k ≤ m) : HCPolySupport.axisCube (halfWindowCorner x m k) (1 / 2 * 3 ^ k) ⊆ ExcessDecay.truncatedWindow x m k

The inscribed half-side cube. Every coordinate slice of U_k keeps at least half the small interval, so the axis cube of side 3^k/2 at the clamped corner sits inside U_k.

theorem Algsuperdiff.Section4.Provider.Regularity.volume_toReal_truncatedWindow_half_ge {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k ≤ m) : (1 / 2 * 3 ^ k) ^ d ≤ (MeasureTheory.volume (ExcessDecay.truncatedWindow x m k)).toReal

The sharp window volume. |U_k| ≥ (3^k/2)^d.

3. The constant arithmetic (abstract reals)

4. The estimate on a truncated window

theorem Algsuperdiff.Section4.Provider.Regularity.eLpNorm_sub_integral_truncatedWindow_le {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {x : HCPolySupport.Vec d} {m k : ℤ} {s : ℝ} {f : HCPolySupport.Vec d → E} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k ≤ m) (hs : 0 ≤ s) (hf : MeasureTheory.Integrable f (MeasureTheory.volume.restrict (ExcessDecay.truncatedWindow x m k))) : MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => f y - ∫ (p : HCPolySupport.Vec d), f p ∂Support.normalizedVolumeMeasureOn (ExcessDecay.truncatedWindow x m k)) 2 (Support.normalizedVolumeMeasureOn (ExcessDecay.truncatedWindow x m k)) ≤ ENNReal.ofReal (2 ^ (↑d / 2) * 3 ^ (↑k * s)) * Support.normalizedGagliardoESeminormOn (ExcessDecay.truncatedWindow x m k) s f

The mean-zero fractional Poincaré inequality on U_k = (x+□_k) ∩ □_m.

  ‖f - ⨍_{U_k} f‖_{L²(U_k)}  ≤  2^{d/2}·3^{ks}·[f]_{H^s(U_k)} ,

with a dimensional, s-uniform constant.

5. The development's Vec d-valued carrier

theorem Algsuperdiff.Section4.Provider.Regularity.eLpNorm_sub_volumeAverageVec_truncatedWindow_le {d : ℕ} {x : HCPolySupport.Vec d} {m k : ℤ} {s : ℝ} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hkm : k ≤ m) (hs : 0 ≤ s) (hf : MeasureTheory.Integrable f (MeasureTheory.volume.restrict (ExcessDecay.truncatedWindow x m k))) : MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => f y - HCPolySupport.volumeAverageVec (ExcessDecay.truncatedWindow x m k) f) 2 (Support.normalizedVolumeMeasureOn (ExcessDecay.truncatedWindow x m k)) ≤ ENNReal.ofReal (2 ^ (↑d / 2) * 3 ^ (↑k * s)) * Support.normalizedGagliardoESeminormOn (ExcessDecay.truncatedWindow x m k) s f

The same estimate with the average written as CoarseGraining's volumeAverageVec — the shape in which the frozen Section-4 surface carries a vector field's window mean.