nndist_integral_add_measure_le_lintegral

English

The distance between the two Bochner integrals under μ and μ+ν is bounded by the lintegral of the norm of f against ν: nndist(∫ f dμ, ∫ f d(μ+ν)) ≤ ∫⁻ ‖f‖ dν.

Русский

Расстояние между двумя интегралами Боchnerа по меркам μ и μ+ν ограничено лин-интегралом нормы f по ν: nndist(∫ f dμ, ∫ f d(μ+ν)) ≤ ∫⁻ ‖f‖ dν.

LaTeX

$$$$\left( nndist \left( \int x, f x \partial\mu \,, \int x, f x \partial(\mu+\nu) \right) : \mathbb{R}_{\ge 0}^{\infty} \right) \le \int⁻ x, \|f x\|_e \partial\nu.$$$$

Lean4

theorem nndist_integral_add_measure_le_lintegral {f : α → G} (h₁ : Integrable f μ) (h₂ : Integrable f ν) :
    (nndist (∫ x, f x ∂μ) (∫ x, f x ∂(μ + ν)) : ℝ≥0∞) ≤ ∫⁻ x, ‖f x‖ₑ ∂ν :=
  by
  rw [integral_add_measure h₁ h₂, nndist_comm, nndist_eq_nnnorm, add_sub_cancel_left]
  exact enorm_integral_le_lintegral_enorm _

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