RootClauseBCloseDatum

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

1. The L² half

theorem Algsuperdiff.Section4.Provider.Regularity.norm_le_of_holderHalf_originCube {d : ℕ} {m : ℤ} {K : ℝ} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hK : 0 ≤ K) (hf : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) K f) {x : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) : ‖f x‖ ≤ ‖f 0‖ + K * (3 ^ m) ^ (1 / 2)

The pointwise bound from the Hölder seminorm, against the cube's own centre.

theorem Algsuperdiff.Section4.Provider.Regularity.memLp_two_normalizedVolume_of_holderHalf {d : ℕ} {m : ℤ} {K : ℝ} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hK : 0 ≤ K) (hf : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) K f) : MeasureTheory.MemLp f 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))

The L² data binder from the root's own Hölder binder.

A C^{0,1/2}(□_m) field is bounded and continuous there, hence L^∞ for the normalized cube measure and a fortiori L².

2. The kernel's measurability

theorem Algsuperdiff.Section4.Provider.Regularity.aestronglyMeasurable_gagliardoKernel_of_holderHalf {d : ℕ} {A : Set (HCPolySupport.Vec d)} {K s : ℝ} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hA : MeasurableSet A) (hK : 0 ≤ K) (hf : Support.HolderSeminormBoundOn A (1 / 2) K f) : MeasureTheory.AEStronglyMeasurable (HCPolySupport.Gagliardo.gagliardoKernel s 2 f) (Support.normalizedGagliardoMeasureOn A)

The Gagliardo kernel is a.e. strongly measurable on the product measure.

The scalar factor |z₁-z₂|^{-(d/2+s)} is GLOBALLY measurable; only the vector factor f(z₁) - f(z₂) needs the window, and the Hölder bound makes it continuous there.

3. The Gagliardo MemLp

theorem Algsuperdiff.Section4.Provider.Regularity.memLp_two_gagliardoKernel_of_holderHalf {d : ℕ} {m : ℤ} {K s : ℝ} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hd : 1 ≤ d) (hs0 : 0 < s) (hs : s < 1 / 2) (hK : 0 ≤ K) (hf : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) K f) : MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 f) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))

The Gagliardo data binder from the root's own Hölder binder.

§2 supplies the measurability and the proved embedding atom normalizedGagliardoESeminormOn_cube_le the finiteness — its bound K·C(d,s)·3^{m(1/2-s)} is a real number, so the L² norm of the kernel is below ⊤.

4. The pair at the §4.4 pin s = 1/4

theorem Algsuperdiff.Section4.Provider.Regularity.memLp_pair_of_holderHalf {d : ℕ} {m : ℤ} {K : ℝ} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hd : 1 ≤ d) (hK : 0 ≤ K) (hf : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) K f) : MeasureTheory.MemLp f 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) ∧ MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel stepOneS 2 f) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))

Both data binders of the §4.4 chain, at the printed exponent.

stepOneS = 1/4 lies strictly inside (0, 1/2), so the embedding applies and the root's C^{0,1/2} binder — printed for 𝐠 at K_g and for ∇h at K_h — discharges BOTH MemLp hypotheses at once.