Merge branch 'master' into Komyyy/Mathlib.Init.ZeroOne

Author: Komyyy

Mathlib.lean

@@ -1214,6 +1214,7 @@ import Mathlib.Analysis.SpecialFunctions.Complex.Circle
 import Mathlib.Analysis.SpecialFunctions.Complex.Log
 import Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
 import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
+import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog
 import Mathlib.Analysis.SpecialFunctions.Exp
 import Mathlib.Analysis.SpecialFunctions.ExpDeriv
 import Mathlib.Analysis.SpecialFunctions.Exponential
@@ -3847,6 +3848,7 @@ import Mathlib.RingTheory.TensorProduct.MvPolynomial
 import Mathlib.RingTheory.Trace.Basic
 import Mathlib.RingTheory.Trace.Defs
 import Mathlib.RingTheory.TwoSidedIdeal.Basic
+import Mathlib.RingTheory.TwoSidedIdeal.Lattice
 import Mathlib.RingTheory.UniqueFactorizationDomain
 import Mathlib.RingTheory.Unramified.Basic
 import Mathlib.RingTheory.Unramified.Derivations

Mathlib/Algebra/Polynomial/Smeval.lean

@@ -5,8 +5,6 @@ Authors: Scott Carnahan
 -/
 import Mathlib.Algebra.Group.NatPowAssoc
 import Mathlib.Algebra.Polynomial.AlgebraMap
-import Mathlib.Algebra.Polynomial.Induction
-import Mathlib.Algebra.Polynomial.Eval
 
 /-!
 # Scalar-multiple polynomial evaluation
@@ -292,6 +290,43 @@ theorem smeval_comp : (p.comp q).smeval x  = p.smeval (q.smeval x) := by
 
 end NatPowAssoc
 
+section Commute
+
+variable (R : Type*) [Semiring R] (p q : R[X]) {S : Type*} [Semiring S]
+  [Module R S] [IsScalarTower R S S] [SMulCommClass R S S] {x y : S}
+
+theorem smeval_commute_left (hc : Commute x y) : Commute (p.smeval x) y := by
+  induction p using Polynomial.induction_on' with
+  | h_add r s hr hs => exact (smeval_add R r s x) ▸ Commute.add_left hr hs
+  | h_monomial n a =>
+    simp only [smeval_monomial]
+    refine Commute.smul_left ?_ a
+    induction n with
+    | zero => simp only [npow_zero, Commute.one_left]
+    | succ n ih =>
+      refine (commute_iff_eq (x ^ (n + 1)) y).mpr ?_
+      rw [commute_iff_eq (x ^ n) y] at ih
+      rw [pow_succ, ← mul_assoc, ← ih]
+      exact Commute.right_comm hc (x ^ n)
+
+theorem smeval_commute (hc : Commute x y) : Commute (p.smeval x) (q.smeval y) := by
+  induction p using Polynomial.induction_on' with
+  | h_add r s hr hs => exact (smeval_add R r s x) ▸ Commute.add_left hr hs
+  | h_monomial n a =>
+    simp only [smeval_monomial]
+    refine Commute.smul_left ?_ a
+    induction n with
+    | zero => simp only [npow_zero, Commute.one_left]
+    | succ n ih =>
+      refine (commute_iff_eq (x ^ (n + 1)) (q.smeval y)).mpr ?_
+      rw [commute_iff_eq (x ^ n) (q.smeval y)] at ih
+      have hxq : x * q.smeval y = q.smeval y * x := by
+        refine (commute_iff_eq x (q.smeval y)).mp ?_
+        exact Commute.symm (smeval_commute_left R q (Commute.symm hc))
+      rw [pow_succ, ← mul_assoc, ← ih, mul_assoc, hxq, mul_assoc]
+
+end Commute
+
 section Algebra
 
 theorem aeval_eq_smeval {R : Type*} [CommSemiring R] {S : Type*} [Semiring S] [Algebra R S]

Mathlib/Algebra/Polynomial/UnitTrinomial.lean

@@ -150,7 +150,7 @@ theorem card_support_eq_three (hp : p.IsUnitTrinomial) : p.support.card = 3 := b
 
 theorem ne_zero (hp : p.IsUnitTrinomial) : p ≠ 0 := by
   rintro rfl
-  exact Nat.zero_ne_bit1 1 hp.card_support_eq_three
+  simpa using hp.card_support_eq_three
 #align polynomial.is_unit_trinomial.ne_zero Polynomial.IsUnitTrinomial.ne_zero
 
 theorem coeff_isUnit (hp : p.IsUnitTrinomial) {k : ℕ} (hk : k ∈ p.support) :

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean

@@ -0,0 +1,163 @@
+/-
+Copyright (c) 2024 Frédéric Dupuis. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Frédéric Dupuis
+-/
+
+import Mathlib.Analysis.NormedSpace.Spectrum
+import Mathlib.Analysis.SpecialFunctions.Exponential
+import Mathlib.Topology.ContinuousFunction.FunctionalCalculus
+
+/-!
+# The exponential and logarithm based on the continuous functional calculus
+
+This file defines the logarithm via the continuous functional calculus (CFC) and builds its API.
+This allows one to take logs of matrices, operators, elements of a C⋆-algebra, etc.
+
+It also shows that exponentials defined via the continuous functional calculus are equal to
+`NormedSpace.exp` (defined via power series) whenever the former are not junk values.
+
+## Main declarations
+
++ `CFC.log`: the real log function based on the CFC, i.e. `cfc Real.log`
++ `CFC.exp_eq_normedSpace_exp`: exponentials based on the CFC are equal to exponentials based
+  on power series.
++ `CFC.log_exp` and `CFC.exp_log`: `CFC.log` and `NormedSpace.exp ℝ` are inverses of each other.
+
+## Implementation notes
+
+Since `cfc Real.exp` and `cfc Complex.exp` are strictly less general than `NormedSpace.exp`
+(defined via power series), we only give minimal API for these here in order to relate
+`NormedSpace.exp` to functions defined via the CFC. In particular, we don't give separate
+definitions for them.
+
+## TODO
+
++ Show that `log (a * b) = log a + log b` whenever `a` and `b` commute (and the same for indexed
+  products).
++ Relate `CFC.log` to `rpow`, `zpow`, `sqrt`, `inv`.
+-/
+
+open NormedSpace
+
+section general_exponential
+variable {𝕜 : Type*} {α : Type*} [RCLike 𝕜] [TopologicalSpace α] [CompactSpace α]
+
+lemma NormedSpace.exp_continuousMap_eq (f : C(α, 𝕜)) :
+    exp 𝕜 f = (⟨exp 𝕜 ∘ f, exp_continuous.comp f.continuous⟩ : C(α, 𝕜)) := by
+  ext a
+  simp only [Function.comp_apply, NormedSpace.exp, FormalMultilinearSeries.sum]
+  have h_sum := NormedSpace.expSeries_summable (𝕂 := 𝕜) f
+  simp_rw [← ContinuousMap.tsum_apply h_sum a, NormedSpace.expSeries_apply_eq]
+  simp [NormedSpace.exp_eq_tsum]
+
+end general_exponential
+
+namespace CFC
+section RCLikeNormed
+
+variable {𝕜 : Type*} {A : Type*} [RCLike 𝕜] {p : A → Prop} [PartialOrder A] [NormedRing A]
+  [StarRing A] [StarOrderedRing A] [TopologicalRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A]
+  [ContinuousFunctionalCalculus 𝕜 p]
+  [UniqueContinuousFunctionalCalculus 𝕜 A]
+
+lemma exp_eq_normedSpace_exp {a : A} (ha : p a := by cfc_tac) :
+    cfc (exp 𝕜 : 𝕜 → 𝕜) a = exp 𝕜 a := by
+  conv_rhs => rw [← cfc_id 𝕜 a ha, cfc_apply id a ha]
+  have h := (cfcHom_closedEmbedding (R := 𝕜) (show p a from ha)).continuous
+  have _ : ContinuousOn (exp 𝕜) (spectrum 𝕜 a) := exp_continuous.continuousOn
+  simp_rw [← map_exp 𝕜 _ h, cfc_apply (exp 𝕜) a ha]
+  congr 1
+  ext
+  simp [exp_continuousMap_eq]
+
+end RCLikeNormed
+
+section RealNormed
+
+variable {A : Type*} {p : A → Prop} [PartialOrder A] [NormedRing A] [StarRing A] [StarOrderedRing A]
+  [TopologicalRing A] [NormedAlgebra ℝ A] [CompleteSpace A]
+  [ContinuousFunctionalCalculus ℝ p]
+  [UniqueContinuousFunctionalCalculus ℝ A]
+
+lemma real_exp_eq_normedSpace_exp {a : A} (ha : p a := by cfc_tac) :
+    cfc Real.exp a = exp ℝ a :=
+  Real.exp_eq_exp_ℝ ▸ exp_eq_normedSpace_exp ha
+
+end RealNormed
+
+section ComplexNormed
+
+variable {A : Type*} {p : A → Prop} [PartialOrder A] [NormedRing A] [StarRing A] [StarOrderedRing A]
+  [TopologicalRing A] [NormedAlgebra ℂ A] [CompleteSpace A]
+  [ContinuousFunctionalCalculus ℂ p]
+  [UniqueContinuousFunctionalCalculus ℂ A]
+
+lemma complex_exp_eq_normedSpace_exp {a : A} (ha : p a := by cfc_tac) :
+    cfc Complex.exp a = exp ℂ a :=
+  Complex.exp_eq_exp_ℂ ▸ exp_eq_normedSpace_exp ha
+
+end ComplexNormed
+
+
+section real_log
+
+open scoped ComplexOrder
+
+variable {A : Type*} [PartialOrder A] [NormedRing A] [StarRing A] [StarOrderedRing A]
+  [TopologicalRing A] [NormedAlgebra ℝ A] [CompleteSpace A]
+  [ContinuousFunctionalCalculus ℝ (IsSelfAdjoint : A → Prop)]
+  [UniqueContinuousFunctionalCalculus ℝ A]
+
+/-- The real logarithm, defined via the continuous functional calculus. This can be used on
+matrices, operators on a Hilbert space, elements of a C⋆-algebra, etc. -/
+noncomputable def log (a : A) : A := cfc Real.log a
+
+@[simp]
+protected lemma _root_.IsSelfAdjoint.log {a : A} : IsSelfAdjoint (log a) := cfc_predicate _ a
+
+lemma log_exp (a : A) (ha : IsSelfAdjoint a := by cfc_tac) : log (NormedSpace.exp ℝ a) = a := by
+  have hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a) := by fun_prop (disch := aesop)
+  rw [log, ← real_exp_eq_normedSpace_exp, ← cfc_comp' Real.log Real.exp a hcont]
+  simp [cfc_id' (R := ℝ) a]
+
+-- TODO: Relate the hypothesis to a notion of strict positivity
+lemma exp_log (a : A) (ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x) (ha₁ : IsSelfAdjoint a := by cfc_tac) :
+    NormedSpace.exp ℝ (log a) = a := by
+  have ha₃ : ContinuousOn Real.log (spectrum ℝ a) := by
+    have : ∀ x ∈ spectrum ℝ a, x ≠ 0 := by peel ha₂ with x hx h; exact h.ne'
+    fun_prop (disch := assumption)
+  rw [← real_exp_eq_normedSpace_exp .log, log, ← cfc_comp' Real.exp Real.log a (by fun_prop) ha₃]
+  conv_rhs => rw [← cfc_id (R := ℝ) a ha₁]
+  exact cfc_congr (Real.exp_log <| ha₂ · ·)
+
+@[simp] lemma log_zero : log (0 : A) = 0 := by simp [log]
+
+@[simp] lemma log_one : log (1 : A) = 0 := by simp [log]
+
+@[simp]
+lemma log_algebraMap {r : ℝ} : log (algebraMap ℝ A r) = algebraMap ℝ A (Real.log r) := by
+  simp [log]
+
+-- TODO: Relate the hypothesis to a notion of strict positivity
+lemma log_smul {r : ℝ} (a : A) (ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x) (hr : 0 < r)
+    (ha₁ : IsSelfAdjoint a := by cfc_tac) :
+    log (r • a) = algebraMap ℝ A (Real.log r) + log a := by
+  have : ∀ x ∈ spectrum ℝ a, x ≠ 0 := by peel ha₂ with x hx h; exact h.ne'
+  rw [log, ← cfc_smul_id (R := ℝ) r a, ← cfc_comp Real.log (r • ·) a, log]
+  calc
+    _ = cfc (fun z => Real.log r + Real.log z) a :=
+      cfc_congr (Real.log_mul hr.ne' <| ne_of_gt <| ha₂ · ·)
+    _ = _ := by rw [cfc_const_add _ _ _]
+
+-- TODO: Relate the hypothesis to a notion of strict positivity
+lemma log_pow (n : ℕ) (a : A) (ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x)
+    (ha₁ : IsSelfAdjoint a := by cfc_tac) : log (a ^ n) = n • log a := by
+  have : ∀ x ∈ spectrum ℝ a, x ≠ 0 := by peel ha₂ with x hx h; exact h.ne'
+  have ha₂' : ContinuousOn Real.log (spectrum ℝ a) := by fun_prop (disch := assumption)
+  have ha₂'' : ContinuousOn Real.log ((· ^ n) '' spectrum ℝ a)  := by fun_prop (disch := aesop)
+  rw [log, ← cfc_pow_id (R := ℝ) a n ha₁, ← cfc_comp' Real.log (· ^ n) a ha₂'', log]
+  simp_rw [Real.log_pow, nsmul_eq_smul_cast ℝ n, cfc_const_mul (n : ℝ) Real.log a ha₂']
+
+end real_log
+end CFC

Mathlib/Data/Complex/Exponential.lean

@@ -232,6 +232,7 @@ theorem exp_nat_mul (x : ℂ) : ∀ n : ℕ, exp (n * x) = exp x ^ n
   | Nat.succ n => by rw [pow_succ, Nat.cast_add_one, add_mul, exp_add, ← exp_nat_mul _ n, one_mul]
 #align complex.exp_nat_mul Complex.exp_nat_mul
 
+@[simp]
 theorem exp_ne_zero : exp x ≠ 0 := fun h =>
   zero_ne_one <| by rw [← exp_zero, ← add_neg_self x, exp_add, h]; simp
 #align complex.exp_ne_zero Complex.exp_ne_zero
@@ -855,6 +856,7 @@ nonrec theorem exp_nat_mul (x : ℝ) (n : ℕ) : exp (n * x) = exp x ^ n :=
   ofReal_injective (by simp [exp_nat_mul])
 #align real.exp_nat_mul Real.exp_nat_mul
 
+@[simp]
 nonrec theorem exp_ne_zero : exp x ≠ 0 := fun h =>
   exp_ne_zero x <| by rw [exp, ← ofReal_inj] at h; simp_all
 #align real.exp_ne_zero Real.exp_ne_zero

Mathlib/Data/Nat/Bits.lean

@@ -7,7 +7,7 @@ import Mathlib.Algebra.Group.Basic
 import Mathlib.Algebra.Group.Nat
 import Mathlib.Data.Nat.Defs
 import Mathlib.Init.Data.List.Basic
-import Mathlib.Init.Data.Nat.Lemmas
+import Mathlib.Init.Data.Nat.Basic
 import Mathlib.Tactic.Convert
 import Mathlib.Tactic.GeneralizeProofs
 import Mathlib.Tactic.Says
@@ -398,74 +398,36 @@ theorem bit_cases_on_inj {C : ℕ → Sort u} (H₁ H₂ : ∀ b n, C (bit b n))
   bit_cases_on_injective.eq_iff
 #align nat.bit_cases_on_inj Nat.bit_cases_on_inj
 
-protected theorem bit0_eq_zero {n : ℕ} : 2 * n = 0 ↔ n = 0 := by
-  omega
-#align nat.bit0_eq_zero Nat.bit0_eq_zero
+#noalign nat.bit0_eq_zero
 
 theorem bit_eq_zero_iff {n : ℕ} {b : Bool} : bit b n = 0 ↔ n = 0 ∧ b = false := by
   constructor
-  · cases b <;> simp [Nat.bit, Nat.bit0_eq_zero, Nat.bit1_ne_zero]; omega
+  · cases b <;> simp [Nat.bit]; omega
   · rintro ⟨rfl, rfl⟩
     rfl
 #align nat.bit_eq_zero_iff Nat.bit_eq_zero_iff
 
-protected lemma bit0_le (h : n ≤ m) : 2 * n ≤ 2 * m := by
-  omega
-#align nat.bit0_le Nat.bit0_le
-
-protected lemma bit1_le {n m : ℕ} (h : n ≤ m) : 2 * n + 1 ≤ 2 * m + 1 := by
-  omega
-#align nat.bit1_le Nat.bit1_le
+#noalign nat.bit0_le
+#noalign nat.bit1_le
 
 lemma bit_le : ∀ (b : Bool) {m n : ℕ}, m ≤ n → bit b m ≤ bit b n
-  | true, _, _, h => Nat.bit1_le h
-  | false, _, _, h => Nat.bit0_le h
+  | true, _, _, h => by dsimp [bit]; omega
+  | false, _, _, h => by dsimp [bit]; omega
 #align nat.bit_le Nat.bit_le
 
-lemma bit0_le_bit : ∀ (b) {m n : ℕ}, m ≤ n → 2 * m ≤ bit b n
-  | true, _, _, h => le_of_lt <| Nat.bit0_lt_bit1 h
-  | false, _, _, h => Nat.bit0_le h
-#align nat.bit0_le_bit Nat.bit0_le_bit
-
-lemma bit_le_bit1 : ∀ (b) {m n : ℕ}, m ≤ n → bit b m ≤ 2 * n + 1
-  | false, _, _, h => le_of_lt <| Nat.bit0_lt_bit1 h
-  | true, _, _, h => Nat.bit1_le h
-#align nat.bit_le_bit1 Nat.bit_le_bit1
-
-lemma bit_lt_bit0 : ∀ (b) {m n : ℕ}, m < n → bit b m < 2 * n
-  | true, _, _, h => Nat.bit1_lt_bit0 h
-  | false, _, _, h => Nat.bit0_lt h
-#align nat.bit_lt_bit0 Nat.bit_lt_bit0
+#noalign nat.bit0_le_bit
+#noalign nat.bit_le_bit1
+#noalign nat.bit_lt_bit0
 
-protected lemma bit0_lt_bit0 : 2 * m < 2 * n ↔ m < n := by omega
-
-lemma bit_lt_bit (a b) (h : m < n) : bit a m < bit b n :=
-  lt_of_lt_of_le (bit_lt_bit0 _ h) (bit0_le_bit _ (le_refl _))
+lemma bit_lt_bit (a b) (h : m < n) : bit a m < bit b n := calc
+  bit a m < 2 * n   := by cases a <;> dsimp [bit] <;> omega
+        _ ≤ bit b n := by cases b <;> dsimp [bit] <;> omega
 #align nat.bit_lt_bit Nat.bit_lt_bit
 
-@[simp]
-lemma bit0_le_bit1_iff : 2 * m ≤ 2 * n + 1 ↔ m ≤ n := by
-  refine ⟨fun h ↦ ?_, fun h ↦ le_of_lt (Nat.bit0_lt_bit1 h)⟩
-  rwa [← Nat.lt_succ_iff, n.bit1_eq_succ_bit0, ← n.bit0_succ_eq, Nat.bit0_lt_bit0, Nat.lt_succ_iff]
-    at h
-#align nat.bit0_le_bit1_iff Nat.bit0_le_bit1_iff
-
-@[simp]
-lemma bit0_lt_bit1_iff : 2 * m < 2 * n + 1 ↔ m ≤ n :=
-  ⟨fun h => bit0_le_bit1_iff.1 (le_of_lt h), Nat.bit0_lt_bit1⟩
-#align nat.bit0_lt_bit1_iff Nat.bit0_lt_bit1_iff
-
-@[simp]
-lemma bit1_le_bit0_iff : 2 * m + 1 ≤ 2 * n ↔ m < n :=
-  ⟨fun h ↦ by rwa [m.bit1_eq_succ_bit0, Nat.succ_le_iff, Nat.bit0_lt_bit0] at h,
-     fun h ↦ le_of_lt (Nat.bit1_lt_bit0 h)⟩
-#align nat.bit1_le_bit0_iff Nat.bit1_le_bit0_iff
-
-@[simp]
-lemma bit1_lt_bit0_iff : 2 * m + 1 < 2 * n ↔ m < n :=
-  ⟨fun h ↦ bit1_le_bit0_iff.1 (le_of_lt h), Nat.bit1_lt_bit0⟩
-#align nat.bit1_lt_bit0_iff Nat.bit1_lt_bit0_iff
-
+#noalign nat.bit0_le_bit1_iff
+#noalign nat.bit0_lt_bit1_iff
+#noalign nat.bit1_le_bit0_iff
+#noalign nat.bit1_lt_bit0_iff
 #noalign nat.one_le_bit0_iff
 #noalign nat.one_lt_bit0_iff
 #noalign nat.bit_le_bit_iff

Mathlib/Data/Nat/Bitwise.lean

@@ -162,7 +162,7 @@ theorem bit_true : bit true = (2 * · + 1) :=
 
 @[simp]
 theorem bit_eq_zero {n : ℕ} {b : Bool} : n.bit b = 0 ↔ n = 0 ∧ b = false := by
-  cases b <;> simp [Nat.bit0_eq_zero, Nat.bit1_ne_zero]
+  cases b <;> simp [bit, Nat.mul_eq_zero]
 #align nat.bit_eq_zero Nat.bit_eq_zero
 
 theorem bit_ne_zero_iff {n : ℕ} {b : Bool} : n.bit b ≠ 0 ↔ n = 0 → b = true := by

Mathlib/Data/Nat/Size.lean

@@ -105,7 +105,7 @@ theorem lt_size_self (n : ℕ) : n < 2 ^ size n := by
   by_cases h : bit b n = 0
   · apply this h
   rw [size_bit h, shiftLeft_succ, shiftLeft_eq, one_mul]
-  exact bit_lt_bit0 _ (by simpa [shiftLeft_eq, shiftRight_eq_div_pow] using IH)
+  cases b <;> dsimp [bit] <;> omega
 #align nat.lt_size_self Nat.lt_size_self
 
 theorem size_le {m n : ℕ} : size m ≤ n ↔ m < 2 ^ n :=
@@ -123,7 +123,8 @@ theorem size_le {m n : ℕ} : size m ≤ n ↔ m < 2 ^ n :=
       · apply succ_le_succ (IH _)
         apply Nat.lt_of_mul_lt_mul_left (a := 2)
         simp only [shiftLeft_succ] at *
-        exact lt_of_le_of_lt (bit0_le_bit b rfl.le) h⟩
+        refine lt_of_le_of_lt ?_ h
+        cases b <;> dsimp [bit] <;> omega⟩
 #align nat.size_le Nat.size_le
 
 theorem lt_size {m n : ℕ} : m < size n ↔ 2 ^ m ≤ n := by

Mathlib/Data/Num/Lemmas.lean

@@ -1600,10 +1600,9 @@ theorem divMod_to_nat (d n : PosNum) :
     -- Porting note: `cases'` didn't rewrite at `this`, so `revert` & `intro` are required.
     revert IH; cases' divMod d n with q r; intro IH
     simp only [divMod] at IH ⊢
-    apply divMod_to_nat_aux <;> simp
-    · rw [← add_assoc, ← add_assoc, ← two_mul, ← two_mul, add_right_comm,
-        mul_left_comm, ← mul_add, IH.1]
-    · exact IH.2
+    apply divMod_to_nat_aux <;> simp only [Num.cast_bit1, cast_bit1]
+    · rw [← two_mul, ← two_mul, add_right_comm, mul_left_comm, ← mul_add, IH.1]
+    · omega
   · unfold divMod
     -- Porting note: `cases'` didn't rewrite at `this`, so `revert` & `intro` are required.
     revert IH; cases' divMod d n with q r; intro IH