lintegral_le_of_lmarginal_le — Mathlib

English

For finite δ, the one-dimensional lintegral over π μ equals the evaluation of lmarginal at the universal set: ∫⁻ x f x dMeasure.pi μ = (∫⋯∫⁻_univ f ∂μ) x.

Русский

Для конечного множества δ интеграл по π μ равен значению lmarginal на единстве: ∫⁻ x f x dMeasure.pi μ = (∫⋯∫⁻_univ f ∂μ) x.

LaTeX

$$$\\int⁻ x, f x ∂Measure.pi μ = (\\int⋯∫⁻_univ, f ∂μ) x$$$

Lean4

theorem lintegral_le_of_lmarginal_le [Fintype δ] (s : Finset δ) {f g : (∀ i, X i) → ℝ≥0∞} (hf : Measurable f)
    (hg : Measurable g) (hfg : ∫⋯∫⁻_s, f ∂μ ≤ ∫⋯∫⁻_s, g ∂μ) : ∫⁻ x, f x ∂Measure.pi μ ≤ ∫⁻ x, g x ∂Measure.pi μ :=
  by
  rcases isEmpty_or_nonempty (∀ i, X i) with h | ⟨⟨x⟩⟩
  · simp_rw [lintegral_of_isEmpty, le_rfl]
  simp_rw [lintegral_eq_lmarginal_univ x, lmarginal_le_of_subset (Finset.subset_univ s) hf hg hfg x]

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