awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
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 ω, ω)) μ)
⊢ @HasFiniteIntegral _ F _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
have pos : ∫⁻ (a : Ω), ‖f (X a, a).2‖ₑ ∂μ < ∞
Tactic: rw [hasFiniteIntegral_iff_enorm, lintegral_map' hf.enorm (hX.prodMk aemeasurable_id)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
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) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
have neg : @Integrable F _ _ _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) 0
Tactic: rw [Measure.map_of_not_aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
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
⊢ @Integrable F _ _ _ Prod.instMeasurableSpace (fun (x : β × Ω) ↦ f x.2) (Measure.map (fun (ω : Ω) ↦ (X ω, ω)) μ)
have neg₁ : ¬AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ
Tactic: rw [Measure.map_of_not_aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Kernel.CondDistrib (goal)
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 μ
⊢ ¬AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ
have neg : ∀ (hX : AEMeasurable (β := β × Ω) (fun (ω : Ω) ↦ (X ω, ω)) μ), AEMeasurable X μ
Tactic: contrapose hX
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
⊢ IsMarkovKernel (condExpKernel μ m)
have inl : ∀ (h : IsEmpty Ω), IsMarkovKernel (condExpKernel μ m)
Tactic: rcases isEmpty_or_nonempty Ω with h | h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
inl : ∀ (h : IsEmpty Ω), IsMarkovKernel (condExpKernel μ m)
⊢ IsMarkovKernel (condExpKernel μ m)
have inr : ∀ (h : Nonempty Ω), IsMarkovKernel (condExpKernel μ m)
Tactic: rcases isEmpty_or_nonempty Ω with h | h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
h : Nonempty Ω
⊢ IsMarkovKernel (condExpKernel μ m)
have simpa : IsMarkovKernel (mβ := mΩ) (Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id sorry)
Tactic: simpa [condExpKernel, h] using by infer_instance
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hm : m ≤ mΩ
⊢ μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ
have inl : ∀ (h : IsEmpty Ω), μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ
Tactic: rcases isEmpty_or_nonempty Ω with h | h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
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 ω)) μ
⊢ μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ
have inr : ∀ (h : Nonempty Ω), μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ
Tactic: rcases isEmpty_or_nonempty Ω with h | h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hm : m ≤ mΩ
h : Nonempty Ω
⊢ μ.trim hm ⊗ₘ condExpKernel μ m = Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ
have inr : Eq (α := Measure (Ω × Ω)) (μ.trim hm ⊗ₘ Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id sorry)
  (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)
Tactic: rw [condExpKernel_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (hypothesis)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hm : m ≤ mΩ
h : Nonempty Ω
⊢ Eq (α := Measure (Ω × Ω)) (μ.trim hm ⊗ₘ Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯)
    (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)
have this : m ⊓ mΩ = m
Tactic: have : m ⊓ mΩ = m := inf_of_le_left hm
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (hypothesis)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hm : m ≤ mΩ
h : Nonempty Ω
this : m ⊓ mΩ = m
⊢ Eq (α := Measure (Ω × Ω)) (μ.trim hm ⊗ₘ Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯)
    (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)
have h₁ : 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
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
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)) μ)
⊢ Eq (α := Measure (Ω × Ω)) (μ.trim hm ⊗ₘ Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯)
    (Measure.map (fun (ω : Ω) ↦ (id ω, id ω)) μ)
have inr : Eq (α := Measure (Ω × Ω)) (Measure.map id μ ⊗ₘ Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id sorry)
  (Measure.map id μ ⊗ₘ condDistrib id id μ)
Tactic: rw [← h, trim_eq_map hm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
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)) μ)
⊢ Eq (α := Measure (Ω × Ω)) (Measure.map id μ ⊗ₘ Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯)
    (Measure.map id μ ⊗ₘ condDistrib id id μ)
have inr : Eq (α := Kernel Ω Ω) (Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id sorry) (condDistrib id id μ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
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)) μ)
⊢ Eq (α := Kernel Ω Ω) (Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯) (condDistrib id id μ)
have inr : ∀ (a : Ω) (s : Set Ω) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id sorry : (a : Ω) → Measure Ω) a : Measure Ω) :
          (a : Set Ω) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((condDistrib id id μ : (a : Ω) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
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∞)
    ((((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∞)
have 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∞)
Tactic: simp only [Kernel.coe_comap, Function.comp_apply, id_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
hm : m ≤ mΩ
⊢ (⇑(condExpKernel μ m) : (a : Ω) → Measure Ω) ∘ₘ μ.trim hm = μ
have hX : Measurable.{u_1, u_1} (α := Ω) id
Tactic: rw [← Measure.snd_compProd, compProd_trim_condExpKernel, @Measure.snd_map_prodMk, Measure.map_id]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (hypothesis)
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
have a : Nontrivial Ω
Tactic: nontriviality Ω
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
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Ω ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y
have simp_rw : StronglyMeasurable.{u_1, u_2} (β := F) fun (ω : Ω) ↦
  @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id ω)) fun (y : Ω) ↦ f y
Tactic: simp_rw [condExpKernel_apply_eq_condDistrib]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (hypothesis)
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 μ
⊢ AEStronglyMeasurable.{u_1, u_2} (β := F)
    (fun (ω : Ω) ↦ @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y) μ
have a : Nontrivial Ω
Tactic: nontriviality Ω
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
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Ω ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y) μ
have simp_rw : AEStronglyMeasurable.{u_1, u_2} (β := F)
  (fun (ω : Ω) ↦ @integral _ _ _ _ mΩ ((condDistrib id id μ : (a : Ω) → Measure Ω) (id ω)) fun (y : Ω) ↦ f y) μ
Tactic: simp_rw [condExpKernel_apply_eq_condDistrib]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
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Ω ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y) μ
have rw : AEStronglyMeasurable.{u_1, u_2} (β := F)
  (fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id sorry : (a : Ω) → Measure Ω) ω)
      fun (y : Ω) ↦ f y)
  μ
Tactic: rw [condExpKernel_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (hypothesis)
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Ω ((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id ⋯ : (a : Ω) → Measure Ω) ω)
        fun (y : Ω) ↦ f y)
    μ
have 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)
  μ
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Ω))
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (hypothesis)
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)
    μ
have 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)
  μ
Tactic: rw [MeasurableSpace.comap_id] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
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
have refine : ∀ᵐ (ω : Ω) ∂(⇑(condExpKernel μ m) : (a : Ω) → Measure Ω) ∘ₘ μ.trim hm, f ω = AEStronglyMeasurable.mk f hf ω
Tactic: refine Measure.ae_ae_of_ae_comp ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
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 μ
⊢ ∀ᵐ (ω : Ω) ∂(⇑(condExpKernel μ m) : (a : Ω) → Measure Ω) ∘ₘ μ.trim hm, f ω = AEStronglyMeasurable.mk f hf ω
have rw : ∀ᵐ (ω : Ω) ∂μ, f ω = AEStronglyMeasurable.mk f hf ω
Tactic: rw [condExpKernel_comp_trim hm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (hypothesis)
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 μ
⊢ ∀ᵐ (ω : Ω) ∂μ, @Integrable _ _ _ _ mΩ f ((condExpKernel μ m : (a : Ω) → Measure Ω) ω)
have a : Nontrivial Ω
Tactic: nontriviality Ω
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (hypothesis)
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 μ
⊢ Integrable (ε := ℝ)
    (fun (ω : Ω) ↦ @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ ‖f y‖) μ
have a : Nontrivial Ω
Tactic: nontriviality Ω
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
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Ω ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ ‖f y‖) μ
have rw : Integrable (ε := ℝ)
  (fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id sorry : (a : Ω) → Measure Ω) ω)
      fun (y : Ω) ↦ ‖f y‖)
  μ
Tactic: rw [condExpKernel_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (hypothesis)
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 μ
⊢ Integrable (ε := ℝ)
    (fun (ω : Ω) ↦
      norm.{u_2} (E := F) (@integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y))
    μ
have a : Nontrivial Ω
Tactic: nontriviality Ω
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
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Ω ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y))
    μ
have rw : Integrable (ε := ℝ)
  (fun (ω : Ω) ↦
    norm.{u_2} (E := F)
      (@integral _ _ _ _ mΩ ((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id sorry : (a : Ω) → Measure Ω) ω)
        fun (y : Ω) ↦ f y))
  μ
Tactic: rw [condExpKernel_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (hypothesis)
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 μ
⊢ Integrable.{u_2, u_1} (ε := F)
    (fun (ω : Ω) ↦ @integral _ _ _ _ mΩ ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y) μ
have a : Nontrivial Ω
Tactic: nontriviality Ω
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
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Ω ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) fun (y : Ω) ↦ f y) μ
have rw : Integrable.{u_2, u_1} (ε := F)
  (fun (ω : Ω) ↦
    @integral _ _ _ _ mΩ ((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id sorry : (a : Ω) → Measure Ω) ω)
      fun (y : Ω) ↦ f y)
  μ
Tactic: rw [condExpKernel_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (hypothesis)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ Measure.real (m := mΩ) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) s) μ
have a : Nontrivial Ω
Tactic: nontriviality Ω
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
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Ω) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) s) μ
have rw : Integrable (ε := ℝ)
  (fun (ω : Ω) ↦
    Measure.real (m := mΩ) ((Kernel.comap (mα := m ⊓ mΩ) (condDistrib id id μ) id sorry : (a : Ω) → Measure Ω) ω) s)
  μ
Tactic: rw [condExpKernel_eq]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ Measure.real (m := mΩ) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) s)
    μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ]
have inl : ∀ (h : IsEmpty Ω),
  (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
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
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Ω]
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ Measure.real (m := mΩ) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) s)
    μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ]
have inr : ∀ (h : Nonempty Ω),
  (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
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (hypothesis)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h : IsEmpty Ω
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ Measure.real (m := mΩ) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) s)
    μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ]
have this : μ = 0
Tactic: have : μ = 0 := Measure.eq_zero_of_isEmpty μ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (hypothesis)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst : StandardBorelSpace Ω
μ : Measure Ω
inst_1 : IsFiniteMeasure μ
s : Set Ω
hs : MeasurableSet s
h : Nonempty Ω
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ Measure.real (m := mΩ) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) s)
    μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ]
have 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Ω)]
Tactic: have h := condDistrib_ae_eq_condExp (μ := μ)
    (measurable_id'' (inf_le_right : m ⊓ mΩ ≤ mΩ)) measurable_id hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (hypothesis)
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 (ω : Ω) ↦ Measure.real (m := mΩ) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) s)
    μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ]
have h₁ : (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Kernel.Condexp (goal)
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Ω) ((condExpKernel μ m : (a : Ω) → Measure Ω) ω) s)
    μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ]
have inr : (ae μ).EventuallyEq (β := ℝ)
  (fun (ω : Ω) ↦ Measure.real (m := mΩ) ((condDistrib id id μ : (a : Ω) → Measure Ω) (id ω)) s)
  μ[s.indicator fun (ω : Ω) ↦ 1 | m ⊓ mΩ]
Tactic: simp_rw [condExpKernel_apply_eq_condDistrib]