awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
refine :
  μ[AEStronglyMeasurable.mk f ⋯ | m] =ᶠ[ae (μ.trim hm)] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
⊢ μ[f | m] =ᶠ[ae (μ.trim hm)] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y

Tactic:
refine (condExp_congr_ae_trim hm hf_int.1.ae_eq_mk).trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.condExp_congr_ae_trim, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, And.left
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
⊢ μ[AEStronglyMeasurable.mk f ⋯ | m] =ᶠ[ae (μ.trim hm)] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y

Tactic:
(condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable hm
    hf_int.1.stronglyMeasurable_mk ?_).trans ?_

Premises used: Filter.EventuallyEq.trans, ProbabilityTheory.condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, And.left
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
refine_1 : Integrable (AEStronglyMeasurable.mk f ⋯) μ
refine_2 :
  EventuallyEq.{u_1, u_2} (β := F) (ae (μ.trim hm))
    (fun (ω : Ω) ↦
      @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ AEStronglyMeasurable.mk f ⋯ y)
    fun (ω : Ω) ↦ @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
⊢ μ[AEStronglyMeasurable.mk f ⋯ | m] =ᶠ[ae (μ.trim hm)] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y

Tactic:
refine (condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable hm
    hf_int.1.stronglyMeasurable_mk ?_).trans ?_

Premises used: Filter.EventuallyEq.trans, ProbabilityTheory.condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, And.left
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hm : m ≤ mΩ
hf_int refine_1 refine_1₁ refine_1₂ refine_1₃ : Integrable f μ
⊢ Integrable (AEStronglyMeasurable.mk f ⋯) μ

Tactic:
rwa [integrable_congr hf_int.1.ae_eq_mk.symm]

Premises used: MeasureTheory.integrable_congr, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, And.left, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
h :
  ∀ (ω : Ω)
    (hω :
      f =ᶠ[ae (F := Measure Ω) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω)] AEStronglyMeasurable.mk f ⋯),
    Eq.{u_2 + 1} (α := F)
      (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ AEStronglyMeasurable.mk f ⋯ y)
      (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y)
⊢ EventuallyEq.{u_1, u_2} (β := F) (ae (μ.trim hm))
    (fun (ω : Ω) ↦
      @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ AEStronglyMeasurable.mk f ⋯ y)
    fun (ω : Ω) ↦ @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y

Tactic:
filter_upwards [aestronglyMeasurable_trim_condExpKernel hm hf_int.1] with ω hω

Premises used: ProbabilityTheory.aestronglyMeasurable_trim_condExpKernel, And.left
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : NormedAddCommGroup F
f : Ω → F
inst_3 : NormedSpace ℝ F
inst_4 : CompleteSpace F
hm : m ≤ mΩ
hf_int : Integrable f μ
ω : Ω
hω : f =ᶠ[ae (F := Measure Ω) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω)] AEStronglyMeasurable.mk f ⋯
h h₁ :
  Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ AEStronglyMeasurable.mk f ⋯ y)
    (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (a : Ω) ↦ AEStronglyMeasurable.mk f ⋯ a)
⊢ Eq.{u_2 + 1} (α := F)
    (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ AEStronglyMeasurable.mk f ⋯ y)
    (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y)

Tactic:
rw [integral_congr_ae hω]

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
pos :
  ∀ (hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    μ[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]
neg :
  ∀ (hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    μ[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]
⊢ μ[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]

Tactic:
by_cases hμs : μ s = 0

Premises used: DFunLike.coe
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
pos : μ[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (F := Measure Ω) 0] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]
⊢ μ[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]

Tactic:
rw [Measure.restrict_eq_zero.2 hμs]

Premises used: Iff.mpr, MeasureTheory.Measure.restrict_eq_zero
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (F := Measure Ω) 0] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]

Tactic:
ae_eq_trans (condExp_restrict_ae_eq_restrict
    (generateFrom_singleton_le hs)
    (measurableSet_generateFrom rfl) hf).symm ?_

Premises used: MeasurableSpace.measurableSet_generateFrom, MeasureTheory.condExp_restrict_ae_eq_restrict, MeasurableSpace.generateFrom_singleton_le, MeasureTheory.ae_eq_trans, Filter.EventuallyEq.symm, rfl
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
neg : (μ.restrict s)[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]
⊢ μ[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]

Tactic:
refine ae_eq_trans (condExp_restrict_ae_eq_restrict
    (generateFrom_singleton_le hs)
    (measurableSet_generateFrom rfl) hf).symm ?_

Premises used: MeasurableSpace.measurableSet_generateFrom, MeasureTheory.condExp_restrict_ae_eq_restrict, MeasurableSpace.generateFrom_singleton_le, MeasureTheory.ae_eq_trans, Filter.EventuallyEq.symm, rfl
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (μ.restrict s)[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]

Tactic:
(ae_eq_condExp_of_forall_setIntegral_eq (generateFrom_singleton_le hs) hf.restrict ?_ ?_
      stronglyMeasurable_const.aestronglyMeasurable).symm

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.Integrable.restrict, MeasurableSpace.generateFrom_singleton_le, MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
neg :
  ∀ (s_1 : Set Ω),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set Ω) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn.{u_1, u_2} (ε := F) (fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]) s_1 (μ.restrict s)
neg₁ :
  ∀ (s_1 : Set Ω),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set Ω) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in s_1, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s)
          (∫ (x : Ω) in s_1, f x ∂μ.restrict s)
⊢ (μ.restrict s)[f | MeasurableSpace.generateFrom {s}] =ᶠ[ae (μ.restrict s)] fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]

Tactic:
refine (ae_eq_condExp_of_forall_setIntegral_eq (generateFrom_singleton_le hs) hf.restrict ?_ ?_
      stronglyMeasurable_const.aestronglyMeasurable).symm

Premises used: MeasureTheory.stronglyMeasurable_const, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.Integrable.restrict, MeasurableSpace.generateFrom_singleton_le, MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
neg :
  enorm.{u_2} (E := F) (∫ (x : Ω), f x ∂μ[|s]) = 0 ∨
    LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn.{u_1, u_2} (ε := F) (fun (x : Ω) ↦ ∫ (x : Ω), f x ∂μ[|s]) t (μ.restrict s)

Tactic:
rw [integrableOn_const_iff]

Premises used: MeasureTheory.integrableOn_const_iff
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
⊢ enorm.{u_2} (E := F) (∫ (x : Ω), f x ∂μ[|s]) = 0 ∨
    LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
Or.inr <| measure_lt_top (μ.restrict s) t

Premises used: MeasureTheory.measure_lt_top, MeasureTheory.Measure.restrict, Or.inr
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
⊢ enorm.{u_2} (E := F) (∫ (x : Ω), f x ∂μ[|s]) = 0 ∨
    LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact Or.inr <| measure_lt_top (μ.restrict s) t

Premises used: MeasureTheory.measure_lt_top, MeasureTheory.Measure.restrict, Or.inr
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
ht : MeasurableSet t
neg :
  ∀ (h : t = ∅),
    Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)
neg₁ :
  ∀ (h : t = s),
    Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)
neg₂ :
  ∀ (h : t = sᶜ),
    Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)
neg₃ :
  ∀ (h : t = univ),
    Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)

Tactic:
obtain (h | h | h | h) := measurableSet_generateFrom_singleton_iff.1 ht

Premises used: MeasureTheory.measurableSet_generateFrom_singleton_iff, Iff.mp
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
ht : MeasurableSet t
h : t = ∅
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)

Tactic:
simp [h]
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
ht : MeasurableSet t
h : t = s
neg : μ.real s • HSMul.hSMul (β := F) (μ.real s)⁻¹ (∫ (x : Ω) in s, f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ.restrict s
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)

Tactic:
simp only [h, cond, integral_smul_measure, ENNReal.toReal_inv, integral_const,
        MeasurableSet.univ, measureReal_restrict_apply, univ_inter, measureReal_restrict_apply_self,
        ← measureReal_def]

Premises used: ENNReal.toReal_inv, Set.univ_inter, MeasureTheory.integral_const, MeasureTheory.measureReal_def, ProbabilityTheory.cond, MeasureTheory.integral_smul_measure, MeasureTheory.measureReal_restrict_apply, MeasurableSet.univ, MeasureTheory.measureReal_restrict_apply_self
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
ht : MeasurableSet t
h : t = s
neg : μ.real s ≠ 0
⊢ μ.real s • HSMul.hSMul (β := F) (μ.real s)⁻¹ (∫ (x : Ω) in s, f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ.restrict s

Tactic:
rw [smul_inv_smul₀, Measure.restrict_restrict hs, inter_self]

Premises used: Set.inter_self, smul_inv_smul₀, MeasureTheory.Measure.restrict_restrict
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
ht : MeasurableSet t
h : t = s
⊢ μ.real s ≠ 0

Tactic:
ENNReal.toReal_ne_zero.2 ⟨hμs, measure_ne_top _ _⟩

Premises used: Iff.mpr, MeasureTheory.Measure.real, MeasureTheory.measure_ne_top, And.intro, ENNReal.toReal_ne_zero
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
ht : MeasurableSet t
h : t = s
⊢ μ.real s ≠ 0

Tactic:
exact ENNReal.toReal_ne_zero.2 ⟨hμs, measure_ne_top _ _⟩

Premises used: Iff.mpr, MeasureTheory.measure_ne_top, And.intro, ENNReal.toReal_ne_zero
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
ht : MeasurableSet t
h : t = sᶜ
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)

Tactic:
simp only [h, integral_const, MeasurableSet.univ, measureReal_restrict_apply, univ_inter,
          measureReal_restrict_apply hs.compl, compl_inter_self, measureReal_empty, zero_smul,
          ((Measure.restrict_apply_eq_zero hs.compl).2 <| compl_inter_self s ▸ measure_empty),
          setIntegral_measure_zero]

Premises used: Iff.mpr, MeasureTheory.setIntegral_measure_zero, MeasureTheory.measureReal_empty, MeasureTheory.Measure.restrict_apply_eq_zero, Set.univ_inter, MeasurableSet.compl, zero_smul, MeasureTheory.integral_const, Set.compl_inter_self, MeasureTheory.measureReal_restrict_apply, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
ht : MeasurableSet t
h : t = univ
neg : μ.real s • HSMul.hSMul (β := F) (μ.real s)⁻¹ (∫ (x : Ω) in s, f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ
⊢ Eq.{u_2 + 1} (α := F) (∫ (x : Ω) in t, ∫ (x : Ω), f x ∂μ[|s] ∂μ.restrict s) (∫ (x : Ω) in t, f x ∂μ.restrict s)

Tactic:
simp only [h, Measure.restrict_univ, cond, integral_smul_measure, ENNReal.toReal_inv, ←
        measureReal_def, integral_const, MeasurableSet.univ, measureReal_restrict_apply, univ_inter]

Premises used: ENNReal.toReal_inv, Set.univ_inter, MeasureTheory.integral_const, MeasureTheory.measureReal_def, ProbabilityTheory.cond, MeasureTheory.integral_smul_measure, MeasureTheory.measureReal_restrict_apply, MeasurableSet.univ, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
ht : MeasurableSet t
h : t = univ
neg : μ.real s ≠ 0
⊢ μ.real s • HSMul.hSMul (β := F) (μ.real s)⁻¹ (∫ (x : Ω) in s, f x ∂μ) = ∫ (x : Ω) in s, f x ∂μ

Tactic:
rw [smul_inv_smul₀]

Premises used: smul_inv_smul₀
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
ht : MeasurableSet t
h : t = univ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s : Set Ω
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ F
inst_3 : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set Ω
ht : MeasurableSet t
h : t = univ
⊢ μ.real s ≠ 0

Tactic:
exact (measureReal_ne_zero_iff (by finiteness)).2 hμs

Premises used: Iff.mpr, MeasureTheory.measureReal_ne_zero_iff
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
rw :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ) μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}]
    fun (x : Ω) ↦ ∫ (x : Ω), t.indicator 1 x ∂μ[|s]
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ) μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}]
    fun (x : Ω) ↦ μ[|s].real t

Tactic:
rw [← integral_indicator_one ht]

Premises used: MeasureTheory.integral_indicator_one
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ) μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}]
    fun (x : Ω) ↦ ∫ (x : Ω), t.indicator 1 x ∂μ[|s]

Tactic:
condExp_generateFrom_singleton hs <| Integrable.indicator (integrable_const 1) ht

Premises used: ProbabilityTheory.condExp_generateFrom_singleton, OfNat.ofNat, MeasureTheory.integrable_const, MeasureTheory.Integrable.indicator
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ) μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}]
    fun (x : Ω) ↦ ∫ (x : Ω), t.indicator 1 x ∂μ[|s]

Tactic:
exact condExp_generateFrom_singleton hs <| Integrable.indicator (integrable_const 1) ht

Premises used: ProbabilityTheory.condExp_generateFrom_singleton, MeasureTheory.Integrable.indicator
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
s t : Set Ω
inst_1 : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ)
    (fun (ω : Ω) ↦
      Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.generateFrom {s}) : (a : Ω) → Measure Ω) ω) t)
    μ[t.indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.generateFrom {s}]

Tactic:
have : (fun ω ↦ (condExpKernel μ (generateFrom {s}) ω).real t) =ᵐ[μ.restrict s]
      μ⟦t | generateFrom {s}⟧ :=
    ae_restrict_le <| condExpKernel_ae_eq_condExp
      (generateFrom_singleton_le hs) ht