English
Under NeZero μ, the conditional expectation with bottom (⊥) equals a scalar multiple of the global integral with a one over μ(real univ).
Русский
При μ ≠ 0 условное ожидание на дне равняется скалярному множителю от общего интеграла.
LaTeX
$$$$\\mu[f|⊥] = \\text{scalar} \\cdot \\int f \\, d\\mu.$$$$
Lean4
theorem condExp_bot' [hμ : NeZero μ] (f : α → E) : μ[f|⊥] = fun _ => (μ.real Set.univ)⁻¹ • ∫ x, f x ∂μ :=
by
by_cases hμ_finite : IsFiniteMeasure μ
swap
· have h : ¬SigmaFinite (μ.trim bot_le) := by rwa [sigmaFinite_trim_bot_iff]
rw [not_isFiniteMeasure_iff] at hμ_finite
rw [condExp_of_not_sigmaFinite bot_le h]
simp only [hμ_finite, ENNReal.toReal_top, inv_zero, zero_smul, measureReal_def]
rfl
have h_meas : StronglyMeasurable[⊥] (μ[f|⊥]) := stronglyMeasurable_condExp
obtain ⟨c, h_eq⟩ := stronglyMeasurable_bot_iff.mp h_meas
rw [h_eq]
have h_integral : ∫ x, (μ[f|⊥]) x ∂μ = ∫ x, f x ∂μ := integral_condExp bot_le
simp_rw [h_eq, integral_const] at h_integral
rw [← h_integral, ← smul_assoc, smul_eq_mul, inv_mul_cancel₀, one_smul]
rw [Ne, measureReal_def, ENNReal.toReal_eq_zero_iff, not_or]
exact ⟨NeZero.ne _, measure_ne_top μ Set.univ⟩
