norm_natCast_cpow_le_norm_natCast_cpow_iff

English

For n > 1 and w,z ∈ ℂ, ‖(n)^w‖ ≤ ‖(n)^z‖ if and only if Re(w) ≤ Re(z).

Русский

Для n>1 и w,z ∈ ℂ, ‖n^w‖ ≤ ‖n^z‖ тогда и только тогда, когда Re(w) ≤ Re(z).

LaTeX

$$Let n > 1 and w,z ∈ ℂ. ‖(n)^w‖ ≤ ‖(n)^z‖ ⇔ Re(w) ≤ Re(z).$$

Lean4

theorem norm_natCast_cpow_le_norm_natCast_cpow_iff {n : ℕ} (hn : 1 < n) {w z : ℂ} :
    ‖(n : ℂ) ^ w‖ ≤ ‖(n : ℂ) ^ z‖ ↔ w.re ≤ z.re := by
  simp_rw [norm_natCast_cpow_of_pos (Nat.zero_lt_of_lt hn), Real.rpow_le_rpow_left_iff (Nat.one_lt_cast.mpr hn)]

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