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
f : α → E
m : MeasurableSpace α
⊢ μ[-f | m] = μ[HSMul.hSMul (α := ℝ) (-1) f | m]
have rw : μ[-f | m] = μ[-f | m]
Tactic: rw [neg_one_smul ℝ f]
-- 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
m : MeasurableSpace α
⊢ μ[-f | m] =ᶠ[ae μ] -μ[f | m]
have f₁ : μ[-f | m] = μ[HSMul.hSMul (α := ℝ) (-1) 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])
-- 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 simp_rw : μ[f + -g | m] =ᶠ[ae μ] μ[f | m] + -μ[g | m]
Tactic: simp_rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m₀ : MeasurableSpace α
μ : Measure α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m₀
inst_3 : SigmaFinite (μ.trim hm₂)
⊢ μ[μ[f | m₂] | m₁] =ᶠ[ae μ] μ[f | m₁]
have pos : ∀ (hμm₁ : SigmaFinite (μ.trim sorry)), μ[μ[f | m₂] | m₁] =ᶠ[ae μ] μ[f | m₁]
Tactic: by_cases hμm₁ : SigmaFinite (μ.trim (hm₁₂.trans hm₂))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m₀ : MeasurableSpace α
μ : Measure α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m₀
inst_3 : SigmaFinite (μ.trim hm₂)
pos : ∀ (hμm₁ : SigmaFinite (μ.trim ⋯)), μ[μ[f | m₂] | m₁] =ᶠ[ae μ] μ[f | m₁]
⊢ μ[μ[f | m₂] | m₁] =ᶠ[ae μ] μ[f | m₁]
have neg : ∀ (hμm₁ : ¬SigmaFinite (μ.trim sorry)), μ[μ[f | m₂] | m₁] =ᶠ[ae μ] μ[f | m₁]
Tactic: by_cases hμm₁ : SigmaFinite (μ.trim (hm₁₂.trans hm₂))
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m₀ : MeasurableSpace α
μ : Measure α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m₀
inst_3 : SigmaFinite (μ.trim hm₂)
hμm₁ : ¬SigmaFinite (μ.trim ⋯)
⊢ μ[μ[f | m₂] | m₁] =ᶠ[ae μ] μ[f | m₁]
have neg : EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 0
Tactic: simp_rw [condExp_of_not_sigmaFinite (hm₁₂.trans hm₂) hμm₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m₀ : MeasurableSpace α
μ : Measure α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m₀
inst_3 : SigmaFinite (μ.trim hm₂)
hμm₁ : SigmaFinite (μ.trim ⋯)
⊢ μ[μ[f | m₂] | m₁] =ᶠ[ae μ] μ[f | m₁]
have pos : ∀ (hf : Integrable f μ), μ[μ[f | m₂] | m₁] =ᶠ[ae μ] μ[f | m₁]
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m₀ : MeasurableSpace α
μ : Measure α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m₀
inst_3 : SigmaFinite (μ.trim hm₂)
hμm₁ : SigmaFinite (μ.trim ⋯)
pos : ∀ (hf : Integrable f μ), μ[μ[f | m₂] | m₁] =ᶠ[ae μ] μ[f | m₁]
⊢ μ[μ[f | m₂] | m₁] =ᶠ[ae μ] μ[f | m₁]
have neg : ∀ (hf : ¬Integrable f μ), μ[μ[f | m₂] | m₁] =ᶠ[ae μ] μ[f | m₁]
Tactic: by_cases hf : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m₀ : MeasurableSpace α
μ : Measure α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m₀
inst_3 : SigmaFinite (μ.trim hm₂)
hμm₁ : SigmaFinite (μ.trim ⋯)
hf : ¬Integrable f μ
⊢ μ[μ[f | m₂] | m₁] =ᶠ[ae μ] μ[f | m₁]
have neg : EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 0
Tactic: simp_rw [condExp_of_not_integrable hf, condExp_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m₀ : MeasurableSpace α
μ : Measure α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m₀
inst_3 : SigmaFinite (μ.trim hm₂)
hμm₁ : SigmaFinite (μ.trim ⋯)
hf : Integrable f μ
⊢ μ[μ[f | m₂] | m₁] =ᶠ[ae μ] μ[f | m₁]
have pos : ∀ (s : Set α),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, μ[μ[f | m₂] | m₁] x ∂μ) (∫ (x : α) in s, μ[f | m₁] x ∂μ)
Tactic: refine ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' (hm₁₂.trans hm₂)
    (fun s _ _ => integrable_condExp.integrableOn) (fun s _ _ => integrable_condExp.integrableOn) ?_
    stronglyMeasurable_condExp.aestronglyMeasurable
    stronglyMeasurable_condExp.aestronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m₀ : MeasurableSpace α
μ : Measure α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m₀
inst_3 : SigmaFinite (μ.trim hm₂)
hμm₁ : SigmaFinite (μ.trim ⋯)
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, μ[μ[f | m₂] | m₁] x ∂μ) (∫ (x : α) in s, μ[f | m₁] x ∂μ)
have pos : Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, μ[f | m₂] x ∂μ) (∫ (x : α) in s, μ[f | m₁] x ∂μ)
Tactic: rw [setIntegral_condExp (hm₁₂.trans hm₂) integrable_condExp hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m₀ : MeasurableSpace α
μ : Measure α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m₀
inst_3 : SigmaFinite (μ.trim hm₂)
hμm₁ : SigmaFinite (μ.trim ⋯)
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, μ[f | m₂] x ∂μ) (∫ (x : α) in s, μ[f | m₁] x ∂μ)
have pos : Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, μ[f | m₂] x ∂μ) (∫ (x : α) in s, f x ∂μ)
Tactic: rw [setIntegral_condExp (hm₁₂.trans hm₂) hf hs, setIntegral_condExp hm₂ hf (hm₁₂ s hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m₀ : MeasurableSpace α
μ : Measure α
hm₁₂ : m₁ ≤ m₂
hm₂ : m₂ ≤ m₀
inst_3 : SigmaFinite (μ.trim hm₂)
hμm₁ : SigmaFinite (μ.trim ⋯)
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
pos : Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, μ[f | m₂] x ∂μ) (∫ (x : α) in s, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, μ[f | m₂] x ∂μ) (∫ (x : α) in s, μ[f | m₁] x ∂μ)
have pos₁ : Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, f x ∂μ)
Tactic: rw [setIntegral_condExp (hm₁₂.trans hm₂) hf hs, setIntegral_condExp hm₂ hf (hm₁₂ s hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : CompleteSpace F
inst_5 : NormedSpace ℝ F
hf_int : Integrable f μ
T : E →L[ℝ] F
⊢ EventuallyEq.{u_1, u_5} (β := F) (ae μ) ((⇑T : (a : E) → F) ∘ μ[f | m]) μ[(⇑T : (a : E) → F) ∘ f | m]
have pos : ∀ (hm : m ≤ m₀), EventuallyEq.{u_1, u_5} (β := F) (ae μ) ((⇑T : (a : E) → F) ∘ μ[f | m]) μ[(⇑T : (a : E) → F) ∘ f | 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 m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : CompleteSpace F
inst_5 : NormedSpace ℝ F
hf_int : Integrable f μ
T : E →L[ℝ] F
pos :
  ∀ (hm : m ≤ m₀), EventuallyEq.{u_1, u_5} (β := F) (ae μ) ((⇑T : (a : E) → F) ∘ μ[f | m]) μ[(⇑T : (a : E) → F) ∘ f | m]
⊢ EventuallyEq.{u_1, u_5} (β := F) (ae μ) ((⇑T : (a : E) → F) ∘ μ[f | m]) μ[(⇑T : (a : E) → F) ∘ f | m]
have neg : ∀ (hm : ¬m ≤ m₀), EventuallyEq.{u_1, u_5} (β := F) (ae μ) ((⇑T : (a : E) → F) ∘ μ[f | m]) μ[(⇑T : (a : E) → F) ∘ f | 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 m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : CompleteSpace F
inst_5 : NormedSpace ℝ F
hf_int : Integrable f μ
T : E →L[ℝ] F
hm : m ≤ m₀
⊢ EventuallyEq.{u_1, u_5} (β := F) (ae μ) ((⇑T : (a : E) → F) ∘ μ[f | m]) μ[(⇑T : (a : E) → F) ∘ f | m]
have pos : ∀ (hμ : SigmaFinite (μ.trim hm)),
  EventuallyEq.{u_1, u_5} (β := F) (ae μ) ((⇑T : (a : E) → F) ∘ μ[f | m]) μ[(⇑T : (a : E) → F) ∘ f | m]
Tactic: by_cases hμ : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : CompleteSpace F
inst_5 : NormedSpace ℝ F
hf_int : Integrable f μ
T : E →L[ℝ] F
hm : m ≤ m₀
pos :
  ∀ (hμ : SigmaFinite (μ.trim hm)),
    EventuallyEq.{u_1, u_5} (β := F) (ae μ) ((⇑T : (a : E) → F) ∘ μ[f | m]) μ[(⇑T : (a : E) → F) ∘ f | m]
⊢ EventuallyEq.{u_1, u_5} (β := F) (ae μ) ((⇑T : (a : E) → F) ∘ μ[f | m]) μ[(⇑T : (a : E) → F) ∘ f | m]
have neg : ∀ (hμ : ¬SigmaFinite (μ.trim hm)),
  EventuallyEq.{u_1, u_5} (β := F) (ae μ) ((⇑T : (a : E) → F) ∘ μ[f | m]) μ[(⇑T : (a : E) → F) ∘ f | m]
Tactic: by_cases hμ : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : CompleteSpace F
inst_5 : NormedSpace ℝ F
hf_int : Integrable f μ
T : E →L[ℝ] F
hm : m ≤ m₀
hμ : SigmaFinite (μ.trim hm)
⊢ EventuallyEq.{u_1, u_5} (β := F) (ae μ) ((⇑T : (a : E) → F) ∘ μ[f | m]) μ[(⇑T : (a : E) → F) ∘ f | m]
have pos : Integrable.{u_5, u_1} (ε := F) ((⇑T : (a : E) → F) ∘ f) μ
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq hm ?_ (fun s ms hs => ?_) (fun s ms hs => ?_) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : CompleteSpace F
inst_5 : NormedSpace ℝ F
hf_int : Integrable f μ
T : E →L[ℝ] F
hm : m ≤ m₀
hμ : SigmaFinite (μ.trim hm)
pos : Integrable.{u_5, u_1} (ε := F) ((⇑T : (a : E) → F) ∘ f) μ
⊢ EventuallyEq.{u_1, u_5} (β := F) (ae μ) ((⇑T : (a : E) → F) ∘ μ[f | m]) μ[(⇑T : (a : E) → F) ∘ f | m]
have pos₁ : ∀ (s : Set α) (ms : MeasurableSet s) (hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  IntegrableOn.{u_1, u_5} (ε := F) ((⇑T : (a : E) → F) ∘ μ[f | m]) s μ
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq hm ?_ (fun s ms hs => ?_) (fun s ms hs => ?_) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : CompleteSpace F
inst_5 : NormedSpace ℝ F
hf_int : Integrable f μ
T : E →L[ℝ] F
hm : m ≤ m₀
hμ : SigmaFinite (μ.trim hm)
pos : Integrable.{u_5, u_1} (ε := F) ((⇑T : (a : E) → F) ∘ f) μ
pos₁ :
  ∀ (s : Set α) (ms : MeasurableSet s) (hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    IntegrableOn.{u_1, u_5} (ε := F) ((⇑T : (a : E) → F) ∘ μ[f | m]) s μ
⊢ EventuallyEq.{u_1, u_5} (β := F) (ae μ) ((⇑T : (a : E) → F) ∘ μ[f | m]) μ[(⇑T : (a : E) → F) ∘ f | m]
have pos₂ : ∀ (s : Set α) (ms : MeasurableSet s) (hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  Eq.{u_5 + 1} (α := F) (∫ (x : α) in s, ((⇑T : (a : E) → F) ∘ μ[f | m]) x ∂μ)
    (∫ (x : α) in s, ((⇑T : (a : E) → F) ∘ f) x ∂μ)
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq hm ?_ (fun s ms hs => ?_) (fun s ms hs => ?_) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : CompleteSpace F
inst_5 : NormedSpace ℝ F
hf_int : Integrable f μ
T : E →L[ℝ] F
hm : m ≤ m₀
hμ : SigmaFinite (μ.trim hm)
pos : Integrable.{u_5, u_1} (ε := F) ((⇑T : (a : E) → F) ∘ f) μ
pos₁ :
  ∀ (s : Set α) (ms : MeasurableSet s) (hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    IntegrableOn.{u_1, u_5} (ε := F) ((⇑T : (a : E) → F) ∘ μ[f | m]) s μ
pos₂ :
  ∀ (s : Set α) (ms : MeasurableSet s) (hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    Eq.{u_5 + 1} (α := F) (∫ (x : α) in s, ((⇑T : (a : E) → F) ∘ μ[f | m]) x ∂μ)
      (∫ (x : α) in s, ((⇑T : (a : E) → F) ∘ f) x ∂μ)
⊢ EventuallyEq.{u_1, u_5} (β := F) (ae μ) ((⇑T : (a : E) → F) ∘ μ[f | m]) μ[(⇑T : (a : E) → F) ∘ f | m]
have pos₃ : AEStronglyMeasurable.{u_1, u_5} (β := F) ((⇑T : (a : E) → F) ∘ μ[f | m]) μ
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq hm ?_ (fun s ms hs => ?_) (fun s ms hs => ?_) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
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
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : CompleteSpace F
inst_5 : NormedSpace ℝ F
inst_6 : IsFiniteMeasure μ
hm : m ≤ m₀
hf_int : Integrable f μ
T : E →L[ℝ] F
a : F
⊢ (fun (x : α) ↦ HAdd.hAdd (α := F) ((T : (a : E) → F) (μ[f | m] x) : F) a) =ᶠ[ae μ]
    HAdd.hAdd (α := α → F) μ[(⇑T : (a : E) → F) ∘ f | m] μ[fun (y : α) ↦ a | m]
have h : ∀ (b : α) (hb : Eq.{u_5 + 1} (α := F) (((⇑T : (a : E) → F) ∘ μ[f | m]) b) (μ[(⇑T : (a : E) → F) ∘ f | m] b)),
  HAdd.hAdd (α := F) ((T : (a : E) → F) (μ[f | m] b) : F) a =
    HAdd.hAdd (α := α → F) (β := α → F) μ[(⇑T : (a : E) → F) ∘ f | m] μ[fun (y : α) ↦ a | m] b
Tactic: filter_upwards [T.comp_condExp_comm hf_int] with b hb
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (hypothesis)
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
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : CompleteSpace F
inst_5 : NormedSpace ℝ F
inst_6 : IsFiniteMeasure μ
hm : m ≤ m₀
hf_int : Integrable f μ
T : E →L[ℝ] F
a : F
⊢ EventuallyEq.{u_1, u_5} (β := F) (ae μ) (fun (x : α) ↦ HAdd.hAdd (α := F) ((T : (a : E) → F) (μ[f | m] x) : F) a)
    μ[fun (y : α) ↦ HAdd.hAdd (α := F) ((T : (a : E) → F) (f y) : F) a | m]
have hp : (fun (x : α) ↦ HAdd.hAdd (α := F) ((T : (a : E) → F) (μ[f | m] x) : F) a) =ᶠ[ae μ]
  HAdd.hAdd (α := α → F) μ[(⇑T : (a : E) → F) ∘ f | m] μ[fun (y : α) ↦ a | m]
Tactic: have hp : (fun x ↦ T (μ[f | m] x) + a) =ᵐ[μ] μ[T ∘ f | m] + μ[(fun y ↦ a) | m] := by
    filter_upwards [T.comp_condExp_comm hf_int] with b hb
    simpa [condExp_const hm a]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst_5 : SigmaFinite (μ.trim hm)
⊢ (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) (toLp f hf2)) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
      α → E) =ᶠ[ae μ]
    μ[f | m]
have refine : ∀ (s : Set α) (hs : MeasurableSet s) (htop : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  Eq.{u_3 + 1} (α := E)
    (∫ (x : α) in s,
      (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) (toLp f hf2)) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
          α → E)
        x ∂μ)
    (∫ (x : α) in s, f x ∂μ)
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq hm hf1
    (fun s hs htop ↦ integrableOn_condExpL2_of_measure_ne_top hm htop.ne _) (fun s hs htop ↦ ?_)
    (aestronglyMeasurable_condExpL2 hm _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst_5 : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
htop : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (x : α) in s,
      (↑(↑(↑((condExpL2 E 𝕜 hm : (a : ↥(Lp E 2 μ)) → ↥(lpMeas E 𝕜 m 2 μ)) (toLp f hf2)) : ↥(Lp E 2 μ)) : α →ₘ[μ] E) :
          α → E)
        x ∂μ)
    (∫ (x : α) in s, f x ∂μ)
have rw : Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) x ∂μ) (∫ (x : α) in s, f x ∂μ)
Tactic: rw [integral_condExpL2_eq hm (hf2.toLp _) hs htop.ne]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst_5 : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
htop : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) x ∂μ) (∫ (x : α) in s, f x ∂μ)
have refine : ∀ᵐ (x : α) ∂μ, x ∈ s → (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) x = f x
Tactic: refine setIntegral_congr_ae (hm _ hs) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst_5 : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
htop : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) x = f x
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) x = f x) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ s → (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) x = f x) x}
          x}
    a
Tactic: filter_upwards [hf2.coeFn_toLp] with ω hω _ using hω
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
𝕜 : Type u_4
inst : RCLike 𝕜
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
inst_3 : CompleteSpace E
inst_4 : InnerProductSpace 𝕜 E
hm : m ≤ m₀
hf1 : Integrable f μ
hf2 : MemLp f 2 μ
inst_5 : SigmaFinite (μ.trim hm)
s : Set α
hs : MeasurableSet s
htop : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) x = f x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ x ∈ s → (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) x = f x) x}
            x}
      a
⊢ ∀ᵐ (x : α) ∂μ, x ∈ s → (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) x = f x
have h₁ : ∀ (a : α), (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) a = f a → a ∈ s → (↑(↑(toLp f hf2) : α →ₘ[μ] E) : α → E) a = f a
Tactic: filter_upwards [hf2.coeFn_toLp] with ω hω _ using hω
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
have pos : ∀ (hm : m ≤ m₀), eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
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 m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
pos : ∀ (hm : m ≤ m₀), eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
have neg : ∀ (hm : ¬m ≤ m₀), eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
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 m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
have pos : ∀ (hfμ : SigmaFinite (μ.trim hm)), eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
Tactic: by_cases hfμ : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
pos : ∀ (hfμ : SigmaFinite (μ.trim hm)), eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
have neg : ∀ (hfμ : ¬SigmaFinite (μ.trim hm)), eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
Tactic: by_cases hfμ : SigmaFinite (μ.trim hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : ¬SigmaFinite (μ.trim hm)
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
have neg : eLpNorm.{u_1, u_3} (ε := E) 0 2 μ ≤ eLpNorm f 2 μ
Tactic: rw [condExp_of_not_sigmaFinite hm hfμ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic (goal)
Goal:
α : Type u_1
E : Type u_3
m m₀ : MeasurableSpace α
μ : Measure α
f : α → E
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m₀
hfμ : SigmaFinite (μ.trim hm)
⊢ eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
have pos : ∀ (hfi : Integrable f μ), eLpNorm μ[f | m] 2 μ ≤ eLpNorm f 2 μ
Tactic: by_cases hfi : Integrable f μ