awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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₁]
neg : ∀ (hμm₁ : ¬SigmaFinite (μ.trim ⋯)), μ[μ[f | m₂] | m₁] =ᶠ[ae μ] μ[f | m₁]
⊢ μ[μ[f | m₂] | m₁] =ᶠ[ae μ] μ[f | m₁]

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

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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 ⋯)
neg : EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 0
⊢ μ[μ[f | m₂] | m₁] =ᶠ[ae μ] μ[f | m₁]

Tactic:
simp_rw [condExp_of_not_sigmaFinite (hm₁₂.trans hm₂) hμm₁]

Premises used: MeasureTheory.condExp_of_not_sigmaFinite, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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 ⋯)
⊢ 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
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₁]
neg : ∀ (hf : ¬Integrable f μ), μ[μ[f | m₂] | m₁] =ᶠ[ae μ] μ[f | m₁]
⊢ μ[μ[f | m₂] | m₁] =ᶠ[ae μ] μ[f | m₁]

Tactic:
by_cases hf : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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 μ
neg : EventuallyEq.{u_1, u_3} (β := E) (ae μ) 0 0
⊢ μ[μ[f | m₂] | m₁] =ᶠ[ae μ] μ[f | m₁]

Tactic:
simp_rw [condExp_of_not_integrable hf, condExp_zero]

Premises used: MeasureTheory.condExp_zero, MeasureTheory.condExp_of_not_integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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 μ
⊢ 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
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₁]

Tactic:
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

Premises used: MeasureTheory.integrable_condExp, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.Integrable.integrableOn, LE.le.trans, MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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 μ
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 ∂μ)
⊢ μ[μ[f | m₂] | m₁] =ᶠ[ae μ] μ[f | m₁]

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

Premises used: MeasureTheory.integrable_condExp, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.Integrable.integrableOn, LE.le.trans, MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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
pos :
  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 ∂μ)
⊢ 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:
_
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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 | m₁] x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, μ[μ[f | m₂] | m₁] x ∂μ) (∫ (x : α) in s, μ[f | m₁] x ∂μ)

Tactic:
rw [setIntegral_condExp (hm₁₂.trans hm₂) integrable_condExp hs]

Premises used: MeasureTheory.setIntegral_condExp, MeasureTheory.integrable_condExp, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
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 ∂μ)
pos₁ pos₂ : Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : α) in s, μ[f | m₂] x ∂μ) (∫ (x : α) in s, μ[f | m₁] x ∂μ)

Tactic:
rw [setIntegral_condExp (hm₁₂.trans hm₂) hf hs, setIntegral_condExp hm₂ hf (hm₁₂ s hs)]

Premises used: MeasureTheory.setIntegral_condExp, LE.le.trans
-- 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
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]
neg :
  ∀ (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]

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
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]
neg :
  ∀ (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]

Tactic:
by_cases hμ : 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
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]

Tactic:
ae_eq_condExp_of_forall_setIntegral_eq hm ?_ (fun s ms hs => ?_) (fun s ms hs => ?_) ?_

Premises used: MeasureTheory.ae_eq_condExp_of_forall_setIntegral_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
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 ∂μ)
pos₃ : AEStronglyMeasurable.{u_1, u_5} (β := F) ((⇑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]

Tactic:
refine ae_eq_condExp_of_forall_setIntegral_eq hm ?_ (fun s ms hs => ?_) (fun s ms hs => ?_) ?_

Premises used: MeasureTheory.ae_eq_condExp_of_forall_setIntegral_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
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)
⊢ Integrable.{u_5, u_1} (ε := F) ((⇑T : (a : E) → F) ∘ f) μ

Tactic:
T.integrable_comp hf_int

Premises used: ContinuousLinearMap.integrable_comp
-- 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
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)
⊢ Integrable.{u_5, u_1} (ε := F) ((⇑T : (a : E) → F) ∘ f) μ

Tactic:
exact T.integrable_comp hf_int

Premises used: ContinuousLinearMap.integrable_comp
-- 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
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)
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:
(T.integrable_comp integrable_condExp).integrableOn

Premises used: MeasureTheory.integrable_condExp, ContinuousLinearMap.integrable_comp, MeasureTheory.Integrable.integrableOn
-- 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
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)
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:
exact (T.integrable_comp integrable_condExp).integrableOn

Premises used: MeasureTheory.integrable_condExp, ContinuousLinearMap.integrable_comp, MeasureTheory.Integrable.integrableOn
-- 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
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)
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 ∂μ : F)
    ((T : (a : E) → F) (∫ (x : α) in s, μ[f | m] x ∂μ) : F)

Tactic:
T.integral_comp_comm integrable_condExp.restrict

Premises used: MeasureTheory.integrable_condExp, MeasureTheory.Integrable.restrict, ContinuousLinearMap.integral_comp_comm
-- 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
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)
s : Set α
ms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_5 + 1} (α := F) ((T : (a : E) → F) (∫ (x : α) in s, μ[f | m] x ∂μ) : F)
    ((T : (a : E) → F) (∫ (x : α) in s, f x ∂μ) : F)

Tactic:
congrArg T (setIntegral_condExp hm hf_int ms)

Premises used: MeasureTheory.setIntegral_condExp, congrArg, DFunLike.coe
-- 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
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)
s : Set α
ms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_5 + 1} (α := F) ((T : (a : E) → F) (∫ (x : α) in s, f x ∂μ) : F)
    (∫ (x : α) in s, ((⇑T : (a : E) → F) ∘ f) x ∂μ : F)

Tactic:
(T.integral_comp_comm hf_int.restrict).symm

Premises used: MeasureTheory.Integrable.restrict, Eq.symm, ContinuousLinearMap.integral_comp_comm
-- 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
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)
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:
calc
          ∫ x in s, (T ∘ μ[f | m]) x ∂μ = T (∫ x in s, μ[f | m] x ∂μ) :=
            T.integral_comp_comm integrable_condExp.restrict
          _ = T (∫ x in s, f x ∂μ) := congrArg T (setIntegral_condExp hm hf_int ms)
          _ = ∫ x in s, (T ∘ f) x ∂μ := (T.integral_comp_comm hf_int.restrict).symm

Premises used: MeasureTheory.setIntegral_condExp, congrArg, MeasureTheory.integrable_condExp, MeasureTheory.Integrable.restrict, MeasureTheory.Measure.restrict, MeasureTheory.condExp, MeasureTheory.integral, Eq.symm, ContinuousLinearMap.integral_comp_comm, DFunLike.coe
-- 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
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)
⊢ AEStronglyMeasurable.{u_1, u_5} (β := F) ((⇑T : (a : E) → F) ∘ μ[f | m]) μ

Tactic:
T.cont.comp_aestronglyMeasurable stronglyMeasurable_condExp.aestronglyMeasurable

Premises used: Continuous.comp_aestronglyMeasurable, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.stronglyMeasurable_condExp, ContinuousLinearMap.cont
-- 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
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)
⊢ AEStronglyMeasurable.{u_1, u_5} (β := F) ((⇑T : (a : E) → F) ∘ μ[f | m]) μ

Tactic:
exact T.cont.comp_aestronglyMeasurable stronglyMeasurable_condExp.aestronglyMeasurable

Premises used: Continuous.comp_aestronglyMeasurable, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.stronglyMeasurable_condExp, ContinuousLinearMap.cont
-- 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
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]

Tactic:
simp [condExp_of_not_sigmaFinite hm hμ]

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
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]

Tactic:
simp [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
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
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
⊢ (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:
filter_upwards [T.comp_condExp_comm hf_int] with b hb

Premises used: ContinuousLinearMap.comp_condExp_comm
-- 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
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
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:
simpa [condExp_const hm a]

Premises used: MeasureTheory.condExp_const
-- 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
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]

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]
-- 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
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
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]
⊢ 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]

Tactic:
hp.trans (condExp_add (T.integrable_comp hf_int) (integrable_const a) m).symm

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_add, ContinuousLinearMap.integrable_comp, MeasureTheory.integrable_const, Filter.EventuallyEq.symm