linearGrowthInf_comp — Mathlib

English

If u is monotone, and Tendsto (v(n)/n) to a (finite, nonzero, not top) then linearGrowthInf(u ∘ v) = a · linearGrowthInf(u).

Русский

Пусть u монотонна; если v(n)/n сходится к a (конечному, не нулю и не бесконечности), то линейный нижний рост композиции равен a · линейному нижнему росту u.

LaTeX

$$$\operatorname{linearGrowthInf}(u \circ v) = a \cdot \operatorname{linearGrowthInf}(u)$$$

Lean4

theorem _root_.Monotone.linearGrowthInf_comp {a : EReal} (h : Monotone u)
    (hv : Tendsto (fun n ↦ (v n : EReal) / n) atTop (𝓝 a)) (ha : a ≠ 0) (ha' : a ≠ ⊤) :
    linearGrowthInf (u ∘ v) = a * linearGrowthInf u :=
  by
  have hv₁ : 0 < liminf (fun n ↦ (v n : EReal) / n) atTop :=
    by
    rw [← hv.liminf_eq] at ha
    exact ha.symm.lt_of_le (linearGrowthInf_natCast_nonneg v)
  have v_top := tendsto_atTop_of_linearGrowthInf_natCast_pos hv₁.ne.symm
  by_cases u_0 : u = ⊥
  · rw [u_0, Pi.bot_comp, linearGrowthInf_bot, ← hv.liminf_eq, mul_bot_of_pos hv₁]
  by_cases h1 : ∃ᶠ n : ℕ in atTop, u n ≤ 0
  · replace h' (n : ℕ) : u n ≤ 0 := by
      obtain ⟨m, n_m, um_1⟩ := (frequently_atTop.1 h1) n
      exact (h n_m).trans um_1
    have u_0' : linearGrowthInf u = 0 :=
      by
      apply le_antisymm _ (h.linearGrowthInf_nonneg u_0)
      exact (linearGrowthInf_monotone h').trans_eq (linearGrowthInf_const zero_ne_bot zero_ne_top)
    rw [u_0', mul_zero]
    apply le_antisymm _ (linearGrowthInf_comp_nonneg h u_0 v_top)
    apply (linearGrowthInf_monotone fun n ↦ h' (v n)).trans_eq
    exact linearGrowthInf_const zero_ne_bot zero_ne_top
  · replace h' := (not_frequently.1 h1).mono fun _ hn ↦ le_of_not_ge hn
    apply le_antisymm
    · rw [← hv.limsup_eq] at ha ha' ⊢
      exact h.linearGrowthInf_comp_le ha ha'
    · rw [← hv.liminf_eq]
      exact le_linearGrowthInf_comp h' v_top

Похожие утверждения