f_le_g_nat — Mathlib

English

For k ∈ ℕ, a ≥ 0, t > 0, and n ∈ ℕ, the absolute value of f_nat(k, a, t, n) is bounded by g_nat(k, a, t, n).

Русский

Для k ∈ ℕ, a ≥ 0, t > 0 и n ∈ ℕ выполняется неравенство |f_nat(k,a,t,n)| ≤ g_nat(k,a,t,n).

LaTeX

$$$\|f_{nat}(k,a,t,n)\| \le g_{nat}(k,a,t,n) \quad (k\in\mathbb{N}, a\ge 0, t>0, n\in\mathbb{N}).$$$

Lean4

theorem f_le_g_nat (k : ℕ) {a t : ℝ} (ha : 0 ≤ a) (ht : 0 < t) (n : ℕ) : ‖f_nat k a t n‖ ≤ g_nat k a t n :=
  by
  rw [f_nat, norm_of_nonneg (by positivity), g_nat]
  simp only [neg_mul, add_sq]
  gcongr
  have H₁ : (n : ℝ) ≤ n ^ 2 := mod_cast Nat.le_self_pow two_ne_zero n
  have H₂ : 0 ≤ 2 * n * a := by positivity
  linear_combination H₁ + H₂

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