TFAE_exists_lt_isLittleO_pow — Mathlib

English

A large theorem (TFAE) listing many equivalent statements about a function f growth relative to exponential rates a^n, including LittleO and BigO relations with a in various ranges and with absolute values.

Русский

Обобщенная теорема эквивалентности (TFAE) для множества утверждений о росте f относительно экспоненциальных степеней a^n, включая LittleO и BigO для разных диапазонов a и с учётом модулей.

LaTeX

$$$$TFAE_{exists\_lt\_isLittleO\_pow}(f,R)$$$$

Lean4

/-- Various statements equivalent to the fact that `f n` grows exponentially slower than `R ^ n`.

* 0: $f n = o(a ^ n)$ for some $-R < a < R$;
* 1: $f n = o(a ^ n)$ for some $0 < a < R$;
* 2: $f n = O(a ^ n)$ for some $-R < a < R$;
* 3: $f n = O(a ^ n)$ for some $0 < a < R$;
* 4: there exist `a < R` and `C` such that one of `C` and `R` is positive and $|f n| ≤ Ca^n$
  for all `n`;
* 5: there exists `0 < a < R` and a positive `C` such that $|f n| ≤ Ca^n$ for all `n`;
* 6: there exists `a < R` such that $|f n| ≤ a ^ n$ for sufficiently large `n`;
* 7: there exists `0 < a < R` such that $|f n| ≤ a ^ n$ for sufficiently large `n`.

NB: For backwards compatibility, if you add more items to the list, please append them at the end of
the list. -/
theorem TFAE_exists_lt_isLittleO_pow (f : ℕ → ℝ) (R : ℝ) :
    TFAE
      [∃ a ∈ Ioo (-R) R, f =o[atTop] (a ^ ·), ∃ a ∈ Ioo 0 R, f =o[atTop] (a ^ ·), ∃ a ∈ Ioo (-R) R, f =O[atTop] (a ^ ·),
        ∃ a ∈ Ioo 0 R, f =O[atTop] (a ^ ·), ∃ a < R, ∃ C : ℝ, (0 < C ∨ 0 < R) ∧ ∀ n, |f n| ≤ C * a ^ n,
        ∃ a ∈ Ioo 0 R, ∃ C > 0, ∀ n, |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ n in atTop, |f n| ≤ a ^ n,
        ∃ a ∈ Ioo 0 R, ∀ᶠ n in atTop, |f n| ≤ a ^ n] :=
  by
  have A : Ico 0 R ⊆ Ioo (-R) R := fun x hx ↦ ⟨(neg_lt_zero.2 (hx.1.trans_lt hx.2)).trans_le hx.1, hx.2⟩
  have B : Ioo 0 R ⊆ Ioo (-R) R := Subset.trans Ioo_subset_Ico_self A
  tfae_have 1 → 3 := fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩
  tfae_have 2 → 1 := fun ⟨a, ha, H⟩ ↦ ⟨a, B ha, H⟩
  tfae_have 3 → 2
    | ⟨a, ha, H⟩ => by
      rcases exists_between (abs_lt.2 ha) with ⟨b, hab, hbR⟩
      exact
        ⟨b, ⟨(abs_nonneg a).trans_lt hab, hbR⟩,
          H.trans_isLittleO (isLittleO_pow_pow_of_abs_lt_left (hab.trans_le (le_abs_self b)))⟩
  tfae_have 2 → 4 := fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩
  tfae_have 4 → 3 := fun ⟨a, ha, H⟩ ↦
    ⟨a, B ha, H⟩
      -- Add 5 and 6 using 4 → 6 → 5 → 3

  tfae_have 4 → 6
    | ⟨a, ha, H⟩ => by
      rcases bound_of_isBigO_nat_atTop H with ⟨C, hC₀, hC⟩
      refine ⟨a, ha, C, hC₀, fun n ↦ ?_⟩
      simpa only [Real.norm_eq_abs, abs_pow, abs_of_nonneg ha.1.le] using hC (pow_ne_zero n ha.1.ne')
  tfae_have 6 → 5 := fun ⟨a, ha, C, H₀, H⟩ ↦ ⟨a, ha.2, C, Or.inl H₀, H⟩
  tfae_have 5 → 3
    | ⟨a, ha, C, h₀, H⟩ =>
      by
      rcases sign_cases_of_C_mul_pow_nonneg fun n ↦ (abs_nonneg _).trans (H n) with (rfl | ⟨hC₀, ha₀⟩)
      · obtain rfl : f = 0 := by
          ext n
          simpa using H n
        simp only [lt_irrefl, false_or] at h₀
        exact ⟨0, ⟨neg_lt_zero.2 h₀, h₀⟩, isBigO_zero _ _⟩
      exact
        ⟨a, A ⟨ha₀, ha⟩, isBigO_of_le' _ fun n ↦ (H n).trans <| mul_le_mul_of_nonneg_left (le_abs_self _) hC₀.le⟩
          -- Add 7 and 8 using 2 → 8 → 7 → 3

  tfae_have 2 → 8
    | ⟨a, ha, H⟩ => by
      refine ⟨a, ha, (H.def zero_lt_one).mono fun n hn ↦ ?_⟩
      rwa [Real.norm_eq_abs, Real.norm_eq_abs, one_mul, abs_pow, abs_of_pos ha.1] at hn
  tfae_have 8 → 7 := fun ⟨a, ha, H⟩ ↦ ⟨a, ha.2, H⟩
  tfae_have 7 → 3
    | ⟨a, ha, H⟩ => by
      refine ⟨a, A ⟨?_, ha⟩, .of_norm_eventuallyLE H⟩
      exact nonneg_of_eventually_pow_nonneg (H.mono fun n ↦ (abs_nonneg _).trans)
  tfae_finish

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