LeanMachineLearning exposition

ProbabilityTheory.lintegral_cond🔗

Minimal Lean file

lintegral_cond🔗

LemmaProbabilityTheory.lintegral_cond
Details

No docstring.

🔗theorem
ProbabilityTheory.lintegral_cond.{u_1} {α : Type u_1}
  {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α)
  (f : α → ENNReal) :
  ∫⁻ (x : α), f x ∂μ[|s] = (μ s)⁻¹ * ∫⁻ (a : α) in s, f a ∂μ
ProbabilityTheory.lintegral_cond.{u_1}
  {α : Type u_1} {mα : MeasurableSpace α}
  {μ : MeasureTheory.Measure α}
  (s : Set α) (f : α → ENNReal) :
  ∫⁻ (x : α), f x ∂μ[|s] =
    (μ s)⁻¹ * ∫⁻ (a : α) in s, f a ∂μ

Code

lemma lintegral_cond {μ : Measure α} (s : Set α) (f : α → ℝ≥0∞) :
    ∫⁻ x, f x ∂μ[|s] = (μ s)⁻¹ * ∫⁻ (a : α) in s, f a ∂μ
Used by (1)

Actions: Source · Open Issue

Proof
by
  unfold cond
  simp [lintegral_smul_measure]