import Mathlib.Data.Real.StarOrdered
import Mathlib.Order.CompletePartialOrder
import Mathlib.Probability.ConditionalExpectation
import Mathlib.Probability.Kernel.Disintegration.StandardBorel

open MeasureTheory Set ProbabilityTheory
/--
  If two constant functions are equal a.e w.r.t. a measure that is positive when applied to univ,
  then the two constants are equal.
-/
lemma constant_ae_eq_imp_eq {α β : Type*} [MeasurableSpace α] {μ : Measure α}
    (hμ : μ univ ≠ 0) (c d : β) (h_ae : (fun (_: α) ↦ c) =ᵐ[μ] (fun (_: α) ↦ d)) :
    c = d := by
Goals accomplished! 🐙
  
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
hμ: μ univ ≠ 0
c, d: β
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
c = dby_contra h
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
hμ: μ univ ≠ 0
c, d: β
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
h: ¬c = d
False
  
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
hμ: μ univ ≠ 0
c, d: β
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
c = dpush_neg at h
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
hμ: μ univ ≠ 0
c, d: β
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
h: c ≠ d
False
  
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
hμ: μ univ ≠ 0
c, d: β
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
c = dhave : μ ({(_ : α) | c = d} ∪ {(_ : α) | c = d}ᶜ) = 0 := 
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
hμ: μ univ ≠ 0
c, d: β
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
h: c ≠ d
Falseby
Goals accomplished! 🐙
    
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
hμ: μ univ ≠ 0
c, d: β
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
h: c ≠ d
Falsehave : μ {(_ : α) | c = d} = 0 := 
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
hμ: μ univ ≠ 0
c, d: β
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
h: c ≠ d
μ ({x | c = d} ∪ {x | c = d}ᶜ) = 0by
Goals accomplished! 🐙
      
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
hμ: μ univ ≠ 0
c, d: β
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
h: c ≠ d
μ ({x | c = d} ∪ {x | c = d}ᶜ) = 0have : {(_ : α) | c = d} = ∅ := subset_eq_empty (fun _ ↦ h) rfl
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
hμ: μ univ ≠ 0
c, d: β
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
h: c ≠ d
this: {x | c = d} = ∅
μ {x | c = d} = 0
      
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
hμ: μ univ ≠ 0
c, d: β
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
h: c ≠ d
μ ({x | c = d} ∪ {x | c = d}ᶜ) = 0rw [
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
hμ: μ univ ≠ 0
c, d: β
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
h: c ≠ d
this: {x | c = d} = ∅
μ {x | c = d} = 0this
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
hμ: μ univ ≠ 0
c, d: β
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
h: c ≠ d
this: {x | c = d} = ∅
μ ∅ = 0]
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
hμ: μ univ ≠ 0
c, d: β
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
h: c ≠ d
this: {x | c = d} = ∅
μ ∅ = 0
      
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
hμ: μ univ ≠ 0
c, d: β
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
h: c ≠ d
μ ({x | c = d} ∪ {x | c = d}ᶜ) = 0exact OuterMeasureClass.measure_empty μ
Goals accomplished! 🐙
    
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
hμ: μ univ ≠ 0
c, d: β
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
h: c ≠ d
Falseexact measure_union_null this h_ae
Goals accomplished! 🐙
  
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
hμ: μ univ ≠ 0
c, d: β
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
c = drw [
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
hμ: μ univ ≠ 0
c, d: β
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
h: c ≠ d
this: μ ({x | c = d} ∪ {x | c = d}ᶜ) = 0
False← union_compl_self {(_ : α) | c = d}
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
c, d: β
hμ: μ ({x | c = d} ∪ {x | c = d}ᶜ) ≠ 0
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
h: c ≠ d
this: μ ({x | c = d} ∪ {x | c = d}ᶜ) = 0
False]
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
c, d: β
hμ: μ ({x | c = d} ∪ {x | c = d}ᶜ) ≠ 0
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
h: c ≠ d
this: μ ({x | c = d} ∪ {x | c = d}ᶜ) = 0
False at hμ
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
c, d: β
hμ: μ ({x | c = d} ∪ {x | c = d}ᶜ) ≠ 0
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
h: c ≠ d
this: μ ({x | c = d} ∪ {x | c = d}ᶜ) = 0
False
  
α: Type u_1
β: Type u_2
inst✝: MeasurableSpace α
μ: Measure α
hμ: μ univ ≠ 0
c, d: β
h_ae: (fun x => c) =ᶠ[ae μ] fun x => d
c = dcontradiction
Goals accomplished! 🐙

/-
  Law of total probability using `condKernel`.
-/
namespace ProbTotalLaw

variable {Ω α: Type} [Nonempty Ω] [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace Ω]

/- instance {μ : Measure α} {ν : Measure Ω} [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
    IsFiniteMeasure (μ.prod ν) where
  measure_univ_lt_top := by
    rw [μ.prod_apply MeasurableSet.univ]
    simp_rw [preimage_univ, lintegral_const]
    suffices ν univ * μ univ < ⊤ * ⊤ by exact this
    exact ENNReal.mul_lt_mul
      (IsFiniteMeasure.measure_univ_lt_top) (IsFiniteMeasure.measure_univ_lt_top) -/

variable (μ : Measure α) (ν : Measure Ω) [IsFiniteMeasure μ] [IsFiniteMeasure ν]

theorem probability_total_law :
    ∀ s, μ s = ∫⁻ x in s, ∫⁻ _, 1 ∂(μ.prod ν).condKernel x ∂μ := by
Goals accomplished! 🐙
  
Ω, α: Type
inst✝⁵: Nonempty Ω
inst✝⁴: MeasurableSpace Ω
inst✝³: MeasurableSpace α
inst✝²: StandardBorelSpace Ω
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure μ
inst✝: IsFiniteMeasure ν
∀ (s : Set α), μ s = ∫⁻ (x : α) in s, ∫⁻ (x : Ω), 1 ∂(μ.prod ν).condKernel x ∂μintro s
Ω, α: Type
inst✝⁵: Nonempty Ω
inst✝⁴: MeasurableSpace Ω
inst✝³: MeasurableSpace α
inst✝²: StandardBorelSpace Ω
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure μ
inst✝: IsFiniteMeasure ν
s: Set α
μ s = ∫⁻ (x : α) in s, ∫⁻ (x : Ω), 1 ∂(μ.prod ν).condKernel x ∂μ
  
Ω, α: Type
inst✝⁵: Nonempty Ω
inst✝⁴: MeasurableSpace Ω
inst✝³: MeasurableSpace α
inst✝²: StandardBorelSpace Ω
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure μ
inst✝: IsFiniteMeasure ν
∀ (s : Set α), μ s = ∫⁻ (x : α) in s, ∫⁻ (x : Ω), 1 ∂(μ.prod ν).condKernel x ∂μsimp_rw [
Ω, α: Type
inst✝⁵: Nonempty Ω
inst✝⁴: MeasurableSpace Ω
inst✝³: MeasurableSpace α
inst✝²: StandardBorelSpace Ω
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure μ
inst✝: IsFiniteMeasure ν
s: Set α
μ s = ∫⁻ (x : α) in s, ∫⁻ (x : Ω), 1 ∂(μ.prod ν).condKernel x ∂μfun _ ↦ lintegral_one
Ω, α: Type
inst✝⁵: Nonempty Ω
inst✝⁴: MeasurableSpace Ω
inst✝³: MeasurableSpace α
inst✝²: StandardBorelSpace Ω
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure μ
inst✝: IsFiniteMeasure ν
s: Set α
μ s = ∫⁻ (x : α) in s, ((μ.prod ν).condKernel x) univ ∂μ]
Ω, α: Type
inst✝⁵: Nonempty Ω
inst✝⁴: MeasurableSpace Ω
inst✝³: MeasurableSpace α
inst✝²: StandardBorelSpace Ω
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure μ
inst✝: IsFiniteMeasure ν
s: Set α
μ s = ∫⁻ (x : α) in s, ((μ.prod ν).condKernel x) univ ∂μ
  
Ω, α: Type
inst✝⁵: Nonempty Ω
inst✝⁴: MeasurableSpace Ω
inst✝³: MeasurableSpace α
inst✝²: StandardBorelSpace Ω
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure μ
inst✝: IsFiniteMeasure ν
∀ (s : Set α), μ s = ∫⁻ (x : α) in s, ∫⁻ (x : Ω), 1 ∂(μ.prod ν).condKernel x ∂μhave is_prob_measure : ∀ x, (μ.prod ν).condKernel x univ = 1 :=
    fun x ↦ isProbabilityMeasure_iff.mp (IsMarkovKernel.isProbabilityMeasure x)
Ω, α: Type
inst✝⁵: Nonempty Ω
inst✝⁴: MeasurableSpace Ω
inst✝³: MeasurableSpace α
inst✝²: StandardBorelSpace Ω
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure μ
inst✝: IsFiniteMeasure ν
s: Set α
is_prob_measure: ∀ (x : α), ((μ.prod ν).condKernel x) univ = 1
μ s = ∫⁻ (x : α) in s, ((μ.prod ν).condKernel x) univ ∂μ
  
Ω, α: Type
inst✝⁵: Nonempty Ω
inst✝⁴: MeasurableSpace Ω
inst✝³: MeasurableSpace α
inst✝²: StandardBorelSpace Ω
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure μ
inst✝: IsFiniteMeasure ν
∀ (s : Set α), μ s = ∫⁻ (x : α) in s, ∫⁻ (x : Ω), 1 ∂(μ.prod ν).condKernel x ∂μsimp_rw [
Ω, α: Type
inst✝⁵: Nonempty Ω
inst✝⁴: MeasurableSpace Ω
inst✝³: MeasurableSpace α
inst✝²: StandardBorelSpace Ω
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure μ
inst✝: IsFiniteMeasure ν
s: Set α
is_prob_measure: ∀ (x : α), ((μ.prod ν).condKernel x) univ = 1
μ s = ∫⁻ (x : α) in s, ((μ.prod ν).condKernel x) univ ∂μis_prob_measure
Ω, α: Type
inst✝⁵: Nonempty Ω
inst✝⁴: MeasurableSpace Ω
inst✝³: MeasurableSpace α
inst✝²: StandardBorelSpace Ω
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure μ
inst✝: IsFiniteMeasure ν
s: Set α
is_prob_measure: ∀ (x : α), ((μ.prod ν).condKernel x) univ = 1
μ s = ∫⁻ (x : α) in s, 1 ∂μ]
Ω, α: Type
inst✝⁵: Nonempty Ω
inst✝⁴: MeasurableSpace Ω
inst✝³: MeasurableSpace α
inst✝²: StandardBorelSpace Ω
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure μ
inst✝: IsFiniteMeasure ν
s: Set α
is_prob_measure: ∀ (x : α), ((μ.prod ν).condKernel x) univ = 1
μ s = ∫⁻ (x : α) in s, 1 ∂μ
  
Ω, α: Type
inst✝⁵: Nonempty Ω
inst✝⁴: MeasurableSpace Ω
inst✝³: MeasurableSpace α
inst✝²: StandardBorelSpace Ω
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure μ
inst✝: IsFiniteMeasure ν
∀ (s : Set α), μ s = ∫⁻ (x : α) in s, ∫⁻ (x : Ω), 1 ∂(μ.prod ν).condKernel x ∂μexact (setLIntegral_one s).symm
Goals accomplished! 🐙

variable [IsProbabilityMeasure ν]

omit [Nonempty Ω] [StandardBorelSpace Ω] [IsFiniteMeasure μ] in
lemma apply_fst : (μ.prod ν).fst = μ := by
Goals accomplished! 🐙
  
Ω, α: Type
inst✝³: MeasurableSpace Ω
inst✝²: MeasurableSpace α
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure ν
inst✝: IsProbabilityMeasure ν
(μ.prod ν).fst = μrw [
Ω, α: Type
inst✝³: MeasurableSpace Ω
inst✝²: MeasurableSpace α
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure ν
inst✝: IsProbabilityMeasure ν
(μ.prod ν).fst = μshow (μ.prod ν).fst = (μ.prod ν).map Prod.fst by 
Ω, α: Type
inst✝³: MeasurableSpace Ω
inst✝²: MeasurableSpace α
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure ν
inst✝: IsProbabilityMeasure ν
(μ.prod ν).fst = μrfl
Goals accomplished! 🐙]
Ω, α: Type
inst✝³: MeasurableSpace Ω
inst✝²: MeasurableSpace α
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure ν
inst✝: IsProbabilityMeasure ν
Measure.map Prod.fst (μ.prod ν) = μ
  
Ω, α: Type
inst✝³: MeasurableSpace Ω
inst✝²: MeasurableSpace α
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure ν
inst✝: IsProbabilityMeasure ν
(μ.prod ν).fst = μrw [
Ω, α: Type
inst✝³: MeasurableSpace Ω
inst✝²: MeasurableSpace α
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure ν
inst✝: IsProbabilityMeasure ν
Measure.map Prod.fst (μ.prod ν) = μMeasure.map_fst_prod,
Ω, α: Type
inst✝³: MeasurableSpace Ω
inst✝²: MeasurableSpace α
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure ν
inst✝: IsProbabilityMeasure ν
ν univ • μ = μ 
Ω, α: Type
inst✝³: MeasurableSpace Ω
inst✝²: MeasurableSpace α
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure ν
inst✝: IsProbabilityMeasure ν
Measure.map Prod.fst (μ.prod ν) = μmeasure_univ,
Ω, α: Type
inst✝³: MeasurableSpace Ω
inst✝²: MeasurableSpace α
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure ν
inst✝: IsProbabilityMeasure ν
1 • μ = μ 
Ω, α: Type
inst✝³: MeasurableSpace Ω
inst✝²: MeasurableSpace α
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure ν
inst✝: IsProbabilityMeasure ν
Measure.map Prod.fst (μ.prod ν) = μone_smul
Ω, α: Type
inst✝³: MeasurableSpace Ω
inst✝²: MeasurableSpace α
μ: Measure α
ν: Measure Ω
inst✝¹: IsFiniteMeasure ν
inst✝: IsProbabilityMeasure ν
μ = μ]
Goals accomplished! 🐙

lemma apply_comp : μ.prod ν = μ ⊗ₘ (μ.prod ν).condKernel := by
Goals accomplished! 🐙
  
Ω, α: Type
inst✝⁶: Nonempty Ω
inst✝⁵: MeasurableSpace Ω
inst✝⁴: MeasurableSpace α
inst✝³: StandardBorelSpace Ω
μ: Measure α
ν: Measure Ω
inst✝²: IsFiniteMeasure μ
inst✝¹: IsFiniteMeasure ν
inst✝: IsProbabilityMeasure ν
μ.prod ν = μ ⊗ₘ (μ.prod ν).condKernelrw (config := {occs := .pos [2]}) [
Ω, α: Type
inst✝⁶: Nonempty Ω
inst✝⁵: MeasurableSpace Ω
inst✝⁴: MeasurableSpace α
inst✝³: StandardBorelSpace Ω
μ: Measure α
ν: Measure Ω
inst✝²: IsFiniteMeasure μ
inst✝¹: IsFiniteMeasure ν
inst✝: IsProbabilityMeasure ν
μ.prod ν = μ ⊗ₘ (μ.prod ν).condKernel← apply_fst μ ν
Ω, α: Type
inst✝⁶: Nonempty Ω
inst✝⁵: MeasurableSpace Ω
inst✝⁴: MeasurableSpace α
inst✝³: StandardBorelSpace Ω
μ: Measure α
ν: Measure Ω
inst✝²: IsFiniteMeasure μ
inst✝¹: IsFiniteMeasure ν
inst✝: IsProbabilityMeasure ν
μ.prod ν = (μ.prod ν).fst ⊗ₘ (μ.prod ν).condKernel]
Ω, α: Type
inst✝⁶: Nonempty Ω
inst✝⁵: MeasurableSpace Ω
inst✝⁴: MeasurableSpace α
inst✝³: StandardBorelSpace Ω
μ: Measure α
ν: Measure Ω
inst✝²: IsFiniteMeasure μ
inst✝¹: IsFiniteMeasure ν
inst✝: IsProbabilityMeasure ν
μ.prod ν = (μ.prod ν).fst ⊗ₘ (μ.prod ν).condKernel
  
Ω, α: Type
inst✝⁶: Nonempty Ω
inst✝⁵: MeasurableSpace Ω
inst✝⁴: MeasurableSpace α
inst✝³: StandardBorelSpace Ω
μ: Measure α
ν: Measure Ω
inst✝²: IsFiniteMeasure μ
inst✝¹: IsFiniteMeasure ν
inst✝: IsProbabilityMeasure ν
μ.prod ν = μ ⊗ₘ (μ.prod ν).condKernelexact ((μ.prod ν).disintegrate (μ.prod ν).condKernel).symm
Goals accomplished! 🐙

end ProbTotalLaw

/-
 Tower property of conditional expectation using `condexp`.
-/
namespace ExpCond

variable {Ω F : Type*}
[NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
{m2 m₁ mΩ : MeasurableSpace Ω} {μ : Measure Ω} {X : Ω → F}

/- example (hm₁ : m₁ ≤ mΩ) (m₂ : m2 ≤ m₁) [SigmaFinite (μ.trim hm₁)] :
    ∀ (s : Set Ω), MeasurableSet[m2] s → ∫ x in s, condexp m2 μ X x ∂μ
    = ∫ x in s, condexp m₁ μ (condexp m2 μ X) x ∂μ := by
  intro s hs
  exact (setIntegral_condexp hm₁ (integrable_condexp) (m₂ s hs)).symm -/

theorem tower_property {X : Ω → F} (hX : Integrable X μ) (hm₁ : m₁ ≤ mΩ) (m₂ : m2 ≤ m₁) [SigmaFinite (μ.trim (m₂.trans hm₁))] :
    μ[X | m2] =ᵐ[μ] μ[μ[X | m₁] | m2] := by
Goals accomplished! 🐙
  
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
μ[X|m2] =ᶠ[ae μ] μ[μ[X|m₁]|m2]have : SigmaFinite (μ.trim hm₁) := sigmaFiniteTrim_mono hm₁ m₂
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
μ[X|m2] =ᶠ[ae μ] μ[μ[X|m₁]|m2]
  
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
μ[X|m2] =ᶠ[ae μ] μ[μ[X|m₁]|m2]apply ae_eq_condexp_of_forall_setIntegral_eq
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
hf
Integrable (μ[X|m₁]) μ
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
hg_int_finite
∀ (s : Set Ω), MeasurableSet s → μ s < ⊤ → IntegrableOn (μ[X|m2]) s μ
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
hg_eq
∀ (s : Set Ω), MeasurableSet s → μ s < ⊤ → ∫ (x : Ω) in s, (μ[X|m2]) x ∂μ = ∫ (x : Ω) in s, (μ[X|m₁]) x ∂μ
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
hgm
AEStronglyMeasurable' m2 (μ[X|m2]) μ
  
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
μ[X|m2] =ᶠ[ae μ] μ[μ[X|m₁]|m2]·
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
hf
Integrable (μ[X|m₁]) μ 
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
hf
Integrable (μ[X|m₁]) μ
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
hg_int_finite
∀ (s : Set Ω), MeasurableSet s → μ s < ⊤ → IntegrableOn (μ[X|m2]) s μ
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
hg_eq
∀ (s : Set Ω), MeasurableSet s → μ s < ⊤ → ∫ (x : Ω) in s, (μ[X|m2]) x ∂μ = ∫ (x : Ω) in s, (μ[X|m₁]) x ∂μ
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
hgm
AEStronglyMeasurable' m2 (μ[X|m2]) μexact integrable_condexp
Goals accomplished! 🐙
  
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
μ[X|m2] =ᶠ[ae μ] μ[μ[X|m₁]|m2]·
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
hg_int_finite
∀ (s : Set Ω), MeasurableSet s → μ s < ⊤ → IntegrableOn (μ[X|m2]) s μ 
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
hg_int_finite
∀ (s : Set Ω), MeasurableSet s → μ s < ⊤ → IntegrableOn (μ[X|m2]) s μ
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
hg_eq
∀ (s : Set Ω), MeasurableSet s → μ s < ⊤ → ∫ (x : Ω) in s, (μ[X|m2]) x ∂μ = ∫ (x : Ω) in s, (μ[X|m₁]) x ∂μ
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
hgm
AEStronglyMeasurable' m2 (μ[X|m2]) μintro s _ _
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
s: Set Ω
a✝¹: MeasurableSet s
a✝: μ s < ⊤
hg_int_finite
IntegrableOn (μ[X|m2]) s μ
    
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
hg_int_finite
∀ (s : Set Ω), MeasurableSet s → μ s < ⊤ → IntegrableOn (μ[X|m2]) s μexact integrable_condexp.integrableOn
Goals accomplished! 🐙
  
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
μ[X|m2] =ᶠ[ae μ] μ[μ[X|m₁]|m2]·
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
hg_eq
∀ (s : Set Ω), MeasurableSet s → μ s < ⊤ → ∫ (x : Ω) in s, (μ[X|m2]) x ∂μ = ∫ (x : Ω) in s, (μ[X|m₁]) x ∂μ 
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
hg_eq
∀ (s : Set Ω), MeasurableSet s → μ s < ⊤ → ∫ (x : Ω) in s, (μ[X|m2]) x ∂μ = ∫ (x : Ω) in s, (μ[X|m₁]) x ∂μ
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
hgm
AEStronglyMeasurable' m2 (μ[X|m2]) μintro s hs _
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
s: Set Ω
hs: MeasurableSet s
a✝: μ s < ⊤
hg_eq
∫ (x : Ω) in s, (μ[X|m2]) x ∂μ = ∫ (x : Ω) in s, (μ[X|m₁]) x ∂μ
    
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
hg_eq
∀ (s : Set Ω), MeasurableSet s → μ s < ⊤ → ∫ (x : Ω) in s, (μ[X|m2]) x ∂μ = ∫ (x : Ω) in s, (μ[X|m₁]) x ∂μrw [
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
s: Set Ω
hs: MeasurableSet s
a✝: μ s < ⊤
hg_eq
∫ (x : Ω) in s, (μ[X|m2]) x ∂μ = ∫ (x : Ω) in s, (μ[X|m₁]) x ∂μsetIntegral_condexp (m₂.trans hm₁) hX hs
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
s: Set Ω
hs: MeasurableSet s
a✝: μ s < ⊤
hg_eq
∫ (x : Ω) in s, X x ∂μ = ∫ (x : Ω) in s, (μ[X|m₁]) x ∂μ]
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
s: Set Ω
hs: MeasurableSet s
a✝: μ s < ⊤
hg_eq
∫ (x : Ω) in s, X x ∂μ = ∫ (x : Ω) in s, (μ[X|m₁]) x ∂μ
    
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
hg_eq
∀ (s : Set Ω), MeasurableSet s → μ s < ⊤ → ∫ (x : Ω) in s, (μ[X|m2]) x ∂μ = ∫ (x : Ω) in s, (μ[X|m₁]) x ∂μhave hs2 : MeasurableSet[m₁] s := m₂ s hs
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
s: Set Ω
hs: MeasurableSet s
a✝: μ s < ⊤
hs2: MeasurableSet s
hg_eq
∫ (x : Ω) in s, X x ∂μ = ∫ (x : Ω) in s, (μ[X|m₁]) x ∂μ
    
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
hg_eq
∀ (s : Set Ω), MeasurableSet s → μ s < ⊤ → ∫ (x : Ω) in s, (μ[X|m2]) x ∂μ = ∫ (x : Ω) in s, (μ[X|m₁]) x ∂μrw [
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
s: Set Ω
hs: MeasurableSet s
a✝: μ s < ⊤
hs2: MeasurableSet s
hg_eq
∫ (x : Ω) in s, X x ∂μ = ∫ (x : Ω) in s, (μ[X|m₁]) x ∂μsetIntegral_condexp hm₁ hX hs2
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
this: SigmaFinite (μ.trim hm₁)
s: Set Ω
hs: MeasurableSet s
a✝: μ s < ⊤
hs2: MeasurableSet s
hg_eq
∫ (x : Ω) in s, X x ∂μ = ∫ (x : Ω) in s, X x ∂μ]
Goals accomplished! 🐙
  
Ω: Type u_1
F: Type u_2
inst✝³: NormedAddCommGroup F
inst✝²: NormedSpace ℝ F
inst✝¹: CompleteSpace F
m2, m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
m₂: m2 ≤ m₁
inst✝: SigmaFinite (μ.trim ⋯)
μ[X|m2] =ᶠ[ae μ] μ[μ[X|m₁]|m2]exact StronglyMeasurable.aeStronglyMeasurable' (stronglyMeasurable_condexp)
Goals accomplished! 🐙

end ExpCond

/-
  Law of total expectation using `condExp`.
-/
namespace ExpTotal

variable {Ω F : Type*}
[NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F]
{m2 m₁ mΩ : MeasurableSpace Ω} {μ : Measure Ω} {X : Ω → F}

open ExpCond

def S : Set (Set Ω) := {∅, univ}

lemma destruct_S : ∀ ⦃t : Set Ω⦄, t ∈ S → t = ∅ ∨ t = univ := fun _ ht ↦ ht

lemma S_apply : (∅ : Set Ω) ∈ S ∧ (univ : Set Ω) ∈ S :=
  ⟨mem_insert ∅ {univ}, mem_insert_of_mem ∅ rfl⟩

/--
  The trivial σ-algebra : {∅, univ}.
-/
def m_trivial : MeasurableSpace Ω := MeasurableSpace.generateFrom S

/--
  The trivial σ-algebra is less or equal then any σ-algebra.
-/
lemma m_trivial_le : ∀ (m : MeasurableSpace Ω), m_trivial ≤ m := by
Goals accomplished! 🐙
  
Ω: Type u_1
∀ (m : MeasurableSpace Ω), m_trivial ≤ mintro _
Ω: Type u_1
m✝: MeasurableSpace Ω
m_trivial ≤ m✝
  
Ω: Type u_1
∀ (m : MeasurableSpace Ω), m_trivial ≤ mapply MeasurableSpace.generateFrom_le
Ω: Type u_1
m✝: MeasurableSpace Ω
h
∀ t ∈ S, MeasurableSet t
  
Ω: Type u_1
∀ (m : MeasurableSpace Ω), m_trivial ≤ mintro _ ht
Ω: Type u_1
m✝: MeasurableSpace Ω
t✝: Set Ω
ht: t✝ ∈ S
h
MeasurableSet t✝
  
Ω: Type u_1
∀ (m : MeasurableSpace Ω), m_trivial ≤ mcases destruct_S ht with
  
Ω: Type u_1
m✝: MeasurableSpace Ω
t✝: Set Ω
ht: t✝ ∈ S
x✝: t✝ = ∅ ∨ t✝ = univ
h
MeasurableSet t✝| inl h =>
    
Ω: Type u_1
m✝: MeasurableSpace Ω
t✝: Set Ω
ht: t✝ ∈ S
h: t✝ = ∅
h.inl
MeasurableSet t✝rw [
Ω: Type u_1
m✝: MeasurableSpace Ω
t✝: Set Ω
ht: t✝ ∈ S
h: t✝ = ∅
h.inl
MeasurableSet t✝h
Ω: Type u_1
m✝: MeasurableSpace Ω
t✝: Set Ω
ht: t✝ ∈ S
h: t✝ = ∅
h.inl
MeasurableSet ∅]
Ω: Type u_1
m✝: MeasurableSpace Ω
t✝: Set Ω
ht: t✝ ∈ S
h: t✝ = ∅
h.inl
MeasurableSet ∅
    
Ω: Type u_1
m✝: MeasurableSpace Ω
t✝: Set Ω
ht: t✝ ∈ S
h: t✝ = ∅
h.inl
MeasurableSet t✝exact MeasurableSet.empty
Goals accomplished! 🐙
  
Ω: Type u_1
m✝: MeasurableSpace Ω
t✝: Set Ω
ht: t✝ ∈ S
x✝: t✝ = ∅ ∨ t✝ = univ
h
MeasurableSet t✝| inr h =>
    
Ω: Type u_1
m✝: MeasurableSpace Ω
t✝: Set Ω
ht: t✝ ∈ S
h: t✝ = univ
h.inr
MeasurableSet t✝rw [
Ω: Type u_1
m✝: MeasurableSpace Ω
t✝: Set Ω
ht: t✝ ∈ S
h: t✝ = univ
h.inr
MeasurableSet t✝h
Ω: Type u_1
m✝: MeasurableSpace Ω
t✝: Set Ω
ht: t✝ ∈ S
h: t✝ = univ
h.inr
MeasurableSet univ]
Ω: Type u_1
m✝: MeasurableSpace Ω
t✝: Set Ω
ht: t✝ ∈ S
h: t✝ = univ
h.inr
MeasurableSet univ
    
Ω: Type u_1
m✝: MeasurableSpace Ω
t✝: Set Ω
ht: t✝ ∈ S
h: t✝ = univ
h.inr
MeasurableSet t✝exact MeasurableSet.univ
Goals accomplished! 🐙

/--
  The trivial σ-algebra is only composed of ∅ and univ.
-/
lemma measurableSet_S {s : Set Ω} : MeasurableSet[m_trivial] s → s ∈ S := by
Goals accomplished! 🐙
  
Ω: Type u_1
s: Set Ω
MeasurableSet s → s ∈ Sapply MeasurableSpace.generateFrom_induction
Ω: Type u_1
s: Set Ω
hC
∀ t ∈ S, t ∈ S
Ω: Type u_1
s: Set Ω
h_empty
∅ ∈ S
Ω: Type u_1
s: Set Ω
h_compl
∀ t ∈ S, tᶜ ∈ S
Ω: Type u_1
s: Set Ω
h_Union
∀ (f : ℕ → Set Ω), (∀ (n : ℕ), f n ∈ S) → ⋃ i, f i ∈ S
  
Ω: Type u_1
s: Set Ω
MeasurableSet s → s ∈ S·
Ω: Type u_1
s: Set Ω
hC
∀ t ∈ S, t ∈ S 
Ω: Type u_1
s: Set Ω
hC
∀ t ∈ S, t ∈ S
Ω: Type u_1
s: Set Ω
h_empty
∅ ∈ S
Ω: Type u_1
s: Set Ω
h_compl
∀ t ∈ S, tᶜ ∈ S
Ω: Type u_1
s: Set Ω
h_Union
∀ (f : ℕ → Set Ω), (∀ (n : ℕ), f n ∈ S) → ⋃ i, f i ∈ Ssimp only [imp_self, implies_true]
Goals accomplished! 🐙
  
Ω: Type u_1
s: Set Ω
MeasurableSet s → s ∈ S·
Ω: Type u_1
s: Set Ω
h_empty
∅ ∈ S 
Ω: Type u_1
s: Set Ω
h_empty
∅ ∈ S
Ω: Type u_1
s: Set Ω
h_compl
∀ t ∈ S, tᶜ ∈ S
Ω: Type u_1
s: Set Ω
h_Union
∀ (f : ℕ → Set Ω), (∀ (n : ℕ), f n ∈ S) → ⋃ i, f i ∈ Sexact S_apply.1
Goals accomplished! 🐙
  
Ω: Type u_1
s: Set Ω
MeasurableSet s → s ∈ Sintro t ht
Ω: Type u_1
s, t: Set Ω
ht: t ∈ S
h_compl
tᶜ ∈ S
Ω: Type u_1
s: Set Ω
h_Union
∀ (f : ℕ → Set Ω), (∀ (n : ℕ), f n ∈ S) → ⋃ i, f i ∈ S
  
Ω: Type u_1
s: Set Ω
MeasurableSet s → s ∈ Scases destruct_S ht with
  
Ω: Type u_1
s, t: Set Ω
ht: t ∈ S
x✝: t = ∅ ∨ t = univ
h_compl
tᶜ ∈ S| inl ht =>
    
Ω: Type u_1
s, t: Set Ω
ht✝: t ∈ S
ht: t = ∅
h_compl.inl
tᶜ ∈ Srw [
Ω: Type u_1
s, t: Set Ω
ht✝: t ∈ S
ht: t = ∅
h_compl.inl
tᶜ ∈ Sht
Ω: Type u_1
s, t: Set Ω
ht✝: t ∈ S
ht: t = ∅
h_compl.inl
∅ᶜ ∈ S]
Ω: Type u_1
s, t: Set Ω
ht✝: t ∈ S
ht: t = ∅
h_compl.inl
∅ᶜ ∈ S
    
Ω: Type u_1
s, t: Set Ω
ht✝: t ∈ S
ht: t = ∅
h_compl.inl
tᶜ ∈ Shave : ∅ᶜ = (univ : Set Ω) := compl_empty
Ω: Type u_1
s, t: Set Ω
ht✝: t ∈ S
ht: t = ∅
this: ∅ᶜ = univ
h_compl.inl
∅ᶜ ∈ S
    
Ω: Type u_1
s, t: Set Ω
ht✝: t ∈ S
ht: t = ∅
h_compl.inl
tᶜ ∈ Srw [
Ω: Type u_1
s, t: Set Ω
ht✝: t ∈ S
ht: t = ∅
this: ∅ᶜ = univ
h_compl.inl
∅ᶜ ∈ Scompl_empty
Ω: Type u_1
s, t: Set Ω
ht✝: t ∈ S
ht: t = ∅
this: ∅ᶜ = univ
h_compl.inl
univ ∈ S]
Ω: Type u_1
s, t: Set Ω
ht✝: t ∈ S
ht: t = ∅
this: ∅ᶜ = univ
h_compl.inl
univ ∈ S
    
Ω: Type u_1
s, t: Set Ω
ht✝: t ∈ S
ht: t = ∅
h_compl.inl
tᶜ ∈ Sexact S_apply.2
Goals accomplished! 🐙
  
Ω: Type u_1
s, t: Set Ω
ht: t ∈ S
x✝: t = ∅ ∨ t = univ
h_compl
tᶜ ∈ S| inr ht =>
    
Ω: Type u_1
s, t: Set Ω
ht✝: t ∈ S
ht: t = univ
h_compl.inr
tᶜ ∈ Srw [
Ω: Type u_1
s, t: Set Ω
ht✝: t ∈ S
ht: t = univ
h_compl.inr
tᶜ ∈ Sht,
Ω: Type u_1
s, t: Set Ω
ht✝: t ∈ S
ht: t = univ
h_compl.inr
univᶜ ∈ S 
Ω: Type u_1
s, t: Set Ω
ht✝: t ∈ S
ht: t = univ
h_compl.inr
tᶜ ∈ Scompl_univ
Ω: Type u_1
s, t: Set Ω
ht✝: t ∈ S
ht: t = univ
h_compl.inr
∅ ∈ S]
Ω: Type u_1
s, t: Set Ω
ht✝: t ∈ S
ht: t = univ
h_compl.inr
∅ ∈ S
    
Ω: Type u_1
s, t: Set Ω
ht✝: t ∈ S
ht: t = univ
h_compl.inr
tᶜ ∈ Sexact S_apply.1
Goals accomplished! 🐙
  
Ω: Type u_1
s: Set Ω
MeasurableSet s → s ∈ Sintro f hf
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h_Union
⋃ i, f i ∈ S
  
Ω: Type u_1
s: Set Ω
MeasurableSet s → s ∈ Sby_cases h : ∃ n, f n = univ
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∃ n, f n = univ
pos
⋃ i, f i ∈ S
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ¬∃ n, f n = univ
neg
⋃ i, f i ∈ S
  
Ω: Type u_1
s: Set Ω
MeasurableSet s → s ∈ S·
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∃ n, f n = univ
pos
⋃ i, f i ∈ S 
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∃ n, f n = univ
pos
⋃ i, f i ∈ S
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ¬∃ n, f n = univ
neg
⋃ i, f i ∈ Shave : ⋃ i, f i = univ := 
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∃ n, f n = univ
pos
⋃ i, f i ∈ Sby
Goals accomplished! 🐙
      
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∃ n, f n = univ
pos
⋃ i, f i ∈ Sapply iUnion_eq_univ_iff.mpr
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∃ n, f n = univ
∀ (x : Ω), ∃ i, x ∈ f i
      
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∃ n, f n = univ
pos
⋃ i, f i ∈ Sintro x
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∃ n, f n = univ
x: Ω
∃ i, x ∈ f i
      
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∃ n, f n = univ
pos
⋃ i, f i ∈ Srcases h with ⟨n, h⟩
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
x: Ω
n: ℕ
h: f n = univ
intro
∃ i, x ∈ f i
      
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∃ n, f n = univ
pos
⋃ i, f i ∈ Suse n
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
x: Ω
n: ℕ
h: f n = univ
h
x ∈ f n
      
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∃ n, f n = univ
pos
⋃ i, f i ∈ Srw [
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
x: Ω
n: ℕ
h: f n = univ
h
x ∈ f nh
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
x: Ω
n: ℕ
h: f n = univ
h
x ∈ univ]
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
x: Ω
n: ℕ
h: f n = univ
h
x ∈ univ
      
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∃ n, f n = univ
pos
⋃ i, f i ∈ Strivial
Goals accomplished! 🐙
    
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∃ n, f n = univ
pos
⋃ i, f i ∈ Srw [
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∃ n, f n = univ
this: ⋃ i, f i = univ
pos
⋃ i, f i ∈ Sthis
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∃ n, f n = univ
this: ⋃ i, f i = univ
pos
univ ∈ S]
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∃ n, f n = univ
this: ⋃ i, f i = univ
pos
univ ∈ S
    
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∃ n, f n = univ
pos
⋃ i, f i ∈ Sexact S_apply.2
Goals accomplished! 🐙
  
Ω: Type u_1
s: Set Ω
MeasurableSet s → s ∈ Spush_neg at h
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∀ (n : ℕ), f n ≠ univ
neg
⋃ i, f i ∈ S
  
Ω: Type u_1
s: Set Ω
MeasurableSet s → s ∈ Shave : ⋃ i, f i = ∅ := 
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∀ (n : ℕ), f n ≠ univ
neg
⋃ i, f i ∈ Sby
Goals accomplished! 🐙
    
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∀ (n : ℕ), f n ≠ univ
neg
⋃ i, f i ∈ Shave : ∀ n, f n = ∅ := 
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∀ (n : ℕ), f n ≠ univ
⋃ i, f i = ∅by
Goals accomplished! 🐙
      
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∀ (n : ℕ), f n ≠ univ
⋃ i, f i = ∅intro n
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∀ (n : ℕ), f n ≠ univ
n: ℕ
f n = ∅
      
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∀ (n : ℕ), f n ≠ univ
⋃ i, f i = ∅specialize h n
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
n: ℕ
h: f n ≠ univ
f n = ∅
      
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∀ (n : ℕ), f n ≠ univ
⋃ i, f i = ∅cases destruct_S (hf n) with
      
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
n: ℕ
h: f n ≠ univ
x✝: f n = ∅ ∨ f n = univ
f n = ∅| inr _ => 
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
n: ℕ
h: f n ≠ univ
h✝: f n = univ
inr
f n = ∅contradiction
Goals accomplished! 🐙
      
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
n: ℕ
h: f n ≠ univ
x✝: f n = ∅ ∨ f n = univ
f n = ∅| inl _ => 
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
n: ℕ
h: f n ≠ univ
h✝: f n = ∅
inl
f n = ∅assumption
Goals accomplished! 🐙
    
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∀ (n : ℕ), f n ≠ univ
neg
⋃ i, f i ∈ Sexact iUnion_eq_empty.mpr this
Goals accomplished! 🐙
  
Ω: Type u_1
s: Set Ω
MeasurableSet s → s ∈ Srw [
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∀ (n : ℕ), f n ≠ univ
this: ⋃ i, f i = ∅
neg
⋃ i, f i ∈ Sthis
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∀ (n : ℕ), f n ≠ univ
this: ⋃ i, f i = ∅
neg
∅ ∈ S]
Ω: Type u_1
s: Set Ω
f: ℕ → Set Ω
hf: ∀ (n : ℕ), f n ∈ S
h: ∀ (n : ℕ), f n ≠ univ
this: ⋃ i, f i = ∅
neg
∅ ∈ S
  
Ω: Type u_1
s: Set Ω
MeasurableSet s → s ∈ Sexact S_apply.1
Goals accomplished! 🐙

variable [IsProbabilityMeasure μ]

/--
  The trivial σ-algebra and any other σ-algebra are independent.
-/
lemma m_trivial_indep (m₁ : MeasurableSpace Ω) : Indep m₁ m_trivial μ := by
Goals accomplished! 🐙
  
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
Indep m₁ m_trivial μapply (Indep_iff m₁ m_trivial μ).mpr
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2
  
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
Indep m₁ m_trivial μintro t1 t2 _ ht2
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
μ (t1 ∩ t2) = μ t1 * μ t2
  
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
Indep m₁ m_trivial μcases destruct_S (measurableSet_S ht2) with
  
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
x✝: t2 = ∅ ∨ t2 = univ
μ (t1 ∩ t2) = μ t1 * μ t2| inl h =>
    
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = ∅
inl
μ (t1 ∩ t2) = μ t1 * μ t2have : t1 ∩ t2 = ∅ := 
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = ∅
inl
μ (t1 ∩ t2) = μ t1 * μ t2by
Goals accomplished! 🐙
      
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = ∅
inl
μ (t1 ∩ t2) = μ t1 * μ t2rw [
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = ∅
t1 ∩ t2 = ∅h
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = ∅
t1 ∩ ∅ = ∅]
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = ∅
t1 ∩ ∅ = ∅
      
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = ∅
inl
μ (t1 ∩ t2) = μ t1 * μ t2exact inter_empty t1
Goals accomplished! 🐙
    
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = ∅
inl
μ (t1 ∩ t2) = μ t1 * μ t2rw [
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = ∅
this: t1 ∩ t2 = ∅
inl
μ (t1 ∩ t2) = μ t1 * μ t2this,
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = ∅
this: t1 ∩ t2 = ∅
inl
μ ∅ = μ t1 * μ t2 
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = ∅
this: t1 ∩ t2 = ∅
inl
μ (t1 ∩ t2) = μ t1 * μ t2h,
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = ∅
this: t1 ∩ t2 = ∅
inl
μ ∅ = μ t1 * μ ∅ 
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = ∅
this: t1 ∩ t2 = ∅
inl
μ (t1 ∩ t2) = μ t1 * μ t2OuterMeasureClass.measure_empty μ,
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = ∅
this: t1 ∩ t2 = ∅
inl
0 = μ t1 * 0 
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = ∅
this: t1 ∩ t2 = ∅
inl
μ (t1 ∩ t2) = μ t1 * μ t2mul_zero
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = ∅
this: t1 ∩ t2 = ∅
inl
0 = 0]
Goals accomplished! 🐙
  
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
x✝: t2 = ∅ ∨ t2 = univ
μ (t1 ∩ t2) = μ t1 * μ t2| inr h =>
    
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = univ
inr
μ (t1 ∩ t2) = μ t1 * μ t2have : t1 ∩ t2 = t1 := 
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = univ
inr
μ (t1 ∩ t2) = μ t1 * μ t2by
Goals accomplished! 🐙
      
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = univ
inr
μ (t1 ∩ t2) = μ t1 * μ t2rw [
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = univ
t1 ∩ t2 = t1h
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = univ
t1 ∩ univ = t1]
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = univ
t1 ∩ univ = t1
      
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = univ
inr
μ (t1 ∩ t2) = μ t1 * μ t2exact inter_univ t1
Goals accomplished! 🐙
    
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = univ
inr
μ (t1 ∩ t2) = μ t1 * μ t2rw [
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = univ
this: t1 ∩ t2 = t1
inr
μ (t1 ∩ t2) = μ t1 * μ t2this,
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = univ
this: t1 ∩ t2 = t1
inr
μ t1 = μ t1 * μ t2 
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = univ
this: t1 ∩ t2 = t1
inr
μ (t1 ∩ t2) = μ t1 * μ t2h,
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = univ
this: t1 ∩ t2 = t1
inr
μ t1 = μ t1 * μ univ 
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = univ
this: t1 ∩ t2 = t1
inr
μ (t1 ∩ t2) = μ t1 * μ t2measure_univ,
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = univ
this: t1 ∩ t2 = t1
inr
μ t1 = μ t1 * 1 
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = univ
this: t1 ∩ t2 = t1
inr
μ (t1 ∩ t2) = μ t1 * μ t2mul_one
Ω: Type u_1
mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝: IsProbabilityMeasure μ
m₁: MeasurableSpace Ω
t1, t2: Set Ω
a✝: MeasurableSet t1
ht2: MeasurableSet t2
h: t2 = univ
this: t1 ∩ t2 = t1
inr
μ t1 = μ t1]
Goals accomplished! 🐙

/--
  The expectation conditioned to the trivial σ-algebra is equal a.e. to the expectation.
-/
lemma condition_m_trivial {X : Ω → F} (hm₁ : m₁ ≤ mΩ)
    (hf : StronglyMeasurable[m₁] X) [SigmaFinite (μ.trim (m_trivial_le mΩ))] :
    μ [X | m_trivial] =ᵐ[μ] (fun _ ↦ μ[X]) :=
  condexp_indep_eq hm₁ (m_trivial_le mΩ) hf (m_trivial_indep m₁)

/--
  The law of total expectation.
-/
theorem total_expectation_law {X : Ω → F} (hX : Integrable X μ)
    (hm₁ : m₁ ≤ mΩ) [SigmaFinite (μ.trim hm₁)] (hm : StronglyMeasurable[m₁] X) :
     μ[μ[X | m₁]] = μ[X] := by
Goals accomplished! 🐙
  
Ω: Type u_1
F: Type u_2
inst✝⁴: NormedAddCommGroup F
inst✝³: NormedSpace ℝ F
inst✝²: CompleteSpace F
m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝¹: IsProbabilityMeasure μ
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
inst✝: SigmaFinite (μ.trim hm₁)
hm: StronglyMeasurable X
∫ (x : Ω), (μ[X|m₁]) x ∂μ = ∫ (x : Ω), X x ∂μhave μ_univ_neq_0 : μ univ ≠ 0 := (NeZero.ne' (μ univ)).symm
Ω: Type u_1
F: Type u_2
inst✝⁴: NormedAddCommGroup F
inst✝³: NormedSpace ℝ F
inst✝²: CompleteSpace F
m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝¹: IsProbabilityMeasure μ
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
inst✝: SigmaFinite (μ.trim hm₁)
hm: StronglyMeasurable X
μ_univ_neq_0: μ univ ≠ 0
∫ (x : Ω), (μ[X|m₁]) x ∂μ = ∫ (x : Ω), X x ∂μ
  
Ω: Type u_1
F: Type u_2
inst✝⁴: NormedAddCommGroup F
inst✝³: NormedSpace ℝ F
inst✝²: CompleteSpace F
m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝¹: IsProbabilityMeasure μ
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
inst✝: SigmaFinite (μ.trim hm₁)
hm: StronglyMeasurable X
∫ (x : Ω), (μ[X|m₁]) x ∂μ = ∫ (x : Ω), X x ∂μapply constant_ae_eq_imp_eq μ_univ_neq_0
Ω: Type u_1
F: Type u_2
inst✝⁴: NormedAddCommGroup F
inst✝³: NormedSpace ℝ F
inst✝²: CompleteSpace F
m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝¹: IsProbabilityMeasure μ
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
inst✝: SigmaFinite (μ.trim hm₁)
hm: StronglyMeasurable X
μ_univ_neq_0: μ univ ≠ 0
h_ae
(fun x => ∫ (x : Ω), (μ[X|m₁]) x ∂μ) =ᶠ[ae μ] fun x => ∫ (x : Ω), X x ∂μ
  
Ω: Type u_1
F: Type u_2
inst✝⁴: NormedAddCommGroup F
inst✝³: NormedSpace ℝ F
inst✝²: CompleteSpace F
m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝¹: IsProbabilityMeasure μ
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
inst✝: SigmaFinite (μ.trim hm₁)
hm: StronglyMeasurable X
∫ (x : Ω), (μ[X|m₁]) x ∂μ = ∫ (x : Ω), X x ∂μhave tower : μ[X|m_trivial] =ᵐ[μ] μ[μ[X|m₁]|m_trivial] := tower_property hX hm₁ (m_trivial_le m₁)
Ω: Type u_1
F: Type u_2
inst✝⁴: NormedAddCommGroup F
inst✝³: NormedSpace ℝ F
inst✝²: CompleteSpace F
m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝¹: IsProbabilityMeasure μ
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
inst✝: SigmaFinite (μ.trim hm₁)
hm: StronglyMeasurable X
μ_univ_neq_0: μ univ ≠ 0
tower: μ[X|m_trivial] =ᶠ[ae μ] μ[μ[X|m₁]|m_trivial]
h_ae
(fun x => ∫ (x : Ω), (μ[X|m₁]) x ∂μ) =ᶠ[ae μ] fun x => ∫ (x : Ω), X x ∂μ
  
Ω: Type u_1
F: Type u_2
inst✝⁴: NormedAddCommGroup F
inst✝³: NormedSpace ℝ F
inst✝²: CompleteSpace F
m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝¹: IsProbabilityMeasure μ
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
inst✝: SigmaFinite (μ.trim hm₁)
hm: StronglyMeasurable X
∫ (x : Ω), (μ[X|m₁]) x ∂μ = ∫ (x : Ω), X x ∂μhave sMeasurable : StronglyMeasurable[m₁] (μ[X | m₁]) := stronglyMeasurable_condexp
Ω: Type u_1
F: Type u_2
inst✝⁴: NormedAddCommGroup F
inst✝³: NormedSpace ℝ F
inst✝²: CompleteSpace F
m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝¹: IsProbabilityMeasure μ
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
inst✝: SigmaFinite (μ.trim hm₁)
hm: StronglyMeasurable X
μ_univ_neq_0: μ univ ≠ 0
tower: μ[X|m_trivial] =ᶠ[ae μ] μ[μ[X|m₁]|m_trivial]
sMeasurable: StronglyMeasurable (μ[X|m₁])
h_ae
(fun x => ∫ (x : Ω), (μ[X|m₁]) x ∂μ) =ᶠ[ae μ] fun x => ∫ (x : Ω), X x ∂μ
  
Ω: Type u_1
F: Type u_2
inst✝⁴: NormedAddCommGroup F
inst✝³: NormedSpace ℝ F
inst✝²: CompleteSpace F
m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝¹: IsProbabilityMeasure μ
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
inst✝: SigmaFinite (μ.trim hm₁)
hm: StronglyMeasurable X
∫ (x : Ω), (μ[X|m₁]) x ∂μ = ∫ (x : Ω), X x ∂μfilter_upwards [condition_m_trivial hm₁ sMeasurable, condition_m_trivial hm₁ hm, tower]
    with a ha1 ha2 ha3
Ω: Type u_1
F: Type u_2
inst✝⁴: NormedAddCommGroup F
inst✝³: NormedSpace ℝ F
inst✝²: CompleteSpace F
m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝¹: IsProbabilityMeasure μ
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
inst✝: SigmaFinite (μ.trim hm₁)
hm: StronglyMeasurable X
μ_univ_neq_0: μ univ ≠ 0
tower: μ[X|m_trivial] =ᶠ[ae μ] μ[μ[X|m₁]|m_trivial]
sMeasurable: StronglyMeasurable (μ[X|m₁])
a: Ω
ha1: (μ[μ[X|m₁]|m_trivial]) a = ∫ (x : Ω), (μ[X|m₁]) x ∂μ
ha2: (μ[X|m_trivial]) a = ∫ (x : Ω), X x ∂μ
ha3: (μ[X|m_trivial]) a = (μ[μ[X|m₁]|m_trivial]) a
h
∫ (x : Ω), (μ[X|m₁]) x ∂μ = ∫ (x : Ω), X x ∂μ
  
Ω: Type u_1
F: Type u_2
inst✝⁴: NormedAddCommGroup F
inst✝³: NormedSpace ℝ F
inst✝²: CompleteSpace F
m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝¹: IsProbabilityMeasure μ
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
inst✝: SigmaFinite (μ.trim hm₁)
hm: StronglyMeasurable X
∫ (x : Ω), (μ[X|m₁]) x ∂μ = ∫ (x : Ω), X x ∂μrw [
Ω: Type u_1
F: Type u_2
inst✝⁴: NormedAddCommGroup F
inst✝³: NormedSpace ℝ F
inst✝²: CompleteSpace F
m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝¹: IsProbabilityMeasure μ
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
inst✝: SigmaFinite (μ.trim hm₁)
hm: StronglyMeasurable X
μ_univ_neq_0: μ univ ≠ 0
tower: μ[X|m_trivial] =ᶠ[ae μ] μ[μ[X|m₁]|m_trivial]
sMeasurable: StronglyMeasurable (μ[X|m₁])
a: Ω
ha1: (μ[μ[X|m₁]|m_trivial]) a = ∫ (x : Ω), (μ[X|m₁]) x ∂μ
ha2: (μ[X|m_trivial]) a = ∫ (x : Ω), X x ∂μ
ha3: (μ[X|m_trivial]) a = (μ[μ[X|m₁]|m_trivial]) a
h
∫ (x : Ω), (μ[X|m₁]) x ∂μ = ∫ (x : Ω), X x ∂μ← ha1,
Ω: Type u_1
F: Type u_2
inst✝⁴: NormedAddCommGroup F
inst✝³: NormedSpace ℝ F
inst✝²: CompleteSpace F
m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝¹: IsProbabilityMeasure μ
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
inst✝: SigmaFinite (μ.trim hm₁)
hm: StronglyMeasurable X
μ_univ_neq_0: μ univ ≠ 0
tower: μ[X|m_trivial] =ᶠ[ae μ] μ[μ[X|m₁]|m_trivial]
sMeasurable: StronglyMeasurable (μ[X|m₁])
a: Ω
ha1: (μ[μ[X|m₁]|m_trivial]) a = ∫ (x : Ω), (μ[X|m₁]) x ∂μ
ha2: (μ[X|m_trivial]) a = ∫ (x : Ω), X x ∂μ
ha3: (μ[X|m_trivial]) a = (μ[μ[X|m₁]|m_trivial]) a
h
(μ[μ[X|m₁]|m_trivial]) a = ∫ (x : Ω), X x ∂μ 
Ω: Type u_1
F: Type u_2
inst✝⁴: NormedAddCommGroup F
inst✝³: NormedSpace ℝ F
inst✝²: CompleteSpace F
m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝¹: IsProbabilityMeasure μ
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
inst✝: SigmaFinite (μ.trim hm₁)
hm: StronglyMeasurable X
μ_univ_neq_0: μ univ ≠ 0
tower: μ[X|m_trivial] =ᶠ[ae μ] μ[μ[X|m₁]|m_trivial]
sMeasurable: StronglyMeasurable (μ[X|m₁])
a: Ω
ha1: (μ[μ[X|m₁]|m_trivial]) a = ∫ (x : Ω), (μ[X|m₁]) x ∂μ
ha2: (μ[X|m_trivial]) a = ∫ (x : Ω), X x ∂μ
ha3: (μ[X|m_trivial]) a = (μ[μ[X|m₁]|m_trivial]) a
h
∫ (x : Ω), (μ[X|m₁]) x ∂μ = ∫ (x : Ω), X x ∂μ← ha3,
Ω: Type u_1
F: Type u_2
inst✝⁴: NormedAddCommGroup F
inst✝³: NormedSpace ℝ F
inst✝²: CompleteSpace F
m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝¹: IsProbabilityMeasure μ
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
inst✝: SigmaFinite (μ.trim hm₁)
hm: StronglyMeasurable X
μ_univ_neq_0: μ univ ≠ 0
tower: μ[X|m_trivial] =ᶠ[ae μ] μ[μ[X|m₁]|m_trivial]
sMeasurable: StronglyMeasurable (μ[X|m₁])
a: Ω
ha1: (μ[μ[X|m₁]|m_trivial]) a = ∫ (x : Ω), (μ[X|m₁]) x ∂μ
ha2: (μ[X|m_trivial]) a = ∫ (x : Ω), X x ∂μ
ha3: (μ[X|m_trivial]) a = (μ[μ[X|m₁]|m_trivial]) a
h
(μ[X|m_trivial]) a = ∫ (x : Ω), X x ∂μ 
Ω: Type u_1
F: Type u_2
inst✝⁴: NormedAddCommGroup F
inst✝³: NormedSpace ℝ F
inst✝²: CompleteSpace F
m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝¹: IsProbabilityMeasure μ
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
inst✝: SigmaFinite (μ.trim hm₁)
hm: StronglyMeasurable X
μ_univ_neq_0: μ univ ≠ 0
tower: μ[X|m_trivial] =ᶠ[ae μ] μ[μ[X|m₁]|m_trivial]
sMeasurable: StronglyMeasurable (μ[X|m₁])
a: Ω
ha1: (μ[μ[X|m₁]|m_trivial]) a = ∫ (x : Ω), (μ[X|m₁]) x ∂μ
ha2: (μ[X|m_trivial]) a = ∫ (x : Ω), X x ∂μ
ha3: (μ[X|m_trivial]) a = (μ[μ[X|m₁]|m_trivial]) a
h
∫ (x : Ω), (μ[X|m₁]) x ∂μ = ∫ (x : Ω), X x ∂μha2
Ω: Type u_1
F: Type u_2
inst✝⁴: NormedAddCommGroup F
inst✝³: NormedSpace ℝ F
inst✝²: CompleteSpace F
m₁, mΩ: MeasurableSpace Ω
μ: Measure Ω
inst✝¹: IsProbabilityMeasure μ
X: Ω → F
hX: Integrable X μ
hm₁: m₁ ≤ mΩ
inst✝: SigmaFinite (μ.trim hm₁)
hm: StronglyMeasurable X
μ_univ_neq_0: μ univ ≠ 0
tower: μ[X|m_trivial] =ᶠ[ae μ] μ[μ[X|m₁]|m_trivial]
sMeasurable: StronglyMeasurable (μ[X|m₁])
a: Ω
ha1: (μ[μ[X|m₁]|m_trivial]) a = ∫ (x : Ω), (μ[X|m₁]) x ∂μ
ha2: (μ[X|m_trivial]) a = ∫ (x : Ω), X x ∂μ
ha3: (μ[X|m_trivial]) a = (μ[μ[X|m₁]|m_trivial]) a
h
∫ (x : Ω), X x ∂μ = ∫ (x : Ω), X x ∂μ]
Goals accomplished! 🐙

end ExpTotal

namespace MeasureTheory

variable {Ω F : Type*} [mΩ : MeasurableSpace Ω] [MeasurableSpace F]

/--
  The σ-algebra generated by a r.v.
-/
def gen_sigma (Y : Ω → F) := MeasurableSpace.generateFrom {S | ∃ (A : Set F), MeasurableSet A ∧ Y⁻¹' A = S}

/--
  The σ-algebra generated by a r.v is less or equal than the encompassing σ-algebra.
-/
lemma sigma_generated_le {Y : Ω → F} (hY : Measurable Y) :
    gen_sigma Y ≤ mΩ := by
Goals accomplished! 🐙
  
Ω: Type u_1
F: Type u_2
mΩ: MeasurableSpace Ω
inst✝: MeasurableSpace F
Y: Ω → F
hY: Measurable Y
gen_sigma Y ≤ mΩapply MeasurableSpace.generateFrom_le
Ω: Type u_1
F: Type u_2
mΩ: MeasurableSpace Ω
inst✝: MeasurableSpace F
Y: Ω → F
hY: Measurable Y
h
∀ t ∈ {S | ∃ A, MeasurableSet A ∧ Y ⁻¹' A = S}, MeasurableSet t
  
Ω: Type u_1
F: Type u_2
mΩ: MeasurableSpace Ω
inst✝: MeasurableSpace F
Y: Ω → F
hY: Measurable Y
gen_sigma Y ≤ mΩintro t ht
Ω: Type u_1
F: Type u_2
mΩ: MeasurableSpace Ω
inst✝: MeasurableSpace F
Y: Ω → F
hY: Measurable Y
t: Set Ω
ht: t ∈ {S | ∃ A, MeasurableSet A ∧ Y ⁻¹' A = S}
h
MeasurableSet t
  
Ω: Type u_1
F: Type u_2
mΩ: MeasurableSpace Ω
inst✝: MeasurableSpace F
Y: Ω → F
hY: Measurable Y
gen_sigma Y ≤ mΩrcases ht with ⟨A, hA, ht⟩
Ω: Type u_1
F: Type u_2
mΩ: MeasurableSpace Ω
inst✝: MeasurableSpace F
Y: Ω → F
hY: Measurable Y
t: Set Ω
A: Set F
hA: MeasurableSet A
ht: Y ⁻¹' A = t
h.intro.intro
MeasurableSet t
  
Ω: Type u_1
F: Type u_2
mΩ: MeasurableSpace Ω
inst✝: MeasurableSpace F
Y: Ω → F
hY: Measurable Y
gen_sigma Y ≤ mΩrw [
Ω: Type u_1
F: Type u_2
mΩ: MeasurableSpace Ω
inst✝: MeasurableSpace F
Y: Ω → F
hY: Measurable Y
t: Set Ω
A: Set F
hA: MeasurableSet A
ht: Y ⁻¹' A = t
h.intro.intro
MeasurableSet t← ht
Ω: Type u_1
F: Type u_2
mΩ: MeasurableSpace Ω
inst✝: MeasurableSpace F
Y: Ω → F
hY: Measurable Y
t: Set Ω
A: Set F
hA: MeasurableSet A
ht: Y ⁻¹' A = t
h.intro.intro
MeasurableSet (Y ⁻¹' A)]
Ω: Type u_1
F: Type u_2
mΩ: MeasurableSpace Ω
inst✝: MeasurableSpace F
Y: Ω → F
hY: Measurable Y
t: Set Ω
A: Set F
hA: MeasurableSet A
ht: Y ⁻¹' A = t
h.intro.intro
MeasurableSet (Y ⁻¹' A)
  
Ω: Type u_1
F: Type u_2
mΩ: MeasurableSpace Ω
inst✝: MeasurableSpace F
Y: Ω → F
hY: Measurable Y
gen_sigma Y ≤ mΩexact hY hA
Goals accomplished! 🐙

/--
  The condition probability.
-/
noncomputable def Measure.condProb (μ : Measure Ω) (A : Set Ω) (Y : Ω → F) :=
  μ[A.indicator (fun (_ : Ω) ↦ (1 : ℝ)) | gen_sigma Y]

end MeasureTheory

namespace TotalProba

open ENNReal

variable {Ω F : Type*} [MeasurableSpace F]
{m2 m₁ mΩ : MeasurableSpace Ω} {μ : Measure Ω} {X Y : Ω → F} (hY : Measurable Y)

/--
  The law of total probability using the law of total expectation.
-/
theorem total_probability_law
    [IsProbabilityMeasure μ] {A : Set Ω} (hA : MeasurableSet[gen_sigma Y] A)
    [SigmaFinite (μ.trim (sigma_generated_le hY))] :
    (μ A).toReal = μ[μ.condProb A Y] := by
Goals accomplished! 🐙
  
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
(μ A).toReal = ∫ (x : Ω), μ.condProb A Y x ∂μhave hAmΩ : MeasurableSet A := (sigma_generated_le hY) A hA
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
(μ A).toReal = ∫ (x : Ω), μ.condProb A Y x ∂μ
  
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
(μ A).toReal = ∫ (x : Ω), μ.condProb A Y x ∂μunfold Measure.condProb
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
(μ A).toReal = ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ
  
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
(μ A).toReal = ∫ (x : Ω), μ.condProb A Y x ∂μhave total_exp : ∫ x, (μ[A.indicator fun _ ↦ (1 : ℝ)|gen_sigma Y]) x ∂μ
      = μ[A.indicator (fun x ↦ 1)] := 
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
(μ A).toReal = ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μby
Goals accomplished! 🐙
    
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
(μ A).toReal = ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μhave hI : HasFiniteIntegral (A.indicator (fun (_ : Ω) ↦ (1 : ℝ))) μ := 
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μby
Goals accomplished! 🐙
      
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μunfold HasFiniteIntegral
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
∫⁻ (a : Ω), ↑‖A.indicator (fun x => 1) a‖₊ ∂μ < ⊤
      
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μhave rmv_norm : ∀ a, ‖A.indicator (fun (_ : Ω) ↦ (1 : ℝ)) a‖₊ =
          A.indicator (fun (_ : Ω) ↦ (1 : ℝ≥0∞)) a := 
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
∫⁻ (a : Ω), ↑‖A.indicator (fun x => 1) a‖₊ ∂μ < ⊤by
Goals accomplished! 🐙
        
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
∫⁻ (a : Ω), ↑‖A.indicator (fun x => 1) a‖₊ ∂μ < ⊤intro a
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
↑‖A.indicator (fun x => 1) a‖₊ = A.indicator (fun x => 1) a
        
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
∫⁻ (a : Ω), ↑‖A.indicator (fun x => 1) a‖₊ ∂μ < ⊤by_cases ha : a ∈ A
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
ha: a ∈ A
pos
↑‖A.indicator (fun x => 1) a‖₊ = A.indicator (fun x => 1) a
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
ha: a ∉ A
neg
↑‖A.indicator (fun x => 1) a‖₊ = A.indicator (fun x => 1) a
        
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
∫⁻ (a : Ω), ↑‖A.indicator (fun x => 1) a‖₊ ∂μ < ⊤·
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
ha: a ∈ A
pos
↑‖A.indicator (fun x => 1) a‖₊ = A.indicator (fun x => 1) a 
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
ha: a ∈ A
pos
↑‖A.indicator (fun x => 1) a‖₊ = A.indicator (fun x => 1) a
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
ha: a ∉ A
neg
↑‖A.indicator (fun x => 1) a‖₊ = A.indicator (fun x => 1) arw [
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
ha: a ∈ A
pos
↑‖A.indicator (fun x => 1) a‖₊ = A.indicator (fun x => 1) aindicator_of_mem ha fun _ ↦ 1,
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
ha: a ∈ A
pos
↑‖1‖₊ = A.indicator (fun x => 1) a 
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
ha: a ∈ A
pos
↑‖A.indicator (fun x => 1) a‖₊ = A.indicator (fun x => 1) aindicator_of_mem ha fun _ ↦ 1,
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
ha: a ∈ A
pos
↑‖1‖₊ = 1 
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
ha: a ∈ A
pos
↑‖A.indicator (fun x => 1) a‖₊ = A.indicator (fun x => 1) annnorm_one
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
ha: a ∈ A
pos
↑1 = 1]
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
ha: a ∈ A
pos
↑1 = 1
          
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
ha: a ∈ A
pos
↑‖A.indicator (fun x => 1) a‖₊ = A.indicator (fun x => 1) arfl
Goals accomplished! 🐙
        
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
∫⁻ (a : Ω), ↑‖A.indicator (fun x => 1) a‖₊ ∂μ < ⊤rw [
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
ha: a ∉ A
neg
↑‖A.indicator (fun x => 1) a‖₊ = A.indicator (fun x => 1) aindicator_of_not_mem ha fun _ ↦ 1,
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
ha: a ∉ A
neg
↑‖0‖₊ = A.indicator (fun x => 1) a 
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
ha: a ∉ A
neg
↑‖A.indicator (fun x => 1) a‖₊ = A.indicator (fun x => 1) aindicator_of_not_mem ha fun _ ↦ 1,
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
ha: a ∉ A
neg
↑‖0‖₊ = 0 
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
ha: a ∉ A
neg
↑‖A.indicator (fun x => 1) a‖₊ = A.indicator (fun x => 1) annnorm_zero
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
ha: a ∉ A
neg
↑0 = 0]
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
a: Ω
ha: a ∉ A
neg
↑0 = 0
        
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
∫⁻ (a : Ω), ↑‖A.indicator (fun x => 1) a‖₊ ∂μ < ⊤rfl
Goals accomplished! 🐙
      
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μsimp_rw [
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
rmv_norm: ∀ (a : Ω), ↑‖A.indicator (fun x => 1) a‖₊ = A.indicator (fun x => 1) a
∫⁻ (a : Ω), ↑‖A.indicator (fun x => 1) a‖₊ ∂μ < ⊤rmv_norm
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
rmv_norm: ∀ (a : Ω), ↑‖A.indicator (fun x => 1) a‖₊ = A.indicator (fun x => 1) a
∫⁻ (a : Ω), A.indicator (fun x => 1) a ∂μ < ⊤]
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
rmv_norm: ∀ (a : Ω), ↑‖A.indicator (fun x => 1) a‖₊ = A.indicator (fun x => 1) a
∫⁻ (a : Ω), A.indicator (fun x => 1) a ∂μ < ⊤
      
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μcalc ∫⁻ a, A.indicator 1 a ∂μ = ∫⁻ _ in A, 1 ∂μ :=
        lintegral_indicator hAmΩ 1
      _ = μ A := setLIntegral_one A
      _ < ⊤ := measure_lt_top μ A
Goals accomplished! 🐙
    
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
(μ A).toReal = ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μhave hAE : StronglyMeasurable[gen_sigma Y] (A.indicator (fun (_ : Ω) ↦ (1 : ℝ))) :=
      StronglyMeasurable.indicator stronglyMeasurable_const hA
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
hI: HasFiniteIntegral (A.indicator fun x => 1) μ
hAE: StronglyMeasurable (A.indicator fun x => 1)
∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
    
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
(μ A).toReal = ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μhave hAEmΩ : AEStronglyMeasurable (A.indicator (fun (_ : Ω) ↦ (1 : ℝ))) μ := 
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
hI: HasFiniteIntegral (A.indicator fun x => 1) μ
hAE: StronglyMeasurable (A.indicator fun x => 1)
∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μby
Goals accomplished! 🐙
      
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
hI: HasFiniteIntegral (A.indicator fun x => 1) μ
hAE: StronglyMeasurable (A.indicator fun x => 1)
∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μsuffices StronglyMeasurable (A.indicator (fun (_ : Ω) ↦ (1 : ℝ))) by
        
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
hI: HasFiniteIntegral (A.indicator fun x => 1) μ
hAE: StronglyMeasurable (A.indicator fun x => 1)
AEStronglyMeasurable (A.indicator fun x => 1) μexact StronglyMeasurable.aestronglyMeasurable this
Goals accomplished! 🐙
      
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
hI: HasFiniteIntegral (A.indicator fun x => 1) μ
hAE: StronglyMeasurable (A.indicator fun x => 1)
∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μexact StronglyMeasurable.mono hAE (sigma_generated_le hY)
Goals accomplished! 🐙
    
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
(μ A).toReal = ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μexact ExpTotal.total_expectation_law ⟨hAEmΩ, hI⟩ (sigma_generated_le hY) hAE
Goals accomplished! 🐙
  
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
(μ A).toReal = ∫ (x : Ω), μ.condProb A Y x ∂μrw [
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
(μ A).toReal = ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μtotal_exp
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
(μ A).toReal = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ]
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
(μ A).toReal = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
  
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
(μ A).toReal = ∫ (x : Ω), μ.condProb A Y x ∂μhave integral_A : ∫ a, A.indicator (fun x ↦ 1) a ∂μ = (μ A).toReal := 
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
(μ A).toReal = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μby
Goals accomplished! 🐙
    
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
(μ A).toReal = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μrw [
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
∫ (a : Ω), A.indicator (fun x => 1) a ∂μ = (μ A).toRealintegral_indicator hAmΩ
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
∫ (x : Ω) in A, 1 ∂μ = (μ A).toReal]
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
∫ (x : Ω) in A, 1 ∂μ = (μ A).toReal
    
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
(μ A).toReal = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μhave ae_pos : 0 ≤ᵐ[μ.restrict A] (fun _ ↦ (1 : ℝ)) := 
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
∫ (x : Ω) in A, 1 ∂μ = (μ A).toRealby
Goals accomplished! 🐙
      
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
∫ (x : Ω) in A, 1 ∂μ = (μ A).toRealsuffices 0 ≤ (fun (_ : Ω) ↦ (1 : ℝ)) by 
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
0 ≤ᶠ[ae (μ.restrict A)] fun x => 1exact ae_of_all (μ.restrict A) this
Goals accomplished! 🐙
      
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
∫ (x : Ω) in A, 1 ∂μ = (μ A).toRealintro _
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
i✝: Ω
0 i✝ ≤ (fun x => 1) i✝
      
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
∫ (x : Ω) in A, 1 ∂μ = (μ A).toRealsimp only [Pi.zero_apply, zero_le_one]
Goals accomplished! 🐙
    
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
(μ A).toReal = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μrw [
      
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
ae_pos: 0 ≤ᶠ[ae (μ.restrict A)] fun x => 1
∫ (x : Ω) in A, 1 ∂μ = (μ A).toRealintegral_eq_lintegral_of_nonneg_ae ae_pos aestronglyMeasurable_const,
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
ae_pos: 0 ≤ᶠ[ae (μ.restrict A)] fun x => 1
(∫⁻ (a : Ω) in A, ENNReal.ofReal 1 ∂μ).toReal = (μ A).toReal
      
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
ae_pos: 0 ≤ᶠ[ae (μ.restrict A)] fun x => 1
∫ (x : Ω) in A, 1 ∂μ = (μ A).toRealofReal_one,
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
ae_pos: 0 ≤ᶠ[ae (μ.restrict A)] fun x => 1
(∫⁻ (a : Ω) in A, 1 ∂μ).toReal = (μ A).toReal 
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
ae_pos: 0 ≤ᶠ[ae (μ.restrict A)] fun x => 1
∫ (x : Ω) in A, 1 ∂μ = (μ A).toRealsetLIntegral_one A
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
ae_pos: 0 ≤ᶠ[ae (μ.restrict A)] fun x => 1
(μ A).toReal = (μ A).toReal
    
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
ae_pos: 0 ≤ᶠ[ae (μ.restrict A)] fun x => 1
∫ (x : Ω) in A, 1 ∂μ = (μ A).toReal]
Goals accomplished! 🐙
  
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
(μ A).toReal = ∫ (x : Ω), μ.condProb A Y x ∂μrw [
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
integral_A: ∫ (a : Ω), A.indicator (fun x => 1) a ∂μ = (μ A).toReal
(μ A).toReal = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μintegral_A
Ω: Type u_1
F: Type u_2
inst✝²: MeasurableSpace F
mΩ: MeasurableSpace Ω
μ: Measure Ω
Y: Ω → F
hY: Measurable Y
inst✝¹: IsProbabilityMeasure μ
A: Set Ω
hA: MeasurableSet A
inst✝: SigmaFinite (μ.trim ⋯)
hAmΩ: MeasurableSet A
total_exp: ∫ (x : Ω), (μ[A.indicator fun x => 1|gen_sigma Y]) x ∂μ = ∫ (x : Ω), A.indicator (fun x => 1) x ∂μ
integral_A: ∫ (a : Ω), A.indicator (fun x => 1) a ∂μ = (μ A).toReal
(μ A).toReal = (μ A).toReal]
Goals accomplished! 🐙

end TotalProba

#min_imports
import Mathlib.Data.Real.StarOrdered
import Mathlib.Order.CompletePartialOrder
import Mathlib.Probability.ConditionalExpectation
import Mathlib.Probability.Kernel.Disintegration.StandardBorel