English
For a subadditive sequence h, if hbdd holds, then h.lim is the limit of u(n)/n and div tends to that limit along atTop.
Русский
Для подпредпоследовательности h, если hbdd выполняется, тогда lim — предел u(n)/n и отношение стремится к этому пределу при n → ∞.
LaTeX
$$$\text{Tendsto}(n \mapsto u(n)/n) \text{ atTop } (\mathcal{nhds} (h.lim))$$$
Lean4
theorem sum_Ico_le_integral_of_le (hab : a ≤ b) (h : ∀ i ∈ Ico a b, ∀ x ∈ Ico (i : ℝ) (i + 1 : ℕ), f i ≤ g x)
(hg : IntegrableOn g (Set.Ico a b)) : ∑ i ∈ Finset.Ico a b, f i ≤ ∫ x in a..b, g x :=
by
have A i (hi : i ∈ Finset.Ico a b) : IntervalIntegrable g volume i (i + 1 : ℕ) :=
by
rw [intervalIntegrable_iff_integrableOn_Ico_of_le (by simp)]
apply hg.mono _ le_rfl
rintro x ⟨hx, h'x⟩
simp only [Finset.mem_Ico, mem_Ico] at hi ⊢
exact ⟨le_trans (mod_cast hi.1) hx, h'x.trans_le (mod_cast hi.2)⟩
calc
∑ i ∈ Finset.Ico a b, f i
_ = ∑ i ∈ Finset.Ico a b, (∫ x in (i : ℝ)..(i + 1 : ℕ), f i) := by simp
_ ≤ ∑ i ∈ Finset.Ico a b, (∫ x in (i : ℝ)..(i + 1 : ℕ), g x) :=
by
gcongr with i hi
apply intervalIntegral.integral_mono_on_of_le_Ioo (by simp) (by simp) (A _ hi) (fun x hx ↦ ?_)
exact h _ (by simpa using hi) _ (Ioo_subset_Ico_self hx)
_ = ∫ x in a..b, g x :=
by
rw [intervalIntegral.sum_integral_adjacent_intervals_Ico (a := fun i ↦ i) hab]
intro i hi
exact A _ (by simpa using hi)
