BoundaryGradH

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

The two ∇h conversions of the boundary Caccioppoli, and the σ-leg fork

The boundary Caccioppoli's data leg is CoarseGraining's dirichletEnergyWith, whose second summand carries the full Besov norm of the transported boundary gradient,

  ‖∇h‖_{B^r} = √(|(∇h)_{□_{n+2}}|²) + [∇h]_{B^r} ,   h = h(· + c) ,

c = wellPlacedCentre x m (n+2).

• the seminorm half — the same lemma read at g := −∇h, together with the gagliardoKernel negation congruence it needs to see that [−∇h] = [∇h].

References

• ABK26, l.harmonic.approximation.good.scales, Step 2; e.cg.RHS, the Dirichlet energy display.

1. The gagliardoKernel negation congruence, on the datum

theorem Algsuperdiff.Section4.Provider.ExcessDecay.memLp_gagliardoKernel_neg {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (A : Set (HCPolySupport.Vec d)) (s : ℝ) {F : HCPolySupport.Vec d → E} (h : MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 F) 2 (Support.normalizedGagliardoMeasureOn A)) : MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 fun (y : HCPolySupport.Vec d) => -F y) 2 (Support.normalizedGagliardoMeasureOn A)

The Gagliardo L² datum does not see a sign.

2. The seminorm half of the ∇h leg

theorem Algsuperdiff.Section4.Provider.ExcessDecay.besovVectorSeminormTwo_datumGrad_coveringCube_atWindow {d : ℕ} [NeZero d] {n m : ℤ} {x z : HCPolySupport.Vec d} {s : ℝ} {H : 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 H 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 H) 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 H) 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) => H (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 H).toReal)

The transported datum-gradient Besov budget under covering-cube containment.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.besovVectorSeminormTwo_datumGrad_coveringCube_le_anchorWindow {d : ℕ} [NeZero d] {n m : ℤ} {x z : HCPolySupport.Vec d} {s : ℝ} {H : 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 H 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 H) 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 H) 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) => H (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 H).toReal)

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

3. The average half of the ∇h leg

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sqrt_vecNormSq_le_sqrt_dim_mul_norm {d : ℕ} (v : HCPolySupport.Vec d) : √(HCPolySupport.vecNormSq v) ≤ √↑d * ‖v‖

The Euclidean length of a vector is at most √d times its ambient (sup) norm.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sqrt_vecNormSq_cubeAverageVec_coveringCube_atWindow {d : ℕ} {n m : ℤ} {x z : HCPolySupport.Vec d} {H : 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)) (hL2W : MeasureTheory.MemLp H 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) : √(HCPolySupport.vecNormSq (HCPolySupport.cubeAverageVec (HCPolySupport.originCube d (n + 2)) fun (y : HCPolySupport.Vec d) => H (y + wellPlacedCentre x m (n + 2)))) ≤ √↑d * 3 ^ d * (MeasureTheory.eLpNorm H 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal

The transported gradient-average budget under covering-cube containment.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sqrt_vecNormSq_cubeAverageVec_coveringCube_le_anchorWindow {d : ℕ} {n m : ℤ} {x z : HCPolySupport.Vec d} {H : 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)) (hL2W : MeasureTheory.MemLp H 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) : √(HCPolySupport.vecNormSq (HCPolySupport.cubeAverageVec (HCPolySupport.originCube d (n + 2)) fun (y : HCPolySupport.Vec d) => H (y + wellPlacedCentre x m (n + 2)))) ≤ √↑d * 3 ^ d * (MeasureTheory.eLpNorm H 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 3)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))).toReal

The transported boundary gradient's cube average, priced on the anchor window.