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 ≤ ν
a : α
inst_1 : IsFiniteKernel ν
s : Set β
hs : MeasurableSet s
t : γ
h1 :
  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))
h2 :
  κ.density ν a t s =
    Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
      ((ν : (a : α) → Measure γ) a) t
⊢ Tendsto (fun (n : ℕ) ↦ κ.densityProcess ν n a t s) atTop (𝓝 (κ.density ν a t s))

Tactic:
h2 ▸ h1

Premises used: Eq.rec, Eq.symm
-- 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 ≤ ν
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
h₁ h₂ :
  ∀ (t : γ)
    (h1 :
      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)))
    (h2 :
      κ.density ν a t s =
        Filtration.limitProcess (m := mγ) (fun (n : ℕ) (x : γ) ↦ κ.densityProcess ν n a x s) (countableFiltration γ)
          ((ν : (a : α) → Measure γ) a) t),
    Tendsto (fun (n : ℕ) ↦ κ.densityProcess ν n a t s) atTop (𝓝 (κ.density ν a t s))
⊢ ∀ᵐ (x : γ) ∂((ν : (a : α) → Measure γ) a : Measure γ),
    Tendsto (fun (n : ℕ) ↦ κ.densityProcess ν n a x s) atTop (𝓝 (κ.density ν a x s))

Tactic:
filter_upwards [tendsto_densityProcess_limitProcess hκν a hs, density_ae_eq_limitProcess hκν a hs]
    with t h1 h2 using h2 ▸ h1

Premises used: ProbabilityTheory.Kernel.density_ae_eq_limitProcess, ProbabilityTheory.Kernel.tendsto_densityProcess_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 α γ
s : Set β
hs : MeasurableSet s
⊢ Measurable (β := ℝ) fun (p : α × γ) ↦ κ.density ν p.1 p.2 s

Tactic:
.limsup (fun n ↦ measurable_densityProcess κ ν n hs)

Premises used: Measurable.limsup, ProbabilityTheory.Kernel.measurable_densityProcess, 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 α γ
x : γ
s : Set β
hs : MeasurableSet s
change : Measurable.{u_1, 0} (α := α) (β := ℝ) ((fun (p : α × γ) ↦ κ.density ν p.1 p.2 s) ∘ fun (a : α) ↦ (a, x))
⊢ Measurable (β := ℝ) fun (a : α) ↦ κ.density ν a x s

Tactic:
change Measurable ((fun (p : α × γ) ↦ density κ ν p.1 p.2 s) ∘ (fun a ↦ (a, x)))

Premises used: Measurable, Function.comp, Prod.mk, Prod.fst, Prod.snd, 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 α γ
x : γ
s : Set β
hs : MeasurableSet s
⊢ Measurable.{u_1, 0} (α := α) (β := ℝ) ((fun (p : α × γ) ↦ κ.density ν p.1 p.2 s) ∘ fun (a : α) ↦ (a, x))

Tactic:
(measurable_density κ ν hs).comp measurable_prodMk_right

Premises used: Measurable.comp, ProbabilityTheory.Kernel.measurable_density, measurable_prodMk_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 α γ
x : γ
s : Set β
hs : MeasurableSet s
⊢ Measurable.{u_1, 0} (α := α) (β := ℝ) ((fun (p : α × γ) ↦ κ.density ν p.1 p.2 s) ∘ fun (a : α) ↦ (a, x))

Tactic:
exact (measurable_density κ ν hs).comp measurable_prodMk_right

Premises used: Measurable.comp, ProbabilityTheory.Kernel.measurable_density, measurable_prodMk_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 α γ
s : Set β
hs : MeasurableSet s
a : α
change : Measurable.{u_3, 0} (α := γ) (β := ℝ) ((fun (p : α × γ) ↦ κ.density ν p.1 p.2 s) ∘ fun (x : γ) ↦ (a, x))
⊢ Measurable (β := ℝ) fun (x : γ) ↦ κ.density ν a x s

Tactic:
change Measurable ((fun (p : α × γ) ↦ density κ ν p.1 p.2 s) ∘ (fun x ↦ (a, x)))

Premises used: Measurable, Function.comp, Prod.mk, Prod.fst, Prod.snd, 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 α γ
s : Set β
hs : MeasurableSet s
a : α
⊢ Measurable.{u_3, 0} (α := γ) (β := ℝ) ((fun (p : α × γ) ↦ κ.density ν p.1 p.2 s) ∘ fun (x : γ) ↦ (a, x))

Tactic:
(measurable_density κ ν hs).comp measurable_prodMk_left

Premises used: Measurable.comp, ProbabilityTheory.Kernel.measurable_density, measurable_prodMk_left
-- 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 α γ
s : Set β
hs : MeasurableSet s
a : α
⊢ Measurable.{u_3, 0} (α := γ) (β := ℝ) ((fun (p : α × γ) ↦ κ.density ν p.1 p.2 s) ∘ fun (x : γ) ↦ (a, x))

Tactic:
exact (measurable_density κ ν hs).comp measurable_prodMk_left

Premises used: Measurable.comp, ProbabilityTheory.Kernel.measurable_density, measurable_prodMk_left
-- 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 ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ κ.density ν a x s ≤ κ.density ν a x s'

Tactic:
limsup_le_limsup ?_ ?_ ?_

Premises used: Filter.limsup_le_limsup, 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 ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
refine_1 :
  EventuallyLE (β := ℝ) atTop (fun (n : ℕ) ↦ κ.densityProcess ν n a x s) fun (n : ℕ) ↦ κ.densityProcess ν n a x s'
refine_2 : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ κ.densityProcess ν n a x s
refine_3 : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ κ.densityProcess ν n a x s'
⊢ κ.density ν a x s ≤ κ.density ν a x s'

Tactic:
refine limsup_le_limsup ?_ ?_ ?_

Premises used: Filter.limsup_le_limsup
-- 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 ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ EventuallyLE (β := ℝ) atTop (fun (n : ℕ) ↦ κ.densityProcess ν n a x s) fun (n : ℕ) ↦ κ.densityProcess ν n a x s'

Tactic:
Eventually.of_forall (fun n ↦ densityProcess_mono_set hκν n a x h)

Premises used: ProbabilityTheory.Kernel.densityProcess_mono_set, Filter.Eventually.of_forall, Filter.EventuallyLE
-- 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 ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ EventuallyLE (β := ℝ) atTop (fun (n : ℕ) ↦ κ.densityProcess ν n a x s) fun (n : ℕ) ↦ κ.densityProcess ν n a x s'

Tactic:
exact Eventually.of_forall (fun n ↦ densityProcess_mono_set hκν n a x h)

Premises used: ProbabilityTheory.Kernel.densityProcess_mono_set, Filter.Eventually.of_forall
-- 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 ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ κ.densityProcess ν n a x s

Tactic:
isCoboundedUnder_le_of_le atTop (fun i ↦ densityProcess_nonneg _ _ _ _ _ _)

Premises used: ProbabilityTheory.Kernel.densityProcess_nonneg, Filter.atTop, Filter.isCoboundedUnder_le_of_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 ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ κ.densityProcess ν n a x s

Tactic:
exact isCoboundedUnder_le_of_le atTop (fun i ↦ densityProcess_nonneg _ _ _ _ _ _)

Premises used: ProbabilityTheory.Kernel.densityProcess_nonneg, Filter.atTop, Filter.isCoboundedUnder_le_of_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 ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ κ.densityProcess ν n a x s'

Tactic:
isBoundedUnder_of ⟨1, fun n ↦ densityProcess_le_one hκν _ _ _ _⟩

Premises used: ProbabilityTheory.Kernel.densityProcess_le_one, Exists.intro, OfNat.ofNat, Filter.isBoundedUnder_of
-- 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 ≤ ν
a : α
x : γ
s s' : Set β
h : s ⊆ s'
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ κ.densityProcess ν n a x s'

Tactic:
exact isBoundedUnder_of ⟨1, fun n ↦ densityProcess_le_one hκν _ _ _ _⟩

Premises used: ProbabilityTheory.Kernel.densityProcess_le_one, Exists.intro, OfNat.ofNat, Filter.isBoundedUnder_of
-- 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 ≤ ν
a : α
x : γ
s : Set β
⊢ 0 ≤ κ.density ν a x s

Tactic:
le_limsup_of_frequently_le ?_ ?_

Premises used: Filter.le_limsup_of_frequently_le, 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 ≤ ν
a : α
x : γ
s : Set β
refine_1 : ∃ᶠ (i : ℕ) in atTop, 0 ≤ κ.densityProcess ν i a x s
refine_2 : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ κ.densityProcess ν n a x s
⊢ 0 ≤ κ.density ν a x s

Tactic:
refine le_limsup_of_frequently_le ?_ ?_

Premises used: Filter.le_limsup_of_frequently_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 ≤ ν
a : α
x : γ
s : Set β
⊢ ∃ᶠ (i : ℕ) in atTop, 0 ≤ κ.densityProcess ν i a x s

Tactic:
Frequently.of_forall (fun n ↦ densityProcess_nonneg _ _ _ _ _ _)

Premises used: Filter.Frequently.of_forall, ProbabilityTheory.Kernel.densityProcess_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 ≤ ν
a : α
x : γ
s : Set β
⊢ ∃ᶠ (i : ℕ) in atTop, 0 ≤ κ.densityProcess ν i a x s

Tactic:
exact Frequently.of_forall (fun n ↦ densityProcess_nonneg _ _ _ _ _ _)

Premises used: Filter.Frequently.of_forall, ProbabilityTheory.Kernel.densityProcess_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 ≤ ν
a : α
x : γ
s : Set β
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ κ.densityProcess ν n a x s

Tactic:
isBoundedUnder_of ⟨1, fun n ↦ densityProcess_le_one hκν _ _ _ _⟩

Premises used: ProbabilityTheory.Kernel.densityProcess_le_one, Exists.intro, OfNat.ofNat, Filter.isBoundedUnder_of
-- 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 ≤ ν
a : α
x : γ
s : Set β
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ κ.densityProcess ν n a x s

Tactic:
exact isBoundedUnder_of ⟨1, fun n ↦ densityProcess_le_one hκν _ _ _ _⟩

Premises used: ProbabilityTheory.Kernel.densityProcess_le_one, Exists.intro, OfNat.ofNat, Filter.isBoundedUnder_of
-- 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 ≤ ν
a : α
x : γ
s : Set β
⊢ κ.density ν a x s ≤ 1

Tactic:
limsup_le_of_le ?_ ?_

Premises used: Filter.limsup_le_of_le, 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 ≤ ν
a : α
x : γ
s : Set β
refine_1 : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ κ.densityProcess ν n a x s
refine_2 : ∀ᶠ (n : ℕ) in atTop, κ.densityProcess ν n a x s ≤ 1
⊢ κ.density ν a x s ≤ 1

Tactic:
refine limsup_le_of_le ?_ ?_

Premises used: Filter.limsup_le_of_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 ≤ ν
a : α
x : γ
s : Set β
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ κ.densityProcess ν n a x s

Tactic:
isCoboundedUnder_le_of_le atTop (fun i ↦ densityProcess_nonneg _ _ _ _ _ _)

Premises used: ProbabilityTheory.Kernel.densityProcess_nonneg, Filter.atTop, Filter.isCoboundedUnder_le_of_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 ≤ ν
a : α
x : γ
s : Set β
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (n : ℕ) ↦ κ.densityProcess ν n a x s

Tactic:
exact isCoboundedUnder_le_of_le atTop (fun i ↦ densityProcess_nonneg _ _ _ _ _ _)

Premises used: ProbabilityTheory.Kernel.densityProcess_nonneg, Filter.atTop, Filter.isCoboundedUnder_le_of_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 ≤ ν
a : α
x : γ
s : Set β
⊢ ∀ᶠ (n : ℕ) in atTop, κ.densityProcess ν n a x s ≤ 1

Tactic:
Eventually.of_forall (fun n ↦ densityProcess_le_one hκν _ _ _ _)

Premises used: ProbabilityTheory.Kernel.densityProcess_le_one, Filter.Eventually.of_forall
-- 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 ≤ ν
a : α
x : γ
s : Set β
⊢ ∀ᶠ (n : ℕ) in atTop, κ.densityProcess ν n a x s ≤ 1

Tactic:
exact Eventually.of_forall (fun n ↦ densityProcess_le_one hκν _ _ _ _)

Premises used: ProbabilityTheory.Kernel.densityProcess_le_one, Filter.Eventually.of_forall
-- 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 ≤ ν
a : α
s : Set β
⊢ @eLpNorm _ ℝ _ mγ (fun (x : γ) ↦ κ.density ν a x s) 1 ((ν : (a : α) → Measure γ) a) ≤
    (((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ

Tactic:
(eLpNorm_le_of_ae_bound (C := 1) (ae_of_all _ (fun t ↦ ?_))).trans ?_

Premises used: MeasureTheory.ae_of_all, LE.le.trans, MeasureTheory.eLpNorm_le_of_ae_bound
-- 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 ≤ ν
a : α
s : Set β
refine_1 : ∀ (t : γ), ‖κ.density ν a t s‖ ≤ 1
refine_2 :
  HPow.hPow (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
        (ENNReal.toReal 1)⁻¹ *
      ENNReal.ofReal 1 ≤
    (((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ
⊢ @eLpNorm _ ℝ _ mγ (fun (x : γ) ↦ κ.density ν a x s) 1 ((ν : (a : α) → Measure γ) a) ≤
    (((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ

Tactic:
refine (eLpNorm_le_of_ae_bound (C := 1) (ae_of_all _ (fun t ↦ ?_))).trans ?_

Premises used: MeasureTheory.ae_of_all, LE.le.trans, MeasureTheory.eLpNorm_le_of_ae_bound
-- 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 ≤ ν
a : α
s : Set β
t : γ
⊢ ‖κ.density ν a t s‖ ≤ 1

Tactic:
simp only [Real.norm_eq_abs, abs_of_nonneg (density_nonneg hκν a t s),
      density_le_one hκν a t s]

Premises used: ProbabilityTheory.Kernel.density_le_one, abs_of_nonneg, ProbabilityTheory.Kernel.density_nonneg, Real.norm_eq_abs
-- 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 ≤ ν
a : α
s : Set β
⊢ HPow.hPow (α := ℝ≥0∞) ((((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ : ℝ≥0∞)
        (ENNReal.toReal 1)⁻¹ *
      ENNReal.ofReal 1 ≤
    (((ν : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) univ

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 α γ
hκν : κ.fst ≤ ν
inst_1 : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
rw : MemLp (ε := ℝ) (m0 := mγ) (fun (x : γ) ↦ κ.density ν a x s) 1 ((ν : (a : α) → Measure γ) a)
⊢ @Integrable ℝ _ _ _ mγ (fun (x : γ) ↦ κ.density ν a x s) ((ν : (a : α) → Measure γ) a)

Tactic:
rw [← memLp_one_iff_integrable]

Premises used: MeasureTheory.memLp_one_iff_integrable
-- 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γ) (fun (x : γ) ↦ κ.density ν a x s) 1 ((ν : (a : α) → Measure γ) a)

Tactic:
⟨Measurable.aestronglyMeasurable ?_, ?_⟩

Premises used: Measurable.aestronglyMeasurable, MeasureTheory.MemLp, And.intro
-- 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 : Measurable (β := ℝ) fun (x : γ) ↦ κ.density ν a x s
refine_2 : @eLpNorm _ ℝ _ mγ (fun (x : γ) ↦ κ.density ν a x s) 1 ((ν : (a : α) → Measure γ) a) < ∞
⊢ MemLp (ε := ℝ) (m0 := mγ) (fun (x : γ) ↦ κ.density ν a x s) 1 ((ν : (a : α) → Measure γ) a)

Tactic:
refine ⟨Measurable.aestronglyMeasurable ?_, ?_⟩
-- 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
⊢ Measurable (β := ℝ) fun (x : γ) ↦ κ.density ν a x s

Tactic:
measurable_density_right κ ν hs a

Premises used: ProbabilityTheory.Kernel.measurable_density_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
⊢ Measurable (β := ℝ) fun (x : γ) ↦ κ.density ν a x s

Tactic:
exact measurable_density_right κ ν hs a

Premises used: ProbabilityTheory.Kernel.measurable_density_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
⊢ @eLpNorm _ ℝ _ mγ (fun (x : γ) ↦ κ.density ν a x s) 1 ((ν : (a : α) → Measure γ) a) < ∞

Tactic:
exact (eLpNorm_density_le hκν a s).trans_lt (measure_lt_top _ _)

Premises used: MeasureTheory.measure_lt_top, ProbabilityTheory.Kernel.eLpNorm_density_le, LE.le.trans_lt