MeasureTheory.condexp_indep_eq

theorem MeasureTheory.condexp_indep_eq : ∀ {Ω : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] {m₁ m₂ m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → E}, m₁ ≤ m → ∀ (hle₂ : m₂ ≤ m) [inst_3 : MeasureTheory.SigmaFinite (μ.trim hle₂)], MeasureTheory.StronglyMeasurable f → ProbabilityTheory.Indep m₁ m₂ μ → μ.ae.EventuallyEq (MeasureTheory.condexp m₂ μ f) fun x => ∫ (x : Ω), f x ∂μ

The theorem `MeasureTheory.condexp_indep_eq` states that for any normed additive commutative group `E`, with a normed space over `ℝ` and completeness property, and for any measure space `Ω`, measurable spaces `m₁`, `m₂`, and `m`, a measure `μ` on `Ω`, and a function `f : Ω → E`, if `m₁` and `m₂`are sub-σ-algebras of `m`, `μ` is σ-finite with respect to the σ-algebra obtained by trimming `m₂`, `f` is strongly measurable, and `m₁` and `m₂` are independent σ-algebras with respect to the measure `μ`, then the conditional expectation of `f` given `m₂`, is almost everywhere equal to the expectation of `f`. In other words, if two σ-algebras are independent and a function is measurable with respect to one of them, then the conditional expectation of the function given the other σ-algebra equals the expectation of the function almost everywhere.

More concisely: If `μ` is a measure on `Ω`, `E` is a normed additive commutative group with a completeness property over `ℝ`, `f : Ω → E` is strongly measurable, `m₁` and `m₂` are sub-σ-algebras of `m` that are independent with respect to `μ`, and `μ` is σ-finite with respect to the σ-algebra obtained by trimming `m₂`, then the conditional expectation of `f` given `m₂` equals the expectation of `f` almost everywhere.