GradHSplit

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

The ∇h flat leg: the L² norm against the print's window average

What this file supplies

The paper's norm convention (/14546) reads

  ‖f‖_{B^s(□_j)}  =  [f]_{B^s(□_j)}  +  3^{-js} |(f)_{□_j}| ,

so the flat half of the harmonic-approximation display's ∇h leg is the scale-weighted window average, not the normalized L² norm. The two readings are equivalent up to a dimensional constant on the anchor's own windows, and this file proves both directions at the frozen carriers. Write

  W₂ = (z+□_{n+2}) ∩ □_m ,      W₃ = (z+□_{n+3}) ∩ □_m .

• ofReal_norm_volumeAverageVec_windowTwo_le_eLpNorm_windowThree — the average ≤ norm direction: |(f)_{W₂}| ≤ 9^d ‖f‖_{L²(W₃)}, by the vector Jensen inequality on W₂ and the RecutAtoms volume transport W₂ ↪ W₃ (whose ratio bound |W₃| ≤ 81^d |W₂| is the anchor's own geometry binder).
• eLpNorm_windowThree_le_volumeAverageVec_windowTwo_add_gagliardo — the norm ≤ average + seminorm direction:

    ‖f‖_{L²(W₃)}  ≤  |(f)_{W₂}|  +  C(d)·3^{ns}·[f]_{H^s(W₃)} ,
  

  by the proved mean-zero fractional Poincaré inequality on W₃ (FractionalPoincareWindow, s-uniform constant 2^{d/2}·27·3^{ns}) together with the same Jensen/transport pair used to move the W₃ mean to the W₂ mean. The factor 3^{ns} is exactly the convention's own 3^{-js}: composed with the display's flat weight 3^n it produces the Gagliardo leg's weight 3^{(1+s)n} on the nose, which is why the split costs no s-power and proves inside the display's existing legs.

The constant is s-uniform in both directions: nothing degenerates as s ↓ 0 or s ↑ 1.

References

• ABK26, (the B^s norm convention); (the display's ∇h leg).

1. Vector Jensen on a window

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ofReal_norm_volumeAverageVec_le_eLpNorm_two {d : ℕ} {W : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (h0 : MeasureTheory.volume W ≠ 0) (htop : MeasureTheory.volume W ≠ ⊤) (hf : MeasureTheory.Integrable f (MeasureTheory.volume.restrict W)) : ENNReal.ofReal ‖HCPolySupport.volumeAverageVec W f‖ ≤ MeasureTheory.eLpNorm f 2 (Support.normalizedVolumeMeasureOn W)

The vector Jensen inequality on a window. The window average of a vector field is at most its normalized L² norm — the lossy direction of the equivalence.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.volumeAverageVec_sub_const {d : ℕ} {W : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (c : HCPolySupport.Vec d) (h0 : MeasureTheory.volume W ≠ 0) (htop : MeasureTheory.volume W ≠ ⊤) (hf : MeasureTheory.Integrable f (MeasureTheory.volume.restrict W)) : (HCPolySupport.volumeAverageVec W fun (y : HCPolySupport.Vec d) => f y - c) = HCPolySupport.volumeAverageVec W f - c

The window average commutes with subtracting a constant.

2. The two anchor windows

theorem Algsuperdiff.Section4.Provider.ExcessDecay.anchorWindow_two_subset_three {d : ℕ} (n m : ℤ) (z : HCPolySupport.Vec d) : (fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) ⊆ (fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

W₂ ⊆ W₃: the n+2 window sits inside the n+3 one.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.eLpNorm_windowTwo_le_windowThree {d : ℕ} {n m : ℤ} {x z : HCPolySupport.Vec d} (hgeom : (fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 1)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (f : HCPolySupport.Vec d → HCPolySupport.Vec d) : MeasureTheory.eLpNorm f 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ≤ ENNReal.ofReal (9 ^ d) * MeasureTheory.eLpNorm f 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))

The L² transport W₂ ↪ W₃ at the dimensional constant 9^d.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ofReal_norm_volumeAverageVec_windowTwo_le_eLpNorm_windowThree {d : ℕ} {n m : ℤ} {x z : HCPolySupport.Vec d} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hgeom : (fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 1)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hf : MeasureTheory.Integrable f (MeasureTheory.volume.restrict ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) : ENNReal.ofReal ‖HCPolySupport.volumeAverageVec ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) f‖ ≤ ENNReal.ofReal (9 ^ d) * MeasureTheory.eLpNorm f 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))

The average ≤ norm direction. The W₂ window average of f is at most 9^d times its normalized L² norm on W₃ — vector Jensen composed with the window transport.

3. The norm ≤ average + seminorm direction

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.gradHSplitConst (d : ℕ) : ℝ

The dimensional, s-uniform constant of the split.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.gradHSplitConst d = (1 + 9 ^ d) * 2 ^ (↑d / 2) * 27

theorem Algsuperdiff.Section4.Provider.ExcessDecay.gradHSplitConst_pos (d : ℕ) : 0 < gradHSplitConst d

theorem Algsuperdiff.Section4.Provider.ExcessDecay.eLpNorm_windowThree_le_volumeAverageVec_windowTwo_add_gagliardo {d : ℕ} {n m : ℤ} {x z : HCPolySupport.Vec d} {s : ℝ} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hnm : n + 3 ≤ m) (hs : 0 ≤ s) (hs1 : s ≤ 1) (hgeom : (fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 1)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hf : MeasureTheory.Integrable f (MeasureTheory.volume.restrict ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) : MeasureTheory.eLpNorm f 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ≤ ENNReal.ofReal ‖HCPolySupport.volumeAverageVec ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) f‖ + ENNReal.ofReal (gradHSplitConst d * Real.rpow 3 (↑n * s)) * Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s f

The norm ≤ average + seminorm direction.

  ‖f‖_{L²(W₃)}  ≤  |(f)_{W₂}|  +  gradHSplitConst d · 3^{ns} · [f]_{H^s(W₃)} .

The 3^{ns} is the paper's own 3^{-js} weight read at j = n: composed with the display's flat weight 3^n it is exactly the Gagliardo leg's 3^{(1+s)n}, so the split consumes no s-power.