awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hm : m ≤ mΩ
h_1 : Nonempty Ω
this : m ⊓ mΩ = m
h : Eq (α := Measure (Ω × Ω)) (Measure.map id μ ⊗ₘ condDistrib id id μ) (Measure.map (fun (a : Ω) ↦ (id a, id a)) μ)
inr :
  ∀ (a : Ω) (s : Set Ω) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯ : (a : Ω) → Measure Ω) a : Measure Ω) :
            (a : Set Ω) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((condDistrib id id μ : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := Kernel Ω Ω) (Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯) (condDistrib id id μ)

Tactic:
ext a s hs
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hm : m ≤ mΩ
h_1 : Nonempty Ω
this : m ⊓ mΩ = m
h : Eq (α := Measure (Ω × Ω)) (Measure.map id μ ⊗ₘ condDistrib id id μ) (Measure.map (fun (a : Ω) ↦ (id a, id a)) μ)
a : Ω
s : Set Ω
hs : MeasurableSet s
inr :
  Eq (α := ℝ≥0∞) ((((condDistrib id id μ : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((((condDistrib id id μ : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯ : (a : Ω) → Measure Ω) a : Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((condDistrib id id μ : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [Kernel.coe_comap, Function.comp_apply, id_eq]

Premises used: Function.comp_apply, ProbabilityTheory.Kernel.coe_comap, id_eq
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hm : m ≤ mΩ
h_1 : Nonempty Ω
this : m ⊓ mΩ = m
h : Eq (α := Measure (Ω × Ω)) (Measure.map id μ ⊗ₘ condDistrib id id μ) (Measure.map (fun (a : Ω) ↦ (id a, id a)) μ)
a : Ω
s : Set Ω
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((condDistrib id id μ : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((((condDistrib id id μ : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
congr
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hm : m ≤ mΩ
hX : Measurable.{u_1, u_1} (α := Ω) id
⊢ (⇑(condExpKernel μ m) : (a : Ω) → Measure Ω) ∘ₘ μ.trim hm = μ

Tactic:
rw [← Measure.snd_compProd, compProd_trim_condExpKernel, @Measure.snd_map_prodMk, Measure.map_id]

Premises used: MeasureTheory.Measure.map_id, MeasureTheory.Measure.snd_compProd, MeasureTheory.Measure.snd_map_prodMk, ProbabilityTheory.compProd_trim_condExpKernel
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hm : m ≤ mΩ
⊢ Measurable.{u_1, u_1} (α := Ω) id

Tactic:
measurable_id'' hm

Premises used: measurable_id''
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hm : m ≤ mΩ
⊢ Measurable.{u_1, u_1} (α := Ω) id

Tactic:
exact measurable_id'' hm

Premises used: measurable_id''
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
⊢ Measurable (β := ℝ≥0∞) fun (ω : Ω) ↦
    (((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s

Tactic:
(condExpKernel μ m).measurable_coe hs

Premises used: ProbabilityTheory.condExpKernel, ProbabilityTheory.Kernel.measurable_coe
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
⊢ StronglyMeasurable (β := ℝ≥0∞) fun (ω : Ω) ↦
    (((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s

Tactic:
Measurable.stronglyMeasurable (measurable_condExpKernel hs)

Premises used: Measurable.stronglyMeasurable, ProbabilityTheory.measurable_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
hf : StronglyMeasurable f
⊢ Nontrivial Ω

Tactic:
nontriviality Ω
-- 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 : StronglyMeasurable f
h : Nontrivial Ω
simp_rw :
  StronglyMeasurable.{u_1, u_2} (β := F) fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id ω)) fun (y : Ω) ↦ f y
⊢ StronglyMeasurable.{u_1, u_2} (β := F) 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
hf : StronglyMeasurable f
h : Nontrivial Ω
⊢ StronglyMeasurable.{u_1, u_2} (β := F) fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id ω)) fun (y : Ω) ↦ f y

Tactic:
(hf.comp_measurable measurable_snd).integral_condDistrib

Premises used: MeasureTheory.StronglyMeasurable.integral_condDistrib, MeasureTheory.StronglyMeasurable.comp_measurable, measurable_snd
-- 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 : StronglyMeasurable f
h : Nontrivial Ω
⊢ StronglyMeasurable.{u_1, u_2} (β := F) fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id ω)) fun (y : Ω) ↦ f y

Tactic:
exact (hf.comp_measurable measurable_snd).integral_condDistrib

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

Tactic:
hf.integral_condExpKernel'.mono inf_le_left

Premises used: MeasureTheory.StronglyMeasurable.integral_condExpKernel', MeasureTheory.StronglyMeasurable.mono, inf_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
hf : AEStronglyMeasurable f μ
⊢ Nontrivial Ω

Tactic:
nontriviality Ω
-- 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 : AEStronglyMeasurable f μ
h : Nontrivial Ω
simp_rw :
  AEStronglyMeasurable.{u_1, u_2} (β := F)
    (fun (ω : Ω) ↦ @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id ω)) fun (y : Ω) ↦ f y) μ
⊢ AEStronglyMeasurable.{u_1, u_2} (β := F)
    (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
hf : AEStronglyMeasurable f μ
h : Nontrivial Ω
⊢ AEStronglyMeasurable.{u_1, u_2} (β := F)
    (fun (ω : Ω) ↦ @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id ω)) fun (y : Ω) ↦ f y) μ

Tactic:
AEStronglyMeasurable.integral_condDistrib
    (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
    (hf.comp_snd_map_prod_id inf_le_right)

Premises used: inf_le_right, MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_id, MeasureTheory.AEStronglyMeasurable.integral_condDistrib, aemeasurable_id, aemeasurable_id''
-- 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 : AEStronglyMeasurable f μ
h : Nontrivial Ω
⊢ AEStronglyMeasurable.{u_1, u_2} (β := F)
    (fun (ω : Ω) ↦ @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id ω)) fun (y : Ω) ↦ f y) μ

Tactic:
exact AEStronglyMeasurable.integral_condDistrib
    (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
    (hf.comp_snd_map_prod_id inf_le_right)

Premises used: inf_le_right, MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_id, MeasureTheory.AEStronglyMeasurable.integral_condDistrib, aemeasurable_id, aemeasurable_id''
-- 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 : AEStronglyMeasurable f μ
h : Nontrivial Ω
rw :
  AEStronglyMeasurable.{u_1, u_2} (β := F)
    (fun (ω : Ω) ↦
      @integral _ _ _ _ mΩ ((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯ : (a : Ω) → Measure Ω) ω)
        fun (y : Ω) ↦ f y)
    μ
⊢ AEStronglyMeasurable.{u_1, u_2} (β := F)
    (fun (ω : Ω) ↦ @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y) μ

Tactic:
rw [condExpKernel_eq]

Premises used: ProbabilityTheory.condExpKernel_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
hf : AEStronglyMeasurable f μ
h : Nontrivial Ω
⊢ AEStronglyMeasurable.{u_1, u_2} (β := F)
    (fun (a : Ω) ↦
      @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id a)) fun (y : Ω) ↦ f (id a, y).2)
    μ

Tactic:
have h := aestronglyMeasurable_integral_condDistrib
    (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
    (hf.comp_snd_map_prod_id (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
hf : AEStronglyMeasurable f μ
h_1 : Nontrivial Ω
h :
  AEStronglyMeasurable.{u_1, u_2} (β := F)
    (fun (a : Ω) ↦
      @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id a)) fun (y : Ω) ↦ f (id a, y).2)
    μ
⊢ AEStronglyMeasurable.{u_1, u_2} (β := F)
    (fun (a : Ω) ↦
      @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id a)) fun (y : Ω) ↦ f (id a, y).2)
    μ

Tactic:
rw [MeasurableSpace.comap_id] at h

Premises used: MeasurableSpace.comap_id
-- 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 : AEStronglyMeasurable f μ
h_1 : Nontrivial Ω
h :
  AEStronglyMeasurable.{u_1, u_2} (β := F)
    (fun (a : Ω) ↦
      @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id a)) fun (y : Ω) ↦ f (id a, y).2)
    μ
⊢ AEStronglyMeasurable.{u_1, u_2} (β := F)
    (fun (ω : Ω) ↦
      @integral _ _ _ _ mΩ ((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯ : (a : Ω) → Measure Ω) ω)
        fun (y : Ω) ↦ f y)
    μ

Tactic:
h.mono inf_le_left

Premises used: inf_le_left, MeasureTheory.AEStronglyMeasurable.mono
-- 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 : AEStronglyMeasurable f μ
h_1 : Nontrivial Ω
h :
  AEStronglyMeasurable.{u_1, u_2} (β := F)
    (fun (a : Ω) ↦
      @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id a)) fun (y : Ω) ↦ f (id a, y).2)
    μ
⊢ AEStronglyMeasurable.{u_1, u_2} (β := F)
    (fun (ω : Ω) ↦
      @integral _ _ _ _ mΩ ((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯ : (a : Ω) → Measure Ω) ω)
        fun (y : Ω) ↦ f y)
    μ

Tactic:
exact h.mono inf_le_left

Premises used: inf_le_left, MeasureTheory.AEStronglyMeasurable.mono
-- 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
hm : m ≤ mΩ
hf : AEStronglyMeasurable f μ
⊢ ∀ᵐ (ω : Ω) ∂μ.trim hm,
    f =ᶠ[ae (F := Measure Ω) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω)] AEStronglyMeasurable.mk f hf

Tactic:
Measure.ae_ae_of_ae_comp ?_

Premises used: Filter.EventuallyEq, MeasureTheory.Measure.ae_ae_of_ae_comp
-- 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
hm : m ≤ mΩ
hf : AEStronglyMeasurable f μ
refine : ∀ᵐ (ω : Ω) ∂(⇑(condExpKernel μ m) : (a : Ω) → Measure Ω) ∘ₘ μ.trim hm, f ω = AEStronglyMeasurable.mk f hf ω
⊢ ∀ᵐ (ω : Ω) ∂μ.trim hm,
    f =ᶠ[ae (F := Measure Ω) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω)] AEStronglyMeasurable.mk f hf

Tactic:
refine Measure.ae_ae_of_ae_comp ?_

Premises used: MeasureTheory.Measure.ae_ae_of_ae_comp
-- 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
hm : m ≤ mΩ
hf : AEStronglyMeasurable f μ
rw : ∀ᵐ (ω : Ω) ∂μ, f ω = AEStronglyMeasurable.mk f hf ω
⊢ ∀ᵐ (ω : Ω) ∂(⇑(condExpKernel μ m) : (a : Ω) → Measure Ω) ∘ₘ μ.trim hm, f ω = AEStronglyMeasurable.mk f hf ω

Tactic:
rw [condExpKernel_comp_trim hm]

Premises used: ProbabilityTheory.condExpKernel_comp_trim
-- 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
hm : m ≤ mΩ
hf : AEStronglyMeasurable f μ
⊢ ∀ᵐ (ω : Ω) ∂μ, f ω = AEStronglyMeasurable.mk f hf ω

Tactic:
hf.ae_eq_mk

Premises used: Filter.EventuallyEq, MeasureTheory.AEStronglyMeasurable.ae_eq_mk
-- 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
hm : m ≤ mΩ
hf : AEStronglyMeasurable f μ
⊢ ∀ᵐ (ω : Ω) ∂μ, f ω = AEStronglyMeasurable.mk f hf ω

Tactic:
exact hf.ae_eq_mk

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk
-- 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
hf_int : Integrable f μ
⊢ Nontrivial Ω

Tactic:
nontriviality Ω
-- 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
hf_int : Integrable f μ
h : Nontrivial Ω
⊢ ∀ᵐ (a : Ω) ∂μ,
    @Integrable.{u_2, u_1} F _ _ _ mΩ (fun (ω : Ω) ↦ f (id a, ω).2) ((condDistrib id id μ : (a : Ω) → Measure Ω) (id a))

Tactic:
Integrable.condDistrib_ae (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
      hf_int.comp_snd_map_prod_id

Premises used: inf_le_right, MeasureTheory.Integrable.condDistrib_ae, MeasureTheory.Integrable.comp_snd_map_prod_id, aemeasurable_id, aemeasurable_id''
-- 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
hf_int : Integrable f μ
h : Nontrivial Ω
⊢ ∀ᵐ (ω : Ω) ∂μ,
    @Integrable _ _ _ _ mΩ f ((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯ : (a : Ω) → Measure Ω) ω)

Tactic:
convert!
    Integrable.condDistrib_ae (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.condDistrib_ae, MeasureTheory.Integrable.comp_snd_map_prod_id, aemeasurable_id, aemeasurable_id''
-- 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
hf_int : Integrable f μ
h : Nontrivial Ω
rw :
  Integrable (ε := ℝ)
    (fun (ω : Ω) ↦
      @integral _ _ _ _ mΩ ((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯ : (a : Ω) → Measure Ω) ω)
        fun (y : Ω) ↦ ‖f y‖)
    μ
⊢ Integrable (ε := ℝ)
    (fun (ω : Ω) ↦ @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ ‖f y‖) μ

Tactic:
rw [condExpKernel_eq]

Premises used: ProbabilityTheory.condExpKernel_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
hf_int : Integrable f μ
h : Nontrivial Ω
⊢ Integrable (ε := ℝ)
    (fun (a : Ω) ↦
      @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id a)) fun (y : Ω) ↦ ‖f (id a, y).2‖)
    μ

Tactic:
Integrable.integral_norm_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ))
      aemeasurable_id hf_int.comp_snd_map_prod_id

Premises used: inf_le_right, MeasureTheory.Integrable.integral_norm_condDistrib, MeasureTheory.Integrable.comp_snd_map_prod_id, aemeasurable_id, aemeasurable_id''
-- 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
hf_int : Integrable f μ
h : Nontrivial Ω
⊢ Integrable (ε := ℝ)
    (fun (ω : Ω) ↦
      @integral _ _ _ _ mΩ ((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯ : (a : Ω) → Measure Ω) ω)
        fun (y : Ω) ↦ ‖f y‖)
    μ

Tactic:
convert!
    Integrable.integral_norm_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_norm_condDistrib, MeasureTheory.Integrable.comp_snd_map_prod_id, aemeasurable_id, aemeasurable_id''
-- 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 μ
⊢ Nontrivial Ω

Tactic:
nontriviality Ω
-- 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 Ω
rw :
  Integrable (ε := ℝ)
    (fun (ω : Ω) ↦
      norm.{u_2} (E := F)
        (@integral _ _ _ _ mΩ ((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯ : (a : Ω) → Measure Ω) ω)
          fun (y : Ω) ↦ f y))
    μ
⊢ Integrable (ε := ℝ)
    (fun (ω : Ω) ↦
      norm.{u_2} (E := F) (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y))
    μ

Tactic:
rw [condExpKernel_eq]

Premises used: ProbabilityTheory.condExpKernel_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
hf_int : Integrable f μ
h : Nontrivial Ω
⊢ Integrable (ε := ℝ)
    (fun (a : Ω) ↦
      norm.{u_2} (E := F)
        (@integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id a)) fun (y : Ω) ↦ f (id a, y).2))
    μ

Tactic:
Integrable.norm_integral_condDistrib (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ))
      aemeasurable_id hf_int.comp_snd_map_prod_id

Premises used: MeasureTheory.Integrable.norm_integral_condDistrib, inf_le_right, MeasureTheory.Integrable.comp_snd_map_prod_id, aemeasurable_id, aemeasurable_id''
-- 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 (ε := ℝ)
    (fun (ω : Ω) ↦
      norm.{u_2} (E := F)
        (@integral _ _ _ _ mΩ ((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯ : (a : Ω) → Measure Ω) ω)
          fun (y : Ω) ↦ f y))
    μ

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

Premises used: MeasureTheory.Integrable.norm_integral_condDistrib, inf_le_right, MeasureTheory.Integrable.comp_snd_map_prod_id, aemeasurable_id, aemeasurable_id''
-- 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 Ω
rw :
  Integrable.{u_2, u_1} (ε := F)
    (fun (ω : Ω) ↦
      @integral _ _ _ _ mΩ ((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯ : (a : Ω) → Measure Ω) ω)
        fun (y : Ω) ↦ f y)
    μ
⊢ Integrable.{u_2, u_1} (ε := F)
    (fun (ω : Ω) ↦ @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y) μ

Tactic:
rw [condExpKernel_eq]

Premises used: ProbabilityTheory.condExpKernel_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
hf_int : Integrable f μ
h : Nontrivial Ω
⊢ Integrable.{u_2, u_1} (ε := F)
    (fun (a : Ω) ↦
      @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id a)) fun (y : Ω) ↦ f (id a, y).2)
    μ

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

Premises used: inf_le_right, MeasureTheory.Integrable.integral_condDistrib, MeasureTheory.Integrable.comp_snd_map_prod_id, aemeasurable_id, aemeasurable_id''