awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map (α := β × Ω) Prod.snd (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [Measure.map_apply measurable_snd hs]

Premises used: MeasureTheory.Measure.map_apply, measurable_snd
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
pos :
  ∀ (hX : AEMeasurable X μ),
    Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
      (0 : ℝ≥0∞)
neg :
  ∀ (hX : ¬AEMeasurable X μ),
    Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
by_cases hX : AEMeasurable X μ

Premises used: AEMeasurable
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hX : AEMeasurable X μ
pos :
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (preimage (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) (Prod.snd ⁻¹' s)) : ℝ≥0∞)
    (0 : ℝ≥0∞)
pos₁ : AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ
pos₂ : MeasurableSet (α := β × Ω) (Prod.snd ⁻¹' s)
⊢ Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [Measure.map_apply_of_aemeasurable]

Premises used: MeasureTheory.Measure.map_apply_of_aemeasurable
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hX : AEMeasurable X μ
pos : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (preimage (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) (Prod.snd ⁻¹' s)) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [← univ_prod, mk_preimage_prod, preimage_univ, univ_inter, preimage_id']

Premises used: Set.univ_prod, Set.preimage_id', Set.univ_inter, Set.preimage_univ, Set.mk_preimage_prod
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hX : AEMeasurable X μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
hμs
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hX : AEMeasurable X μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact hμs
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hX : AEMeasurable X μ
⊢ AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ

Tactic:
hX.prodMk aemeasurable_id

Premises used: AEMeasurable.prodMk, aemeasurable_id
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hX : AEMeasurable X μ
⊢ AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ

Tactic:
exact hX.prodMk aemeasurable_id

Premises used: AEMeasurable.prodMk, aemeasurable_id
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hX : AEMeasurable X μ
⊢ MeasurableSet (α := β × Ω) (Prod.snd ⁻¹' s)

Tactic:
measurable_snd hs

Premises used: measurable_snd
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hX : AEMeasurable X μ
⊢ MeasurableSet (α := β × Ω) (Prod.snd ⁻¹' s)

Tactic:
exact measurable_snd hs

Premises used: measurable_snd
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hX : ¬AEMeasurable X μ
neg : Eq (α := ℝ≥0∞) ((0 : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)
neg₁ : ¬AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ
⊢ Eq (α := ℝ≥0∞) ((Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
rw [Measure.map_of_not_aemeasurable]

Premises used: MeasureTheory.Measure.map_of_not_aemeasurable
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hX : ¬AEMeasurable X μ
⊢ Eq (α := ℝ≥0∞) ((0 : (a : Set (β × Ω)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hX : ¬AEMeasurable X μ
neg : ∀ (hX : AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ), AEMeasurable X μ
⊢ ¬AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ

Tactic:
contrapose hX
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hX : AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ
⊢ AEMeasurable X μ

Tactic:
measurable_fst.comp_aemeasurable hX

Premises used: Measurable.comp_aemeasurable, measurable_fst
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hX : AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ
⊢ AEMeasurable X μ

Tactic:
exact measurable_fst.comp_aemeasurable hX

Premises used: Measurable.comp_aemeasurable, measurable_fst
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
pos :
  ∀ (hX : AEMeasurable X μ),
    @Integrable F _ _ _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
neg :
  ∀ (hX : ¬AEMeasurable X μ),
    @Integrable F _ _ _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
⊢ @Integrable F _ _ _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)

Tactic:
by_cases hX : AEMeasurable X μ

Premises used: AEMeasurable
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (β := F) (m₀ := Prod.instMeasurableSpace) (fun (x : β × Ω) ↦ f x.2)
    (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)

Tactic:
have hf := hf_int.1.comp_snd_map_prodMk X (mΩ := mΩ) (mβ := mβ)
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable X μ
hf :
  AEStronglyMeasurable (β := F) (m₀ := Prod.instMeasurableSpace) (fun (x : β × Ω) ↦ f x.2)
    (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
⊢ @Integrable F _ _ _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)

Tactic:
⟨hf, ?_⟩

Premises used: MeasureTheory.Integrable, And.intro
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable X μ
hf :
  AEStronglyMeasurable (β := F) (m₀ := Prod.instMeasurableSpace) (fun (x : β × Ω) ↦ f x.2)
    (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
pos :
  @HasFiniteIntegral _ F _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
⊢ @Integrable F _ _ _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)

Tactic:
refine ⟨hf, ?_⟩
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable X μ
hf :
  AEStronglyMeasurable (β := F) (m₀ := Prod.instMeasurableSpace) (fun (x : β × Ω) ↦ f x.2)
    (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
pos : ∫⁻ (a : Ω), ‖f (X a, a).2‖ₑ ∂μ < ∞
⊢ @HasFiniteIntegral _ F _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)

Tactic:
rw [hasFiniteIntegral_iff_enorm, lintegral_map' hf.enorm (hX.prodMk aemeasurable_id)]

Premises used: AEMeasurable.prodMk, MeasureTheory.AEStronglyMeasurable.enorm, aemeasurable_id, MeasureTheory.lintegral_map', MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable X μ
hf :
  AEStronglyMeasurable (β := F) (m₀ := Prod.instMeasurableSpace) (fun (x : β × Ω) ↦ f x.2)
    (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
⊢ ∫⁻ (a : Ω), ‖f (X a, a).2‖ₑ ∂μ < ∞

Tactic:
hf_int.2

Premises used: And.right, MeasureTheory.HasFiniteIntegral
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable X μ
hf :
  AEStronglyMeasurable (β := F) (m₀ := Prod.instMeasurableSpace) (fun (x : β × Ω) ↦ f x.2)
    (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
⊢ ∫⁻ (a : Ω), ‖f (X a, a).2‖ₑ ∂μ < ∞

Tactic:
exact hf_int.2

Premises used: And.right
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : ¬AEMeasurable X μ
neg : @Integrable F _ _ _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) 0
neg₁ : ¬AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ
⊢ @Integrable F _ _ _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)

Tactic:
rw [Measure.map_of_not_aemeasurable]

Premises used: MeasureTheory.Measure.map_of_not_aemeasurable
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : ¬AEMeasurable X μ
⊢ @Integrable F _ _ _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) 0

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : ¬AEMeasurable X μ
neg : ∀ (hX : AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ), AEMeasurable X μ
⊢ ¬AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ

Tactic:
contrapose hX
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ
⊢ AEMeasurable X μ

Tactic:
measurable_fst.comp_aemeasurable hX

Premises used: Measurable.comp_aemeasurable, measurable_fst
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
f : Ω → F
hf_int : Integrable f μ
hX : AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ
⊢ AEMeasurable X μ

Tactic:
exact measurable_fst.comp_aemeasurable hX

Premises used: Measurable.comp_aemeasurable, measurable_fst
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
x : MeasurableSpace Ω
inst : TopologicalSpace F
X : Ω → β
μ : Measure Ω
hX : Measurable X
f : Ω → F
⊢ AEStronglyMeasurable (β := F) (m₀ := Prod.instMeasurableSpace) (fun (x : β × Ω) ↦ f x.2)
      (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ) ↔
    AEStronglyMeasurable f μ

Tactic:
⟨fun h => h.comp_measurable (hX.prodMk measurable_id), fun h => h.comp_snd_map_prodMk X⟩

Premises used: MeasureTheory.AEStronglyMeasurable.comp_measurable, measurable_id, Measurable.prodMk, Iff.intro, MeasureTheory.AEStronglyMeasurable.comp_snd_map_prodMk
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
mβ : MeasurableSpace β
Ω : Type u_5
x : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
hX : Measurable X
f : Ω → F
⊢ @Integrable F _ _ _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ) ↔
    Integrable f μ

Tactic:
⟨fun h => h.comp_measurable (hX.prodMk measurable_id), fun h => h.comp_snd_map_prodMk X⟩

Premises used: measurable_id, MeasureTheory.Integrable.comp_snd_map_prodMk, MeasureTheory.Integrable.comp_measurable, Measurable.prodMk, Iff.intro
-- Module: Mathlib.Probability.Kernel.CondDistrib
Goal:
β : Type u_2
Ω : Type u_3
F : Type u_4
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
mβ : MeasurableSpace β
inst_4 : NormedSpace ℝ F
inst_5 : CompleteSpace F
X : Ω → β
μ : Measure Ω
inst_6 : IsFiniteMeasure μ
hX : Measurable X
f : Ω → F
hf_int : Integrable f μ
⊢ μ[f | MeasurableSpace.comap X mβ] =ᶠ[ae μ] fun (a : Ω) ↦
    @integral _ _ _ _ inst (((condDistrib id X μ : Kernel β Ω) : (a : β) → Measure Ω) (X a)) fun (y : Ω) ↦ f y

Tactic:
condExp_prod_ae_eq_integral_condDistrib' hX aemeasurable_id (hf_int.comp_snd_map_prodMk X)

Premises used: MeasureTheory.Integrable.comp_snd_map_prodMk, aemeasurable_id, ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib'
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst : TopologicalSpace F
hm : m ≤ mΩ
hf : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable.{u_1, u_2} (β := F) (m₀ := m.prod mΩ) (fun (x : Ω × Ω) ↦ f x.2)
    (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)

Tactic:
simpa using (aestronglyMeasurable_comp_snd_map_prodMk_iff hm).mpr hf

Premises used: Iff.mpr, ProbabilityTheory.aestronglyMeasurable_comp_snd_map_prodMk_iff
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
μ : Measure Ω
f : Ω → F
inst : NormedAddCommGroup F
hf : Integrable f μ
⊢ @Integrable.{u_2, u_1} F _ _ _ (m.prod mΩ) (fun (x : Ω × Ω) ↦ f x.2) (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)

Tactic:
simpa using Integrable.comp_snd_map_prodMk id hf

Premises used: MeasureTheory.Integrable.comp_snd_map_prodMk, id
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
h : Nonempty Ω
m : MeasurableSpace Ω
⊢ condExpKernel μ m = Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯

Tactic:
simp [condExpKernel, h]

Premises used: ProbabilityTheory.condExpKernel
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inst_2 : Nonempty Ω
ω : Ω
⊢ Eq (α := Measure Ω) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω : Measure Ω)
    ((condDistrib id id μ : (a : Ω) → Measure Ω) (id ω) : Measure Ω)

Tactic:
simp [condExpKernel_eq, Kernel.comap_apply]

Premises used: ProbabilityTheory.condExpKernel_eq, ProbabilityTheory.Kernel.comap_apply
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inl : ∀ (h : IsEmpty Ω), IsMarkovKernel (condExpKernel μ m)
inr : ∀ (h : Nonempty Ω), IsMarkovKernel (condExpKernel μ m)
⊢ IsMarkovKernel (condExpKernel μ m)

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 μ
h : IsEmpty Ω
⊢ IsMarkovKernel (condExpKernel μ m)

Tactic:
⟨fun a ↦ (IsEmpty.false a).elim⟩

Premises used: False.elim, IsEmpty.false, ProbabilityTheory.IsMarkovKernel.mk
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
h : IsEmpty Ω
⊢ IsMarkovKernel (condExpKernel μ m)

Tactic:
exact ⟨fun a ↦ (IsEmpty.false a).elim⟩
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
h : Nonempty Ω
⊢ IsMarkovKernel (mβ := mΩ) (Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
h : Nonempty Ω
simpa : IsMarkovKernel (mβ := mΩ) (Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯)
⊢ IsMarkovKernel (condExpKernel μ m)

Tactic:
simpa [condExpKernel, h] using by infer_instance

Premises used: ProbabilityTheory.condExpKernel
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hm : m ≤ mΩ
inl : ∀ (h : IsEmpty Ω), μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ
inr : ∀ (h : Nonempty Ω), μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ
⊢ μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ

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 μ
hm : m ≤ mΩ
h : IsEmpty Ω
⊢ μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ

Tactic:
simp [Measure.eq_zero_of_isEmpty μ]

Premises used: MeasureTheory.Measure.eq_zero_of_isEmpty
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hm : m ≤ mΩ
h : Nonempty Ω
inr :
  Eq (α := Measure (Ω × Ω)) (μ.trim hm ⊗ₘ Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯)
    (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)
⊢ μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ

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 μ
hm : m ≤ mΩ
h : Nonempty Ω
⊢ m ⊓ mΩ = m

Tactic:
have : m ⊓ mΩ = m := inf_of_le_left hm
-- Module: Mathlib.Probability.Kernel.Condexp
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hm : m ≤ mΩ
h : Nonempty Ω
this : m ⊓ mΩ = m
⊢ Eq (α := Measure (Ω × Ω)) (Measure.map id μ ⊗ₘ condDistrib id id μ) (Measure.map (fun (a : Ω) ↦ (id a, id a)) μ)

Tactic:
have h := compProd_map_condDistrib (mβ := m) (μ := μ) (X := id) measurable_id.aemeasurable
-- 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 :
  Eq (α := Measure (Ω × Ω)) (Measure.map id μ ⊗ₘ Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯)
    (Measure.map id μ ⊗ₘ condDistrib id id μ)
⊢ Eq (α := Measure (Ω × Ω)) (μ.trim hm ⊗ₘ Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯)
    (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)

Tactic:
rw [← h, trim_eq_map hm]

Premises used: MeasureTheory.trim_eq_map
-- 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 : Eq (α := Kernel Ω Ω) (Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯) (condDistrib id id μ)
⊢ Eq (α := Measure (Ω × Ω)) (Measure.map id μ ⊗ₘ Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯)
    (Measure.map id μ ⊗ₘ condDistrib id id μ)

Tactic:
congr 1