awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
refine_2 :
  Tendsto (β := ℝ) (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a_1 : β) ↦ f (a, a_1) (seq i))
    atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a_1 : β) ↦ f (a, a_1) (seq i))
    atTop (𝓝 (@integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a : β) ↦ 0))

Tactic:
rw [integral_zero]

Premises used: MeasureTheory.integral_zero
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a_1 : β) ↦ f (a, a_1) (seq i))
    atTop (𝓝 0)

Tactic:
hf.tendsto_integral_of_antitone a seq hseq hseq_tendsto

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_integral_of_antitone
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a_1 : β) ↦ f (a, a_1) (seq i))
    atTop (𝓝 0)

Tactic:
exact hf.tendsto_integral_of_antitone a seq hseq hseq_tendsto

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_integral_of_antitone
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
t : β
ht : Monotone (f (a, t))
⊢ Antitone (β := ℝ) fun (i : ℕ) ↦ f (a, t) (seq i)

Tactic:
fun n m hnm ↦ ht (hseq hnm)

Premises used: Antitone
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (c : β) ↦ Monotone (f (a, c))) x} x →
          Membership.mem (γ := Set β) {x : β | (fun (a_3 : β) ↦ Antitone (β := ℝ) fun (i : ℕ) ↦ f (a, a_3) (seq i)) x}
            x}
      a_1
h₁ h₂ : ∀ (t : β) (ht : Monotone (f (a, t))), Antitone (β := ℝ) fun (i : ℕ) ↦ f (a, t) (seq i)
⊢ ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), Antitone (β := ℝ) fun (i : ℕ) ↦ f (a, a_1) (seq i)

Tactic:
filter_upwards [hf.mono a] with t ht using fun n m hnm ↦ ht (hseq hnm)

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.mono
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
c : β
hc : ∀ (q : ℚ), 0 ≤ f (a, c) q
⊢ ∀ (i : ℕ), 0 ≤ f (a, c) (seq i)

Tactic:
fun i ↦ hc (seq i)
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Antitone seq
hseq_tendsto : Tendsto seq atTop atBot
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (c : β) ↦ ∀ (q : ℚ), 0 ≤ f (a, c) q) x} x →
          Membership.mem (γ := Set β) {x : β | (fun (a_3 : β) ↦ ∀ (i : ℕ), 0 ≤ f (a, a_3) (seq i)) x} x}
      a_1
h₁ h₂ : ∀ (c : β) (hc : ∀ (q : ℚ), 0 ≤ f (a, c) q) (i : ℕ), 0 ≤ f (a, c) (seq i)
⊢ ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), ∀ (i : ℕ), 0 ≤ f (a, a_1) (seq i)

Tactic:
filter_upwards [hf.nonneg a] with c hc using fun i ↦ hc (seq i)

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.nonneg
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
⊢ ∀ᵐ (c : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (m : ℕ) ↦ f (a, c) (seq m)) atTop (𝓝 1)

Tactic:
tendsto_of_integral_tendsto_of_monotone ?_ (integrable_const _) ?_ ?_ ?_

Premises used: MeasureTheory.tendsto_of_integral_tendsto_of_monotone, MeasureTheory.integrable_const
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
refine_1 : ∀ (n : ℕ), @Integrable ℝ _ _ _ mβ (fun (c : β) ↦ f (a, c) (seq n)) ((ν : (a : α) → Measure β) a)
refine_2 :
  Tendsto (β := ℝ) (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a_1 : β) ↦ f (a, a_1) (seq i))
    atTop (𝓝 (@integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a : β) ↦ 1))
refine_3 : ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), Monotone (β := ℝ) fun (i : ℕ) ↦ f (a, a_1) (seq i)
refine_4 : ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), ∀ (i : ℕ), f (a, a_1) (seq i) ≤ 1
⊢ ∀ᵐ (c : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (m : ℕ) ↦ f (a, c) (seq m)) atTop (𝓝 1)

Tactic:
refine tendsto_of_integral_tendsto_of_monotone ?_ (integrable_const _) ?_ ?_ ?_

Premises used: MeasureTheory.tendsto_of_integral_tendsto_of_monotone, MeasureTheory.integrable_const
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
⊢ ∀ (n : ℕ), @Integrable ℝ _ _ _ mβ (fun (c : β) ↦ f (a, c) (seq n)) ((ν : (a : α) → Measure β) a)

Tactic:
fun n ↦ hf.integrable a (seq n)

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.integrable
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
⊢ ∀ (n : ℕ), @Integrable ℝ _ _ _ mβ (fun (c : β) ↦ f (a, c) (seq n)) ((ν : (a : α) → Measure β) a)

Tactic:
exact fun n ↦ hf.integrable a (seq n)

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.integrable
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
refine_2 :
  Tendsto (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a_1 : β) ↦ f (a, a_1) (seq i)) atTop
    (𝓝 (Measure.real.{u_2} (α := β) (m := mβ) ((ν : (a : α) → Measure β) a) univ))
⊢ Tendsto (β := ℝ) (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a_1 : β) ↦ f (a, a_1) (seq i))
    atTop (𝓝 (@integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a : β) ↦ 1))

Tactic:
rw [MeasureTheory.integral_const, smul_eq_mul, mul_one]

Premises used: MeasureTheory.integral_const, smul_eq_mul, mul_one
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
⊢ Tendsto (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a_1 : β) ↦ f (a, a_1) (seq i)) atTop
    (𝓝 (Measure.real.{u_2} (α := β) (m := mβ) ((ν : (a : α) → Measure β) a) univ))

Tactic:
hf.tendsto_integral_of_monotone a seq hseq hseq_tendsto

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_integral_of_monotone
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
⊢ Tendsto (fun (i : ℕ) ↦ @integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (a_1 : β) ↦ f (a, a_1) (seq i)) atTop
    (𝓝 (Measure.real.{u_2} (α := β) (m := mβ) ((ν : (a : α) → Measure β) a) univ))

Tactic:
exact hf.tendsto_integral_of_monotone a seq hseq hseq_tendsto

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_integral_of_monotone
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
t : β
ht : Monotone (f (a, t))
⊢ Monotone (β := ℝ) fun (i : ℕ) ↦ f (a, t) (seq i)

Tactic:
fun n m hnm ↦ ht (hseq hnm)

Premises used: Monotone
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (c : β) ↦ Monotone (f (a, c))) x} x →
          Membership.mem (γ := Set β) {x : β | (fun (a_3 : β) ↦ Monotone (β := ℝ) fun (i : ℕ) ↦ f (a, a_3) (seq i)) x}
            x}
      a_1
h₁ h₂ : ∀ (t : β) (ht : Monotone (f (a, t))), Monotone (β := ℝ) fun (i : ℕ) ↦ f (a, t) (seq i)
⊢ ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), Monotone (β := ℝ) fun (i : ℕ) ↦ f (a, a_1) (seq i)

Tactic:
filter_upwards [hf.mono a] with t ht using fun n m hnm ↦ ht (hseq hnm)

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.mono
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
c : β
hc : ∀ (q : ℚ), f (a, c) q ≤ 1
⊢ ∀ (i : ℕ), f (a, c) (seq i) ≤ 1

Tactic:
fun i ↦ hc (seq i)
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) {x : β | (fun (c : β) ↦ ∀ (q : ℚ), f (a, c) q ≤ 1) x} x →
          Membership.mem (γ := Set β) {x : β | (fun (a_3 : β) ↦ ∀ (i : ℕ), f (a, a_3) (seq i) ≤ 1) x} x}
      a_1
h₁ h₂ : ∀ (c : β) (hc : ∀ (q : ℚ), f (a, c) q ≤ 1) (i : ℕ), f (a, c) (seq i) ≤ 1
⊢ ∀ᵐ (a_1 : β) ∂((ν : (a : α) → Measure β) a : Measure β), ∀ (i : ℕ), f (a, a_1) (seq i) ≤ 1

Tactic:
filter_upwards [hf.le_one a] with c hc using fun i ↦ hc (seq i)

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.le_one
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
this :
  ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (↑n : ℚ)) atTop (𝓝 1)
h :
  ∀ (t : β) (ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (↑n : ℚ)) atTop (𝓝 1)) (h_mono : Monotone (f (a, t))),
    Tendsto (f (a, t)) atTop (𝓝 1)
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (f (a, t)) atTop (𝓝 1)

Tactic:
filter_upwards [this, hf.mono a] with t ht h_mono

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.mono
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
this :
  ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (↑n : ℚ)) atTop (𝓝 1)
t : β
ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (↑n : ℚ)) atTop (𝓝 1)
h_mono : Monotone (f (a, t))
h : Tendsto (f (a, t) ∘ Nat.cast) atTop (𝓝 1)
⊢ Tendsto (f (a, t)) atTop (𝓝 1)

Tactic:
rw [tendsto_iff_tendsto_subseq_of_monotone h_mono tendsto_natCast_atTop_atTop]

Premises used: tendsto_iff_tendsto_subseq_of_monotone, tendsto_natCast_atTop_atTop
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
this :
  ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (↑n : ℚ)) atTop (𝓝 1)
t : β
ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (↑n : ℚ)) atTop (𝓝 1)
h_mono : Monotone (f (a, t))
⊢ Tendsto (f (a, t) ∘ Nat.cast) atTop (𝓝 1)

Tactic:
ht
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
this :
  ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (↑n : ℚ)) atTop (𝓝 1)
t : β
ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (↑n : ℚ)) atTop (𝓝 1)
h_mono : Monotone (f (a, t))
⊢ Tendsto (f (a, t) ∘ Nat.cast) atTop (𝓝 1)

Tactic:
exact ht
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
suffices :
  ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (↑n : ℚ)) atTop (𝓝 1)
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (f (a, t)) atTop (𝓝 1)

Tactic:
suffices ∀ᵐ t ∂(ν a), Tendsto (fun (n : ℕ) ↦ f (a, t) n) atTop (𝓝 1) by
    filter_upwards [this, hf.mono a] with t ht h_mono
    rw [tendsto_iff_tendsto_subseq_of_monotone h_mono tendsto_natCast_atTop_atTop]
    exact ht
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
x : β
hx : Tendsto (β := ℝ) (fun (m : ℕ) ↦ f (a, x) (↑m : ℚ)) atTop (𝓝 1)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, x) (↑n : ℚ)) atTop (𝓝 1)

Tactic:
hx
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β | (fun (c : β) ↦ Tendsto (β := ℝ) (fun (m : ℕ) ↦ f (a, c) (↑m : ℚ)) atTop (𝓝 1)) x} x →
          Membership.mem (γ := Set β)
            {x : β | (fun (t : β) ↦ Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (↑n : ℚ)) atTop (𝓝 1)) x} x}
      a_1
h₁ h₂ :
  ∀ (x : β) (hx : Tendsto (β := ℝ) (fun (m : ℕ) ↦ f (a, x) (↑m : ℚ)) atTop (𝓝 1)),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, x) (↑n : ℚ)) atTop (𝓝 1)
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (↑n : ℚ)) atTop (𝓝 1)

Tactic:
filter_upwards [hf.tendsto_one_of_monotone a Nat.cast Nat.mono_cast tendsto_natCast_atTop_atTop]
    with x hx using hx

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_one_of_monotone, Nat.mono_cast, Nat.cast, tendsto_natCast_atTop_atTop
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (q : ℚ) ↦ f (a, t) (-q)) atTop (𝓝 0)
h : ∀ (t : β) (ht : Tendsto (β := ℝ) (fun (q : ℚ) ↦ f (a, t) (-q)) atTop (𝓝 0)), Tendsto (f (a, t)) atBot (𝓝 0)
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (f (a, t)) atBot (𝓝 0)

Tactic:
filter_upwards [this] with t ht
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (q : ℚ) ↦ f (a, t) (-q)) atTop (𝓝 0)
t : β
ht : Tendsto (β := ℝ) (fun (q : ℚ) ↦ f (a, t) (-q)) atTop (𝓝 0)
⊢ Tendsto (f (a, t)) atBot (𝓝 0)

Tactic:
tendsto_comp_neg_atTop_iff.mp ht

Premises used: Iff.mp, Filter.tendsto_comp_neg_atTop_iff
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (q : ℚ) ↦ f (a, t) (-q)) atTop (𝓝 0)
t : β
ht : Tendsto (β := ℝ) (fun (q : ℚ) ↦ f (a, t) (-q)) atTop (𝓝 0)
⊢ Tendsto (f (a, t)) atBot (𝓝 0)

Tactic:
exact tendsto_comp_neg_atTop_iff.mp ht

Premises used: Iff.mp, Filter.tendsto_comp_neg_atTop_iff
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
suffices :
  ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (q : ℚ) ↦ f (a, t) (-q)) atTop (𝓝 0)
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (f (a, t)) atBot (𝓝 0)

Tactic:
suffices ∀ᵐ t ∂(ν a), Tendsto (fun q : ℚ ↦ f (a, t) (-q)) atTop (𝓝 0) by
    filter_upwards [this] with t ht
    exact tendsto_comp_neg_atTop_iff.mp ht
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
this :
  ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (-(↑n : ℚ))) atTop (𝓝 0)
h :
  ∀ (t : β) (ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (-(↑n : ℚ))) atTop (𝓝 0)) (h_mono : Monotone (f (a, t))),
    Tendsto (β := ℝ) (fun (q : ℚ) ↦ f (a, t) (-q)) atTop (𝓝 0)
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (q : ℚ) ↦ f (a, t) (-q)) atTop (𝓝 0)

Tactic:
filter_upwards [this, hf.mono a] with t ht h_mono

Premises used: ProbabilityTheory.IsRatCondKernelCDFAux.mono
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
this :
  ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (-(↑n : ℚ))) atTop (𝓝 0)
t : β
ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (-(↑n : ℚ))) atTop (𝓝 0)
h_mono : Monotone (f (a, t))
⊢ Antitone (β := ℝ) fun (q : ℚ) ↦ f (a, t) (-q)

Tactic:
have h_anti : Antitone (fun q ↦ f (a, t) (-q)) := h_mono.comp_antitone monotone_id.neg
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
this :
  ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (-(↑n : ℚ))) atTop (𝓝 0)
t : β
ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (-(↑n : ℚ))) atTop (𝓝 0)
h_mono : Monotone (f (a, t))
h_anti : Antitone (β := ℝ) fun (q : ℚ) ↦ f (a, t) (-q)
⊢ Tendsto (β := ℝ) (fun (q : ℚ) ↦ f (a, t) (-q)) atTop (𝓝 0)

Tactic:
(tendsto_iff_tendsto_subseq_of_antitone h_anti tendsto_natCast_atTop_atTop).mpr ht

Premises used: Iff.mpr, tendsto_iff_tendsto_subseq_of_antitone, tendsto_natCast_atTop_atTop
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
this :
  ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (-(↑n : ℚ))) atTop (𝓝 0)
t : β
ht : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (-(↑n : ℚ))) atTop (𝓝 0)
h_mono : Monotone (f (a, t))
h_anti : Antitone (β := ℝ) fun (q : ℚ) ↦ f (a, t) (-q)
⊢ Tendsto (β := ℝ) (fun (q : ℚ) ↦ f (a, t) (-q)) atTop (𝓝 0)

Tactic:
exact (tendsto_iff_tendsto_subseq_of_antitone h_anti tendsto_natCast_atTop_atTop).mpr ht

Premises used: Iff.mpr, tendsto_iff_tendsto_subseq_of_antitone, tendsto_natCast_atTop_atTop
-- Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel ν
a : α
suffices :
  ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (a, t) (-(↑n : ℚ))) atTop (𝓝 0)
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (β := ℝ) (fun (q : ℚ) ↦ f (a, t) (-q)) atTop (𝓝 0)

Tactic:
suffices ∀ᵐ t ∂(ν a), Tendsto (fun (n : ℕ) ↦ f (a, t) (-n)) atTop (𝓝 0) by
    filter_upwards [this, hf.mono a] with t ht h_mono
    have h_anti : Antitone (fun q ↦ f (a, t) (-q)) := h_mono.comp_antitone monotone_id.neg
    exact (tendsto_iff_tendsto_subseq_of_antitone h_anti tendsto_natCast_atTop_atTop).mpr ht