awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ Tendsto
    (fun (m : ℕ) ↦
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
        (SProd.sprod (α := Set γ) univ (seq m)))
    atTop (𝓝 (Measure.real (α := γ × β) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) univ))
have refine_2 : ∀
  (h_cont :
    ContinuousAt ENNReal.toReal
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ)),
  Tendsto
    (fun (m : ℕ) ↦
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
        (SProd.sprod (α := Set γ) univ (seq m)))
    atTop (𝓝 (Measure.real (α := γ × β) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) univ))
Tactic: have h_cont := ENNReal.continuousOn_toReal.continuousAt (x := κ a univ) ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
refine_2 :
  ∀
    (h_cont :
      ContinuousAt ENNReal.toReal
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ)),
    Tendsto
      (fun (m : ℕ) ↦
        Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
          (SProd.sprod (α := Set γ) univ (seq m)))
      atTop (𝓝 (Measure.real (α := γ × β) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) univ))
⊢ Tendsto
    (fun (m : ℕ) ↦
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
        (SProd.sprod (α := Set γ) univ (seq m)))
    atTop (𝓝 (Measure.real (α := γ × β) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) univ))
have refine_1 : Membership.mem (γ := Filter ℝ≥0∞)
  (𝓝 ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ) : Filter ℝ≥0∞)
  {a : ℝ≥0∞ | a ≠ ∞}
Tactic: have h_cont := ENNReal.continuousOn_toReal.continuousAt (x := κ a univ) ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ Membership.mem (γ := Filter ℝ≥0∞)
    (𝓝 ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ) : Filter ℝ≥0∞)
    {a : ℝ≥0∞ | a ≠ ∞}
have refine_1 : ∃ t ⊆ {a : ℝ≥0∞ | a ≠ ∞},
  IsOpen t ∧
    Membership.mem (α := ℝ≥0∞) t
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [mem_nhds_iff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ ∃ t ⊆ {a : ℝ≥0∞ | a ≠ ∞},
    IsOpen t ∧
      Membership.mem (α := ℝ≥0∞) t
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ : ℝ≥0∞)
have refine_1 : ∀ (x : ℝ≥0∞)
  (hx :
    x ∈
      Iio
        (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
          ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞))),
  x <
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: refine ⟨Iio (κ a univ + 1), fun x hx ↦ ne_top_of_lt (?_ : x < κ a univ + 1), isOpen_Iio, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
refine_1 :
  ∀ (x : ℝ≥0∞)
    (hx :
      x ∈
        Iio
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
            ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ : ℝ≥0∞)
            (1 : ℝ≥0∞))),
    x <
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ ∃ t ⊆ {a : ℝ≥0∞ | a ≠ ∞},
    IsOpen t ∧
      Membership.mem (α := ℝ≥0∞) t
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ : ℝ≥0∞)
have refine_1₁ : Membership.mem (α := ℝ≥0∞)
  (Iio
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)))
  ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: refine ⟨Iio (κ a univ + 1), fun x hx ↦ ne_top_of_lt (?_ : x < κ a univ + 1), isOpen_Iio, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont :
  ContinuousAt ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ)
⊢ Tendsto
    (fun (m : ℕ) ↦
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
        (SProd.sprod (α := Set γ) univ (seq m)))
    atTop (𝓝 (Measure.real (α := γ × β) (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a) univ))
have refine_2 : Tendsto (β := ℝ≥0∞)
  (fun (m : ℕ) ↦
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set γ) univ (seq m)) :
      ℝ≥0∞))
  atTop (𝓝 ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ) : Filter ℝ≥0∞)
Tactic: refine h_cont.tendsto.comp ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont :
  ContinuousAt ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (m : ℕ) ↦
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (α := Set γ) univ (seq m)) :
        ℝ≥0∞))
    atTop (𝓝 ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ) : Filter ℝ≥0∞)
have h : Eq (α := Set (γ × β)) univ (⋃ (n : ℕ), SProd.sprod (α := Set γ) univ (seq n))
Tactic: convert! tendsto_measure_iUnion_atTop (monotone_const.set_prod hseq)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont :
  ContinuousAt ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ)
⊢ Eq (α := Set (γ × β)) univ (⋃ (n : ℕ), SProd.sprod (α := Set γ) univ (seq n))
have h : univ = SProd.sprod (α := Set γ) (β := Set β) univ (⋃ (i : ℕ), seq i)
Tactic: rw [← prod_iUnion, hseq_iUnion, univ_prod_univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont :
  ContinuousAt ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ)
h : univ = SProd.sprod (α := Set γ) (β := Set β) univ (⋃ (i : ℕ), seq i)
⊢ Eq (α := Set (γ × β)) univ (⋃ (n : ℕ), SProd.sprod (α := Set γ) univ (seq n))
have h₁ : univ = SProd.sprod (α := Set γ) (β := Set β) univ univ
Tactic: rw [← prod_iUnion, hseq_iUnion, univ_prod_univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), seq i) univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont :
  ContinuousAt ENNReal.toReal ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞) univ)
h : univ = SProd.sprod (α := Set γ) (β := Set β) univ (⋃ (i : ℕ), seq i)
h₁ : univ = SProd.sprod (α := Set γ) (β := Set β) univ univ
⊢ Eq (α := Set (γ × β)) univ (⋃ (n : ℕ), SProd.sprod (α := Set γ) univ (seq n))
have h₂ : Eq (α := Set (γ × β)) univ univ
Tactic: rw [← prod_iUnion, hseq_iUnion, univ_prod_univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (β := ℝ)
    (fun (m : ℕ) ↦ @integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) fun (x : γ) ↦ κ.density ν a x (seq m)) atTop (𝓝 0)
have this : IsFiniteKernel κ
Tactic: have : IsFiniteKernel κ := isFiniteKernel_of_isFiniteKernel_fst (h := isFiniteKernel_of_le hκν)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ Tendsto (β := ℝ)
    (fun (m : ℕ) ↦ @integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) fun (x : γ) ↦ κ.density ν a x (seq m)) atTop (𝓝 0)
have simp_rw : Tendsto (β := ℝ)
  (fun (m : ℕ) ↦
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
      (SProd.sprod (α := Set γ) univ (seq m)))
  atTop (𝓝 0)
Tactic: simp_rw [integral_density hκν a (hseq_meas _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ Tendsto
    (fun (m : ℕ) ↦
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
        (SProd.sprod (α := Set γ) univ (seq m)))
    atTop (𝓝 (ENNReal.toReal 0))
have h_cont : ContinuousAt ENNReal.toReal 0
Tactic: have h_cont := ENNReal.continuousAt_toReal ENNReal.zero_ne_top
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
⊢ Tendsto
    (fun (m : ℕ) ↦
      Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (γ × β)) a)
        (SProd.sprod (α := Set γ) univ (seq m)))
    atTop (𝓝 (ENNReal.toReal 0))
have refine : Tendsto (β := ℝ≥0∞)
  (fun (m : ℕ) ↦
    (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
      (SProd.sprod (α := Set γ) univ (seq m)))
  atTop (𝓝 0)
Tactic: refine h_cont.tendsto.comp ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
⊢ Tendsto (β := ℝ≥0∞)
    (fun (m : ℕ) ↦
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (α := Set γ) univ (seq m)) :
        ℝ≥0∞))
    atTop
    (𝓝
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (⋂ (n : ℕ), (fun (m : ℕ) ↦ SProd.sprod (α := Set γ) univ (seq m)) n)) :
      Filter ℝ≥0∞)
have hs : ∀ (i : ℕ), NullMeasurableSet (SProd.sprod (α := Set γ) univ (seq i)) ((κ : (a : α) → Measure (γ × β)) a)
Tactic: apply tendsto_measure_iInter_atTop
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
hs : ∀ (i : ℕ), NullMeasurableSet (SProd.sprod (α := Set γ) univ (seq i)) ((κ : (a : α) → Measure (γ × β)) a)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (m : ℕ) ↦
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (α := Set γ) univ (seq m)) :
        ℝ≥0∞))
    atTop
    (𝓝
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (⋂ (n : ℕ), (fun (m : ℕ) ↦ SProd.sprod (α := Set γ) univ (seq m)) n)) :
      Filter ℝ≥0∞)
have hm : Antitone (β := Set (γ × β)) fun (m : ℕ) ↦ SProd.sprod (α := Set γ) univ (seq m)
Tactic: apply tendsto_measure_iInter_atTop
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
hs : ∀ (i : ℕ), NullMeasurableSet (SProd.sprod (α := Set γ) univ (seq i)) ((κ : (a : α) → Measure (γ × β)) a)
hm : Antitone (β := Set (γ × β)) fun (m : ℕ) ↦ SProd.sprod (α := Set γ) univ (seq m)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (m : ℕ) ↦
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (α := Set γ) univ (seq m)) :
        ℝ≥0∞))
    atTop
    (𝓝
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (⋂ (n : ℕ), (fun (m : ℕ) ↦ SProd.sprod (α := Set γ) univ (seq m)) n)) :
      Filter ℝ≥0∞)
have hf : ∃ (i : ℕ),
  Ne (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set γ) univ (seq i)) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: apply tendsto_measure_iInter_atTop
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
⊢ Tendsto (β := ℝ≥0∞)
    (fun (m : ℕ) ↦
      (((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set γ) univ (seq m)))
    atTop (𝓝 0)
have h : Tendsto (β := ℝ≥0∞)
  (fun (m : ℕ) ↦
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (SProd.sprod (α := Set γ) univ (seq m)) :
      ℝ≥0∞))
  atTop
  (𝓝
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (⋂ (n : ℕ), (fun (m : ℕ) ↦ SProd.sprod (α := Set γ) univ (seq m)) n)) :
    Filter ℝ≥0∞)
Tactic: have h : Tendsto (fun m ↦ κ a (univ ×ˢ seq m)) atTop
      (𝓝 ((κ a) (⋂ n, (fun m ↦ univ ×ˢ seq m) n))) := by
    apply tendsto_measure_iInter_atTop
    · measurability
    · exact antitone_const.set_prod hseq
    · exact ⟨0, measure_ne_top _ _⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ∀ᵐ (x : γ) ∂((ν : (a : α) → Measure γ) a : Measure γ),
    Tendsto (β := ℝ) (fun (m : ℕ) ↦ κ.density ν a x (seq m)) atTop (𝓝 0)
have refine_1 : ∀ (n : ℕ), @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.density ν a x (seq n)) ((ν : (a : α) → Measure γ) a)
Tactic: refine tendsto_of_integral_tendsto_of_antitone ?_ (integrable_const _) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
refine_1 : ∀ (n : ℕ), @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.density ν a x (seq n)) ((ν : (a : α) → Measure γ) a)
⊢ ∀ᵐ (x : γ) ∂((ν : (a : α) → Measure γ) a : Measure γ),
    Tendsto (β := ℝ) (fun (m : ℕ) ↦ κ.density ν a x (seq m)) atTop (𝓝 0)
have refine_2 : Tendsto (β := ℝ)
  (fun (i : ℕ) ↦ @integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) fun (a_1 : γ) ↦ κ.density ν a a_1 (seq i)) atTop
  (𝓝 (@integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) fun (a : γ) ↦ 0))
Tactic: refine tendsto_of_integral_tendsto_of_antitone ?_ (integrable_const _) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
refine_1 : ∀ (n : ℕ), @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.density ν a x (seq n)) ((ν : (a : α) → Measure γ) a)
refine_2 :
  Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) fun (a_1 : γ) ↦ κ.density ν a a_1 (seq i)) atTop
    (𝓝 (@integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) fun (a : γ) ↦ 0))
⊢ ∀ᵐ (x : γ) ∂((ν : (a : α) → Measure γ) a : Measure γ),
    Tendsto (β := ℝ) (fun (m : ℕ) ↦ κ.density ν a x (seq m)) atTop (𝓝 0)
have refine_3 : ∀ᵐ (a_1 : γ) ∂((ν : (a : α) → Measure γ) a : Measure γ), Antitone (β := ℝ) fun (i : ℕ) ↦ κ.density ν a a_1 (seq i)
Tactic: refine tendsto_of_integral_tendsto_of_antitone ?_ (integrable_const _) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Density (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
refine_1 : ∀ (n : ℕ), @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.density ν a x (seq n)) ((ν : (a : α) → Measure γ) a)
refine_2 :
  Tendsto (β := ℝ)
    (fun (i : ℕ) ↦ @integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) fun (a_1 : γ) ↦ κ.density ν a a_1 (seq i)) atTop
    (𝓝 (@integral _ _ _ _ mγ ((ν : (a : α) → Measure γ) a) fun (a : γ) ↦ 0))
refine_3 :
  ∀ᵐ (a_1 : γ) ∂((ν : (a : α) → Measure γ) a : Measure γ), Antitone (β := ℝ) fun (i : ℕ) ↦ κ.density ν a a_1 (seq i)
⊢ ∀ᵐ (x : γ) ∂((ν : (a : α) → Measure γ) a : Measure γ),
    Tendsto (β := ℝ) (fun (m : ℕ) ↦ κ.density ν a x (seq m)) atTop (𝓝 0)
have refine_4 : ∀ᵐ (a_1 : γ) ∂((ν : (a : α) → Measure γ) a : Measure γ), ∀ (i : ℕ), 0 ≤ κ.density ν a a_1 (seq i)
Tactic: refine tendsto_of_integral_tendsto_of_antitone ?_ (integrable_const _) ?_ ?_ ?_