BoundaryTransports

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

The boundary lane's data transports onto the anchor window

The boundary Caccioppoli's data legs — the force [g] and the boundary gradient [∇h] — are Gagliardo seminorms, not L² norms, and this module supplies the same move for them:

  [f]_{H^s(c+□_{n+2})} ≤ 3^d · [f]_{H^s(W')} ,

together with the composition that the boundary Caccioppoli's right-hand side actually reads: CoarseGraining's cube Besov seminorm of the transported force, in the covering cube's own frame, priced by the anchor's own window seminorm.

References

• ABK26, l.harmonic.approximation.good.scales, Step 2.

1. The Gagliardo window move

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedGagliardoESeminormOn_coveringCube_atWindow {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n m : ℤ} {x z : HCPolySupport.Vec d} (hcov : (fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (s : ℝ) (f : HCPolySupport.Vec d → E) : Support.normalizedGagliardoESeminormOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) s f ≤ ENNReal.ofReal (gagliardoWindowConst d) * Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s f

Gagliardo transport assuming containment of the covering cube in the window.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedGagliardoESeminormOn_coveringCube_le_anchorWindow {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n m : ℤ} {x z : HCPolySupport.Vec d} (hnm : n + 2 ≤ m) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (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)) (s : ℝ) (f : HCPolySupport.Vec d → E) : Support.normalizedGagliardoESeminormOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) s f ≤ ENNReal.ofReal (gagliardoWindowConst d) * 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 Gagliardo seminorm transport onto the anchor's window.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedGagliardoESeminormOn_coveringCube_toReal_le_atWindow {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n m : ℤ} {x z : HCPolySupport.Vec d} {s : ℝ} (hcov : (fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (f : HCPolySupport.Vec d → E) (hfin : MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 f) 2 (Support.normalizedGagliardoMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) : (Support.normalizedGagliardoESeminormOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) s f).toReal ≤ gagliardoWindowConst d * (Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s f).toReal

Real-valued Gagliardo transport under the same containment and finiteness hypotheses.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedGagliardoESeminormOn_coveringCube_toReal_le {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n m : ℤ} {x z : HCPolySupport.Vec d} {s : ℝ} (hnm : n + 2 ≤ m) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (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 → E) (hfin : MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 f) 2 (Support.normalizedGagliardoMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) : (Support.normalizedGagliardoESeminormOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))) s f).toReal ≤ gagliardoWindowConst d * (Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s f).toReal

The Gagliardo window move, in the real-valued form the boundary assembly consumes. The finiteness hypothesis is the anchor's own clause (iv), read on the anchor's window.

2. The force leg of the boundary Caccioppoli, onto the anchor's window

theorem Algsuperdiff.Section4.Provider.ExcessDecay.besovVectorSeminormTwo_coveringCube_atWindow {d : ℕ} [NeZero d] {n m : ℤ} {x z : HCPolySupport.Vec d} {s : ℝ} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hcov : (fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hs : 0 < s) (hs1 : s ≤ 1) (hL2 : MeasureTheory.MemLp g 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))))) (hWcov : MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 g) 2 (Support.normalizedGagliardoMeasureOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))))) (hW : MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 g) 2 (Support.normalizedGagliardoMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) : (HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo (HCPolySupport.originCube d (n + 2)) s fun (y : HCPolySupport.Vec d) => -g (y + wellPlacedCentre x m (n + 2))) ≤ besovGagliardoConstant d * Real.rpow 3 (s * ↑(n + 2)) * (gagliardoWindowConst d * (Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s g).toReal)

The transported force Besov budget under covering-cube containment.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.besovVectorSeminormTwo_coveringCube_le_anchorWindow {d : ℕ} [NeZero d] {n m : ℤ} {x z : HCPolySupport.Vec d} {s : ℝ} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hnm : n + 2 ≤ m) (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (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)) (hs : 0 < s) (hs1 : s ≤ 1) (hL2 : MeasureTheory.MemLp g 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))))) (hWcov : MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 g) 2 (Support.normalizedGagliardoMeasureOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))))) (hW : MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 g) 2 (Support.normalizedGagliardoMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) : (HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo (HCPolySupport.originCube d (n + 2)) s fun (y : HCPolySupport.Vec d) => -g (y + wellPlacedCentre x m (n + 2))) ≤ besovGagliardoConstant d * Real.rpow 3 (s * ↑(n + 2)) * (gagliardoWindowConst d * (Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s g).toReal)

The transported force's cube Besov seminorm, priced on the anchor's window.

BoundaryOuterAssembly reads its force leg as CoarseGraining's cube Besov seminorm of y ↦ −g(y + c) on the covering cube □_{n+2} in that cube's own frame. This is the composition of BesovBridge's Besov--Gagliardo comparison at the covering cube with the window move of section 1: the whole leg is priced by the anchor's own [g]_{H^s(W')} at the scale weight 3^{s(n+2)} and the coefficient-free constant besovGagliardoConstant d · 3^d.

3. The covering cube's own clause-(iv) data

theorem Algsuperdiff.Section4.Provider.ExcessDecay.memLp_two_coveringCube_of_clause_iv {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] {n m : ℤ} {x : HCPolySupport.Vec d} {f : HCPolySupport.Vec d → E} (hnm : n + 2 ≤ m) (hf : MeasureTheory.MemLp f 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) : MeasureTheory.MemLp f 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))))

The anchor's L² datum, restricted to the boundary covering cube.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.memLp_two_gagliardo_coveringCube_of_clause_iv {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {n m : ℤ} {x : HCPolySupport.Vec d} {s : ℝ} {f : HCPolySupport.Vec d → E} (hnm : n + 2 ≤ m) (hf : MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 f) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) : MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 f) 2 (Support.normalizedGagliardoMeasureOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n + 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2))))

The anchor's Gagliardo datum, restricted to the boundary covering cube.