lintegral_strict_mono_of_ae_le_of_frequently_ae_lt

English

If g is AEMeasurable, the integral of f is finite, and f ≤ᵐ g with f ≠ g on a set of positive measure, then ∫ f < ∫ g.

Русский

Если g измерима почти повсюду, интеграл f конечен, и f ≤ᵐ g, причём множество {x : f(x) ≠ g(x)} имеет положительную меру, то ∫ f < ∫ g.

LaTeX

$$$AEMeasurable\\ g\\ μ\\;\\wedge\\; ∫ f dμ \\neq ∞\\;\\wedge\\; f \\le_g^μ f \\wedge (μ\\{x : f(x) \\neq g(x)\\}>0) \\Rightarrow ∫ f dμ < ∫ g dμ$$$

Lean4

theorem lintegral_strict_mono_of_ae_le_of_frequently_ae_lt {f g : α → ℝ≥0∞} (hg : AEMeasurable g μ)
    (hfi : ∫⁻ x, f x ∂μ ≠ ∞) (h_le : f ≤ᵐ[μ] g) (h : ∃ᵐ x ∂μ, f x ≠ g x) : ∫⁻ x, f x ∂μ < ∫⁻ x, g x ∂μ :=
  by
  contrapose! h
  simp only [not_frequently, Ne, Classical.not_not]
  exact ae_eq_of_ae_le_of_lintegral_le h_le hfi hg h

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