VectorPerturbation

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

The W^{1,∞} positive Besov bound for a vector field

Vector-valued counterpart of Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Besov.Perturbation. The scalar file proves

[u]_{B^{s}_{2,2}(Q), N} ≤ C(s) · ℓ(Q) · ‖∇u‖_{L^∞(Q)}

for a B-Lipschitz scalar field. Term A of the D_h split needs exactly the same estimate for the vector field x ↦ hᵀ(x) p, whose positive Besov seminorm is measured by cubeBesovPositiveVectorPartialSeminormTwo. The proof is identical; the one-cube oscillation input is the vector oscillation lemma of Provider.DhBound.Besov.Product.

L² is dominated by L^∞ on a normalized cube, for vector fields

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeLpNorm_two_le_cubeLpNorm_infty_of_memLp_infty_vec {d : ℕ} (Q : HCPolySupport.TriadicCube d) (u : HCPolySupport.Vec d → HCPolySupport.Vec d) (hu : MeasureTheory.MemLp u ⊤ (HCPolySupport.normalizedCubeMeasure Q)) : HCPolySupport.cubeLpNorm Q 2 u ≤ HCPolySupport.cubeLpNorm Q ⊤ u

The one-cube L² oscillation of a Lipschitz vector field

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeLpNorm_two_cubeFluctuationVec_le_cubeScaleFactor_mul_of_lipschitzOn {d : ℕ} (Q : HCPolySupport.TriadicCube d) {ξ : HCPolySupport.Vec d → HCPolySupport.Vec d} {B : ℝ} (hB : 0 ≤ B) (hξLp : MeasureTheory.MemLp ξ ⊤ (HCPolySupport.normalizedCubeMeasure Q)) (hLip : ∀ x ∈ HCPolySupport.cubeSet Q, ∀ y ∈ HCPolySupport.cubeSet Q, ‖ξ x - ξ y‖ ≤ B * ‖x - y‖) : HCPolySupport.cubeLpNorm Q 2 (HCPolySupport.cubeFluctuationVec Q ξ) ≤ HCPolySupport.cubeScaleFactor Q * B

The L² oscillation of a B-Lipschitz vector field on a cube is at most the side length times B.

The depth-j and finite-depth bounds

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovPositiveVectorDepthSeminorm_le_of_lipschitzOn {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (j : ℕ) {ξ : HCPolySupport.Vec d → HCPolySupport.Vec d} {B : ℝ} (hB : 0 ≤ B) (hξLp : MeasureTheory.MemLp ξ ⊤ (HCPolySupport.normalizedCubeMeasure Q)) (hLip : ∀ x ∈ HCPolySupport.cubeSet Q, ∀ y ∈ HCPolySupport.cubeSet Q, ‖ξ x - ξ y‖ ≤ B * ‖x - y‖) : HCPolySupport.cubeBesovPositiveVectorDepthSeminorm Q s ξ j ≤ HCPolySupport.cubeScaleFactor Q * HCPolySupport.cubeL2ScalarDepthSeminorm Q (s - 1) (fun (x : HCPolySupport.Vec d) => B) j

Depth-j positive Besov contribution of a B-Lipschitz vector field.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeBesovPositiveVectorPartialSeminormTwo_le_of_lipschitzOn {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (N : ℕ) {ξ : HCPolySupport.Vec d → HCPolySupport.Vec d} {B : ℝ} (hB : 0 ≤ B) (hs : s < 1) (hξLp : MeasureTheory.MemLp ξ ⊤ (HCPolySupport.normalizedCubeMeasure Q)) (hLip : ∀ x ∈ HCPolySupport.cubeSet Q, ∀ y ∈ HCPolySupport.cubeSet Q, ‖ξ x - ξ y‖ ≤ B * ‖x - y‖) : HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo Q s N ξ ≤ Besov.besovPerturbConst s * (HCPolySupport.cubeScaleFactor Q * B)

The vector perturbation Besov seminorm bound.