VectorMemLp #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Componentwise L^p bookkeeping for Vec d-valued fields #
Vec d = Fin d → ℝ carries the supremum norm, and every vector is the finite
sum of its coordinate multiples of the standard basis.
theorem
Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.memLp_vec_of_components
{d : ℕ}
{α : Type u_1}
{m : MeasurableSpace α}
{μ : MeasureTheory.Measure α}
{q : ENNReal}
{f : α → HCPolySupport.Vec d}
(h : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : α) => f x i) q μ)
:
MeasureTheory.MemLp f q μ
Componentwise criterion for MemLp of a Vec d-valued field.
theorem
Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.cubeLpNorm_infty_le_of_ae_bound
{d : ℕ}
{E : Type u_1}
[NormedAddCommGroup E]
(Q : HCPolySupport.TriadicCube d)
(f : HCPolySupport.Vec d → E)
{M : ℝ}
(hM : 0 ≤ M)
(h : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.normalizedCubeMeasure Q, ‖f x‖ ≤ M)
:
An a.e. bound gives an L^∞ cube-norm bound.
theorem
Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.sqrt_vecNormSq_cubeAverageVec_le_of_ae_bound
{d : ℕ}
(Q : HCPolySupport.TriadicCube d)
{F : HCPolySupport.Vec d → HCPolySupport.Vec d}
{M : ℝ}
(hM : 0 ≤ M)
(hmem :
∀ (i : Fin d), MeasureTheory.MemLp (fun (x : HCPolySupport.Vec d) => F x i) 2 (HCPolySupport.normalizedCubeMeasure Q))
(h : ∀ (i : Fin d), ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.normalizedCubeMeasure Q, |F x i| ≤ M)
:
The mean term of the positive Besov norm is controlled by any componentwise a.e. bound.