awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
pos :
  ∀ (hfm : StronglyMeasurable f),
    (if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯) =ᶠ[ae μ]
      (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
neg :
  ∀ (hfm : ¬StronglyMeasurable f),
    (if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯) =ᶠ[ae μ]
      (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
⊢ (if StronglyMeasurable f then f
    else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯) =ᶠ[ae μ]
    (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)

Tactic:
by_cases hfm : StronglyMeasurable[m] f

Premises used: MeasureTheory.StronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
hfm : StronglyMeasurable f
pos : f =ᶠ[ae μ] (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
⊢ (if StronglyMeasurable f then f
    else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯) =ᶠ[ae μ]
    (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)

Tactic:
rw [if_pos hfm]

Premises used: if_pos
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
hfm : StronglyMeasurable f
⊢ f =ᶠ[ae μ] (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)

Tactic:
(condExpL1_of_aestronglyMeasurable' hfm.aestronglyMeasurable hfi).symm

Premises used: MeasureTheory.condExpL1_of_aestronglyMeasurable', MeasureTheory.StronglyMeasurable.aestronglyMeasurable, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
hfm : StronglyMeasurable f
⊢ f =ᶠ[ae μ] (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)

Tactic:
exact (condExpL1_of_aestronglyMeasurable' hfm.aestronglyMeasurable hfi).symm

Premises used: MeasureTheory.condExpL1_of_aestronglyMeasurable', MeasureTheory.StronglyMeasurable.aestronglyMeasurable, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
hfm : ¬StronglyMeasurable f
neg :
  AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯ =ᶠ[ae μ]
    (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)
⊢ (if StronglyMeasurable f then f
    else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯) =ᶠ[ae μ]
    (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)

Tactic:
rw [if_neg hfm]

Premises used: if_neg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
hfm : ¬StronglyMeasurable f
⊢ AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯ =ᶠ[ae μ]
    (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)

Tactic:
aestronglyMeasurable_condExpL1.ae_eq_mk.symm

Premises used: MeasureTheory.aestronglyMeasurable_condExpL1, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : Integrable f μ
hfm : ¬StronglyMeasurable f
⊢ AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯ =ᶠ[ae μ]
    (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)

Tactic:
exact aestronglyMeasurable_condExpL1.ae_eq_mk.symm

Premises used: MeasureTheory.aestronglyMeasurable_condExpL1, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : ¬Integrable f μ
neg : EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 (↑(↑0 : α →ₘ[μ] E) : α → E)
⊢ (if Integrable f μ then
      if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯
    else 0) =ᶠ[ae μ]
    (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E)

Tactic:
rw [if_neg hfi, condExpL1_undef hfi]

Premises used: MeasureTheory.condExpL1_undef, if_neg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : ¬Integrable f μ
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 (↑(↑0 : α →ₘ[μ] E) : α → E)

Tactic:
(coeFn_zero _ _ _).symm

Premises used: MeasureTheory.Lp.coeFn_zero, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
f : α → E
hfi : ¬Integrable f μ
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 (↑(↑0 : α →ₘ[μ] E) : α → E)

Tactic:
exact (coeFn_zero _ _ _).symm

Premises used: MeasureTheory.Lp.coeFn_zero, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
inst_3 : SigmaFinite (μ.trim hm)
hf : Integrable f μ
⊢ μ[f | m] =ᶠ[ae μ]
    (↑(↑((condExpL1CLM E hm μ : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 μ)) (Integrable.toL1 f hf)) : α →ₘ[μ] E) : α → E)

Tactic:
(condExp_ae_eq_condExpL1 hm f).trans (Eventually.of_forall fun x => ?_)

Premises used: Filter.EventuallyEq.trans, Filter.Eventually.of_forall, MeasureTheory.condExp_ae_eq_condExpL1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
inst_3 : SigmaFinite (μ.trim hm)
hf : Integrable f μ
refine :
  ∀ (x : α),
    (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) x =
      (↑(↑((condExpL1CLM E hm μ : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 μ)) (Integrable.toL1 f hf)) : α →ₘ[μ] E) : α → E) x
⊢ μ[f | m] =ᶠ[ae μ]
    (↑(↑((condExpL1CLM E hm μ : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 μ)) (Integrable.toL1 f hf)) : α →ₘ[μ] E) : α → E)

Tactic:
refine (condExp_ae_eq_condExpL1 hm f).trans (Eventually.of_forall fun x => ?_)

Premises used: Filter.EventuallyEq.trans, Filter.Eventually.of_forall, MeasureTheory.condExp_ae_eq_condExpL1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
inst_3 : SigmaFinite (μ.trim hm)
hf : Integrable f μ
x : α
rw rw₁ :
  Eq.{u_3 + 1} (α := E)
    ((↑(↑((condExpL1CLM E hm μ : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 μ)) (Integrable.toL1 f hf)) : α →ₘ[μ] E) : α → E) x)
    ((↑(↑((condExpL1CLM E hm μ : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 μ)) (Integrable.toL1 f hf)) : α →ₘ[μ] E) : α → E) x)
⊢ (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) x =
    (↑(↑((condExpL1CLM E hm μ : (a : ↥(Lp E 1 μ)) → ↥(Lp E 1 μ)) (Integrable.toL1 f hf)) : α →ₘ[μ] E) : α → E) x

Tactic:
rw [condExpL1_eq hf]

Premises used: MeasureTheory.condExpL1_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hf : ¬Integrable f μ
pos : ∀ (hm : m ≤ m₀), μ[f | m] = 0
neg : ∀ (hm : ¬m ≤ m₀), μ[f | m] = 0
⊢ μ[f | m] = 0

Tactic:
by_cases hm : m ≤ m₀
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hf : ¬Integrable f μ
hm : ¬m ≤ m₀
neg neg₁ : Eq (α := α → E) 0 0
⊢ μ[f | m] = 0

Tactic:
rw [condExp_of_not_le hm]

Premises used: MeasureTheory.condExp_of_not_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hf : ¬Integrable f μ
hm : m ≤ m₀
pos : ∀ (hμm : SigmaFinite (μ.trim hm)), μ[f | m] = 0
neg : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), μ[f | m] = 0
⊢ μ[f | m] = 0

Tactic:
by_cases hμm : SigmaFinite (μ.trim hm)

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hf : ¬Integrable f μ
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
neg neg₁ : Eq (α := α → E) 0 0
⊢ μ[f | m] = 0

Tactic:
rw [condExp_of_not_sigmaFinite hm hμm]

Premises used: MeasureTheory.condExp_of_not_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hf : ¬Integrable f μ
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
pos :
  (if Integrable f μ then
      if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯
    else 0) =
    0
pos₁ pos₂ : Eq (α := α → E) 0 0
⊢ μ[f | m] = 0

Tactic:
rw [condExp_of_sigmaFinite, if_neg hf]

Premises used: MeasureTheory.condExp_of_sigmaFinite, if_neg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
pos : ∀ (hm : m ≤ m₀), Eq (α := α → E) μ[0 | m] 0
neg : ∀ (hm : ¬m ≤ m₀), Eq (α := α → E) μ[0 | m] 0
⊢ Eq (α := α → E) μ[0 | m] 0

Tactic:
by_cases hm : m ≤ m₀
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : ¬m ≤ m₀
neg neg₁ : Eq (α := α → E) 0 0
⊢ Eq (α := α → E) μ[0 | m] 0

Tactic:
rw [condExp_of_not_le hm]

Premises used: MeasureTheory.condExp_of_not_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
pos : ∀ (hμm : SigmaFinite (μ.trim hm)), Eq (α := α → E) μ[0 | m] 0
neg : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), Eq (α := α → E) μ[0 | m] 0
⊢ Eq (α := α → E) μ[0 | m] 0

Tactic:
by_cases hμm : SigmaFinite (μ.trim hm)

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
neg neg₁ : Eq (α := α → E) 0 0
⊢ Eq (α := α → E) μ[0 | m] 0

Tactic:
rw [condExp_of_not_sigmaFinite hm hμm]

Premises used: MeasureTheory.condExp_of_not_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ Eq (α := α → E) μ[0 | m] 0

Tactic:
condExp_of_stronglyMeasurable hm stronglyMeasurable_zero (integrable_zero _ _ _)

Premises used: MeasureTheory.condExp_of_stronglyMeasurable, MeasureTheory.integrable_zero, MeasureTheory.stronglyMeasurable_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ Eq (α := α → E) μ[0 | m] 0

Tactic:
exact condExp_of_stronglyMeasurable hm stronglyMeasurable_zero (integrable_zero _ _ _)

Premises used: MeasureTheory.condExp_of_stronglyMeasurable, MeasureTheory.stronglyMeasurable_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
pos : ∀ (hm : m ≤ m₀), StronglyMeasurable μ[f | m]
neg : ∀ (hm : ¬m ≤ m₀), StronglyMeasurable μ[f | m]
⊢ StronglyMeasurable μ[f | m]

Tactic:
by_cases hm : m ≤ m₀
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : ¬m ≤ m₀
neg : StronglyMeasurable.{u_1, u_3} (α := α) (β := E) 0
⊢ StronglyMeasurable μ[f | m]

Tactic:
rw [condExp_of_not_le hm]

Premises used: MeasureTheory.condExp_of_not_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : ¬m ≤ m₀
⊢ StronglyMeasurable.{u_1, u_3} (α := α) (β := E) 0

Tactic:
stronglyMeasurable_zero

Premises used: MeasureTheory.stronglyMeasurable_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : ¬m ≤ m₀
⊢ StronglyMeasurable.{u_1, u_3} (α := α) (β := E) 0

Tactic:
exact stronglyMeasurable_zero

Premises used: MeasureTheory.stronglyMeasurable_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
pos : ∀ (hμm : SigmaFinite (μ.trim hm)), StronglyMeasurable μ[f | m]
neg : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), StronglyMeasurable μ[f | m]
⊢ StronglyMeasurable μ[f | m]

Tactic:
by_cases hμm : SigmaFinite (μ.trim hm)

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
neg : StronglyMeasurable.{u_1, u_3} (α := α) (β := E) 0
⊢ StronglyMeasurable μ[f | m]

Tactic:
rw [condExp_of_not_sigmaFinite hm hμm]

Premises used: MeasureTheory.condExp_of_not_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ StronglyMeasurable.{u_1, u_3} (α := α) (β := E) 0

Tactic:
stronglyMeasurable_zero

Premises used: MeasureTheory.stronglyMeasurable_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ StronglyMeasurable.{u_1, u_3} (α := α) (β := E) 0

Tactic:
exact stronglyMeasurable_zero

Premises used: MeasureTheory.stronglyMeasurable_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
pos :
  StronglyMeasurable
    (if Integrable f μ then
      if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯
    else 0)
⊢ StronglyMeasurable μ[f | m]

Tactic:
rw [condExp_of_sigmaFinite hm]

Premises used: MeasureTheory.condExp_of_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
pos : ∀ (hfi : Integrable f μ) (hfm : StronglyMeasurable f), StronglyMeasurable f
neg :
  ∀ (hfi : Integrable f μ) (hfm : ¬StronglyMeasurable f),
    StronglyMeasurable
      (AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯)
neg₁ : ∀ (hfi : ¬Integrable f μ), StronglyMeasurable.{u_1, u_3} (α := α) (β := E) 0
⊢ StronglyMeasurable
    (if Integrable f μ then
      if StronglyMeasurable f then f
      else AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯
    else 0)

Tactic:
split_ifs with hfi hfm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hfm : StronglyMeasurable f
⊢ StronglyMeasurable f

Tactic:
hfm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hfm : StronglyMeasurable f
⊢ StronglyMeasurable f

Tactic:
exact hfm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hfm : ¬StronglyMeasurable f
⊢ StronglyMeasurable
    (AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯)

Tactic:
aestronglyMeasurable_condExpL1.stronglyMeasurable_mk

Premises used: MeasureTheory.aestronglyMeasurable_condExpL1, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hfi : Integrable f μ
hfm : ¬StronglyMeasurable f
⊢ StronglyMeasurable
    (AEStronglyMeasurable.mk (m := m) (m₀ := m₀) (μ := μ) (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) ⋯)

Tactic:
exact aestronglyMeasurable_condExpL1.stronglyMeasurable_mk

Premises used: MeasureTheory.aestronglyMeasurable_condExpL1, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hfi : ¬Integrable f μ
⊢ StronglyMeasurable.{u_1, u_3} (α := α) (β := E) 0

Tactic:
stronglyMeasurable_zero

Premises used: MeasureTheory.stronglyMeasurable_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
hfi : ¬Integrable f μ
⊢ StronglyMeasurable.{u_1, u_3} (α := α) (β := E) 0

Tactic:
exact stronglyMeasurable_zero

Premises used: MeasureTheory.stronglyMeasurable_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
h : f =ᶠ[ae μ] g
pos : ∀ (hm : m ≤ m₀), μ[f | m] =ᶠ[ae μ] μ[g | m]
neg : ∀ (hm : ¬m ≤ m₀), μ[f | m] =ᶠ[ae μ] μ[g | m]
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]

Tactic:
by_cases hm : m ≤ m₀
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : ¬m ≤ m₀
neg : EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 0
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]

Tactic:
simp_rw [condExp_of_not_le hm]

Premises used: MeasureTheory.condExp_of_not_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : ¬m ≤ m₀
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 0

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : m ≤ m₀
pos : ∀ (hμm : SigmaFinite (μ.trim hm)), μ[f | m] =ᶠ[ae μ] μ[g | m]
neg : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), μ[f | m] =ᶠ[ae μ] μ[g | m]
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]

Tactic:
by_cases hμm : SigmaFinite (μ.trim hm)

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
neg : EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 0
⊢ μ[f | m] =ᶠ[ae μ] μ[g | m]

Tactic:
simp_rw [condExp_of_not_sigmaFinite hm hμm]

Premises used: MeasureTheory.condExp_of_not_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 0

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
h : f =ᶠ[ae μ] g
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
rw rw₁ : (↑(↑(condExpL1 hm μ g) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑(condExpL1 hm μ g) : α →ₘ[μ] E) : α → E)
⊢ (↑(↑(condExpL1 hm μ f) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] (↑(↑(condExpL1 hm μ g) : α →ₘ[μ] E) : α → E)

Tactic:
rw [condExpL1_congr_ae hm h]

Premises used: MeasureTheory.condExpL1_congr_ae