integral_truncation_le_integral_of_nonneg

English

For finite measure μ, if f is AEStronglyMeasurable, truncation f A is in L^p for all p.

Русский

При конечной мере μ, если f AEStronglyMeasurable, то truncation(f,A) ∈ L^p для всех p.

LaTeX

$$$[IsFiniteMeasure\, μ] \to\; AEStronglyMeasurable\, f\, μ \Rightarrow\; ∀ A,p,\; truncation(f,A) ∈ L^p(μ)$$$

Lean4

theorem integral_truncation_le_integral_of_nonneg (hf : Integrable f μ) (h'f : 0 ≤ f) {A : ℝ} :
    ∫ x, truncation f A x ∂μ ≤ ∫ x, f x ∂μ :=
  by
  apply integral_mono_of_nonneg (Eventually.of_forall fun x => ?_) hf (Eventually.of_forall fun x => ?_)
  · exact truncation_nonneg _ (h'f x)
  ·
    calc
      truncation f A x ≤ |truncation f A x| := le_abs_self _
      _ ≤ |f x| := (abs_truncation_le_abs_self _ _ _)
      _ = f x := abs_of_nonneg (h'f x)

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