Source indexedlemma · leanprover/lean4:v4.32.0

Complex.norm_inv_pow_le_one_of_one_le_norm

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.Norm · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/Norm.lean:44 to 53

Source documentation

If ‖u‖ ≥ 1, then inverse powers of u have norm at most one.

Exact Lean statement

lemma norm_inv_pow_le_one_of_one_le_norm (u : ℂ) (n : ℕ) (hu : (1 : ℝ) ≤ ‖u‖) :
    ‖(u ^ n)⁻¹‖ ≤ 1

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma norm_inv_pow_le_one_of_one_le_norm (u : ℂ) (n : ℕ) (hu : (1 : ℝ) ≤ ‖u‖) :    ‖(u ^ n)⁻¹‖ ≤ 1 := by  have hge : (1 : ℝ) ≤ ‖u ^ n‖ := by    rw [Complex.norm_pow]    exact one_le_pow₀ hu  calc ‖(u ^ n)⁻¹‖ = ‖(1 : ℂ) / u ^ n‖ := by rw [inv_eq_one_div]    _ = 1 / ‖u ^ n‖ := by        have hone : ‖(1 : ℂ)‖ = (1 : ℝ) := by simpa using Complex.norm_natCast 1        rw [Complex.norm_div, hone]    _ ≤ 1 := by simpa [one_div] using inv_le_one_of_one_le₀ hge