awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 :
  ∀ (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∞)
⊢ ∀ᵐ (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))

Tactic:
refine Submartingale.ae_tendsto_limitProcess (martingale_densityProcess hκν a hs).submartingale
    (R := (ν a univ).toNNReal) (fun n ↦ ?_)

Premises used: MeasureTheory.Martingale.submartingale, ProbabilityTheory.Kernel.martingale_densityProcess, MeasureTheory.Submartingale.ae_tendsto_limitProcess
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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∞)

Tactic:
(eLpNorm_densityProcess_le hκν n a s).trans_eq ?_

Premises used: LE.le.trans_eq, ProbabilityTheory.Kernel.eLpNorm_densityProcess_le
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 : ℕ
refine :
  (((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ =
    (↑(ENNReal.toNNReal ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ)) : ℝ≥0∞)
⊢ @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 (eLpNorm_densityProcess_le hκν n a s).trans_eq ?_

Premises used: LE.le.trans_eq, ProbabilityTheory.Kernel.eLpNorm_densityProcess_le
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 : ℕ
rw : Ne (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ =
    (↑(ENNReal.toNNReal ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ)) : ℝ≥0∞)

Tactic:
rw [ENNReal.coe_toNNReal]

Premises used: ENNReal.coe_toNNReal
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 : ℕ
⊢ Ne (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_ne_top _ _

Premises used: MeasureTheory.measure_ne_top
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 : ℕ
⊢ Ne (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact measure_ne_top _ _

Premises used: MeasureTheory.measure_ne_top
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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)

Tactic:
Submartingale.memLp_limitProcess (martingale_densityProcess hκν a hs).submartingale
    (R := (ν a univ).toNNReal) (fun n ↦ ?_)

Premises used: MeasureTheory.Martingale.submartingale, ProbabilityTheory.Kernel.martingale_densityProcess, MeasureTheory.Submartingale.memLp_limitProcess
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 :
  ∀ (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∞)
⊢ MemLp (ε := ℝ) (m0 := mγ)
    (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
      ((ν : (a : α) → Measure γ) a))
    1 ((ν : (a : α) → Measure γ) a)

Tactic:
refine Submartingale.memLp_limitProcess (martingale_densityProcess hκν a hs).submartingale
    (R := (ν a univ).toNNReal) (fun n ↦ ?_)

Premises used: MeasureTheory.Martingale.submartingale, ProbabilityTheory.Kernel.martingale_densityProcess, MeasureTheory.Submartingale.memLp_limitProcess
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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)

Tactic:
Submartingale.tendsto_eLpNorm_one_limitProcess ?_ ?_

Premises used: MeasureTheory.Submartingale.tendsto_eLpNorm_one_limitProcess
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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)
refine_2 :
  @UniformIntegrable _ ℝ _ _ mγ (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (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)

Tactic:
refine Submartingale.tendsto_eLpNorm_one_limitProcess ?_ ?_

Premises used: MeasureTheory.Submartingale.tendsto_eLpNorm_one_limitProcess
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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
⊢ Submartingale (E := ℝ) (m0 := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
    ((ν : (a : α) → Measure γ) a)

Tactic:
(martingale_densityProcess hκν a hs).submartingale

Premises used: MeasureTheory.Martingale.submartingale, ProbabilityTheory.Kernel.martingale_densityProcess
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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
⊢ Submartingale (E := ℝ) (m0 := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
    ((ν : (a : α) → Measure γ) a)

Tactic:
exact (martingale_densityProcess hκν a hs).submartingale

Premises used: MeasureTheory.Martingale.submartingale, ProbabilityTheory.Kernel.martingale_densityProcess
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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)

Tactic:
uniformIntegrable_of le_rfl ENNReal.one_ne_top ?_ ?_

Premises used: le_rfl, MeasureTheory.uniformIntegrable_of, ENNReal.one_ne_top
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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)
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 ε
⊢ @UniformIntegrable _ ℝ _ _ mγ (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) 1 ((ν : (a : α) → Measure γ) a)

Tactic:
refine uniformIntegrable_of le_rfl ENNReal.one_ne_top ?_ ?_

Premises used: le_rfl, MeasureTheory.uniformIntegrable_of, ENNReal.one_ne_top
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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
⊢ ∀ (i : ℕ),
    AEStronglyMeasurable (β := ℝ) (m₀ := mγ) (fun (x : γ) ↦ κ.densityProcess ν i a x s) ((ν : (a : α) → Measure γ) a)

Tactic:
fun n ↦ (measurable_densityProcess_right κ ν n a hs).aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable, ProbabilityTheory.Kernel.measurable_densityProcess_right
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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
⊢ ∀ (i : ℕ),
    AEStronglyMeasurable (β := ℝ) (m₀ := mγ) (fun (x : γ) ↦ κ.densityProcess ν i a x s) ((ν : (a : α) → Measure γ) a)

Tactic:
exact fun n ↦ (measurable_densityProcess_right κ ν n a hs).aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable, ProbabilityTheory.Kernel.measurable_densityProcess_right
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 ε

Tactic:
fun ε _ ↦ ⟨2, fun n ↦ le_of_eq_of_le ?_ (?_ : 0 ≤ ENNReal.ofReal ε)⟩

Premises used: Exists.intro, le_of_eq_of_le, OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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
refine_2₁ : ∀ (ε : ℝ), 0 < ε → ∀ (n : ℕ), 0 ≤ ENNReal.ofReal ε
⊢ ∀ (ε : ℝ),
    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 fun ε _ ↦ ⟨2, fun n ↦ le_of_eq_of_le ?_ (?_ : 0 ≤ ENNReal.ofReal ε)⟩
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 : ℕ
this : Eq.{u_3 + 1} (α := Set γ) {x : γ | 2 ≤ ‖κ.densityProcess ν n a x s‖₊} ∅
⊢ @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:
simp [this]
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 : ℕ
refine_2 : Eq.{u_3 + 1} (α := Set γ) {x : γ | 2 ≤ ‖κ.densityProcess ν n a x s‖₊} ∅
⊢ @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:
suffices {x | 2 ≤ ‖densityProcess κ ν n a x s‖₊} = ∅ by simp [this]
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 : ℕ
refine_2 :
  ∀ (x : γ), Membership.mem (γ := Set γ) {x : γ | 2 ≤ ‖κ.densityProcess ν n a x s‖₊} x ↔ Membership.mem (γ := Set γ) ∅ x
⊢ Eq.{u_3 + 1} (α := Set γ) {x : γ | 2 ≤ ‖κ.densityProcess ν n a x s‖₊} ∅

Tactic:
ext x
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 : γ
refine_2 : ‖κ.densityProcess ν n a x s‖₊ < 2
⊢ Membership.mem (γ := Set γ) {x : γ | 2 ≤ ‖κ.densityProcess ν n a x s‖₊} x ↔ Membership.mem (γ := Set γ) ∅ x

Tactic:
simp only [mem_setOf_eq, mem_empty_iff_false, iff_false, not_le]

Premises used: not_le, iff_false, Set.mem_setOf_eq, Set.mem_empty_iff_false
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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

Tactic:
(?_ : _ ≤ (1 : ℝ≥0)).trans_lt one_lt_two

Premises used: one_lt_two, LE.le.trans_lt
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 : γ
refine_2 : ‖κ.densityProcess ν n a x s‖₊ ≤ 1
⊢ ‖κ.densityProcess ν n a x s‖₊ < 2

Tactic:
refine (?_ : _ ≤ (1 : ℝ≥0)).trans_lt one_lt_two

Premises used: one_lt_two, LE.le.trans_lt
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 : γ
refine_2 : NNReal.mk (κ.densityProcess ν n a x s) ⋯ ≤ 1
⊢ ‖κ.densityProcess ν n a x s‖₊ ≤ 1

Tactic:
rw [Real.nnnorm_of_nonneg (densityProcess_nonneg _ _ _ _ _ _)]

Premises used: ProbabilityTheory.Kernel.densityProcess_nonneg, Real.nnnorm_of_nonneg
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 : γ
⊢ NNReal.mk (κ.densityProcess ν n a x s) ⋯ ≤ 1

Tactic:
mod_cast (densityProcess_le_one hκν _ _ _ _)

Premises used: ProbabilityTheory.Kernel.densityProcess_le_one, congrArg, cast, NNReal.mk, LE.le, ProbabilityTheory.Kernel.densityProcess_nonneg, ProbabilityTheory.Kernel.densityProcess, Eq.symm, Nat.cast_one, Eq.trans
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 : γ
⊢ NNReal.mk (κ.densityProcess ν n a x s) ⋯ ≤ 1

Tactic:
exact mod_cast (densityProcess_le_one hκν _ _ _ _)

Premises used: ProbabilityTheory.Kernel.densityProcess_le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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 : ℕ
⊢ 0 ≤ ENNReal.ofReal ε

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
inst_1 : IsFiniteKernel ν
hκν : κ.fst ≤ ν
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
⊢ 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 (Measure.restrict ((ν : (a : α) → Measure γ) a) A))
    atTop (𝓝 0)

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
    (tendsto_eLpNorm_one_densityProcess_limitProcess hκν a hs) (fun _ ↦ zero_le)
    (fun _ ↦ eLpNorm_restrict_le ..)

Premises used: zero_le, tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds, HSub.hSub, ProbabilityTheory.countableFiltration, ProbabilityTheory.Kernel.densityProcess, ProbabilityTheory.Kernel.tendsto_eLpNorm_one_densityProcess_limitProcess, MeasureTheory.Filtration.limitProcess, OfNat.ofNat, DFunLike.coe, MeasureTheory.eLpNorm_restrict_le
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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
t : γ
ht :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ κ.densityProcess ν n a t s) atTop
    (𝓝
      (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
        ((ν : (a : α) → Measure γ) a) t))
⊢ κ.density ν a t s =
    Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
      ((ν : (a : α) → Measure γ) a) t

Tactic:
ht.limsup_eq

Premises used: Filter.Tendsto.limsup_eq, ProbabilityTheory.Kernel.density
-- Module: Mathlib.Probability.Kernel.Disintegration.Density
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
h₁ h₂ :
  ∀ (t : γ)
    (ht :
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ κ.densityProcess ν n a t s) atTop
        (𝓝
          (Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
            ((ν : (a : α) → Measure γ) a) t))),
    κ.density ν a t s =
      Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
        ((ν : (a : α) → Measure γ) a) t
⊢ (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))

Tactic:
filter_upwards [tendsto_densityProcess_limitProcess hκν a hs] with t ht using ht.limsup_eq

Premises used: ProbabilityTheory.Kernel.tendsto_densityProcess_limitProcess