rpow_neg_one_add_norm_sq_le — Mathlib

English

For x in a normed space E and r > 0, ((1 + ‖x‖^2))^(-r/2) ≤ 2^(r/2) (1 + ‖x‖)^(-r).

Русский

Для x в нормированном пространстве E и r > 0, ((1 + ‖x‖^2))^(-r/2) ≤ 2^(r/2) (1 + ‖x‖)^(-r).

LaTeX

$$$$((1 + \|x\|^2))^{-r/2} \le 2^{r/2} (1 + \|x\|)^{-r} \quad (r > 0).$$$$

Lean4

theorem rpow_neg_one_add_norm_sq_le {r : ℝ} (x : E) (hr : 0 < r) :
    ((1 : ℝ) + ‖x‖ ^ 2) ^ (-r / 2) ≤ (2 : ℝ) ^ (r / 2) * (1 + ‖x‖) ^ (-r) :=
  calc
    ((1 : ℝ) + ‖x‖ ^ 2) ^ (-r / 2) = (2 : ℝ) ^ (r / 2) * ((√2 * √((1 : ℝ) + ‖x‖ ^ 2)) ^ r)⁻¹ := by
      rw [rpow_div_two_eq_sqrt, rpow_div_two_eq_sqrt, mul_rpow, mul_inv, rpow_neg, mul_inv_cancel_left₀] <;> positivity
    _ ≤ (2 : ℝ) ^ (r / 2) * ((1 + ‖x‖) ^ r)⁻¹ := by
      gcongr
      apply one_add_norm_le_sqrt_two_mul_sqrt
    _ = (2 : ℝ) ^ (r / 2) * (1 + ‖x‖) ^ (-r) := by rw [rpow_neg]; positivity

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