English
For a fixed a, almost every t, the limit of f(a,t) as t→−∞ equals 0.
Русский
Для фиксированного a почти каждое t: предел f(a,t) при t→−∞ равен 0.
LaTeX
$$$\forall a,\; \text{ae}_{t\sim ν(a)}(\lim_{t\to-\infty} f(a,t)=0).$$$
Lean4
theorem tendsto_atBot_zero (hf : IsRatCondKernelCDFAux f κ ν) [IsFiniteKernel ν] (a : α) :
∀ᵐ t ∂(ν a), Tendsto (f (a, t)) atBot (𝓝 0) :=
by
suffices ∀ᵐ t ∂(ν a), Tendsto (fun q : ℚ ↦ f (a, t) (-q)) atTop (𝓝 0)
by
filter_upwards [this] with t ht
have h_eq_neg : f (a, t) = fun q : ℚ ↦ f (a, t) (- -q) := by simp_rw [neg_neg]
rw [h_eq_neg]
convert ht.comp tendsto_neg_atBot_atTop
simp
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
exact hf.tendsto_zero_of_antitone _ _ Nat.mono_cast.neg (tendsto_neg_atBot_iff.mpr tendsto_natCast_atTop_atTop)
