awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable μ[f | ⊥]
c : E
h_eq : μ[f | ⊥] = fun (x : α) ↦ c
h_integral : Eq.{u_3 + 1} (α := E) (∫ (x : α), μ[f | ⊥] x ∂μ) (∫ (x : α), f x ∂μ)
⊢ μ.real Set.univ • c = ∫ (x : α), f x ∂μ

Tactic:
simp_rw [h_eq, integral_const] at h_integral

Premises used: MeasureTheory.integral_const
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable μ[f | ⊥]
c : E
h_eq : μ[f | ⊥] = fun (x : α) ↦ c
h_integral : μ.real Set.univ • c = ∫ (x : α), f x ∂μ
pos : μ.real Set.univ ≠ 0
⊢ Eq (α := α → E) (fun (x : α) ↦ c) fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)

Tactic:
rw [← h_integral, ← smul_assoc, smul_eq_mul, inv_mul_cancel₀, one_smul]

Premises used: smul_assoc, one_smul, smul_eq_mul, inv_mul_cancel₀
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable μ[f | ⊥]
c : E
h_eq : μ[f | ⊥] = fun (x : α) ↦ c
h_integral : μ.real Set.univ • c = ∫ (x : α), f x ∂μ
pos :
  ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real Set.univ ≠ 0

Tactic:
rw [Ne, measureReal_def, ENNReal.toReal_eq_zero_iff, not_or]

Premises used: Ne, not_or, MeasureTheory.measureReal_def, ENNReal.toReal_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable μ[f | ⊥]
c : E
h_eq : μ[f | ⊥] = fun (x : α) ↦ c
h_integral : μ.real Set.univ • c = ∫ (x : α), f x ∂μ
⊢ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
⟨NeZero.ne _, measure_ne_top μ Set.univ⟩

Premises used: Set.univ, MeasureTheory.measure_ne_top, And.intro, NeZero.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hμ : NeZero μ
f : α → E
hμ_finite : IsFiniteMeasure μ
h_meas : StronglyMeasurable μ[f | ⊥]
c : E
h_eq : μ[f | ⊥] = fun (x : α) ↦ c
h_integral : μ.real Set.univ • c = ∫ (x : α), f x ∂μ
⊢ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact ⟨NeZero.ne _, measure_ne_top μ Set.univ⟩
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
inl :
  condExp ⊥ (m₀ := m₀) 0 f =ᶠ[ae (F := Measure α) 0] fun (x : α) ↦
    HSMul.hSMul (β := E) (Measure.real.{u_1} (α := α) (m := m₀) 0 Set.univ)⁻¹ (@integral _ _ _ _ m₀ 0 fun (x : α) ↦ f x)
inr : ∀ (hμ : NeZero μ), μ[f | ⊥] =ᶠ[ae μ] fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
⊢ μ[f | ⊥] =ᶠ[ae μ] fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)

Tactic:
rcases eq_zero_or_neZero μ with rfl | hμ

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
inl :
  condExp ⊥ (m₀ := m₀) 0 f =ᶠ[⊥] fun (x : α) ↦
    HSMul.hSMul (β := E) (Measure.real.{u_1} (α := α) (m := m₀) 0 Set.univ)⁻¹ (@integral _ _ _ _ m₀ 0 fun (x : α) ↦ f x)
⊢ condExp ⊥ (m₀ := m₀) 0 f =ᶠ[ae (F := Measure α) 0] fun (x : α) ↦
    HSMul.hSMul (β := E) (Measure.real.{u_1} (α := α) (m := m₀) 0 Set.univ)⁻¹ (@integral _ _ _ _ m₀ 0 fun (x : α) ↦ f x)

Tactic:
rw [ae_zero]

Premises used: MeasureTheory.ae_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
⊢ condExp ⊥ (m₀ := m₀) 0 f =ᶠ[⊥] fun (x : α) ↦
    HSMul.hSMul (β := E) (Measure.real.{u_1} (α := α) (m := m₀) 0 Set.univ)⁻¹ (@integral _ _ _ _ m₀ 0 fun (x : α) ↦ f x)

Tactic:
eventually_bot

Premises used: Filter.EventuallyEq, Filter.eventually_bot
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
⊢ condExp ⊥ (m₀ := m₀) 0 f =ᶠ[⊥] fun (x : α) ↦
    HSMul.hSMul (β := E) (Measure.real.{u_1} (α := α) (m := m₀) 0 Set.univ)⁻¹ (@integral _ _ _ _ m₀ 0 fun (x : α) ↦ f x)

Tactic:
exact eventually_bot

Premises used: Filter.eventually_bot
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
hμ : NeZero μ
⊢ μ[f | ⊥] =ᶠ[ae μ] fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)

Tactic:
Eventually.of_forall <| congr_fun (condExp_bot' f)

Premises used: Filter.EventuallyEq, Filter.Eventually.of_forall, congr_fun, MeasureTheory.condExp_bot'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
hμ : NeZero μ
⊢ μ[f | ⊥] =ᶠ[ae μ] fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)

Tactic:
exact Eventually.of_forall <| congr_fun (condExp_bot' f)

Premises used: Filter.Eventually.of_forall, congr_fun, MeasureTheory.condExp_bot'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : IsProbabilityMeasure μ
f : α → E
⊢ μ[f | ⊥] = fun (x : α) ↦ ∫ (x : α), f x ∂μ

Tactic:
(condExp_bot' f).trans ?_

Premises used: MeasureTheory.condExp_bot', Eq.trans
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : IsProbabilityMeasure μ
f : α → E
refine :
  Eq (α := α → E) (fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)) fun (x : α) ↦
    ∫ (x : α), f x ∂μ
⊢ μ[f | ⊥] = fun (x : α) ↦ ∫ (x : α), f x ∂μ

Tactic:
refine (condExp_bot' f).trans ?_

Premises used: MeasureTheory.condExp_bot', Eq.trans
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : IsProbabilityMeasure μ
f : α → E
rw :
  Eq (α := α → E) (fun (x : α) ↦ HSMul.hSMul (α := ℝ) (β := E) 1⁻¹ (∫ (x : α), f x ∂μ)) fun (x : α) ↦ ∫ (x : α), f x ∂μ
rw₁ :
  Eq (α := α → E) (fun (x : α) ↦ HSMul.hSMul (α := ℝ) (β := E) 1 (∫ (x : α), f x ∂μ)) fun (x : α) ↦ ∫ (x : α), f x ∂μ
rw₂ rw₃ : Eq (α := α → E) (fun (x : α) ↦ ∫ (x : α), f x ∂μ) fun (x : α) ↦ ∫ (x : α), f x ∂μ
⊢ Eq (α := α → E) (fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)) fun (x : α) ↦
    ∫ (x : α), f x ∂μ

Tactic:
rw [probReal_univ, inv_one, one_smul]

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

Tactic:
by_cases hm : m ≤ m₀
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : ¬m ≤ m₀
neg : 0 =ᶠ[ae μ] HAdd.hAdd (α := α → E) 0 0
⊢ μ[f + g | m] =ᶠ[ae μ] μ[f | m] + μ[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₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : ¬m ≤ m₀
⊢ 0 =ᶠ[ae μ] HAdd.hAdd (α := α → E) 0 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
pos : ∀ (hμm : SigmaFinite (μ.trim hm)), μ[f + g | m] =ᶠ[ae μ] μ[f | m] + μ[g | m]
neg : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), μ[f + g | m] =ᶠ[ae μ] μ[f | m] + μ[g | m]
⊢ μ[f + g | m] =ᶠ[ae μ] μ[f | m] + μ[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₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
neg : 0 =ᶠ[ae μ] HAdd.hAdd (α := α → E) 0 0
⊢ μ[f + g | m] =ᶠ[ae μ] μ[f | m] + μ[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₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
hμm : ¬SigmaFinite (μ.trim hm)
⊢ 0 =ᶠ[ae μ] HAdd.hAdd (α := α → E) 0 0

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

Tactic:
(condExp_ae_eq_condExpL1 hm _).trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_ae_eq_condExpL1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
pos : (↑(↑(condExpL1 hm μ (f + g)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] μ[f | m] + μ[g | m]
⊢ μ[f + g | m] =ᶠ[ae μ] μ[f | m] + μ[g | m]

Tactic:
refine (condExp_ae_eq_condExpL1 hm _).trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_ae_eq_condExpL1
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
pos :
  (↑(↑(HAdd.hAdd (α := ↥(Lp E 1 μ)) (condExpL1 hm μ f) (condExpL1 hm μ g)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    μ[f | m] + μ[g | m]
⊢ (↑(↑(condExpL1 hm μ (f + g)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] μ[f | m] + μ[g | m]

Tactic:
rw [condExpL1_add hf hg]

Premises used: MeasureTheory.condExpL1_add
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ (↑(↑(HAdd.hAdd (α := ↥(Lp E 1 μ)) (condExpL1 hm μ f) (condExpL1 hm μ g)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    μ[f | m] + μ[g | m]

Tactic:
(coeFn_add _ _).trans
    ((condExp_ae_eq_condExpL1 hm _).symm.add (condExp_ae_eq_condExpL1 hm _).symm)

Premises used: MeasureTheory.Lp.coeFn_add, Filter.EventuallyEq.trans, MeasureTheory.condExp_ae_eq_condExpL1, Filter.EventuallyEq.add, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
hm : m ≤ m₀
hμm : SigmaFinite (μ.trim hm)
⊢ (↑(↑(HAdd.hAdd (α := ↥(Lp E 1 μ)) (condExpL1 hm μ f) (condExpL1 hm μ g)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
    μ[f | m] + μ[g | m]

Tactic:
exact (coeFn_add _ _).trans
    ((condExp_ae_eq_condExpL1 hm _).symm.add (condExp_ae_eq_condExpL1 hm _).symm)

Premises used: MeasureTheory.Lp.coeFn_add, Filter.EventuallyEq.trans, MeasureTheory.condExp_ae_eq_condExpL1, Filter.EventuallyEq.add, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_5
f : ι → α → E
m : MeasurableSpace α
hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable (f i) μ
empty : EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[0 | m] (∑ i ∈ ∅, μ[f i | m])
empty₁ : EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[0 | m] 0
empty₂ empty₃ : EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 0
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ ∅, f i | m] (∑ i ∈ ∅, μ[f i | m])

Tactic:
rw [Finset.sum_empty, Finset.sum_empty, condExp_zero]

Premises used: MeasureTheory.condExp_zero, Finset.sum_empty
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_5
f : ι → α → E
m : MeasurableSpace α
i : ι
s : Finset ι
his : i ∉ s
heq :
  ∀ (hf : ∀ i ∈ s, Integrable (f i) μ),
    EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ s, f i | m] (∑ i ∈ s, μ[f i | m])
hf : ∀ i_1 ∈ Insert.insert i s, Integrable (f i_1) μ
insert : μ[f i + ∑ x ∈ s, f x | m] =ᶠ[ae μ] μ[f i | m] + ∑ x ∈ s, μ[f x | m]
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ Insert.insert i s, f i | m] (∑ i ∈ Insert.insert i s, μ[f i | m])

Tactic:
rw [Finset.sum_insert his, Finset.sum_insert his]

Premises used: Finset.sum_insert
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_5
f : ι → α → E
m : MeasurableSpace α
i : ι
s : Finset ι
his : i ∉ s
heq :
  ∀ (hf : ∀ i ∈ s, Integrable (f i) μ),
    EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ s, f i | m] (∑ i ∈ s, μ[f i | m])
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
⊢ μ[f i + ∑ x ∈ s, f x | m] =ᶠ[ae μ] μ[f i | m] + ∑ x ∈ s, μ[f x | m]

Tactic:
(condExp_add (hf i <| Finset.mem_insert_self i s)
      (integrable_finsetSum' _ <| Finset.forall_of_forall_insert hf) _).trans
        ((EventuallyEq.refl _ _).add <| heq <| Finset.forall_of_forall_insert hf)

Premises used: Finset.forall_of_forall_insert, Filter.EventuallyEq.trans, Finset.mem_insert_self, MeasureTheory.condExp_add, MeasureTheory.integrable_finsetSum', Filter.EventuallyEq.refl, Filter.EventuallyEq.add
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_5
f : ι → α → E
m : MeasurableSpace α
i : ι
s : Finset ι
his : i ∉ s
heq :
  ∀ (hf : ∀ i ∈ s, Integrable (f i) μ),
    EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ s, f i | m] (∑ i ∈ s, μ[f i | m])
hf : ∀ i_1 ∈ insert i s, Integrable (f i_1) μ
⊢ μ[f i + ∑ x ∈ s, f x | m] =ᶠ[ae μ] μ[f i | m] + ∑ x ∈ s, μ[f x | m]

Tactic:
exact (condExp_add (hf i <| Finset.mem_insert_self i s)
      (integrable_finsetSum' _ <| Finset.forall_of_forall_insert hf) _).trans
        ((EventuallyEq.refl _ _).add <| heq <| Finset.forall_of_forall_insert hf)

Premises used: Finset.forall_of_forall_insert, Filter.EventuallyEq.trans, Finset.mem_insert_self, MeasureTheory.condExp_add, MeasureTheory.integrable_finsetSum', Filter.EventuallyEq.refl, Filter.EventuallyEq.add
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_5
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, Integrable (f i) μ
m : MeasurableSpace α
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable (f i) μ),
    EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ ∅, f i | m] (∑ i ∈ ∅, μ[f i | m])
insert :
  ∀ (i : ι) (s : Finset ι) (his : i ∉ s)
    (heq :
      ∀ (hf : ∀ i ∈ s, Integrable (f i) μ),
        EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ s, f i | m] (∑ i ∈ s, μ[f i | m]))
    (hf : ∀ i_1 ∈ Insert.insert i s, Integrable (f i_1) μ),
    EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ Insert.insert i s, f i | m] (∑ i ∈ Insert.insert i s, μ[f i | m])
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ s, f i | m] (∑ i ∈ s, μ[f i | m])

Tactic:
induction s using Finset.induction_on with
  | empty => rw [Finset.sum_empty, Finset.sum_empty, condExp_zero]
  | insert i s his heq =>
    rw [Finset.sum_insert his, Finset.sum_insert his]
    exact (condExp_add (hf i <| Finset.mem_insert_self i s)
      (integrable_finsetSum' _ <| Finset.forall_of_forall_insert hf) _).trans
        ((EventuallyEq.refl _ _).add <| heq <| Finset.forall_of_forall_insert hf)

Premises used: MeasureTheory.condExp_zero, Insert.insert, Finset.sum_empty
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
ι : Type u_5
s : Finset ι
f : ι → α → E
hf : ∀ i ∈ s, Integrable (f i) μ
m : MeasurableSpace α
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable (f i) μ),
    EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ ∅, f i | m] (∑ i ∈ ∅, μ[f i | m])
insert :
  ∀ (i : ι) (s : Finset ι) (his : i ∉ s)
    (heq :
      ∀ (hf : ∀ i ∈ s, Integrable (f i) μ),
        EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ s, f i | m] (∑ i ∈ s, μ[f i | m]))
    (hf : ∀ i_1 ∈ Insert.insert i s, Integrable (f i_1) μ),
    EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ Insert.insert i s, f i | m] (∑ i ∈ Insert.insert i s, μ[f i | m])
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ s, f i | m] (∑ i ∈ s, μ[f i | m])

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => rw [Finset.sum_empty, Finset.sum_empty, condExp_zero]
  | insert i s his heq =>
    rw [Finset.sum_insert his, Finset.sum_insert his]
    exact (condExp_add (hf i <| Finset.mem_insert_self i s)
      (integrable_finsetSum' _ <| Finset.forall_of_forall_insert hf) _).trans
        ((EventuallyEq.refl _ _).add <| heq <| Finset.forall_of_forall_insert hf)

Premises used: MeasureTheory.condExp_zero, Insert.insert, Finset.sum_empty
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
m : MeasurableSpace α
rw rw₁ : μ[-f | m] = μ[-f | m]
⊢ μ[-f | m] = μ[HSMul.hSMul (α := ℝ) (-1) f | m]

Tactic:
rw [neg_one_smul ℝ f]

Premises used: Real, neg_one_smul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
m : MeasurableSpace α
⊢ μ[HSMul.hSMul (α := ℝ) (-1) f | m] =ᶠ[ae μ] HSMul.hSMul (α := ℝ) (-1) μ[f | m]

Tactic:
condExp_smul ..

Premises used: MeasureTheory.condExp_smul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
m : MeasurableSpace α
⊢ HSMul.hSMul (α := ℝ) (-1) μ[f | m] = -μ[f | m]

Tactic:
neg_one_smul ℝ (μ[f | m])

Premises used: Real, neg_one_smul, MeasureTheory.condExp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
m : MeasurableSpace α
f₁ : μ[-f | m] = μ[HSMul.hSMul (α := ℝ) (-1) f | m]
⊢ μ[-f | m] =ᶠ[ae μ] -μ[f | m]

Tactic:
calc
    μ[-f | m] = μ[(-1 : ℝ) • f | m] := by rw [neg_one_smul ℝ f]
    _ =ᵐ[μ] (-1 : ℝ) • μ[f | m] := condExp_smul ..
    _ = -μ[f | m] := neg_one_smul ℝ (μ[f | m])

Premises used: Real, neg_one_smul, MeasureTheory.condExp_smul, MeasureTheory.condExp, OfNat.ofNat, Neg.neg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
simp_rw : μ[f + -g | m] =ᶠ[ae μ] μ[f | m] + -μ[g | m]
⊢ μ[f - g | m] =ᶠ[ae μ] μ[f | m] - μ[g | m]

Tactic:
simp_rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
⊢ μ[f + -g | m] =ᶠ[ae μ] μ[f | m] + -μ[g | m]

Tactic:
(condExp_add hf hg.neg _).trans (EventuallyEq.rfl.add (condExp_neg ..))

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Integrable.neg, MeasureTheory.condExp_neg, MeasureTheory.condExp_add, Filter.EventuallyEq.add, Filter.EventuallyEq.rfl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
f g : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hf : Integrable f μ
hg : Integrable g μ
m : MeasurableSpace α
⊢ μ[f + -g | m] =ᶠ[ae μ] μ[f | m] + -μ[g | m]

Tactic:
exact (condExp_add hf hg.neg _).trans (EventuallyEq.rfl.add (condExp_neg ..))

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Integrable.neg, MeasureTheory.condExp_neg, MeasureTheory.condExp_add, Filter.EventuallyEq.add, Filter.EventuallyEq.rfl