Elementary facts about one-dimensional marginal laws

These lemmas package the three facts needed when replacing independent random variables by their product of marginal distributions: integrability, the first moment, and nonnegative support.

theorem Feige.integrable_id_map {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hXmeas : Measurable X) (hXint : MeasureTheory.Integrable X μ) : MeasureTheory.Integrable (fun (x : ℝ) => x) (MeasureTheory.Measure.map X μ)

theorem Feige.integral_id_map {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hXmeas : Measurable X) : ∫ (x : ℝ), x ∂MeasureTheory.Measure.map X μ = ∫ (ω : Ω), X ω ∂μ

theorem Feige.map_apply_Iio_zero_of_nonnegative {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} (hXmeas : Measurable X) (hXnonneg : ∀ (ω : Ω), 0 ≤ X ω) : (MeasureTheory.Measure.map X μ) (Set.Iio 0) = 0