lintegral_map_le — Mathlib

English

For any f and g, the lintegral of f with respect to map g μ is at most the lintegral of f(g) with respect to μ; i.e. lintegral(map g μ) f ≤ lintegral μ (f ∘ g).

Русский

Для любых f и g линеграл по отображению satisfies: линеграл по map g μ f ≤ линеграл по μ (f ∘ g).

LaTeX

$$$$ \int f\, d(map\ g\ μ) \leq \int f\circ g\, dμ, $$$$

Lean4

theorem lintegral_map_le (f : β → ℝ≥0∞) (g : α → β) : ∫⁻ a, f a ∂Measure.map g μ ≤ ∫⁻ a, f (g a) ∂μ :=
  by
  by_cases hg : AEMeasurable g μ
  · rw [← iSup_lintegral_measurable_le_eq_lintegral]
    refine iSup₂_le fun i hi => iSup_le fun h'i => ?_
    rw [lintegral_map' hi.aemeasurable hg]
    exact lintegral_mono fun _ ↦ h'i _
  · simp [map_of_not_aemeasurable hg]

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