English
For every t in [0,1] and for every z with ||z||<1, the norm of (1+t z)^{-1} is bounded by (1-||z||)^{-1}.
Русский
Для каждого t ∈ [0,1] и для каждого z с ||z||<1 величина ||(1+t z)^{-1}|| ограничена сверху (1-||z||)^{-1}.
LaTeX
$$$\\displaystyle \\| (1 + t z)^{-1} \\| \\le (1 - \\|z\\|)^{-1} \\quad \\text{при } t \\in [0,1], \\ \\|z\\| < 1$$$
Lean4
/-- Give a bound on `‖(1 + t * z)⁻¹‖` for `0 ≤ t ≤ 1` and `‖z‖ < 1`. -/
theorem norm_one_add_mul_inv_le {t : ℝ} (ht : t ∈ Set.Icc 0 1) {z : ℂ} (hz : ‖z‖ < 1) : ‖(1 + t * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹ :=
by
rw [Set.mem_Icc] at ht
rw [norm_inv]
refine inv_anti₀ (by linarith) ?_
calc
1 - ‖z‖
_ ≤ 1 - t * ‖z‖ := by nlinarith [norm_nonneg z]
_ = 1 - ‖t * z‖ := by rw [norm_mul, Complex.norm_of_nonneg ht.1]
_ ≤ ‖1 + t * z‖ := by
rw [← norm_neg (t * z), ← sub_neg_eq_add]
convert norm_sub_norm_le 1 (-(t * z))
exact norm_one.symm
