sq_normThreshold_add_one_le — Mathlib

English

For all n, (normThreshold(a,n+1))^2 ≤ a^2(1+√2)^2 2^{n+2}.

Русский

Для всех n выполнено: (normThreshold(a,n+1))^2 ≤ a^2(1+√2)^2 2^{n+2}.

LaTeX

$$\\left(\\operatorname{normThreshold}(a,n+1)\\right)^2 \\le a^2\\,(1+\\sqrt{2})^2\\,2^{n+2}$$

Lean4

theorem sq_normThreshold_add_one_le (n : ℕ) : normThreshold a (n + 1) ^ 2 ≤ a ^ 2 * (1 + √2) ^ 2 * 2 ^ (n + 2) :=
  by
  simp_rw [normThreshold_eq, mul_pow, mul_assoc]
  gcongr
  calc
    (√2 ^ (n + 2) - 1) ^ 2
    _ ≤ (√2 ^ (n + 2)) ^ 2 := by
      gcongr
      ·
        calc
          0 ≤ √2 ^ (0 + 2) - 1 := by simp
          _ ≤ √2 ^ (n + 2) - 1 := by gcongr <;> simp
      · exact sub_le_self _ (by simp)
    _ = 2 ^ (n + 2) := by rw [← pow_mul, mul_comm, pow_mul, Real.sq_sqrt (by positivity)]

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