# Integration in Probability Theory #

Integration results for independent random variables. Specifically, for two independent random variables X and Y over the extended non-negative reals, `E[X * Y] = E[X] * E[Y]`, and similar results.

## Implementation notes #

Many lemmas in this file take two arguments of the same typeclass. It is worth remembering that lean will always pick the later typeclass in this situation, and does not care whether the arguments are `[]`, `{}`, or `()`. All of these use the `MeasurableSpace` `M2` to define `μ`:

    example {M1 : MeasurableSpace Ω} [M2 : MeasurableSpace Ω] {μ : Measure Ω} : sorry := sorry
    example [M1 : MeasurableSpace Ω] {M2 : MeasurableSpace Ω} {μ : Measure Ω} : sorry := sorry

source
theorem ProbabilityTheory.lintegral_mul_indicator_eq_lintegral_mul_lintegral_indicator {Ω : Type u_1} {f : Ω → ENNReal} {Mf mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (hMf : Mf ≤ mΩ) (c : ENNReal) {T : Set Ω} (h_meas_T : MeasurableSet T) (h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ) (h_meas_f : Measurable f) :
∫⁻ (ω : Ω), f ω * T.indicator (fun (x : Ω) => c) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) => c) ω ∂μ

If a random variable `f` in `ℝ≥0∞` is independent of an event `T`, then if you restrict the random variable to `T`, then `E[f * indicator T c 0]=E[f] * E[indicator T c 0]`. It is useful for `lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurableSpace`.

source
theorem ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_independent_measurableSpace {Ω : Type u_1} {f g : Ω → ENNReal} {Mf Mg mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (hMf : Mf ≤ mΩ) (hMg : Mg ≤ mΩ) (h_ind : Indep Mf Mg μ) (h_meas_f : Measurable f) (h_meas_g : Measurable g) :
∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ

If `f` and `g` are independent random variables with values in `ℝ≥0∞`, then `E[f * g] = E[f] * E[g]`. However, instead of directly using the independence of the random variables, it uses the independence of measurable spaces for the domains of `f` and `g`. This is similar to the sigma-algebra approach to independence. See `lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun` for a more common variant of the product of independent variables.

source
theorem ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f g : Ω → ENNReal} (h_meas_f : Measurable f) (h_meas_g : Measurable g) (h_indep_fun : IndepFun f g μ) :
∫⁻ (ω : Ω), (f * g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ

If `f` and `g` are independent random variables with values in `ℝ≥0∞`, then `E[f * g] = E[f] * E[g]`.

source
theorem ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f g : Ω → ENNReal} (h_meas_f : AEMeasurable f μ) (h_meas_g : AEMeasurable g μ) (h_indep_fun : IndepFun f g μ) :
∫⁻ (ω : Ω), (f * g) ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ

If `f` and `g` with values in `ℝ≥0∞` are independent and almost everywhere measurable, then `E[f * g] = E[f] * E[g]` (slightly generalizing `lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun`).

source
theorem ProbabilityTheory.lintegral_mul_eq_lintegral_mul_lintegral_of_indepFun'' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f g : Ω → ENNReal} (h_meas_f : AEMeasurable f μ) (h_meas_g : AEMeasurable g μ) (h_indep_fun : IndepFun f g μ) :
∫⁻ (ω : Ω), f ω * g ω ∂μ = (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), g ω ∂μ
source
theorem ProbabilityTheory.lintegral_prod_eq_prod_lintegral_of_indepFun {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_3} (s : Finset ι) (X : ι → Ω → ENNReal) (hX : iIndepFun X μ) (x_mea : ∀ (i : ι), Measurable (X i)) :
∫⁻ (ω : Ω), ∏ i ∈ s, X i ω ∂μ = ∏ i ∈ s, ∫⁻ (ω : Ω), X i ω ∂μ
source
theorem ProbabilityTheory.IndepFun.integrable_mul {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_3} [MeasurableSpace β] {X Y : Ω → β} [NormedDivisionRing β] [BorelSpace β] (hXY : IndepFun X Y μ) (hX : MeasureTheory.Integrable X μ) (hY : MeasureTheory.Integrable Y μ) :
MeasureTheory.Integrable (X * Y) μ

The product of two independent, integrable, real-valued random variables is integrable.

source
theorem ProbabilityTheory.IndepFun.integrable_left_of_integrable_mul {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_3} [MeasurableSpace β] {X Y : Ω → β} [NormedDivisionRing β] [OpensMeasurableSpace β] (hXY : IndepFun X Y μ) (h'XY : MeasureTheory.Integrable (X * Y) μ) (hX : MeasureTheory.AEStronglyMeasurable X μ) (hY : MeasureTheory.AEStronglyMeasurable Y μ) (h'Y : ¬Y =ᵐ[μ] 0) :
MeasureTheory.Integrable X μ

If the product of two independent real-valued random variables is integrable and the second one is not almost everywhere zero, then the first one is integrable.

source
theorem ProbabilityTheory.IndepFun.integrable_right_of_integrable_mul {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : Type u_3} [MeasurableSpace β] {X Y : Ω → β} [NormedDivisionRing β] [OpensMeasurableSpace β] (hXY : IndepFun X Y μ) (h'XY : MeasureTheory.Integrable (X * Y) μ) (hX : MeasureTheory.AEStronglyMeasurable X μ) (hY : MeasureTheory.AEStronglyMeasurable Y μ) (h'X : ¬X =ᵐ[μ] 0) :
MeasureTheory.Integrable Y μ

If the product of two independent real-valued random variables is integrable and the first one is not almost everywhere zero, then the second one is integrable.

source
theorem ProbabilityTheory.IndepFun.integral_fun_comp_mul_comp {Ω : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝓧 : Type u_3} {𝓨 : Type u_4} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {X : Ω → 𝓧} {Y : Ω → 𝓨} {f : 𝓧 → 𝕜} {g : 𝓨 → 𝕜} (hXY : IndepFun X Y μ) (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map X μ)) (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map Y μ)) :
∫ (ω : Ω), f (X ω) * g (Y ω) ∂μ = (∫ (ω : Ω), f (X ω) ∂μ) * ∫ (ω : Ω), g (Y ω) ∂μ
source
theorem ProbabilityTheory.IndepFun.integral_comp_mul_comp {Ω : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝓧 : Type u_3} {𝓨 : Type u_4} {m𝓧 : MeasurableSpace 𝓧} {m𝓨 : MeasurableSpace 𝓨} {X : Ω → 𝓧} {Y : Ω → 𝓨} {f : 𝓧 → 𝕜} {g : 𝓨 → 𝕜} (hXY : IndepFun X Y μ) (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ) (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map X μ)) (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map Y μ)) :
∫ (x : Ω), (f ∘ X * g ∘ Y) x ∂μ = (∫ (x : Ω), (f ∘ X) x ∂μ) * ∫ (x : Ω), (g ∘ Y) x ∂μ
source
theorem ProbabilityTheory.IndepFun.integral_mul_eq_mul_integral {Ω : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → 𝕜} (hXY : IndepFun X Y μ) (hX : MeasureTheory.AEStronglyMeasurable X μ) (hY : MeasureTheory.AEStronglyMeasurable Y μ) :
∫ (x : Ω), (X * Y) x ∂μ = (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ
source
theorem ProbabilityTheory.IndepFun.integral_fun_mul_eq_mul_integral {Ω : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → 𝕜} (hXY : IndepFun X Y μ) (hX : MeasureTheory.AEStronglyMeasurable X μ) (hY : MeasureTheory.AEStronglyMeasurable Y μ) :
∫ (ω : Ω), X ω * Y ω ∂μ = (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ
source
@[deprecated ProbabilityTheory.IndepFun.integral_mul_eq_mul_integral (since := "2025-07-30")]
theorem ProbabilityTheory.IndepFun.integral_mul_of_nonneg {Ω : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → 𝕜} (hXY : IndepFun X Y μ) (hX : MeasureTheory.AEStronglyMeasurable X μ) (hY : MeasureTheory.AEStronglyMeasurable Y μ) :
∫ (x : Ω), (X * Y) x ∂μ = (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ

Alias of `ProbabilityTheory.IndepFun.integral_mul_eq_mul_integral`.

source
@[deprecated ProbabilityTheory.IndepFun.integral_mul_eq_mul_integral (since := "2025-07-30")]
theorem ProbabilityTheory.IndepFun.integral_mul_of_integrable {Ω : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → 𝕜} (hXY : IndepFun X Y μ) (hX : MeasureTheory.AEStronglyMeasurable X μ) (hY : MeasureTheory.AEStronglyMeasurable Y μ) :
∫ (x : Ω), (X * Y) x ∂μ = (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ

Alias of `ProbabilityTheory.IndepFun.integral_mul_eq_mul_integral`.

source
@[deprecated ProbabilityTheory.IndepFun.integral_mul_eq_mul_integral (since := "2025-07-30")]
theorem ProbabilityTheory.IndepFun.integral_mul {Ω : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → 𝕜} (hXY : IndepFun X Y μ) (hX : MeasureTheory.AEStronglyMeasurable X μ) (hY : MeasureTheory.AEStronglyMeasurable Y μ) :
∫ (x : Ω), (X * Y) x ∂μ = (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ

Alias of `ProbabilityTheory.IndepFun.integral_mul_eq_mul_integral`.

source
@[deprecated ProbabilityTheory.IndepFun.integral_fun_mul_eq_mul_integral (since := "2025-07-30")]
theorem ProbabilityTheory.IndepFun.integral_mul' {Ω : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → 𝕜} (hXY : IndepFun X Y μ) (hX : MeasureTheory.AEStronglyMeasurable X μ) (hY : MeasureTheory.AEStronglyMeasurable Y μ) :
∫ (ω : Ω), X ω * Y ω ∂μ = (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ

Alias of `ProbabilityTheory.IndepFun.integral_fun_mul_eq_mul_integral`.

source
theorem ProbabilityTheory.indepFun_iff_integral_comp_mul {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {β : Type u_3} {β' : Type u_4} {mβ : MeasurableSpace β} {mβ' : MeasurableSpace β'} {f : Ω → β} {g : Ω → β'} {hfm : Measurable f} {hgm : Measurable g} :
IndepFun f g μ ↔ ∀ {φ : β → ℝ} {ψ : β' → ℝ}, Measurable φ → Measurable ψ → MeasureTheory.Integrable (φ ∘ f) μ → MeasureTheory.Integrable (ψ ∘ g) μ → MeasureTheory.integral μ (φ ∘ f * ψ ∘ g) = MeasureTheory.integral μ (φ ∘ f) * MeasureTheory.integral μ (ψ ∘ g)

Independence of functions `f` and `g` into arbitrary types is characterized by the relation `E[(φ ∘ f) * (ψ ∘ g)] = E[φ ∘ f] * E[ψ ∘ g]` for all measurable `φ` and `ψ` with values in `ℝ` satisfying appropriate integrability conditions.

source
theorem ProbabilityTheory.iIndepFun.integral_fun_prod_comp {Ω : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_3} [Fintype ι] {𝓧 : ι → Type u_4} {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i} {f : (i : ι) → 𝓧 i → 𝕜} (hX : iIndepFun X μ) (mX : ∀ (i : ι), AEMeasurable (X i) μ) (hf : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) (MeasureTheory.Measure.map (X i) μ)) :
∫ (ω : Ω), ∏ i : ι, f i (X i ω) ∂μ = ∏ i : ι, ∫ (ω : Ω), f i (X i ω) ∂μ
source
theorem ProbabilityTheory.iIndepFun.integral_prod_comp {Ω : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_3} [Fintype ι] {𝓧 : ι → Type u_4} {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i} {f : (i : ι) → 𝓧 i → 𝕜} (hX : iIndepFun X μ) (mX : ∀ (i : ι), AEMeasurable (X i) μ) (hf : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) (MeasureTheory.Measure.map (X i) μ)) :
∫ (x : Ω), (∏ i : ι, f i ∘ X i) x ∂μ = ∏ i : ι, ∫ (x : Ω), (f i ∘ X i) x ∂μ
source
theorem ProbabilityTheory.iIndepFun.integral_prod_eq_prod_integral {Ω : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_3} [Fintype ι] {X : ι → Ω → 𝕜} (hX : iIndepFun X μ) (mX : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (X i) μ) :
∫ (x : Ω), (∏ i : ι, X i) x ∂μ = ∏ i : ι, ∫ (x : Ω), X i x ∂μ
source
theorem ProbabilityTheory.iIndepFun.integral_fun_prod_eq_prod_integral {Ω : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_3} [Fintype ι] {X : ι → Ω → 𝕜} (hX : iIndepFun X μ) (mX : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable (X i) μ) :
∫ (ω : Ω), ∏ i : ι, X i ω ∂μ = ∏ i : ι, ∫ (x : Ω), X i x ∂μ