English
For a subadditive u, hbdd ensures the lim of u(n)/n exists and equals the infimum of those quotients, with a LIM expression.
Русский
Для подпредпоследовательности u, ограничения снизу обеспечивают существование предела u(n)/n и его равенство инфу нижних значений.
LaTeX
$$$\text{lim} = \inf\{u(n)/n : n \ge 1\}$$$
Lean4
theorem integral_le_sum (hf : AntitoneOn f (Icc x₀ (x₀ + a))) :
(∫ x in x₀..x₀ + a, f x) ≤ ∑ i ∈ Finset.range a, f (x₀ + i) :=
by
have hint : ∀ k : ℕ, k < a → IntervalIntegrable f volume (x₀ + k) (x₀ + (k + 1 : ℕ)) :=
by
intro k hk
refine (hf.mono ?_).intervalIntegrable
rw [uIcc_of_le]
· apply Icc_subset_Icc
· simp only [le_add_iff_nonneg_right, Nat.cast_nonneg]
· simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt hk]
· simp only [add_le_add_iff_left, Nat.cast_le, Nat.le_succ]
calc
∫ x in x₀..x₀ + a, f x = ∑ i ∈ Finset.range a, ∫ x in x₀ + i..x₀ + (i + 1 : ℕ), f x :=
by
convert (intervalIntegral.sum_integral_adjacent_intervals hint).symm
simp only [Nat.cast_zero, add_zero]
_ ≤ ∑ i ∈ Finset.range a, ∫ _ in x₀ + i..x₀ + (i + 1 : ℕ), f (x₀ + i) :=
by
apply Finset.sum_le_sum fun i hi => ?_
have ia : i < a := Finset.mem_range.1 hi
refine intervalIntegral.integral_mono_on (by simp) (hint _ ia) (by simp) fun x hx => ?_
apply hf _ _ hx.1
·
simp only [ia.le, mem_Icc, le_add_iff_nonneg_right, Nat.cast_nonneg, add_le_add_iff_left, Nat.cast_le,
and_self_iff]
· refine mem_Icc.2 ⟨le_trans (by simp) hx.1, le_trans hx.2 ?_⟩
simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt ia]
_ = ∑ i ∈ Finset.range a, f (x₀ + i) := by simp
