From 928698b7ca2081d8aae94bd8df7ca5d7032a0b59 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Fri, 28 Apr 2023 03:53:23 +0000 Subject: [PATCH] feat: port LinearAlgebra.Matrix.Zpow (#3671) Co-authored-by: Moritz Firsching --- Mathlib.lean | 1 + Mathlib/LinearAlgebra/Matrix/ZPow.lean | 357 +++++++++++++++++++++++++ 2 files changed, 358 insertions(+) create mode 100644 Mathlib/LinearAlgebra/Matrix/ZPow.lean diff --git a/Mathlib.lean b/Mathlib.lean index 06ce8aa3ed0cf6..bade665296a8ab 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1432,6 +1432,7 @@ import Mathlib.LinearAlgebra.Matrix.Polynomial import Mathlib.LinearAlgebra.Matrix.Reindex import Mathlib.LinearAlgebra.Matrix.Symmetric import Mathlib.LinearAlgebra.Matrix.Trace +import Mathlib.LinearAlgebra.Matrix.ZPow import Mathlib.LinearAlgebra.Multilinear.Basic import Mathlib.LinearAlgebra.Multilinear.Basis import Mathlib.LinearAlgebra.Multilinear.TensorProduct diff --git a/Mathlib/LinearAlgebra/Matrix/ZPow.lean b/Mathlib/LinearAlgebra/Matrix/ZPow.lean new file mode 100644 index 00000000000000..81f47cbf6994a8 --- /dev/null +++ b/Mathlib/LinearAlgebra/Matrix/ZPow.lean @@ -0,0 +1,357 @@ +/- +Copyright (c) 2021 Yakov Pechersky. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yakov Pechersky + +! This file was ported from Lean 3 source module linear_algebra.matrix.zpow +! leanprover-community/mathlib commit 03fda9112aa6708947da13944a19310684bfdfcb +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.LinearAlgebra.Matrix.NonsingularInverse + +/-! +# Integer powers of square matrices + +In this file, we define integer power of matrices, relying on +the nonsingular inverse definition for negative powers. + +## Implementation details + +The main definition is a direct recursive call on the integer inductive type, +as provided by the `DivInvMonoid.Pow` default implementation. +The lemma names are taken from `Algebra.group_with_zero.power`. + +## Tags + +matrix inverse, matrix powers +-/ + + +open Matrix + +namespace Matrix + +variable {n' : Type _} [DecidableEq n'] [Fintype n'] {R : Type _} [CommRing R] + +-- mathport name: exprM +local notation "M" => Matrix n' n' R + +noncomputable instance : DivInvMonoid M := + { show Monoid M by infer_instance, show Inv M by infer_instance with } + +section NatPow + +@[simp] +theorem inv_pow' (A : M) (n : ℕ) : A⁻¹ ^ n = (A ^ n)⁻¹ := by + induction' n with n ih + · simp + · rw [pow_succ A, mul_eq_mul, mul_inv_rev, ← ih, ← mul_eq_mul, ← pow_succ'] +#align matrix.inv_pow' Matrix.inv_pow' + +theorem pow_sub' (A : M) {m n : ℕ} (ha : IsUnit A.det) (h : n ≤ m) : + A ^ (m - n) = A ^ m ⬝ (A ^ n)⁻¹ := by + rw [← tsub_add_cancel_of_le h, pow_add, mul_eq_mul, Matrix.mul_assoc, mul_nonsing_inv, + tsub_add_cancel_of_le h, Matrix.mul_one] + simpa using ha.pow n +#align matrix.pow_sub' Matrix.pow_sub' + +theorem pow_inv_comm' (A : M) (m n : ℕ) : A⁻¹ ^ m ⬝ A ^ n = A ^ n ⬝ A⁻¹ ^ m := by + induction' n with n IH generalizing m + · simp + cases' m with m m + · simp + rcases nonsing_inv_cancel_or_zero A with (⟨h, h'⟩ | h) + · simp only [Nat.succ_eq_add_one] + calc + A⁻¹ ^ (m + 1) ⬝ A ^ (n + 1) = A⁻¹ ^ m ⬝ (A⁻¹ ⬝ A) ⬝ A ^ n := by + simp only [pow_succ' A⁻¹, pow_succ A, mul_eq_mul, Matrix.mul_assoc] + _ = A ^ n ⬝ A⁻¹ ^ m := by simp only [h, Matrix.mul_one, Matrix.one_mul, IH m] + _ = A ^ n ⬝ (A ⬝ A⁻¹) ⬝ A⁻¹ ^ m := by simp only [h', Matrix.mul_one, Matrix.one_mul] + _ = A ^ (n + 1) ⬝ A⁻¹ ^ (m + 1) := by + simp only [pow_succ' A, pow_succ A⁻¹, mul_eq_mul, Matrix.mul_assoc] + + · simp [h] +#align matrix.pow_inv_comm' Matrix.pow_inv_comm' + +end NatPow + +section ZPow + +open Int + +@[simp] +theorem one_zpow : ∀ n : ℤ, (1 : M) ^ n = 1 + | (n : ℕ) => by rw [zpow_ofNat, one_pow] + | -[n+1] => by rw [zpow_negSucc, one_pow, inv_one] +#align matrix.one_zpow Matrix.one_zpow + +theorem zero_zpow : ∀ z : ℤ, z ≠ 0 → (0 : M) ^ z = 0 + | (n : ℕ), h => by + rw [zpow_ofNat, zero_pow] + refine' lt_of_le_of_ne n.zero_le (Ne.symm _) + simpa using h + | -[n+1], _ => by simp [zero_pow n.zero_lt_succ] +#align matrix.zero_zpow Matrix.zero_zpow + +theorem zero_zpow_eq (n : ℤ) : (0 : M) ^ n = if n = 0 then 1 else 0 := by + split_ifs with h + · rw [h, zpow_zero] + · rw [zero_zpow _ h] +#align matrix.zero_zpow_eq Matrix.zero_zpow_eq + +theorem inv_zpow (A : M) : ∀ n : ℤ, A⁻¹ ^ n = (A ^ n)⁻¹ + | (n : ℕ) => by rw [zpow_ofNat, zpow_ofNat, inv_pow'] + | -[n+1] => by rw [zpow_negSucc, zpow_negSucc, inv_pow'] +#align matrix.inv_zpow Matrix.inv_zpow + +@[simp] +theorem zpow_neg_one (A : M) : A ^ (-1 : ℤ) = A⁻¹ := by + convert DivInvMonoid.zpow_neg' 0 A + simp only [zpow_one, Int.ofNat_zero, Int.ofNat_succ, zpow_eq_pow, zero_add] +#align matrix.zpow_neg_one Matrix.zpow_neg_one + +theorem zpow_coe_nat (A : M) (n : ℕ) : A ^ (n : ℤ) = A ^ n := + zpow_ofNat _ _ +#align matrix.zpow_coe_nat Matrix.zpow_coe_nat + +@[simp] +theorem zpow_neg_coe_nat (A : M) (n : ℕ) : A ^ (-n : ℤ) = (A ^ n)⁻¹ := by + cases n + · simp + · exact DivInvMonoid.zpow_neg' _ _ +#align matrix.zpow_neg_coe_nat Matrix.zpow_neg_coe_nat + +theorem _root_.IsUnit.det_zpow {A : M} (h : IsUnit A.det) (n : ℤ) : IsUnit (A ^ n).det := by + cases' n with n n + · simpa using h.pow n + · simpa using h.pow n.succ +#align is_unit.det_zpow IsUnit.det_zpow + +theorem isUnit_det_zpow_iff {A : M} {z : ℤ} : IsUnit (A ^ z).det ↔ IsUnit A.det ∨ z = 0 := by + induction' z using Int.induction_on with z _ z _ + · simp + · rw [← Int.ofNat_succ, zpow_ofNat, det_pow, isUnit_pow_succ_iff, ← Int.ofNat_zero, Int.ofNat_inj] + simp + · rw [← neg_add', ← Int.ofNat_succ, zpow_neg_coe_nat, isUnit_nonsing_inv_det_iff, det_pow, + isUnit_pow_succ_iff, neg_eq_zero, ← Int.ofNat_zero, Int.ofNat_inj] + simp +#align matrix.is_unit_det_zpow_iff Matrix.isUnit_det_zpow_iff + +theorem zpow_neg {A : M} (h : IsUnit A.det) : ∀ n : ℤ, A ^ (-n) = (A ^ n)⁻¹ + | (n : ℕ) => zpow_neg_coe_nat _ _ + | -[n+1] => by + rw [zpow_negSucc, neg_negSucc, zpow_ofNat, nonsing_inv_nonsing_inv] + rw [det_pow] + exact h.pow _ +#align matrix.zpow_neg Matrix.zpow_neg + +theorem inv_zpow' {A : M} (h : IsUnit A.det) (n : ℤ) : A⁻¹ ^ n = A ^ (-n) := by + rw [zpow_neg h, inv_zpow] +#align matrix.inv_zpow' Matrix.inv_zpow' + +theorem zpow_add_one {A : M} (h : IsUnit A.det) : ∀ n : ℤ, A ^ (n + 1) = A ^ n * A + | (n : ℕ) => by simp only [← Nat.cast_succ, pow_succ', zpow_ofNat] + | -((n : ℕ) + 1) => + calc + A ^ (-(n + 1) + 1 : ℤ) = (A ^ n)⁻¹ := by + rw [neg_add, neg_add_cancel_right, zpow_neg h, zpow_ofNat] + _ = (A ⬝ A ^ n)⁻¹ ⬝ A := by + rw [mul_inv_rev, Matrix.mul_assoc, nonsing_inv_mul _ h, Matrix.mul_one] + _ = A ^ (-(n + 1 : ℤ)) * A := by + rw [zpow_neg h, ← Int.ofNat_succ, zpow_ofNat, pow_succ, mul_eq_mul, mul_eq_mul] + +#align matrix.zpow_add_one Matrix.zpow_add_one + +theorem zpow_sub_one {A : M} (h : IsUnit A.det) (n : ℤ) : A ^ (n - 1) = A ^ n * A⁻¹ := + calc + A ^ (n - 1) = A ^ (n - 1) * A * A⁻¹ := by + rw [mul_assoc, mul_eq_mul A, mul_nonsing_inv _ h, mul_one] + _ = A ^ n * A⁻¹ := by rw [← zpow_add_one h, sub_add_cancel] + +#align matrix.zpow_sub_one Matrix.zpow_sub_one + +theorem zpow_add {A : M} (ha : IsUnit A.det) (m n : ℤ) : A ^ (m + n) = A ^ m * A ^ n := by + induction' n using Int.induction_on with n ihn n ihn + case hz => simp + · simp only [← add_assoc, zpow_add_one ha, ihn, mul_assoc] + · rw [zpow_sub_one ha, ← mul_assoc, ← ihn, ← zpow_sub_one ha, add_sub_assoc] +#align matrix.zpow_add Matrix.zpow_add + +theorem zpow_add_of_nonpos {A : M} {m n : ℤ} (hm : m ≤ 0) (hn : n ≤ 0) : + A ^ (m + n) = A ^ m * A ^ n := by + rcases nonsing_inv_cancel_or_zero A with (⟨h, _⟩ | h) + · exact zpow_add (isUnit_det_of_left_inverse h) m n + · obtain ⟨k, rfl⟩ := exists_eq_neg_ofNat hm + obtain ⟨l, rfl⟩ := exists_eq_neg_ofNat hn + simp_rw [← neg_add, ← Int.ofNat_add, zpow_neg_coe_nat, ← inv_pow', h, pow_add] +#align matrix.zpow_add_of_nonpos Matrix.zpow_add_of_nonpos + +theorem zpow_add_of_nonneg {A : M} {m n : ℤ} (hm : 0 ≤ m) (hn : 0 ≤ n) : + A ^ (m + n) = A ^ m * A ^ n := by + obtain ⟨k, rfl⟩ := eq_ofNat_of_zero_le hm + obtain ⟨l, rfl⟩ := eq_ofNat_of_zero_le hn + rw [← Int.ofNat_add, zpow_ofNat, zpow_ofNat, zpow_ofNat, pow_add] +#align matrix.zpow_add_of_nonneg Matrix.zpow_add_of_nonneg + +theorem zpow_one_add {A : M} (h : IsUnit A.det) (i : ℤ) : A ^ (1 + i) = A * A ^ i := by + rw [zpow_add h, zpow_one] +#align matrix.zpow_one_add Matrix.zpow_one_add + +theorem SemiconjBy.zpow_right {A X Y : M} (hx : IsUnit X.det) (hy : IsUnit Y.det) + (h : SemiconjBy A X Y) : ∀ m : ℤ, SemiconjBy A (X ^ m) (Y ^ m) + | (n : ℕ) => by simp [h.pow_right n] + | -[n+1] => by + have hx' : IsUnit (X ^ n.succ).det := by + rw [det_pow] + exact hx.pow n.succ + have hy' : IsUnit (Y ^ n.succ).det := by + rw [det_pow] + exact hy.pow n.succ + rw [zpow_negSucc, zpow_negSucc, nonsing_inv_apply _ hx', nonsing_inv_apply _ hy', SemiconjBy] + refine' (isRegular_of_isLeftRegular_det hy'.isRegular.left).left _ + dsimp only + rw [← mul_assoc, ← (h.pow_right n.succ).eq, mul_assoc, mul_eq_mul (X ^ _), mul_smul, + mul_adjugate, mul_eq_mul, mul_eq_mul, mul_eq_mul, ← Matrix.mul_assoc, + mul_smul (Y ^ _) (↑hy'.unit⁻¹ : R), mul_adjugate, smul_smul, smul_smul, hx'.val_inv_mul, + hy'.val_inv_mul, one_smul, Matrix.mul_one, Matrix.one_mul] +#align matrix.semiconj_by.zpow_right Matrix.SemiconjBy.zpow_right + +theorem Commute.zpow_right {A B : M} (h : Commute A B) (m : ℤ) : Commute A (B ^ m) := by + rcases nonsing_inv_cancel_or_zero B with (⟨hB, _⟩ | hB) + · refine' SemiconjBy.zpow_right _ _ h _ <;> exact isUnit_det_of_left_inverse hB + · cases m + · simpa using h.pow_right _ + · simp [← inv_pow', hB] +#align matrix.commute.zpow_right Matrix.Commute.zpow_right + +theorem Commute.zpow_left {A B : M} (h : Commute A B) (m : ℤ) : Commute (A ^ m) B := + (Commute.zpow_right h.symm m).symm +#align matrix.commute.zpow_left Matrix.Commute.zpow_left + +theorem Commute.zpow_zpow {A B : M} (h : Commute A B) (m n : ℤ) : Commute (A ^ m) (B ^ n) := + Commute.zpow_right (Commute.zpow_left h _) _ +#align matrix.commute.zpow_zpow Matrix.Commute.zpow_zpow + +theorem Commute.zpow_self (A : M) (n : ℤ) : Commute (A ^ n) A := + Commute.zpow_left (Commute.refl A) _ +#align matrix.commute.zpow_self Matrix.Commute.zpow_self + +theorem Commute.self_zpow (A : M) (n : ℤ) : Commute A (A ^ n) := + Commute.zpow_right (Commute.refl A) _ +#align matrix.commute.self_zpow Matrix.Commute.self_zpow + +theorem Commute.zpow_zpow_self (A : M) (m n : ℤ) : Commute (A ^ m) (A ^ n) := + Commute.zpow_zpow (Commute.refl A) _ _ +#align matrix.commute.zpow_zpow_self Matrix.Commute.zpow_zpow_self + +set_option linter.deprecated false in +theorem zpow_bit0 (A : M) (n : ℤ) : A ^ bit0 n = A ^ n * A ^ n := by + cases' le_total 0 n with nonneg nonpos + · exact zpow_add_of_nonneg nonneg nonneg + · exact zpow_add_of_nonpos nonpos nonpos +#align matrix.zpow_bit0 Matrix.zpow_bit0 + +theorem zpow_add_one_of_ne_neg_one {A : M} : ∀ n : ℤ, n ≠ -1 → A ^ (n + 1) = A ^ n * A + | (n : ℕ), _ => by simp only [pow_succ', ← Nat.cast_succ, zpow_ofNat] + | -1, h => absurd rfl h + | -((n : ℕ) + 2), _ => by + rcases nonsing_inv_cancel_or_zero A with (⟨h, _⟩ | h) + · apply zpow_add_one (isUnit_det_of_left_inverse h) + · show A ^ (-((n + 1 : ℕ) : ℤ)) = A ^ (-((n + 2 : ℕ) : ℤ)) * A + simp_rw [zpow_neg_coe_nat, ← inv_pow', h, zero_pow Nat.succ_pos', MulZeroClass.zero_mul] +#align matrix.zpow_add_one_of_ne_neg_one Matrix.zpow_add_one_of_ne_neg_one + +set_option linter.deprecated false in +theorem zpow_bit1 (A : M) (n : ℤ) : A ^ bit1 n = A ^ n * A ^ n * A := by + rw [bit1, zpow_add_one_of_ne_neg_one, zpow_bit0] + intro h + simpa using congr_arg bodd h +#align matrix.zpow_bit1 Matrix.zpow_bit1 + +theorem zpow_mul (A : M) (h : IsUnit A.det) : ∀ m n : ℤ, A ^ (m * n) = (A ^ m) ^ n + | (m : ℕ), (n : ℕ) => by rw [zpow_ofNat, zpow_ofNat, ← pow_mul, ← zpow_ofNat, Int.ofNat_mul] + | (m : ℕ), -[n+1] => by + rw [zpow_ofNat, zpow_negSucc, ← pow_mul, ofNat_mul_negSucc, zpow_neg_coe_nat] + | -[m+1], (n : ℕ) => by + rw [zpow_ofNat, zpow_negSucc, ← inv_pow', ← pow_mul, negSucc_mul_ofNat, zpow_neg_coe_nat, + inv_pow'] + | -[m+1], -[n+1] => by + rw [zpow_negSucc, zpow_negSucc, negSucc_mul_negSucc, ← Int.ofNat_mul, zpow_ofNat, inv_pow', ← + pow_mul, nonsing_inv_nonsing_inv] + rw [det_pow] + exact h.pow _ +#align matrix.zpow_mul Matrix.zpow_mul + +theorem zpow_mul' (A : M) (h : IsUnit A.det) (m n : ℤ) : A ^ (m * n) = (A ^ n) ^ m := by + rw [mul_comm, zpow_mul _ h] +#align matrix.zpow_mul' Matrix.zpow_mul' + + +@[simp, norm_cast] +theorem coe_units_zpow (u : Mˣ) : ∀ n : ℤ, ((u ^ n : Mˣ) : M) = (u : M) ^ n + | (n : ℕ) => by rw [_root_.zpow_coe_nat, zpow_ofNat, Units.val_pow_eq_pow_val] + | -[k+1] => by + rw [zpow_negSucc, zpow_negSucc, ← inv_pow, u⁻¹.val_pow_eq_pow_val, ← inv_pow', coe_units_inv] +#align matrix.coe_units_zpow Matrix.coe_units_zpow + +theorem zpow_ne_zero_of_isUnit_det [Nonempty n'] [Nontrivial R] {A : M} (ha : IsUnit A.det) + (z : ℤ) : A ^ z ≠ 0 := by + have := ha.det_zpow z + -- oorting note: was `contrapose! this` + revert this + contrapose! + rw [ne_eq, not_not] + intro this + rw [this, det_zero ‹_›] + exact not_isUnit_zero +#align matrix.zpow_ne_zero_of_is_unit_det Matrix.zpow_ne_zero_of_isUnit_det + +theorem zpow_sub {A : M} (ha : IsUnit A.det) (z1 z2 : ℤ) : A ^ (z1 - z2) = A ^ z1 / A ^ z2 := by + rw [sub_eq_add_neg, zpow_add ha, zpow_neg ha, div_eq_mul_inv] +#align matrix.zpow_sub Matrix.zpow_sub + +theorem Commute.mul_zpow {A B : M} (h : Commute A B) : ∀ i : ℤ, (A * B) ^ i = A ^ i * B ^ i + | (n : ℕ) => by simp [h.mul_pow n, -mul_eq_mul] + | -[n+1] => by + rw [zpow_negSucc, zpow_negSucc, zpow_negSucc, mul_eq_mul _⁻¹, ← mul_inv_rev, ← mul_eq_mul, + h.mul_pow n.succ, (h.pow_pow _ _).eq] +#align matrix.commute.mul_zpow Matrix.Commute.mul_zpow + +set_option linter.deprecated false in +theorem zpow_bit0' (A : M) (n : ℤ) : A ^ bit0 n = (A * A) ^ n := + (zpow_bit0 A n).trans (Commute.mul_zpow (Commute.refl A) n).symm +#align matrix.zpow_bit0' Matrix.zpow_bit0' + +set_option linter.deprecated false in +theorem zpow_bit1' (A : M) (n : ℤ) : A ^ bit1 n = (A * A) ^ n * A := by + rw [zpow_bit1, Commute.mul_zpow (Commute.refl A)] +#align matrix.zpow_bit1' Matrix.zpow_bit1' + +theorem zpow_neg_mul_zpow_self (n : ℤ) {A : M} (h : IsUnit A.det) : A ^ (-n) * A ^ n = 1 := by + rw [zpow_neg h, mul_eq_mul, nonsing_inv_mul _ (h.det_zpow _)] +#align matrix.zpow_neg_mul_zpow_self Matrix.zpow_neg_mul_zpow_self + +theorem one_div_pow {A : M} (n : ℕ) : (1 / A) ^ n = 1 / A ^ n := by simp only [one_div, inv_pow'] +#align matrix.one_div_pow Matrix.one_div_pow + +theorem one_div_zpow {A : M} (n : ℤ) : (1 / A) ^ n = 1 / A ^ n := by simp only [one_div, inv_zpow] +#align matrix.one_div_zpow Matrix.one_div_zpow + +@[simp] +theorem transpose_zpow (A : M) : ∀ n : ℤ, (A ^ n)ᵀ = Aᵀ ^ n + | (n : ℕ) => by rw [zpow_ofNat, zpow_ofNat, transpose_pow] + | -[n+1] => by rw [zpow_negSucc, zpow_negSucc, transpose_nonsing_inv, transpose_pow] +#align matrix.transpose_zpow Matrix.transpose_zpow + +-- porting note: without etaExperiment, conjTranspose_pow can't find the StarRing R instance. +set_option synthInstance.etaExperiment true in +@[simp] +theorem conjTranspose_zpow [StarRing R] (A : M) : ∀ n : ℤ, (A ^ n)ᴴ = Aᴴ ^ n + | (n : ℕ) => by rw [zpow_ofNat, zpow_ofNat, conjTranspose_pow] + | -[n+1] => by rw [zpow_negSucc, zpow_negSucc, conjTranspose_nonsing_inv, conjTranspose_pow] +#align matrix.conj_transpose_zpow Matrix.conjTranspose_zpow + +end ZPow + +end Matrix