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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
hs : ∀ (i : ℕ), NullMeasurableSet (countablePartitionSet n x ×ˢ seq i) ((κ : (a : α) → Measure (γ × β)) a)
hm : Antitone (β := Set (γ × β)) fun (m : ℕ) ↦ countablePartitionSet n x ×ˢ seq m
⊢ Tendsto (β := ℝ≥0∞)
    (fun (m : ℕ) ↦
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ seq m) :
        ℝ≥0∞))
    atTop
    (𝓝
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (⋂ (n_1 : ℕ), countablePartitionSet n x ×ˢ seq n_1)) :
      Filter ℝ≥0∞)
have hf : ∃ (i : ℕ),
  Ne (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ 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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
h0 :
  ¬Eq (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (countablePartitionSet n x) : ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (m : ℕ) ↦
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (countablePartitionSet n x ×ˢ seq m) :
        ℝ≥0∞))
    atTop
    (𝓝
        ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
          (SProd.sprod (β := Set β) (countablePartitionSet n x) ∅)) :
      Filter ℝ≥0∞)
have this : Tendsto (β := ℝ≥0∞)
  (fun (m : ℕ) ↦
    ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (countablePartitionSet n x ×ˢ seq m) :
      ℝ≥0∞))
  atTop
  (𝓝
      ((((κ : (a : α) → Measure (γ × β)) a : Measure (γ × β)) : (a : Set (γ × β)) → ℝ≥0∞)
        (⋂ (n_1 : ℕ), countablePartitionSet n x ×ˢ seq n_1)) :
    Filter ℝ≥0∞)
Tactic: have : Tendsto (fun m ↦ κ a (countablePartitionSet n x ×ˢ seq m)) atTop
      (𝓝 ((κ a) (⋂ n_1, countablePartitionSet n x ×ˢ seq n_1))) := by
    apply tendsto_measure_iInter_atTop
    · measurability
    · exact fun _ _ h ↦ prod_mono_right <| hseq h
    · 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 α γ
inst_1 : IsFiniteKernel κ
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : Eq.{u_2 + 1} (α := Set β) (⋂ (i : ℕ), seq i) ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (β := ℝ) (fun (m : ℕ) ↦ κ.densityProcess ν n a x (seq m)) atTop (𝓝 0)
have rw : Tendsto (fun (m : ℕ) ↦ κ.densityProcess ν n a x (seq m)) atTop (𝓝 (κ.densityProcess ν n a x ∅))
Tactic: rw [← densityProcess_empty κ ν n a x]
-- 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 : α
s : Set β
hs : MeasurableSet s
⊢ ∀ᵐ (x : γ) ∂((ν : (a : α) → Measure γ) a : Measure γ),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ κ.densityProcess ν n a x s) atTop
      (𝓝
        (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
          ((ν : (a : α) → Measure γ) a) x))
have refine : ∀ (n : ℕ),
  @eLpNorm _ ℝ _ mγ (fun (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a) ≤
    (↑(ENNReal.toNNReal ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ)) : ℝ≥0∞)
Tactic: refine Submartingale.ae_tendsto_limitProcess (martingale_densityProcess hκν a hs).submartingale
    (R := (ν a univ).toNNReal) (fun n ↦ ?_)
-- 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 : α
s : Set β
hs : MeasurableSet s
n : ℕ
⊢ @eLpNorm _ ℝ _ mγ (fun (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a) ≤
    (↑(ENNReal.toNNReal ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ)) : ℝ≥0∞)
have refine : (((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ =
  (↑(ENNReal.toNNReal ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ)) : ℝ≥0∞)
Tactic: refine (eLpNorm_densityProcess_le hκν n a s).trans_eq ?_
-- 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 : α
s : Set β
hs : MeasurableSet s
n : ℕ
⊢ (((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ =
    (↑(ENNReal.toNNReal ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ)) : ℝ≥0∞)
have rw : Ne (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [ENNReal.coe_toNNReal]
-- 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 : α
s : Set β
hs : MeasurableSet s
⊢ MemLp (ε := ℝ) (m0 := mγ)
    (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
      ((ν : (a : α) → Measure γ) a))
    1 ((ν : (a : α) → Measure γ) a)
have refine : ∀ (n : ℕ),
  @eLpNorm _ ℝ _ mγ (fun (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a) ≤
    (↑(ENNReal.toNNReal ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ)) : ℝ≥0∞)
Tactic: refine Submartingale.memLp_limitProcess (martingale_densityProcess hκν a hs).submartingale
    (R := (ν a univ).toNNReal) (fun n ↦ ?_)
-- 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 : α
s : Set β
hs : MeasurableSet s
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      @eLpNorm _ _ _ mγ
        (HSub.hSub (α := (x : γ) → ℝ) (fun (x : γ) ↦ κ.densityProcess ν n a x s)
          (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
            ((ν : (a : α) → Measure γ) a)))
        1 ((ν : (a : α) → Measure γ) a))
    atTop (𝓝 0)
have refine_1 : Submartingale (E := ℝ) (m0 := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
  ((ν : (a : α) → Measure γ) a)
Tactic: refine Submartingale.tendsto_eLpNorm_one_limitProcess ?_ ?_
-- 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 : α
s : Set β
hs : MeasurableSet s
refine_1 :
  Submartingale (E := ℝ) (m0 := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
    ((ν : (a : α) → Measure γ) a)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      @eLpNorm _ _ _ mγ
        (HSub.hSub (α := (x : γ) → ℝ) (fun (x : γ) ↦ κ.densityProcess ν n a x s)
          (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
            ((ν : (a : α) → Measure γ) a)))
        1 ((ν : (a : α) → Measure γ) a))
    atTop (𝓝 0)
have refine_2 : @UniformIntegrable _ ℝ _ _ mγ (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a)
Tactic: refine Submartingale.tendsto_eLpNorm_one_limitProcess ?_ ?_
-- 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 : α
s : Set β
hs : MeasurableSet s
⊢ @UniformIntegrable _ ℝ _ _ mγ (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a)
have refine_2 : ∀ (i : ℕ),
  AEStronglyMeasurable (β := ℝ) (m₀ := mγ) (fun (x : γ) ↦ κ.densityProcess ν i a x s) ((ν : (a : α) → Measure γ) a)
Tactic: refine uniformIntegrable_of le_rfl ENNReal.one_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 : α
s : Set β
hs : MeasurableSet s
refine_2 :
  ∀ (i : ℕ),
    AEStronglyMeasurable (β := ℝ) (m₀ := mγ) (fun (x : γ) ↦ κ.densityProcess ν i a x s) ((ν : (a : α) → Measure γ) a)
⊢ @UniformIntegrable _ ℝ _ _ mγ (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a)
have refine_2₁ : ∀ (ε : ℝ),
  0 < ε →
    ∃ (C : ℝ≥0),
      ∀ (i : ℕ),
        @eLpNorm.{u_3, 0} γ ℝ _ mγ
            (indicator {x : γ | C ≤ ‖κ.densityProcess ν i a x s‖₊} fun (x : γ) ↦ κ.densityProcess ν i a x s) 1
            ((ν : (a : α) → Measure γ) a) ≤
          ENNReal.ofReal ε
Tactic: refine uniformIntegrable_of le_rfl ENNReal.one_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 : α
s : Set β
hs : MeasurableSet s
⊢ ∀ (ε : ℝ),
    0 < ε →
      ∃ (C : ℝ≥0),
        ∀ (i : ℕ),
          @eLpNorm.{u_3, 0} γ ℝ _ mγ
              (indicator {x : γ | C ≤ ‖κ.densityProcess ν i a x s‖₊} fun (x : γ) ↦ κ.densityProcess ν i a x s) 1
              ((ν : (a : α) → Measure γ) a) ≤
            ENNReal.ofReal ε
have refine_2 : ∀ (ε : ℝ),
  0 < ε →
    ∀ (n : ℕ),
      @eLpNorm.{u_3, 0} γ ℝ _ mγ
          (indicator {x : γ | 2 ≤ ‖κ.densityProcess ν n a x s‖₊} fun (x : γ) ↦ κ.densityProcess ν n a x s) 1
          ((ν : (a : α) → Measure γ) a) =
        0
Tactic: refine fun ε _ ↦ ⟨2, fun n ↦ le_of_eq_of_le ?_ (?_ : 0 ≤ ENNReal.ofReal ε)⟩
-- 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 : α
s : Set β
hs : MeasurableSet s
refine_2 :
  ∀ (ε : ℝ),
    0 < ε →
      ∀ (n : ℕ),
        @eLpNorm.{u_3, 0} γ ℝ _ mγ
            (indicator {x : γ | 2 ≤ ‖κ.densityProcess ν n a x s‖₊} fun (x : γ) ↦ κ.densityProcess ν n a x s) 1
            ((ν : (a : α) → Measure γ) a) =
          0
⊢ ∀ (ε : ℝ),
    0 < ε →
      ∃ (C : ℝ≥0),
        ∀ (i : ℕ),
          @eLpNorm.{u_3, 0} γ ℝ _ mγ
              (indicator {x : γ | C ≤ ‖κ.densityProcess ν i a x s‖₊} fun (x : γ) ↦ κ.densityProcess ν i a x s) 1
              ((ν : (a : α) → Measure γ) a) ≤
            ENNReal.ofReal ε
have refine_2₁ : ∀ (ε : ℝ), 0 < ε → ∀ (n : ℕ), 0 ≤ ENNReal.ofReal ε
Tactic: refine fun ε _ ↦ ⟨2, fun n ↦ le_of_eq_of_le ?_ (?_ : 0 ≤ ENNReal.ofReal ε)⟩
-- 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 : α
s : Set β
hs : MeasurableSet s
ε : ℝ
h : 0 < ε
n : ℕ
⊢ @eLpNorm.{u_3, 0} γ ℝ _ mγ
      (indicator {x : γ | 2 ≤ ‖κ.densityProcess ν n a x s‖₊} fun (x : γ) ↦ κ.densityProcess ν n a x s) 1
      ((ν : (a : α) → Measure γ) a) =
    0
have refine_2 : Eq.{u_3 + 1} (α := Set γ) {x : γ | 2 ≤ ‖κ.densityProcess ν n a x s‖₊} ∅
Tactic: suffices {x | 2 ≤ ‖densityProcess κ ν n a x s‖₊} = ∅ by simp [this]
-- 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 : α
s : Set β
hs : MeasurableSet s
ε : ℝ
h : 0 < ε
n : ℕ
⊢ Eq.{u_3 + 1} (α := Set γ) {x : γ | 2 ≤ ‖κ.densityProcess ν n a x s‖₊} ∅
have refine_2 : ∀ (x : γ), Membership.mem (γ := Set γ) {x : γ | 2 ≤ ‖κ.densityProcess ν n a x s‖₊} x ↔ Membership.mem (γ := Set γ) ∅ x
Tactic: ext x
-- 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 : α
s : Set β
hs : MeasurableSet s
ε : ℝ
h : 0 < ε
n : ℕ
x : γ
⊢ Membership.mem (γ := Set γ) {x : γ | 2 ≤ ‖κ.densityProcess ν n a x s‖₊} x ↔ Membership.mem (γ := Set γ) ∅ x
have refine_2 : ‖κ.densityProcess ν n a x s‖₊ < 2
Tactic: simp only [mem_setOf_eq, mem_empty_iff_false, iff_false, not_le]
-- 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 : α
s : Set β
hs : MeasurableSet s
ε : ℝ
h : 0 < ε
n : ℕ
x : γ
⊢ ‖κ.densityProcess ν n a x s‖₊ < 2
have refine_2 : ‖κ.densityProcess ν n a x s‖₊ ≤ 1
Tactic: refine (?_ : _ ≤ (1 : ℝ≥0)).trans_lt one_lt_two
-- 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 : α
s : Set β
hs : MeasurableSet s
ε : ℝ
h : 0 < ε
n : ℕ
x : γ
⊢ ‖κ.densityProcess ν n a x s‖₊ ≤ 1
have refine_2 : NNReal.mk (κ.densityProcess ν n a x s) sorry ≤ 1
Tactic: rw [Real.nnnorm_of_nonneg (densityProcess_nonneg _ _ _ _ _ _)]
-- 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 : α
s : Set β
hs : MeasurableSet s
⊢ (ae (F := Measure γ) ((ν : (a : α) → Measure γ) a : Measure γ)).EventuallyEq (β := ℝ)
    (fun (x : γ) ↦ κ.density ν a x s)
    (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
      ((ν : (a : α) → Measure γ) a))
have h : ∀ (a_1 : γ),
  Membership.mem (γ := Set γ)
    {x : γ |
      Membership.mem (γ := Set γ)
          {x : γ |
            (fun (x : γ) ↦
                Tendsto (β := ℝ) (fun (n : ℕ) ↦ κ.densityProcess ν n a x s) atTop
                  (𝓝
                    (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s)
                      (countableFiltration γ) ((ν : (a : α) → Measure γ) a) x)))
              x}
          x →
        Membership.mem (γ := Set γ)
          {x : γ |
            (fun (x : γ) ↦
                Eq (α := ℝ) ((fun (x : γ) ↦ κ.density ν a x s) x)
                  (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s)
                    (countableFiltration γ) ((ν : (a : α) → Measure γ) a) x))
              x}
          x}
    a_1
Tactic: filter_upwards [tendsto_densityProcess_limitProcess hκν a hs] with t ht using ht.limsup_eq
-- 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 : α
s : Set β
hs : MeasurableSet s
h :
  ∀ (a_1 : γ),
    Membership.mem (γ := Set γ)
      {x : γ |
        Membership.mem (γ := Set γ)
            {x : γ |
              (fun (x : γ) ↦
                  Tendsto (β := ℝ) (fun (n : ℕ) ↦ κ.densityProcess ν n a x s) atTop
                    (𝓝
                      (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s)
                        (countableFiltration γ) ((ν : (a : α) → Measure γ) a) x)))
                x}
            x →
          Membership.mem (γ := Set γ)
            {x : γ |
              (fun (x : γ) ↦
                  Eq (α := ℝ) ((fun (x : γ) ↦ κ.density ν a x s) x)
                    (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s)
                      (countableFiltration γ) ((ν : (a : α) → Measure γ) a) x))
                x}
            x}
      a_1
⊢ (ae (F := Measure γ) ((ν : (a : α) → Measure γ) a : Measure γ)).EventuallyEq (β := ℝ)
    (fun (x : γ) ↦ κ.density ν a x s)
    (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
      ((ν : (a : α) → Measure γ) a))
have h₁ : ∀ (a_1 : γ),
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ κ.densityProcess ν n a a_1 s) atTop
      (𝓝
        (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
          ((ν : (a : α) → Measure γ) a) a_1)) →
    κ.density ν a a_1 s =
      Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
        ((ν : (a : α) → Measure γ) a) a_1
Tactic: filter_upwards [tendsto_densityProcess_limitProcess hκν a hs] with t ht using ht.limsup_eq
-- 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 ≤ ν
a : α
inst_1 : IsFiniteKernel ν
s : Set β
hs : MeasurableSet s
⊢ ∀ᵐ (x : γ) ∂((ν : (a : α) → Measure γ) a : Measure γ),
    Tendsto (fun (n : ℕ) ↦ κ.densityProcess ν n a x s) atTop (𝓝 (κ.density ν a x s))
have h : ∀ (a_1 : γ),
  Membership.mem (γ := Set γ)
    {x : γ |
      Membership.mem (γ := Set γ)
          {x : γ |
            (fun (x : γ) ↦
                Tendsto (β := ℝ) (fun (n : ℕ) ↦ κ.densityProcess ν n a x s) atTop
                  (𝓝
                    (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s)
                      (countableFiltration γ) ((ν : (a : α) → Measure γ) a) x)))
              x}
          x →
        Membership.mem (γ := Set γ)
          {x : γ |
            Membership.mem (γ := Set γ)
                {x : γ |
                  (fun (x : γ) ↦
                      Eq (α := ℝ) ((fun (x : γ) ↦ κ.density ν a x s) x)
                        (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s)
                          (countableFiltration γ) ((ν : (a : α) → Measure γ) a) x))
                    x}
                x →
              Membership.mem (γ := Set γ)
                {x : γ |
                  (fun (x : γ) ↦ Tendsto (fun (n : ℕ) ↦ κ.densityProcess ν n a x s) atTop (𝓝 (κ.density ν a x s))) x}
                x}
          x}
    a_1
Tactic: filter_upwards [tendsto_densityProcess_limitProcess hκν a hs, density_ae_eq_limitProcess hκν a hs]
    with t h1 h2 using h2 ▸ h1
-- 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 ≤ ν
a : α
inst_1 : IsFiniteKernel ν
s : Set β
hs : MeasurableSet s
h :
  ∀ (a_1 : γ),
    Membership.mem (γ := Set γ)
      {x : γ |
        Membership.mem (γ := Set γ)
            {x : γ |
              (fun (x : γ) ↦
                  Tendsto (β := ℝ) (fun (n : ℕ) ↦ κ.densityProcess ν n a x s) atTop
                    (𝓝
                      (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s)
                        (countableFiltration γ) ((ν : (a : α) → Measure γ) a) x)))
                x}
            x →
          Membership.mem (γ := Set γ)
            {x : γ |
              Membership.mem (γ := Set γ)
                  {x : γ |
                    (fun (x : γ) ↦
                        Eq (α := ℝ) ((fun (x : γ) ↦ κ.density ν a x s) x)
                          (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s)
                            (countableFiltration γ) ((ν : (a : α) → Measure γ) a) x))
                      x}
                  x →
                Membership.mem (γ := Set γ)
                  {x : γ |
                    (fun (x : γ) ↦ Tendsto (fun (n : ℕ) ↦ κ.densityProcess ν n a x s) atTop (𝓝 (κ.density ν a x s))) x}
                  x}
            x}
      a_1
⊢ ∀ᵐ (x : γ) ∂((ν : (a : α) → Measure γ) a : Measure γ),
    Tendsto (fun (n : ℕ) ↦ κ.densityProcess ν n a x s) atTop (𝓝 (κ.density ν a x s))
have h₁ : ∀ (a_1 : γ),
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ κ.densityProcess ν n a a_1 s) atTop
      (𝓝
        (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
          ((ν : (a : α) → Measure γ) a) a_1)) →
    κ.density ν a a_1 s =
        Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
          ((ν : (a : α) → Measure γ) a) a_1 →
      Tendsto (fun (n : ℕ) ↦ κ.densityProcess ν n a a_1 s) atTop (𝓝 (κ.density ν a a_1 s))
Tactic: filter_upwards [tendsto_densityProcess_limitProcess hκν a hs, density_ae_eq_limitProcess hκν a hs]
    with t h1 h2 using h2 ▸ h1
-- 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 α γ
x : γ
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ) fun (a : α) ↦ κ.density ν a x s
have change : Measurable.{u_1, 0} (α := α) (β := ℝ) ((fun (p : α × γ) ↦ κ.density ν p.1 p.2 s) ∘ fun (a : α) ↦ (a, x))
Tactic: change Measurable ((fun (p : α × γ) ↦ density κ ν p.1 p.2 s) ∘ (fun a ↦ (a, x)))