norm_log_one_add_half_le_self — Mathlib

English

If ∥z∥ ≤ 1/2, then ∥log(1+z)∥ ≤ (3/2) ∥z∥.

Русский

Если ∥z∥ ≤ 1/2, то ∥log(1+z)∥ ≤ (3/2) ∥z∥.

LaTeX

$$$\\|\\log(1+z)\\| \\le \\frac{3}{2}\\,\\|z\\| \\quad\\text{при } \\|z\\| \\le \\tfrac{1}{2}$$$

Lean4

/-- For `‖z‖ ≤ 1/2`, the complex logarithm is bounded by `(3/2) * ‖z‖`. -/
theorem norm_log_one_add_half_le_self {z : ℂ} (hz : ‖z‖ ≤ 1 / 2) : ‖log (1 + z)‖ ≤ (3 / 2) * ‖z‖ :=
  by
  apply le_trans (norm_log_one_add_le (lt_of_le_of_lt hz one_half_lt_one))
  have hz3 : (1 - ‖z‖)⁻¹ ≤ 2 := by
    rw [inv_eq_one_div, div_le_iff₀]
    · linarith
    · linarith
  have hz4 : ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 ≤ ‖z‖ / 2 * 2 / 2 :=
    by
    gcongr
    · rw [inv_nonneg]
      linarith
    · rw [sq, div_eq_mul_one_div]
      gcongr
  simp only [isUnit_iff_ne_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, IsUnit.div_mul_cancel] at hz4
  linarith

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