eLpNorm_densityProcess_le — Mathlib

English

The eLp-norm of densityProcess is bounded by the a.e. value of ν a, i.e., eLpNorm ≤ ν a.

Русский

eLp-норма densityProcess ограничена значением ν a, то есть ≤ ν a.

LaTeX

$$$\text{eLpNorm}_{1}(\text{densityProcess}(\kappa,\nu,n,a,\cdot,\cdot)) \le (\nu a)(\cdot)$$$

Lean4

theorem eLpNorm_densityProcess_le (hκν : fst κ ≤ ν) (n : ℕ) (a : α) (s : Set β) :
    eLpNorm (fun x ↦ densityProcess κ ν n a x s) 1 (ν a) ≤ ν a univ :=
  by
  refine (eLpNorm_le_of_ae_bound (C := 1) (ae_of_all _ (fun x ↦ ?_))).trans ?_
  · simp only [Real.norm_eq_abs, abs_of_nonneg (densityProcess_nonneg κ ν n a x s), densityProcess_le_one hκν n a x s]
  · simp

Похожие утверждения