BesovBridge #

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

The Gagliardo-versus-Besov bridge for the force leg #

This module supplies the comparison in the direction the chain needs, Besov ≤ C(d) · scale · Gagliardo, which is the direction CoarseGraining's Sobolev/Fractional/BesovLeGagliardo.lean proves.

What is assumed and what is derived #

The hypothesis is the manuscript's own premise g ∈ H^s(□;ℝ^d), in its exact ℝ^d-valued form: g is L² for the normalized cube measure and its difference-quotient kernel is L² for the Gagliardo product measure (Gagliardo.MemWsp Q s 2 g, CoarseGraining's definition instantiated at E:= Vec d). Everything else is derived:

the componentwise package Ch03.Legacy.ForceSobolevRegularity that CoarseGraining's comparison consumes — each coordinate is the image of the vector datum under the (continuous linear) coordinate projection, both for the function and for its kernel, because the Gagliardo kernel commutes with the projection (the kernel exponent s + d/p does not see the target space);
finiteness of the vector Gagliardo seminorm (MemWsp.eSeminorm_lt_top), which is what makes the real-valued comparison non-vacuous.

The constant #

  besovGagliardoConstant d = 3^{d/2} · (2³·3^{3d+2}) · d ,

The scale factor cubeBesovScaleWeight (-s) Q = (3^{Q.scale})^{s} is the manuscript's own normalization difference: the Besov object is note-normalized (3^{sm}[·]_{B^s}), the Gagliardo object is not.

References #

ABK26, ([·]_{W^{s,p}}), (l.coarse.grained.Caccioppoli.RHS).
CoarseGraining, Homogenization/Sobolev/Fractional/BesovLeGagliardo.lean, Homogenization/Book/Ch01/Theorems/FractionalSobolevVsBesov.lean, Homogenization/Book/Ch03/Theorems/SobolevPublic.lean.

1. The coordinate projections of the force datum #

source

theorem Algsuperdiff.Section4.Provider.ExcessDecay.gagliardoKernel_coord {d : ℕ} (s : ℝ) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (i : Fin d) :

(HCPolySupport.Gagliardo.gagliardoKernel s 2 fun (x : HCPolySupport.Vec d) => g x i) = fun (w : HCPolySupport.Vec d × HCPolySupport.Vec d) => HCPolySupport.Gagliardo.gagliardoKernel s 2 g w i

The Gagliardo kernel commutes with the coordinate projection: the kernel of a coordinate is the coordinate of the kernel. (The kernel exponent depends only on d, s, p, never on the target space.)

source

theorem Algsuperdiff.Section4.Provider.ExcessDecay.forceSobolevRegularity_of_memWsp {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (hL2 : MeasureTheory.MemLp g 2 (HCPolySupport.normalizedCubeMeasure Q)) (hW : HCPolySupport.Gagliardo.MemWsp Q s 2 g) :

HCPolySupport.Book.Ch03.Legacy.ForceSobolevRegularity Q s g

The componentwise force package, derived from the vector one. This is the input format of CoarseGraining's Besov-versus-Gagliardo comparison.

source

theorem Algsuperdiff.Section4.Provider.ExcessDecay.forceBesovRegularity_of_memWsp {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) {s : ℝ} (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (hs : 0 < s) (hs1 : s ≤ 1) (hL2 : MeasureTheory.MemLp g 2 (HCPolySupport.normalizedCubeMeasure Q)) (hW : HCPolySupport.Gagliardo.MemWsp Q s 2 g) :

HCPolySupport.Book.Ch03.ForceBesovRegularity Q s g

2. Coordinate seminorms versus the vector seminorm #

source

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cubeGagliardoESeminorm_coord_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (i : Fin d) :

(HCPolySupport.Gagliardo.cubeGagliardoESeminorm Q s 2 fun (x : HCPolySupport.Vec d) => g x i) ≤ HCPolySupport.Gagliardo.cubeGagliardoESeminorm Q s 2 g

Each coordinate's Gagliardo seminorm is dominated by the vector one: the ambient norm of Vec d is the supremum norm, so the coordinate kernel is pointwise dominated by the vector kernel.

source

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sum_cubeGagliardoSeminorm_coord_le {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (hfin : HCPolySupport.Gagliardo.cubeGagliardoESeminorm Q s 2 g ≠ ⊤) :

(∑ i : Fin d, HCPolySupport.Gagliardo.cubeGagliardoSeminorm Q s 2 fun (x : HCPolySupport.Vec d) => g x i) ≤ ↑d * (HCPolySupport.Gagliardo.cubeGagliardoESeminorm Q s 2 g).toReal

The sum of the d coordinate seminorms is at most d times the vector seminorm. Finiteness of the vector seminorm is what makes the toReal comparison valid, and it is supplied by the manuscript's g ∈ H^s.