awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ f x = AEStronglyMeasurable.mk f hf x) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦
                  Eq.{u_4 + 1} (α := G)
                    ((fun (ω : Ω) ↦ ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)) x)
                    ((fun (ω : Ω) ↦
                        ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G)
                            (g ω) :
                          G))
                      x))
                x}
            x}
      a
h₁ h₂ :
  ∀ (a : Ω) (ha : f a = AEStronglyMeasurable.mk f hf a),
    Eq.{u_4 + 1} (α := G) ((((B : (a : F) → E →L[ℝ] G) (f a) : E →L[ℝ] G) : (a : E) → G) (g a) : G)
      ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf a) : E →L[ℝ] G) : (a : E) → G) (g a) : G)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (g ω)

Tactic:
filter_upwards [hf.ae_eq_mk] with a ha using by rw [ha]

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
    fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)

Tactic:
condExp_bilin_of_stronglyMeasurable_left B hf.stronglyMeasurable_mk
      ((integrable_congr ?_).mp hfg) hg

Premises used: MeasureTheory.condExp_bilin_of_stronglyMeasurable_left, MeasureTheory.integrable_congr, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
refine :
  EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (g ω)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m]
    fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)

Tactic:
refine condExp_bilin_of_stronglyMeasurable_left B hf.stronglyMeasurable_mk
      ((integrable_congr ?_).mp hfg) hg

Premises used: MeasureTheory.condExp_bilin_of_stronglyMeasurable_left, MeasureTheory.integrable_congr, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
ω : Ω
hω : f ω = AEStronglyMeasurable.mk f hf ω
rw rw₁ :
  Eq.{u_4 + 1} (α := G)
    ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)
    ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)
⊢ Eq.{u_4 + 1} (α := G) ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)
    ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)

Tactic:
rw [hω]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ f x = AEStronglyMeasurable.mk f hf x) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦
                  Eq.{u_4 + 1} (α := G)
                    ((fun (ω : Ω) ↦ ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)) x)
                    ((fun (ω : Ω) ↦
                        ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G)
                            (g ω) :
                          G))
                      x))
                x}
            x}
      a
h₁ h₂ :
  ∀ (ω : Ω) (hω : f ω = AEStronglyMeasurable.mk f hf ω),
    Eq.{u_4 + 1} (α := G) ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)
      ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (g ω) : G)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (g ω)

Tactic:
filter_upwards [hf.ae_eq_mk] with ω hω using by rw [hω]

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
a : Ω
ha : f a = AEStronglyMeasurable.mk f hf a
rw rw₁ :
  Eq.{u_4 + 1} (α := G)
    ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf a) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] a) : G)
    ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf a) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] a) : G)
⊢ Eq.{u_4 + 1} (α := G)
    ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf a) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] a) : G)
    ((((B : (a : F) → E →L[ℝ] G) (f a) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] a) : G)

Tactic:
rw [ha]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace E
f : Ω → F
g : Ω → E
hf : AEStronglyMeasurable f μ
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hg : Integrable g μ
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ f x = AEStronglyMeasurable.mk f hf x) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦
                  Eq.{u_4 + 1} (α := G)
                    ((fun (ω : Ω) ↦
                        ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G)
                            (μ[g | m] ω) :
                          G))
                      x)
                    ((fun (ω : Ω) ↦ ((((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω) : G))
                      x))
                x}
            x}
      a
h₁ h₂ :
  ∀ (a : Ω) (ha : f a = AEStronglyMeasurable.mk f hf a),
    Eq.{u_4 + 1} (α := G)
      ((((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf a) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] a) : G)
      ((((B : (a : F) → E →L[ℝ] G) (f a) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] a) : G)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    (fun (ω : Ω) ↦
      (((B : (a : F) → E →L[ℝ] G) (AEStronglyMeasurable.mk f hf ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω))
    fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (μ[g | m] ω)

Tactic:
filter_upwards [hf.ae_eq_mk] with a ha using by rw [ha]

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace F
f : Ω → F
g : Ω → E
hg : AEStronglyMeasurable g μ
hfg :
  Integrable.{u_4, u_1} (ε := G) (fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω)) μ
hf : Integrable f μ
simp_rw :
  EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦ (((B.flip : (a : E) → F →L[ℝ] G) (g ω) : F →L[ℝ] G) : (a : F) → G) (f ω) | m] fun (ω : Ω) ↦
    (((B.flip : (a : E) → F →L[ℝ] G) (g ω) : F →L[ℝ] G) : (a : F) → G) (μ[f | m] ω)
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦ (((B : (a : F) → E →L[ℝ] G) (f ω) : E →L[ℝ] G) : (a : E) → G) (g ω) | m] fun (ω : Ω) ↦
    (((B : (a : F) → E →L[ℝ] G) (μ[f | m] ω) : E →L[ℝ] G) : (a : E) → G) (g ω)

Tactic:
simp_rw [← B.flip_apply] at hfg ⊢

Premises used: ContinuousLinearMap.flip_apply
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace F
f : Ω → F
g : Ω → E
hg : AEStronglyMeasurable g μ
hfg :
  Integrable.{u_4, u_1} (ε := G)
    (fun (ω : Ω) ↦ (((B.flip : (a : E) → F →L[ℝ] G) (g ω) : F →L[ℝ] G) : (a : F) → G) (f ω)) μ
hf : Integrable f μ
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦ (((B.flip : (a : E) → F →L[ℝ] G) (g ω) : F →L[ℝ] G) : (a : F) → G) (f ω) | m] fun (ω : Ω) ↦
    (((B.flip : (a : E) → F →L[ℝ] G) (g ω) : F →L[ℝ] G) : (a : F) → G) (μ[f | m] ω)

Tactic:
condExp_bilin_of_aestronglyMeasurable_left B.flip hg hfg hf

Premises used: MeasureTheory.condExp_bilin_of_aestronglyMeasurable_left, ContinuousLinearMap.flip
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
F : Type u_3
G : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : CompleteSpace G
B : F →L[ℝ] E →L[ℝ] G
inst_7 : CompleteSpace F
f : Ω → F
g : Ω → E
hg : AEStronglyMeasurable g μ
hfg :
  Integrable.{u_4, u_1} (ε := G)
    (fun (ω : Ω) ↦ (((B.flip : (a : E) → F →L[ℝ] G) (g ω) : F →L[ℝ] G) : (a : F) → G) (f ω)) μ
hf : Integrable f μ
⊢ EventuallyEq.{u_1, u_4} (β := G) (ae μ)
    μ[fun (ω : Ω) ↦ (((B.flip : (a : E) → F →L[ℝ] G) (g ω) : F →L[ℝ] G) : (a : F) → G) (f ω) | m] fun (ω : Ω) ↦
    (((B.flip : (a : E) → F →L[ℝ] G) (g ω) : F →L[ℝ] G) : (a : F) → G) (μ[f | m] ω)

Tactic:
exact condExp_bilin_of_aestronglyMeasurable_left B.flip hg hfg hf

Premises used: MeasureTheory.condExp_bilin_of_aestronglyMeasurable_left, ContinuousLinearMap.flip
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : Ω → ℝ
g : Ω → E
hf : AEStronglyMeasurable f μ
hfg : Integrable (f • g) μ
hg : Integrable g μ
⊢ μ[f • g | m] =ᶠ[ae μ] f • μ[g | m]

Tactic:
condExp_bilin_of_aestronglyMeasurable_left (.lsmul ℝ ℝ) hf hfg hg

Premises used: Real, MeasureTheory.condExp_bilin_of_aestronglyMeasurable_left, ContinuousLinearMap.lsmul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : Ω → ℝ
g : Ω → E
hf : Integrable f μ
hfg : Integrable (f • g) μ
hg : AEStronglyMeasurable g μ
⊢ μ[f • g | m] =ᶠ[ae μ] μ[f | m] • g

Tactic:
condExp_bilin_of_aestronglyMeasurable_left (ContinuousLinearMap.lsmul ℝ ℝ).flip hg hfg hf

Premises used: Real, MeasureTheory.condExp_bilin_of_aestronglyMeasurable_left, ContinuousLinearMap.flip, ContinuousLinearMap.lsmul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ
hf : AEStronglyMeasurable f μ
hfg : Integrable (f * g) μ
hg : Integrable g μ
⊢ μ[f * g | m] =ᶠ[ae μ] f * μ[g | m]

Tactic:
condExp_bilin_of_aestronglyMeasurable_left (.mul ℝ ℝ) hf hfg hg

Premises used: Real, MeasureTheory.condExp_bilin_of_aestronglyMeasurable_left, ContinuousLinearMap.mul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ
hg : AEStronglyMeasurable g μ
hfg : Integrable (f * g) μ
hf : Integrable f μ
⊢ μ[f * g | m] =ᶠ[ae μ] μ[f | m] * g

Tactic:
condExp_bilin_of_aestronglyMeasurable_right (.mul ℝ ℝ) hg hfg hf

Premises used: Real, MeasureTheory.condExp_bilin_of_aestronglyMeasurable_right, ContinuousLinearMap.mul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ
hf : StronglyMeasurable f
hfg : Integrable (f * g) μ
hg : Integrable g μ
⊢ μ[f * g | m] =ᶠ[ae μ] f * μ[g | m]

Tactic:
condExp_bilin_of_aestronglyMeasurable_left (.mul ℝ ℝ)
    hf.aestronglyMeasurable hfg hg

Premises used: Real, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.condExp_bilin_of_aestronglyMeasurable_left, ContinuousLinearMap.mul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f g : Ω → ℝ
hg : StronglyMeasurable g
hfg : Integrable (f * g) μ
hf : Integrable f μ
⊢ μ[f * g | m] =ᶠ[ae μ] μ[f | m] * g

Tactic:
condExp_bilin_of_aestronglyMeasurable_right (.mul ℝ ℝ)
    hg.aestronglyMeasurable hfg hf

Premises used: Real, MeasureTheory.condExp_bilin_of_aestronglyMeasurable_right, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, ContinuousLinearMap.mul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ mΩ
f : SimpleFunc Ω ℝ
g : Ω → ℝ
hg : Integrable g μ
⊢ μ[(⇑f : (a : Ω) → ℝ) * g | m] =ᶠ[ae μ] (⇑f : (a : Ω) → ℝ) * μ[g | m]

Tactic:
condExp_stronglyMeasurable_simpleFunc_bilin (.mul ℝ ℝ) hm f hg

Premises used: Real, MeasureTheory.condExp_stronglyMeasurable_simpleFunc_bilin, ContinuousLinearMap.mul
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ mΩ
inst : IsFiniteMeasure μ
f g : Ω → ℝ
hf : StronglyMeasurable f
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
⊢ μ[f * g | m] =ᶠ[ae μ] f * μ[g | m]

Tactic:
condExp_stronglyMeasurable_bilin_of_bound (.mul ℝ ℝ) hm hf hg c hf_bound

Premises used: Real, ContinuousLinearMap.mul, MeasureTheory.condExp_stronglyMeasurable_bilin_of_bound
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ mΩ
inst : IsFiniteMeasure μ
f g : Ω → ℝ
hf : AEStronglyMeasurable f μ
hg : Integrable g μ
c : ℝ
hf_bound : ∀ᵐ (ω : Ω) ∂μ, ‖f ω‖ ≤ c
⊢ μ[f * g | m] =ᶠ[ae μ] f * μ[g | m]

Tactic:
condExp_aestronglyMeasurable_bilin_of_bound (.mul ℝ ℝ) hm hf hg c hf_bound

Premises used: Real, ContinuousLinearMap.mul, MeasureTheory.condExp_aestronglyMeasurable_bilin_of_bound
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
⊢ SigmaFinite (m0 := m𝓨) (Measure.map g (ν.trim ⋯))

Tactic:
rw [← map_trim_comap hg] at hσ

Premises used: MeasureTheory.map_trim_comap
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (m0 := m𝓨) (Measure.map g (ν.trim ⋯))
⊢ SigmaFinite (ν.trim ⋯)

Tactic:
SigmaFinite.of_map (ν.trim hg.comap_le) ?_ hσ

Premises used: MeasureTheory.SigmaFinite.of_map, Measurable.comap_le, MeasureTheory.Measure.trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (m0 := m𝓨) (Measure.map g (ν.trim ⋯))
refine : AEMeasurable g (ν.trim ⋯)
⊢ SigmaFinite (ν.trim ⋯)

Tactic:
refine SigmaFinite.of_map (ν.trim hg.comap_le) ?_ hσ

Premises used: MeasureTheory.SigmaFinite.of_map, Measurable.comap_le, MeasureTheory.Measure.trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (m0 := m𝓨) (Measure.map g (ν.trim ⋯))
⊢ AEMeasurable g (ν.trim ⋯)

Tactic:
Measurable.aemeasurable ?_

Premises used: Measurable.aemeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (m0 := m𝓨) (Measure.map g (ν.trim ⋯))
refine : Measurable g
⊢ AEMeasurable g (ν.trim ⋯)

Tactic:
refine Measurable.aemeasurable ?_

Premises used: Measurable.aemeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (m0 := m𝓨) (Measure.map g (ν.trim ⋯))
⊢ Measurable g

Tactic:
measurable_iff_comap_le.mpr le_rfl

Premises used: Iff.mpr, le_rfl, measurable_iff_comap_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (m0 := m𝓨) (Measure.map g (ν.trim ⋯))
⊢ Measurable g

Tactic:
exact measurable_iff_comap_le.mpr le_rfl

Premises used: Iff.mpr, le_rfl, measurable_iff_comap_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
⊢ SigmaFinite (ν.trim ⋯)

Tactic:
have : SigmaFinite (ν.trim hg.comap_le) := by
    rw [← map_trim_comap hg] at hσ
    refine SigmaFinite.of_map (ν.trim hg.comap_le) ?_ hσ
    refine Measurable.aemeasurable ?_
    exact measurable_iff_comap_le.mpr le_rfl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
this : SigmaFinite (ν.trim ⋯)
⊢ SigmaFinite ν

Tactic:
have : SigmaFinite ν := SigmaFinite.of_map _ hg.aemeasurable hσ
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
this_1 : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
⊢ Integrable (ε := ℝ) (fun (a : 𝓧) ↦ (μ.rnDeriv ν a).toReal) ν

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
this_1 : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
refine_1 :
  ∀ (s : Set 𝓧),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ)
          (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal) s ν
refine_2 :
  ∀ (s : Set 𝓧),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : 𝓧) in s, (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x)).toReal ∂ν)
          (∫ (x : 𝓧) in s, (μ.rnDeriv ν x).toReal ∂ν)
refine_3 :
  AEStronglyMeasurable (β := ℝ)
    (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal) ν
⊢ (ae ν).EventuallyEq (β := ℝ)
    (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal)
    ν[fun (a : 𝓧) ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]

Tactic:
refine ae_eq_condExp_of_forall_setIntegral_eq _ (by fun_prop) ?_ ?_ ?_

Premises used: MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq