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
hf_int : Integrable f μ
h : Nontrivial Ω
⊢ Integrable.{u_2, u_1} (ε := F)
    (fun (ω : Ω) ↦
      @integral _ _ _ _ mΩ ((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯ : (a : Ω) → Measure Ω) ω)
        fun (y : Ω) ↦ f y)
    μ

Tactic:
convert!
    Integrable.integral_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ))
      aemeasurable_id hf_int.comp_snd_map_prod_id using 1

Premises used: inf_le_right, MeasureTheory.Integrable.integral_condDistrib, MeasureTheory.Integrable.comp_snd_map_prod_id, aemeasurable_id, aemeasurable_id''
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
⊢ Nontrivial Ω

Tactic:
nontriviality Ω
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h : Nontrivial Ω
rw :
  Integrable (ε := ℝ)
    (fun (ω : Ω) ↦
      Measure.real (m := mΩ) ((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯ : (a : Ω) → Measure Ω) ω) s)
    μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ Measure.real (m := mΩ) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) s) μ

Tactic:
rw [condExpKernel_eq]

Premises used: ProbabilityTheory.condExpKernel_eq
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h : Nontrivial Ω
⊢ Integrable (ε := ℝ)
    (fun (ω : Ω) ↦
      Measure.real (m := mΩ) ((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯ : (a : Ω) → Measure Ω) ω) s)
    μ

Tactic:
integrable_toReal_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) hs

Premises used: inf_le_right, ProbabilityTheory.integrable_toReal_condDistrib, aemeasurable_id''
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h : Nontrivial Ω
⊢ Integrable (ε := ℝ)
    (fun (ω : Ω) ↦
      Measure.real (m := mΩ) ((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯ : (a : Ω) → Measure Ω) ω) s)
    μ

Tactic:
exact integrable_toReal_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) hs

Premises used: inf_le_right, ProbabilityTheory.integrable_toReal_condDistrib, aemeasurable_id''
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
inl :
  ∀ (h : IsEmpty Ω),
    (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ Measure.real (m := mΩ) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) s)
      μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ]
inr :
  ∀ (h : Nonempty Ω),
    (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ Measure.real (m := mΩ) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) s)
      μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ]
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ Measure.real (m := mΩ) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) s)
    μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ]

Tactic:
rcases isEmpty_or_nonempty Ω with h | h

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h : IsEmpty Ω
⊢ μ = 0

Tactic:
have : μ = 0 := Measure.eq_zero_of_isEmpty μ
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h : IsEmpty Ω
this : μ = 0
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ Measure.real (m := mΩ) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) s)
    μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ]

Tactic:
simpa [this] using trivial

Premises used: trivial
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h : Nonempty Ω
⊢ (ae μ).EventuallyEq (β := ℝ)
    (fun (a : Ω) ↦ Measure.real (m := mΩ) ((condDistrib id id μ : (a : Ω) → Measure Ω) (id a)) s)
    μ[(id ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap id (m ⊓ mΩ)]

Tactic:
have h := condDistrib_ae_eq_condExp (μ := μ)
    (measurable_id'' (inf_le_right : m ⊓ mΩ ≤ mΩ)) measurable_id hs
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h_1 : Nonempty Ω
h :
  (ae μ).EventuallyEq (β := ℝ)
    (fun (a : Ω) ↦ Measure.real (m := mΩ) ((condDistrib id id μ : (a : Ω) → Measure Ω) (id a)) s)
    μ[(id ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap id (m ⊓ mΩ)]
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (a : Ω) ↦ Measure.real (m := mΩ) ((condDistrib id id μ : (a : Ω) → Measure Ω) a) s)
    μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ]

Tactic:
simp only [id_eq, MeasurableSpace.comap_id, preimage_id_eq] at h

Premises used: MeasurableSpace.comap_id, Set.preimage_id_eq, id_eq
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h_1 : Nonempty Ω
h :
  (ae μ).EventuallyEq (β := ℝ) (fun (a : Ω) ↦ Measure.real (m := mΩ) ((condDistrib id id μ : (a : Ω) → Measure Ω) a) s)
    μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ]
inr :
  (ae μ).EventuallyEq (β := ℝ)
    (fun (ω : Ω) ↦ Measure.real (m := mΩ) ((condDistrib id id μ : (a : Ω) → Measure Ω) (id ω)) s)
    μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ]
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ Measure.real (m := mΩ) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) s)
    μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ]

Tactic:
simp_rw [condExpKernel_apply_eq_condDistrib]

Premises used: ProbabilityTheory.condExpKernel_apply_eq_condDistrib
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h_1 : Nonempty Ω
h :
  (ae μ).EventuallyEq (β := ℝ) (fun (a : Ω) ↦ Measure.real (m := mΩ) ((condDistrib id id μ : (a : Ω) → Measure Ω) a) s)
    μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ]
⊢ (ae μ).EventuallyEq (β := ℝ)
    (fun (ω : Ω) ↦ Measure.real (m := mΩ) ((condDistrib id id μ : (a : Ω) → Measure Ω) (id ω)) s)
    μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ]

Tactic:
h
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h_1 : Nonempty Ω
h :
  (ae μ).EventuallyEq (β := ℝ) (fun (a : Ω) ↦ Measure.real (m := mΩ) ((condDistrib id id μ : (a : Ω) → Measure Ω) a) s)
    μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ]
⊢ (ae μ).EventuallyEq (β := ℝ)
    (fun (ω : Ω) ↦ Measure.real (m := mΩ) ((condDistrib id id μ : (a : Ω) → Measure Ω) (id ω)) s)
    μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ]

Tactic:
exact h
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
rw rw₁ : (ae μ).EventuallyEq (β := ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m] μ[s.indicator fun (ω : Ω) ↦ 1 | m]
⊢ (ae μ).EventuallyEq (β := ℝ) μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ] μ[s.indicator fun (ω : Ω) ↦ 1 | m]

Tactic:
rw [inf_of_le_left hm]

Premises used: inf_of_le_left
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
rw :
  (ae μ).EventuallyEq (β := ℝ)
    (fun (x : Ω) ↦ ENNReal.toReal ((((condExpKernel μ m : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
    μ[s.indicator fun (ω : Ω) ↦ 1 | m]
⊢ (ae (μ.trim hm)).EventuallyEq (β := ℝ)
    (fun (ω : Ω) ↦ ENNReal.toReal ((((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
    μ[s.indicator fun (ω : Ω) ↦ 1 | m]

Tactic:
rw [(measurable_condExpKernel hs).ennreal_toReal.stronglyMeasurable.ae_eq_trim_iff hm
    stronglyMeasurable_condExp]

Premises used: Measurable.stronglyMeasurable, ProbabilityTheory.measurable_condExpKernel, MeasureTheory.stronglyMeasurable_condExp, Measurable.ennreal_toReal, MeasureTheory.StronglyMeasurable.ae_eq_trim_iff
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ (ae μ).EventuallyEq (β := ℝ)
    (fun (x : Ω) ↦ ENNReal.toReal ((((condExpKernel μ m : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
    μ[s.indicator fun (ω : Ω) ↦ 1 | m]

Tactic:
condExpKernel_ae_eq_condExp hm hs

Premises used: MeasureTheory.Measure.real, ProbabilityTheory.condExpKernel_ae_eq_condExp
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ (ae μ).EventuallyEq (β := ℝ)
    (fun (x : Ω) ↦ ENNReal.toReal ((((condExpKernel μ m : (a : Ω) → Measure Ω) x : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s))
    μ[s.indicator fun (ω : Ω) ↦ 1 | m]

Tactic:
exact condExpKernel_ae_eq_condExp hm hs

Premises used: ProbabilityTheory.condExpKernel_ae_eq_condExp
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
X : Ω → β
Y : Ω → γ
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
simp_rw :
  (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : Ω) ↦
      ((((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a) : Measure β) : (a : Set β) → ℝ≥0∞) s)
    fun (a : Ω) ↦
    (((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
      (X ⁻¹' s)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : Ω) ↦
      ((((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a) : Measure β) : (a : Set β) → ℝ≥0∞) s)
    fun (a : Ω) ↦
    ((((Kernel.map (condExpKernel μ (MeasurableSpace.comap Y mγ)) X : Kernel Ω β) : (a : Ω) → Measure β) a :
          Measure β) :
        (a : Set β) → ℝ≥0∞)
      s

Tactic:
simp_rw [Kernel.map_apply' _ hX _ hs]

Premises used: ProbabilityTheory.Kernel.map_apply'
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
X : Ω → β
Y : Ω → γ
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
h :
  ∀ (a : Ω)
    (ha₁ :
      Measure.real (m := mβ) (((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a)) s =
        μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap Y mγ] a)
    (ha₂ :
      Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a) (X ⁻¹' s) =
        μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap Y mγ] a),
    Eq (α := ℝ≥0∞)
      (((((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      ((((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
          (X ⁻¹' s) :
        ℝ≥0∞)
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : Ω) ↦
      ((((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a) : Measure β) : (a : Set β) → ℝ≥0∞) s)
    fun (a : Ω) ↦
    (((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
      (X ⁻¹' s)

Tactic:
filter_upwards [condDistrib_ae_eq_condExp hY hX (μ := μ) hs,
    condExpKernel_ae_eq_condExp hY.comap_le (μ := μ) (hX hs)] with a ha₁ ha₂

Premises used: ProbabilityTheory.condDistrib_ae_eq_condExp, Measurable.comap_le, ProbabilityTheory.condExpKernel_ae_eq_condExp
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
β : Type u_3
γ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst_2 : StandardBorelSpace β
inst_3 : Nonempty β
X : Ω → β
Y : Ω → γ
hX : Measurable X
hY : Measurable Y
s : Set β
hs : MeasurableSet s
a : Ω
ha₁ :
  Measure.real (m := mβ) (((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a)) s =
    μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap Y mγ] a
ha₂ :
  Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a) (X ⁻¹' s) =
    μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap Y mγ] a
h :
  Measure.real (m := mβ) (((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a)) s =
    Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a) (X ⁻¹' s)
h₁ :
  μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap Y mγ] a =
    Measure.real (m := mΩ) ((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a) (X ⁻¹' s)
h₂ h₃ :
  Eq (α := ℝ) (μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap Y mγ] a)
    (μ[(X ⁻¹' s).indicator fun (ω : Ω) ↦ 1 | MeasurableSpace.comap Y mγ] a)
⊢ Eq (α := ℝ≥0∞)
    (((((condDistrib X Y μ : Kernel γ β) : (a : γ) → Measure β) (Y a) : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    ((((condExpKernel μ (MeasurableSpace.comap Y mγ) : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
        (X ⁻¹' s) :
      ℝ≥0∞)

Tactic:
rw [← measureReal_eq_measureReal_iff, ha₁, ha₂]

Premises used: MeasureTheory.measureReal_eq_measureReal_iff
-- 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
hf_int : Integrable f μ
inl :
  ∀ (h : IsEmpty Ω),
    μ[f | m ⊓ mΩ] =ᶠ[ae μ] fun (ω : Ω) ↦
      @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
inr :
  ∀ (h : Nonempty Ω),
    μ[f | m ⊓ mΩ] =ᶠ[ae μ] fun (ω : Ω) ↦
      @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
⊢ μ[f | m ⊓ mΩ] =ᶠ[ae μ] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y

Tactic:
rcases isEmpty_or_nonempty Ω with h | h

Premises used: isEmpty_or_nonempty
-- 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
hf_int : Integrable f μ
h : IsEmpty Ω
⊢ μ = 0

Tactic:
have : μ = 0 := Measure.eq_zero_of_isEmpty μ
-- 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
hf_int : Integrable f μ
h : IsEmpty Ω
this : μ = 0
⊢ μ[f | m ⊓ mΩ] =ᶠ[ae μ] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y

Tactic:
simpa [this] using trivial

Premises used: trivial
-- 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
hf_int : Integrable f μ
h : Nonempty Ω
⊢ Measurable.{u_1, u_1} (α := Ω) id

Tactic:
have hX : @Measurable Ω Ω mΩ (m ⊓ mΩ) id := measurable_id.mono le_rfl (inf_le_right : m ⊓ mΩ ≤ mΩ)
-- 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
hf_int : Integrable f μ
h : Nonempty Ω
hX : Measurable.{u_1, u_1} (α := Ω) id
inr :
  μ[f | m ⊓ mΩ] =ᶠ[ae μ] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id ω)) fun (y : Ω) ↦ f y
⊢ μ[f | m ⊓ mΩ] =ᶠ[ae μ] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y

Tactic:
simp_rw [condExpKernel_apply_eq_condDistrib]

Premises used: ProbabilityTheory.condExpKernel_apply_eq_condDistrib
-- 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
hf_int : Integrable f μ
h : Nonempty Ω
hX : Measurable.{u_1, u_1} (α := Ω) id
⊢ μ[f | MeasurableSpace.comap id (m ⊓ mΩ)] =ᶠ[ae μ] fun (a : Ω) ↦
    @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id a)) fun (y : Ω) ↦ f y

Tactic:
have h := condExp_ae_eq_integral_condDistrib_id hX hf_int
-- 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
hf_int : Integrable f μ
h_1 : Nonempty Ω
hX : Measurable.{u_1, u_1} (α := Ω) id
h :
  μ[f | MeasurableSpace.comap id (m ⊓ mΩ)] =ᶠ[ae μ] fun (a : Ω) ↦
    @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id a)) fun (y : Ω) ↦ f y
⊢ μ[f | m ⊓ mΩ] =ᶠ[ae μ] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id ω)) fun (y : Ω) ↦ f y

Tactic:
simpa only [MeasurableSpace.comap_id, id_eq] using h

Premises used: MeasurableSpace.comap_id, id_eq
-- 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 μ
rw rw₁ : μ[f | m] =ᶠ[ae μ] μ[f | m]
⊢ μ[f | m ⊓ mΩ] =ᶠ[ae μ] μ[f | m]

Tactic:
rw [inf_of_le_left hm]

Premises used: inf_of_le_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 : StronglyMeasurable f
hf_int : Integrable f μ
⊢ μ[f | m] =ᶠ[ae (μ.trim hm)] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y

Tactic:
StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable hm ?_ ?_ ?_

Premises used: MeasureTheory.StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable
-- 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 : StronglyMeasurable f
hf_int : Integrable f μ
refine_1 : StronglyMeasurable μ[f | m]
refine_2 :
  StronglyMeasurable.{u_1, u_2} (β := F) fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
refine_3 :
  μ[f | m] =ᶠ[ae μ] 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 StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable hm ?_ ?_ ?_

Premises used: MeasureTheory.StronglyMeasurable.ae_eq_trim_of_stronglyMeasurable
-- 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 : StronglyMeasurable f
hf_int : Integrable f μ
⊢ StronglyMeasurable μ[f | m]

Tactic:
stronglyMeasurable_condExp

Premises used: MeasureTheory.stronglyMeasurable_condExp
-- 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 : StronglyMeasurable f
hf_int : Integrable f μ
⊢ StronglyMeasurable μ[f | m]

Tactic:
exact stronglyMeasurable_condExp

Premises used: MeasureTheory.stronglyMeasurable_condExp
-- 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 : StronglyMeasurable f
hf_int : Integrable f μ
⊢ StronglyMeasurable.{u_1, u_2} (β := F) fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y

Tactic:
hf.integral_condExpKernel

Premises used: MeasureTheory.StronglyMeasurable.integral_condExpKernel
-- 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 : StronglyMeasurable f
hf_int : Integrable f μ
⊢ StronglyMeasurable.{u_1, u_2} (β := F) fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y

Tactic:
exact hf.integral_condExpKernel

Premises used: MeasureTheory.StronglyMeasurable.integral_condExpKernel
-- 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 : StronglyMeasurable f
hf_int : Integrable f μ
⊢ μ[f | m] =ᶠ[ae μ] fun (ω : Ω) ↦ @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y

Tactic:
condExp_ae_eq_integral_condExpKernel hm hf_int

Premises used: ProbabilityTheory.condExp_ae_eq_integral_condExpKernel
-- 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 : StronglyMeasurable f
hf_int : Integrable f μ
⊢ μ[f | m] =ᶠ[ae μ] fun (ω : Ω) ↦ @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y

Tactic:
exact condExp_ae_eq_integral_condExpKernel hm hf_int

Premises used: ProbabilityTheory.condExp_ae_eq_integral_condExpKernel
-- 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 μ
⊢ μ[f | m] =ᶠ[ae (μ.trim hm)] fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y

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