awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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
⊢ μ[f | ⊥] = fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
have pos : ∀ (hμ_finite : IsFiniteMeasure μ), μ[f | ⊥] = fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
Tactic: by_cases hμ_finite : IsFiniteMeasure μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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
pos :
  ∀ (hμ_finite : IsFiniteMeasure μ),
    μ[f | ⊥] = fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
⊢ μ[f | ⊥] = fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
have neg : ∀ (hμ_finite : ¬IsFiniteMeasure μ),
  μ[f | ⊥] = fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
Tactic: by_cases hμ_finite : IsFiniteMeasure μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (hypothesis)
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 μ
⊢ μ[f | ⊥] = fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
have h : ¬SigmaFinite (m0 := ⊥) (μ.trim sorry)
Tactic: have h : ¬SigmaFinite (μ.trim bot_le) := by rwa [sigmaFinite_trim_bot_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (hypothesis)
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 : ¬SigmaFinite (m0 := ⊥) (μ.trim ⋯)
⊢ μ[f | ⊥] = fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
have hμ_finite₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [not_isFiniteMeasure_iff] at hμ_finite
Cleared hypotheses: hμ_finite, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
h : ¬SigmaFinite (m0 := ⊥) (μ.trim ⋯)
⊢ μ[f | ⊥] = fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
have neg : Eq (α := α → E) 0 fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
Tactic: rw [condExp_of_not_sigmaFinite bot_le h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
h : ¬SigmaFinite (m0 := ⊥) (μ.trim ⋯)
⊢ Eq (α := α → E) 0 fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
have neg : Eq (α := α → E) 0 fun (x : α) ↦ 0
Tactic: simp only [hμ_finite, ENNReal.toReal_top, inv_zero, zero_smul, measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (hypothesis)
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 μ
⊢ μ[f | ⊥] = fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
have h_meas : StronglyMeasurable μ[f | ⊥]
Tactic: have h_meas : StronglyMeasurable[⊥] (μ[f | ⊥]) := stronglyMeasurable_condExp
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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 | ⊥]
⊢ μ[f | ⊥] = fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
have pos : ∀ (c : E) (h_eq : μ[f | ⊥] = fun (x : α) ↦ c),
  μ[f | ⊥] = fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
Tactic: obtain ⟨c, h_eq⟩ := stronglyMeasurable_bot_iff.mp h_meas
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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
⊢ μ[f | ⊥] = fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
have pos : Eq (α := α → E) (fun (x : α) ↦ c) fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
Tactic: rw [h_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (hypothesis)
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
⊢ Eq (α := α → E) (fun (x : α) ↦ c) fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
have h_integral : Eq.{u_3 + 1} (α := E) (∫ (x : α), μ[f | ⊥] x ∂μ) (∫ (x : α), f x ∂μ)
Tactic: have h_integral : ∫ x, (μ[f | ⊥]) x ∂μ = ∫ x, f x ∂μ := integral_condExp bot_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (hypothesis)
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 ∂μ)
⊢ Eq (α := α → E) (fun (x : α) ↦ c) fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
have h_integral₁ : μ.real Set.univ • c = ∫ (x : α), f x ∂μ
Tactic: simp_rw [h_eq, integral_const] at h_integral
Cleared hypotheses: h_integral
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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 (α := α → E) (fun (x : α) ↦ c) fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
have pos : μ.real Set.univ ≠ 0
Tactic: rw [← h_integral, ← smul_assoc, smul_eq_mul, inv_mul_cancel₀, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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 ∂μ
⊢ μ.real Set.univ ≠ 0
have pos : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (0 : ℝ≥0∞) ∧
  ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [Ne, measureReal_def, ENNReal.toReal_eq_zero_iff, not_or]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m₀ : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
⊢ μ[f | ⊥] =ᶠ[ae μ] fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
have 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)
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
Cleared hypotheses: μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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)
⊢ μ[f | ⊥] =ᶠ[ae μ] fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
have inr : ∀ (hμ : NeZero μ), μ[f | ⊥] =ᶠ[ae μ] fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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 =ᶠ[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)
have 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)
Tactic: rw [ae_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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 ∂μ
have refine : Eq (α := α → E) (fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)) fun (x : α) ↦
  ∫ (x : α), f x ∂μ
Tactic: refine (condExp_bot' f).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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
⊢ Eq (α := α → E) (fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)) fun (x : α) ↦
    ∫ (x : α), f x ∂μ
have rw : Eq (α := α → E) (fun (x : α) ↦ HSMul.hSMul (α := ℝ) (β := E) 1⁻¹ (∫ (x : α), f x ∂μ)) fun (x : α) ↦ ∫ (x : α), f x ∂μ
Tactic: rw [probReal_univ, inv_one, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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 ∂μ
⊢ Eq (α := α → E) (fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)) fun (x : α) ↦
    ∫ (x : α), f x ∂μ
have rw₁ : Eq (α := α → E) (fun (x : α) ↦ HSMul.hSMul (α := ℝ) (β := E) 1 (∫ (x : α), f x ∂μ)) fun (x : α) ↦ ∫ (x : α), f x ∂μ
Tactic: rw [probReal_univ, inv_one, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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 ∂μ
⊢ Eq (α := α → E) (fun (x : α) ↦ HSMul.hSMul (β := E) (μ.real Set.univ)⁻¹ (∫ (x : α), f x ∂μ)) fun (x : α) ↦
    ∫ (x : α), f x ∂μ
have rw₂ : Eq (α := α → E) (fun (x : α) ↦ ∫ (x : α), f x ∂μ) fun (x : α) ↦ ∫ (x : α), f x ∂μ
Tactic: rw [probReal_univ, inv_one, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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]
have pos : ∀ (hm : m ≤ m₀), μ[f + g | m] =ᶠ[ae μ] μ[f | m] + μ[g | m]
Tactic: by_cases hm : m ≤ m₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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]
⊢ μ[f + g | m] =ᶠ[ae μ] μ[f | m] + μ[g | m]
have neg : ∀ (hm : ¬m ≤ m₀), μ[f + g | m] =ᶠ[ae μ] μ[f | m] + μ[g | m]
Tactic: by_cases hm : m ≤ m₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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₀
⊢ μ[f + g | m] =ᶠ[ae μ] μ[f | m] + μ[g | m]
have neg : 0 =ᶠ[ae μ] HAdd.hAdd (α := α → E) 0 0
Tactic: simp_rw [condExp_of_not_le hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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₀
⊢ μ[f + g | m] =ᶠ[ae μ] μ[f | m] + μ[g | m]
have pos : ∀ (hμm : SigmaFinite (μ.trim hm)), μ[f + g | m] =ᶠ[ae μ] μ[f | m] + μ[g | m]
Tactic: by_cases hμm : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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]
⊢ μ[f + g | m] =ᶠ[ae μ] μ[f | m] + μ[g | m]
have neg : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), μ[f + g | m] =ᶠ[ae μ] μ[f | m] + μ[g | m]
Tactic: by_cases hμm : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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]
have neg : 0 =ᶠ[ae μ] HAdd.hAdd (α := α → E) 0 0
Tactic: simp_rw [condExp_of_not_sigmaFinite hm hμm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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]
have pos : (↑(↑(condExpL1 hm μ (f + g)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] μ[f | m] + μ[g | m]
Tactic: refine (condExp_ae_eq_condExpL1 hm _).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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)
⊢ (↑(↑(condExpL1 hm μ (f + g)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ] μ[f | m] + μ[g | m]
have pos : (↑(↑(HAdd.hAdd (α := ↥(Lp E 1 μ)) (condExpL1 hm μ f) (condExpL1 hm μ g)) : α →ₘ[μ] E) : α → E) =ᶠ[ae μ]
  μ[f | m] + μ[g | m]
Tactic: rw [condExpL1_add hf hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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) μ
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ ∅, f i | m] (∑ i ∈ ∅, μ[f i | m])
have empty : EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[0 | m] (∑ i ∈ ∅, μ[f i | m])
Tactic: rw [Finset.sum_empty, Finset.sum_empty, condExp_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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])
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ ∅, f i | m] (∑ i ∈ ∅, μ[f i | m])
have empty₁ : EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[0 | m] 0
Tactic: rw [Finset.sum_empty, Finset.sum_empty, condExp_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ ∅, f i | m] (∑ i ∈ ∅, μ[f i | m])
have empty₂ : EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 0
Tactic: rw [Finset.sum_empty, Finset.sum_empty, condExp_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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) μ
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ insert i s, f i | m] (∑ i ∈ insert i s, μ[f i | m])
have insert : μ[f i + ∑ x ∈ s, f x | m] =ᶠ[ae μ] μ[f i | m] + ∑ x ∈ s, μ[f x | m]
Tactic: rw [Finset.sum_insert his, Finset.sum_insert his]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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 α
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ s, f i | m] (∑ i ∈ s, μ[f i | m])
have 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])
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)
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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])
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ s, f i | m] (∑ i ∈ s, μ[f i | m])
have 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 i s, Integrable (f i_1) μ),
  EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ insert i s, f i | m] (∑ i ∈ insert 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)
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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 α
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ s, f i | m] (∑ i ∈ s, μ[f i | m])
have 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])
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)
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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])
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ s, f i | m] (∑ i ∈ s, μ[f i | m])
have 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 i s, Integrable (f i_1) μ),
  EventuallyEq.{u_1, u_3} (β := E) (ae μ) μ[∑ i ∈ insert i s, f i | m] (∑ i ∈ insert 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)
Cleared hypotheses: s, hf