awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
f : β × Ω → ℝ≥0∞
hf : Measurable f
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
    ∫⁻ (x : β × Ω) in SProd.sprod (α := Set β) Set.univ t, f x ∂ρ
have rw : ∫⁻ (b : β), ∫⁻ (ω : Ω) in t, f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst =
  ∫⁻ (b : β) in Set.univ, ∫⁻ (ω : Ω) in t, f (b, ω) ∂(ρ.condKernel : (a : β) → Measure Ω) b ∂ρ.fst
Tactic: rw [← setLIntegral_condKernel hf MeasurableSet.univ ht]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (hypothesis)
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
hf : AEStronglyMeasurable f ρ
⊢ AEStronglyMeasurable.{u_1, u_3} (β := E)
    (fun (x : β) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : β) → Measure Ω) x) fun (y : Ω) ↦ f (x, y)) ρ.fst
have hf₁ : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)
Tactic: rw [← ρ.disintegrate ρ.condKernel] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
hf : Integrable f ρ
| ∫ (x : β × Ω), f x ∂ρ
have rw : ∫ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel
Tactic: rw [← ρ.disintegrate ρ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
hf : Integrable f ρ
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (b : β), @integral _ _ _ _ inst ((ρ.condKernel : (a : β) → Measure Ω) b) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (x : β × Ω), f x ∂ρ)
have conv_rhs : Eq.{u_3 + 1} (α := E)
  (∫ (b : β), @integral _ _ _ _ inst ((ρ.condKernel : (a : β) → Measure Ω) b) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
  (∫ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel)
Tactic: conv_rhs => rw [← ρ.disintegrate ρ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (hypothesis)
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
hf : Integrable f ρ
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (b : β), @integral _ _ _ _ inst ((ρ.condKernel : (a : β) → Measure Ω) b) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel)
have hf₁ : Integrable f (ρ.fst ⊗ₘ ρ.condKernel)
Tactic: rw [← ρ.disintegrate ρ.condKernel] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
hf : Integrable f (ρ.fst ⊗ₘ ρ.condKernel)
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (b : β), @integral _ _ _ _ inst ((ρ.condKernel : (a : β) → Measure Ω) b) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (x : β × Ω), f x ∂ρ.fst ⊗ₘ ρ.condKernel)
have rw : Eq.{u_3 + 1} (α := E)
  (∫ (b : β), @integral _ _ _ _ inst ((ρ.condKernel : (a : β) → Measure Ω) b) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
  (∫ (a : β), @integral _ _ _ _ inst ((ρ.condKernel : (a : β) → Measure Ω) a) fun (b : Ω) ↦ f (a, b) ∂ρ.fst)
Tactic: rw [integral_compProd hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ρ
| ∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ
have rw : ∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel
Tactic: rw [← ρ.disintegrate ρ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ρ
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (b : β) in s,
      @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) b) t) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ)
have conv_rhs : Eq.{u_3 + 1} (α := E)
  (∫ (b : β) in s,
    @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) b) t) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
  (∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel)
Tactic: conv_rhs => rw [← ρ.disintegrate ρ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (hypothesis)
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) ρ
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (b : β) in s,
      @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) b) t) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel)
have hf₁ : IntegrableOn f (s ×ˢ t) (ρ.fst ⊗ₘ ρ.condKernel)
Tactic: rw [← ρ.disintegrate ρ.condKernel] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (s ×ˢ t) (ρ.fst ⊗ₘ ρ.condKernel)
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (b : β) in s,
      @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) b) t) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (x : β × Ω) in s ×ˢ t, f x ∂ρ.fst ⊗ₘ ρ.condKernel)
have rw : Eq.{u_3 + 1} (α := E)
  (∫ (b : β) in s,
    @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) b) t) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
  (∫ (a : β) in s,
    @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) a) t) fun (b : Ω) ↦ f (a, b) ∂ρ.fst)
Tactic: rw [setIntegral_compProd hs ht hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
s : Set β
hs : MeasurableSet s
hf : IntegrableOn f (SProd.sprod (β := Set Ω) s Set.univ) ρ
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (b : β) in s, @integral _ _ _ _ inst ((ρ.condKernel : (a : β) → Measure Ω) b) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (x : β × Ω) in SProd.sprod (β := Set Ω) s Set.univ, f x ∂ρ)
have rw : Eq.{u_3 + 1} (α := E)
  (∫ (b : β) in s, @integral _ _ _ _ inst ((ρ.condKernel : (a : β) → Measure Ω) b) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
  (∫ (b : β) in s,
    @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) b) Set.univ) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
Tactic: rw [← setIntegral_condKernel hs MeasurableSet.univ hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
ρ : Measure (β × Ω)
inst_3 : IsFiniteMeasure ρ
E : Type u_3
f : β × Ω → E
inst_4 : NormedAddCommGroup E
inst_5 : NormedSpace ℝ E
t : Set Ω
ht : MeasurableSet t
hf : IntegrableOn f (SProd.sprod (α := Set β) Set.univ t) ρ
⊢ Eq.{u_3 + 1} (α := E)
    (∫ (b : β),
      @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) b) t) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
    (∫ (x : β × Ω) in SProd.sprod (α := Set β) Set.univ t, f x ∂ρ)
have rw : Eq.{u_3 + 1} (α := E)
  (∫ (b : β),
    @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) b) t) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
  (∫ (b : β) in Set.univ,
    @integral _ _ _ _ inst (restrict ((ρ.condKernel : (a : β) → Measure Ω) b) t) fun (ω : Ω) ↦ f (b, ω) ∂ρ.fst)
Tactic: rw [← setIntegral_condKernel MeasurableSet.univ ht hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (hypothesis)
Goal:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
f : α × Ω → F
hf : AEStronglyMeasurable f ρ
⊢ (∀ᵐ (a : α) ∂ρ.fst,
        @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)) ∧
      Integrable (ε := ℝ)
        (fun (a : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (ω : Ω) ↦ ‖f (a, ω)‖) ρ.fst ↔
    Integrable f ρ
have hf₁ : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)
Tactic: rw [← ρ.disintegrate ρ.condKernel] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
f : α × Ω → F
hf : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)
| Integrable f ρ
have rw : Integrable f (ρ.fst ⊗ₘ ρ.condKernel)
Tactic: rw [← ρ.disintegrate ρ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
f : α × Ω → F
hf : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)
⊢ (∀ᵐ (a : α) ∂ρ.fst,
        @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)) ∧
      Integrable (ε := ℝ)
        (fun (a : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (ω : Ω) ↦ ‖f (a, ω)‖) ρ.fst ↔
    Integrable f ρ
have conv_rhs : (∀ᵐ (a : α) ∂ρ.fst,
      @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)) ∧
    Integrable (ε := ℝ)
      (fun (a : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (ω : Ω) ↦ ‖f (a, ω)‖) ρ.fst ↔
  Integrable f (ρ.fst ⊗ₘ ρ.condKernel)
Tactic: conv_rhs => rw [← ρ.disintegrate ρ.condKernel]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
f : α × Ω → F
hf : AEStronglyMeasurable f (ρ.fst ⊗ₘ ρ.condKernel)
⊢ (∀ᵐ (a : α) ∂ρ.fst,
        @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)) ∧
      Integrable (ε := ℝ)
        (fun (a : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (ω : Ω) ↦ ‖f (a, ω)‖) ρ.fst ↔
    Integrable f (ρ.fst ⊗ₘ ρ.condKernel)
have rw : (∀ᵐ (a : α) ∂ρ.fst,
      @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)) ∧
    Integrable (ε := ℝ)
      (fun (a : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (ω : Ω) ↦ ‖f (a, ω)‖) ρ.fst ↔
  (∀ᵐ (x : α) ∂ρ.fst,
      @Integrable.{u_4, u_2} F _ _ _ inst (fun (y : Ω) ↦ f (x, y)) ((ρ.condKernel : (a : α) → Measure Ω) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ ‖f (x, y)‖) ρ.fst
Tactic: rw [Measure.integrable_compProd_iff hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (hypothesis)
Goal:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
f : α × Ω → F
hf_int : Integrable f ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst,
    @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)
have hf_ae : AEStronglyMeasurable f ρ
Tactic: have hf_ae : AEStronglyMeasurable f ρ := hf_int.1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (hypothesis)
Goal:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
f : α × Ω → F
hf_int : Integrable f ρ
hf_ae : AEStronglyMeasurable f ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst,
    @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)
have hf_int₁ : (∀ᵐ (a : α) ∂ρ.fst,
    @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)) ∧
  Integrable (ε := ℝ)
    (fun (a : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (ω : Ω) ↦ ‖f (a, ω)‖) ρ.fst
Tactic: rw [← hf_ae.ae_integrable_condKernel_iff] at hf_int
Cleared hypotheses: hf_int, hf_ae
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (hypothesis)
Goal:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
f : α × Ω → F
hf_int : Integrable f ρ
⊢ Integrable (ε := ℝ)
    (fun (x : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ ‖f (x, y)‖) ρ.fst
have hf_ae : AEStronglyMeasurable f ρ
Tactic: have hf_ae : AEStronglyMeasurable f ρ := hf_int.1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (hypothesis)
Goal:
α : Type u_1
Ω : Type u_2
F : Type u_4
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup F
ρ : Measure (α × Ω)
inst_4 : IsFiniteMeasure ρ
f : α × Ω → F
hf_int : Integrable f ρ
hf_ae : AEStronglyMeasurable f ρ
⊢ Integrable (ε := ℝ)
    (fun (x : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ ‖f (x, y)‖) ρ.fst
have hf_int₁ : (∀ᵐ (a : α) ∂ρ.fst,
    @Integrable.{u_4, u_2} F _ _ _ inst (fun (ω : Ω) ↦ f (a, ω)) ((ρ.condKernel : (a : α) → Measure Ω) a)) ∧
  Integrable (ε := ℝ)
    (fun (a : α) ↦ @integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (ω : Ω) ↦ ‖f (a, ω)‖) ρ.fst
Tactic: rw [← hf_ae.ae_integrable_condKernel_iff] at hf_int
Cleared hypotheses: hf_int, hf_ae
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst_5 : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
⊢ Integrable (ε := ℝ)
    (fun (x : α) ↦
      Norm.norm.{u_3} (E := E) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ f (x, y)))
    ρ.fst
have refine : ∀ᵐ (a : α) ∂ρ.fst,
  ‖Norm.norm.{u_3} (E := E) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (y : Ω) ↦ f (a, y))‖ ≤
    Norm.norm (E := ℝ) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (y : Ω) ↦ ‖f (a, y)‖)
Tactic: refine hf_int.integral_norm_condKernel.mono hf_int.1.integral_condKernel.norm ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst_5 : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst,
    ‖Norm.norm.{u_3} (E := E)
          (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (y : Ω) ↦ f (a, y))‖ ≤
      Norm.norm (E := ℝ) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) a) fun (y : Ω) ↦ ‖f (a, y)‖)
have refine : ∀ (x : α),
  ‖Norm.norm.{u_3} (E := E) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ f (x, y))‖ ≤
    Norm.norm (E := ℝ) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ ‖f (x, y)‖)
Tactic: refine Filter.Eventually.of_forall fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst_5 : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
x : α
⊢ ‖Norm.norm.{u_3} (E := E) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ f (x, y))‖ ≤
    Norm.norm (E := ℝ) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ ‖f (x, y)‖)
have rw : Norm.norm.{u_3} (E := E) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ f (x, y)) ≤
  Norm.norm (E := ℝ) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ ‖f (x, y)‖)
Tactic: rw [norm_norm]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Integral (goal)
Goal:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
inst_2 : Nonempty Ω
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst_5 : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
x : α
⊢ Norm.norm.{u_3} (E := E) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ f (x, y)) ≤
    Norm.norm (E := ℝ) (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (y : Ω) ↦ ‖f (x, y)‖)
have refine : LE.le (α := ℝ) 0 (@integral _ _ _ _ inst ((ρ.condKernel : (a : α) → Measure Ω) x) fun (a : Ω) ↦ ‖f (x, a)‖)
Tactic: refine (norm_integral_le_integral_norm _).trans_eq (Real.norm_of_nonneg ?_).symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
f : α → StieltjesFunction ℝ
hf : ∀ (q : ℝ), Measurable (β := ℝ) fun (a : α) ↦ (↑(f a) : ℝ → ℝ) q
hf_bot : ∀ (a : α), Tendsto (↑(f a) : ℝ → ℝ) atBot (𝓝 0)
hf_top : ∀ (a : α), Tendsto (↑(f a) : ℝ → ℝ) atTop (𝓝 1)
this : ∀ (a : α), IsProbabilityMeasure (m0 := Real.measurableSpace) (f a).measure
⊢ ∀ (s : Set ℝ),
    Membership.mem (γ := Set (Set ℝ)) (range Iic) s →
      Measurable (β := ℝ≥0∞) fun (a : α) ↦ ((f a).measure : (a : Set ℝ) → ℝ≥0∞) s
have simp_rw : ∀ (i : ℝ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ ENNReal.ofReal ((↑(f a) : ℝ → ℝ) i)
Tactic: simp_rw [forall_mem_range, StieltjesFunction.measure_Iic (f _) (hf_bot _), sub_zero]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
a : α
⊢ IsRatStieltjesPoint (fun (p : Unit × α) ↦ f p.2) ((), a) ↔ IsRatStieltjesPoint f a
have mp : IsRatStieltjesPoint (fun (p : Unit × α) ↦ f p.2) ((), a) → IsRatStieltjesPoint f a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
a : α
mp : IsRatStieltjesPoint (fun (p : Unit × α) ↦ f p.2) ((), a) → IsRatStieltjesPoint f a
⊢ IsRatStieltjesPoint (fun (p : Unit × α) ↦ f p.2) ((), a) ↔ IsRatStieltjesPoint f a
have mpr : IsRatStieltjesPoint f a → IsRatStieltjesPoint (fun (p : Unit × α) ↦ f p.2) ((), a)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
⊢ MeasurableSet.{u_1} (α := α) {a : α | ∀ (q r : ℚ), q ≤ r → f a q ≤ f a r}
have simp_rw : MeasurableSet.{u_1} (α := α) (⋂ (i : ℚ), ⋂ (i_1 : ℚ), ⋂ (_ : i ≤ i_1), {x : α | f x i ≤ f x i_1})
Tactic: simp_rw [Set.setOf_forall]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
⊢ MeasurableSet.{u_1} (α := α) (⋂ (i : ℚ), ⋂ (i_1 : ℚ), ⋂ (_ : i ≤ i_1), {x : α | f x i ≤ f x i_1})
have refine : ∀ (q : ℚ), MeasurableSet.{u_1} (α := α) (⋂ (i : ℚ), ⋂ (_ : q ≤ i), {x : α | f x q ≤ f x i})
Tactic: refine MeasurableSet.iInter (fun q ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
q : ℚ
⊢ MeasurableSet.{u_1} (α := α) (⋂ (i : ℚ), ⋂ (_ : q ≤ i), {x : α | f x q ≤ f x i})
have refine : ∀ (r : ℚ), MeasurableSet.{u_1} (α := α) (⋂ (_ : q ≤ r), {x : α | f x q ≤ f x r})
Tactic: refine MeasurableSet.iInter (fun r ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (goal)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
q r : ℚ
⊢ MeasurableSet.{u_1} (α := α) (⋂ (_ : q ≤ r), {x : α | f x q ≤ f x r})
have refine : q ≤ r → MeasurableSet.{u_1} (α := α) {x : α | f x q ≤ f x r}
Tactic: refine MeasurableSet.iInter (fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (hypothesis)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
⊢ MeasurableSet.{u_1} (α := α) {a : α | IsRatStieltjesPoint f a}
have h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
Tactic: have h1 : MeasurableSet {a | Monotone (f a)} := by
    change MeasurableSet {a | ∀ q r (_ : q ≤ r), f a q ≤ f a r}
    simp_rw [Set.setOf_forall]
    refine MeasurableSet.iInter (fun q ↦ ?_)
    refine MeasurableSet.iInter (fun r ↦ ?_)
    refine MeasurableSet.iInter (fun _ ↦ ?_)
    exact measurableSet_le hf.eval hf.eval
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (hypothesis)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
⊢ MeasurableSet.{u_1} (α := α) {a : α | IsRatStieltjesPoint f a}
have h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
Tactic: have h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)} :=
    measurableSet_tendsto _ (fun q ↦ hf.eval)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes (hypothesis)
Goal:
α : Type u_1
f : α → ℚ → ℝ
inst : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet.{u_1} (α := α) {a : α | Monotone (f a)}
h2 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atTop (𝓝 1)}
⊢ MeasurableSet.{u_1} (α := α) {a : α | IsRatStieltjesPoint f a}
have h3 : MeasurableSet.{u_1} (α := α) {a : α | Tendsto (f a) atBot (𝓝 0)}
Tactic: have h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)} :=
    measurableSet_tendsto _ (fun q ↦ hf.eval)