eLpNorm_density_le — Mathlib

English

For finite kernel, measurable s and measurable A, the integral of density over A equals the density on A × s.

Русский

Для конечного ядра, измеримого s и измеримого A, интеграл density по A равен density на A × s.

LaTeX

$$∫ x in A, density κ ν a x s ∂(ν a) = (κ a).real (A ×ˢ s)$$

Lean4

theorem eLpNorm_density_le (hκν : fst κ ≤ ν) (a : α) (s : Set β) :
    eLpNorm (fun x ↦ density κ ν a x s) 1 (ν a) ≤ ν a univ :=
  by
  refine (eLpNorm_le_of_ae_bound (C := 1) (ae_of_all _ (fun t ↦ ?_))).trans ?_
  · simp only [Real.norm_eq_abs, abs_of_nonneg (density_nonneg hκν a t s), density_le_one hκν a t s]
  · simp

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