[Merged by Bors] - feat(ContinuousFunctionalCalculus): cfc applied to products and pi types

Mathlib.lean

@@ -1284,6 +1284,7 @@ import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Note
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital

Mathlib/Algebra/Star/StarAlgHom.lean

@@ -6,7 +6,9 @@ Authors: Jireh Loreaux
 import Mathlib.Algebra.Algebra.Equiv
 import Mathlib.Algebra.Algebra.NonUnitalHom
 import Mathlib.Algebra.Algebra.Prod
+import Mathlib.Algebra.Algebra.Pi
 import Mathlib.Algebra.Star.Prod
+import Mathlib.Algebra.Star.Pi
 import Mathlib.Algebra.Star.StarRingHom
 
 /-!
@@ -520,6 +522,30 @@ def prodEquiv : (A →⋆ₙₐ[R] B) × (A →⋆ₙₐ[R] C) ≃ (A →⋆ₙ
 
 end Prod
 
+section Pi
+
+variable {ι : Type*}
+
+/-- `Function.eval` as a `NonUnitalStarAlgHom`. -/
+@[simps]
+def _root_.Pi.evalNonUnitalStarAlgHom (R : Type*) (A : ι → Type*) (i : ι) [Monoid R]
+    [∀ i, NonUnitalNonAssocSemiring (A i)] [∀ i, DistribMulAction R (A i)] [∀ i, Star (A i)] :
+    (∀ i, A i) →⋆ₙₐ[R] A i :=
+  { Pi.evalMulHom A i, Pi.evalAddHom A i with
+    map_smul' _ _ := rfl
+    map_zero' := rfl
+    map_star' _ := rfl }
+
+/-- `Function.eval` as a `StarAlgHom`. -/
+@[simps]
+def _root_.Pi.evalStarAlgHom (R : Type*) (A : ι → Type*) (i : ι) [CommSemiring R]
+    [∀ i, Semiring (A i)] [∀ i, Algebra R (A i)] [∀ i, Star (A i)] :
+    (∀ i, A i) →⋆ₐ[R] A i :=
+  { Pi.evalNonUnitalStarAlgHom R A i, Pi.evalRingHom A i with
+    commutes' _ := rfl }
+
+end Pi
+
 section InlInr
 
 variable (R A B C : Type*) [Monoid R] [NonUnitalNonAssocSemiring A] [DistribMulAction R A]

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Pi.lean

@@ -0,0 +1,135 @@
+/-
+Copyright (c) 2025 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.CStarAlgebra.ContinuousFunctionalCalculus.Unique
+import Mathlib.Algebra.Algebra.Spectrum.Pi
+import Mathlib.Algebra.Star.StarAlgHom
+
+/-! # The continuous functional calculus on product types
+
+This file contains results about the continuous functional calculus on (indexed) product types.
+
+## Main theorems
+
++ `cfc_map_pi` and `cfcₙ_map_pi`: given `a : ∀ i, A i`, then `cfc f a = fun i => cfc f (a i)`
+  (and likewise for the non-unital version)
++ `cfc_map_prod` and `cfcₙ_map_prod`: given `a : A` and `b : B`, then
+  `cfc f ⟨a, b⟩ = ⟨cfc f a, cfc f b⟩` (and likewise for the non-unital version)
+-/
+
+section nonunital_pi
+
+variable {ι R S : Type*} {A : ι → Type*} [CommSemiring R] [Nontrivial R] [StarRing R]
+  [MetricSpace R]
+  [IsTopologicalSemiring R] [ContinuousStar R] [CommRing S] [Algebra R S]
+  [∀ i, NonUnitalRing (A i)] [∀ i, Module S (A i)] [∀ i, Module R (A i)]
+  [∀ i, IsScalarTower R S (A i)] [∀ i, SMulCommClass R (A i) (A i)]
+  [∀ i, IsScalarTower R (A i) (A i)]
+  [∀ i, StarRing (A i)] [∀ i, TopologicalSpace (A i)] {p : (∀ i, A i) → Prop}
+  {q : (i : ι) → A i → Prop}
+  [NonUnitalContinuousFunctionalCalculus R (∀ i, A i) p]
+  [∀ i, NonUnitalContinuousFunctionalCalculus R (A i) (q i)]
+  [∀ i, ContinuousMapZero.UniqueHom R (A i)]
+
+include S in
+lemma cfcₙ_map_pi (f : R → R) (a : ∀ i, A i)
+    (hf : ContinuousOn f (⋃ i, quasispectrum R (a i)) := by cfc_cont_tac)
+    (ha : p a := by cfc_tac) (ha' : ∀ i, q i (a i) := by cfc_tac) :
+    cfcₙ f a = fun i => cfcₙ f (a i) := by
+  by_cases hempty : Nonempty ι
+  · by_cases hf₀ : f 0 = 0
+    · ext i
+      let φ := Pi.evalNonUnitalStarAlgHom S A i
+      exact φ.map_cfcₙ f a (by rwa [Pi.quasispectrum_eq]) hf₀ (continuous_apply i) ha (ha' i)
+    · simp only [cfcₙ_apply_of_not_map_zero _ hf₀]; rfl
+  · simp only [not_nonempty_iff] at hempty
+    ext i
+    exact hempty.elim i
+
+end nonunital_pi
+
+section nonunital_prod
+
+variable {A B R S : Type*} [CommSemiring R] [CommRing S] [Nontrivial R] [StarRing R]
+  [MetricSpace R] [IsTopologicalSemiring R] [ContinuousStar R] [Algebra R S] [NonUnitalRing A]
+  [NonUnitalRing B] [Module S A] [Module R A] [Module R B] [Module S B]
+  [SMulCommClass R A A] [SMulCommClass R B B] [IsScalarTower R A A] [IsScalarTower R B B]
+  [StarRing A] [StarRing B] [TopologicalSpace A] [TopologicalSpace B]
+  [IsScalarTower R S A] [IsScalarTower R S B]
+  {pab : A × B → Prop} {pa : A → Prop} {pb : B → Prop}
+  [NonUnitalContinuousFunctionalCalculus R (A × B) pab]
+  [NonUnitalContinuousFunctionalCalculus R A pa]
+  [NonUnitalContinuousFunctionalCalculus R B pb]
+  [ContinuousMapZero.UniqueHom R A] [ContinuousMapZero.UniqueHom R B]
+
+include S in
+lemma cfcₙ_map_prod (f : R → R) (a : A) (b : B)
+    (hf : ContinuousOn f (quasispectrum R a ∪ quasispectrum R b) := by cfc_cont_tac)
+    (hab : pab ⟨a, b⟩ := by cfc_tac) (ha : pa a := by cfc_tac) (hb : pb b := by cfc_tac) :
+    cfcₙ f (⟨a, b⟩ : A × B) = ⟨cfcₙ f a, cfcₙ f b⟩ := by
+  by_cases hf₀ : f 0 = 0
+  case pos =>
+    ext
+    case fst =>
+      let φ := NonUnitalStarAlgHom.fst S A B
+      exact φ.map_cfcₙ f ⟨a, b⟩ (by rwa [Prod.quasispectrum_eq]) hf₀ continuous_fst hab ha
+    case snd =>
+      let φ := NonUnitalStarAlgHom.snd S A B
+      exact φ.map_cfcₙ f ⟨a, b⟩ (by rwa [Prod.quasispectrum_eq]) hf₀ continuous_snd hab hb
+  case neg =>
+    simp [cfcₙ_apply_of_not_map_zero _ hf₀]
+
+end nonunital_prod
+
+section unital_pi
+
+variable {ι R S : Type*} {A : ι → Type*} [CommSemiring R] [StarRing R] [MetricSpace R]
+  [IsTopologicalSemiring R] [ContinuousStar R] [CommRing S] [Algebra R S]
+  [∀ i, Ring (A i)] [∀ i, Algebra S (A i)] [∀ i, Algebra R (A i)] [∀ i, IsScalarTower R S (A i)]
+  [hinst : IsScalarTower R S (∀ i, A i)]
+  [∀ i, StarRing (A i)] [∀ i, TopologicalSpace (A i)] {p : (∀ i, A i) → Prop}
+  {q : (i : ι) → A i → Prop}
+  [ContinuousFunctionalCalculus R (∀ i, A i) p]
+  [∀ i, ContinuousFunctionalCalculus R (A i) (q i)]
+  [∀ i, ContinuousMap.UniqueHom R (A i)]
+
+include S in
+lemma cfc_map_pi (f : R → R) (a : ∀ i, A i)
+    (hf : ContinuousOn f (⋃ i, spectrum R (a i)) := by cfc_cont_tac)
+    (ha : p a := by cfc_tac) (ha' : ∀ i, q i (a i) := by cfc_tac) :
+    cfc f a = fun i => cfc f (a i) := by
+  ext i
+  let φ := Pi.evalStarAlgHom S A i
+  exact φ.map_cfc f a (by rwa [Pi.spectrum_eq]) (continuous_apply i) ha (ha' i)
+
+end unital_pi
+
+section unital_prod
+
+variable {A B R S : Type*} [CommSemiring R] [StarRing R] [MetricSpace R]
+  [IsTopologicalSemiring R] [ContinuousStar R] [CommRing S] [Algebra R S]
+  [Ring A] [Ring B] [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B]
+  [IsScalarTower R S A] [IsScalarTower R S B]
+  [StarRing A] [StarRing B] [TopologicalSpace A] [TopologicalSpace B] {pab : A × B → Prop}
+  {pa : A → Prop} {pb : B → Prop}
+  [ContinuousFunctionalCalculus R (A × B) pab]
+  [ContinuousFunctionalCalculus R A pa] [ContinuousFunctionalCalculus R B pb]
+  [ContinuousMap.UniqueHom R A] [ContinuousMap.UniqueHom R B]
+
+include S in
+lemma cfc_map_prod (f : R → R) (a : A) (b : B)
+    (hf : ContinuousOn f (spectrum R a ∪ spectrum R b) := by cfc_cont_tac)
+    (hab : pab ⟨a, b⟩ := by cfc_tac) (ha : pa a := by cfc_tac) (hb : pb b := by cfc_tac) :
+    cfc f (⟨a, b⟩ : A × B) = ⟨cfc f a, cfc f b⟩ := by
+  ext
+  case fst =>
+    let φ := StarAlgHom.fst S A B
+    exact φ.map_cfc f ⟨a, b⟩ (by rwa [Prod.spectrum_eq]) continuous_fst hab ha
+  case snd =>
+    let φ := StarAlgHom.snd S A B
+    exact φ.map_cfc f ⟨a, b⟩ (by rwa [Prod.spectrum_eq]) continuous_snd hab hb
+
+end unital_prod

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

@@ -6,6 +6,7 @@ Authors: Frédéric Dupuis
 
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi
 import Mathlib.Analysis.SpecialFunctions.Pow.Continuity
 
 /-!
@@ -73,6 +74,18 @@ variable {A : Type*} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [St
   [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A]
   [NonUnitalContinuousFunctionalCalculus ℝ≥0 A (0 ≤ ·)]
 
+variable {B : Type*} [PartialOrder B] [NonUnitalRing B] [TopologicalSpace B] [StarRing B]
+  [Module ℝ B] [SMulCommClass ℝ B B] [IsScalarTower ℝ B B]
+  [NonUnitalContinuousFunctionalCalculus ℝ≥0 B (0 ≤ ·)]
+  [NonUnitalContinuousFunctionalCalculus ℝ≥0 (A × B) (0 ≤ ·)]
+
+variable {ι : Type*} {C : ι → Type*} [∀ i, PartialOrder (C i)] [∀ i, NonUnitalRing (C i)]
+  [∀ i, TopologicalSpace (C i)] [∀ i, StarRing (C i)]
+  [∀ i, Module ℝ (C i)] [∀ i, SMulCommClass ℝ (C i) (C i)] [∀ i, IsScalarTower ℝ (C i) (C i)]
+  [∀ i, NonUnitalContinuousFunctionalCalculus ℝ≥0 (C i) (0 ≤ ·)]
+  [NonUnitalContinuousFunctionalCalculus ℝ≥0 (∀ i, C i) (0 ≤ ·)]
+  [∀ i, IsTopologicalRing (C i)] [∀ i, T2Space (C i)]
+
 /- ## `nnrpow` -/
 
 /-- Real powers of operators, based on the non-unital continuous functional calculus. -/
@@ -122,7 +135,7 @@ lemma zero_nnrpow {x : ℝ≥0} : (0 : A) ^ x = 0 := by simp [nnrpow_def]
 
 section Unique
 
-variable [IsTopologicalRing A] [T2Space A]
+variable [IsTopologicalRing A] [T2Space A] [IsTopologicalRing B] [T2Space B]
 
 @[simp]
 lemma nnrpow_nnrpow {a : A} {x y : ℝ≥0} : (a ^ x) ^ y = a ^ (x * y) := by
@@ -151,6 +164,25 @@ lemma nnrpow_inv_eq (a b : A) {x : ℝ≥0} (hx : x ≠ 0) (ha : 0 ≤ a := by c
   ⟨fun h ↦ nnrpow_inv_nnrpow a hx ▸ congr($(h) ^ x).symm,
     fun h ↦ nnrpow_nnrpow_inv b hx ▸ congr($(h) ^ x⁻¹).symm⟩
 
+/- Note that there is higher-priority instance of `Pow (A × B) ℝ≥0` coming from the `Pow` instance
+for products, hence the direct use of `nnrpow` here. -/
+lemma nnrpow_map_prod {a : A} {b : B} {x : ℝ≥0}
+    (ha : 0 ≤ a := by cfc_tac) (hb : 0 ≤ b := by cfc_tac) :
+    nnrpow (⟨a, b⟩ : A × B) x = ⟨a ^ x, b ^ x⟩ := by
+  simp only [nnrpow_def]
+  unfold nnrpow
+  refine cfcₙ_map_prod (S := ℝ) _ a b (by cfc_cont_tac) ?_
+  rw [Prod.le_def]
+  constructor <;> simp [ha, hb]
+
+/- Note that there is higher-priority instance of `Pow (∀ i, C i) ℝ≥0` coming from the `Pow`
+instance for pi types, hence the direct use of `nnrpow` here. -/
+lemma nnrpow_map_pi {c : ∀ i, C i} {x : ℝ≥0} (hc : ∀ i, 0 ≤ c i := by cfc_tac) :
+    nnrpow c x = fun i => (c i) ^ x := by
+  simp only [nnrpow_def]
+  unfold nnrpow
+  exact cfcₙ_map_pi (S := ℝ) _ c
+
 end Unique
 
 /- ## `sqrt` -/
@@ -172,7 +204,7 @@ lemma sqrt_eq_nnrpow {a : A} : sqrt a = a ^ (1 / 2 : ℝ≥0) := by
 @[simp]
 lemma sqrt_zero : sqrt (0 : A) = 0 := by simp [sqrt]
 
-variable [IsTopologicalRing A] [T2Space A]
+variable [IsTopologicalRing A] [T2Space A] [IsTopologicalRing B] [T2Space B]
 
 @[simp]
 lemma nnrpow_sqrt {a : A} {x : ℝ≥0} : (sqrt a) ^ x = a ^ (x / 2) := by
@@ -211,6 +243,16 @@ lemma sqrt_eq_iff (a b : A) (ha : 0 ≤ a := by cfc_tac) (hb : 0 ≤ b := by cfc
 lemma sqrt_eq_zero_iff (a : A) (ha : 0 ≤ a := by cfc_tac) : sqrt a = 0 ↔ a = 0 := by
   rw [sqrt_eq_iff a _, mul_zero, eq_comm]
 
+lemma sqrt_map_prod {a : A} {b : B} (ha : 0 ≤ a := by cfc_tac) (hb : 0 ≤ b := by cfc_tac) :
+    sqrt (⟨a, b⟩ : A × B) = ⟨sqrt a, sqrt b⟩ := by
+  simp only [sqrt_eq_nnrpow]
+  exact nnrpow_map_prod
+
+lemma sqrt_map_pi {c : ∀ i, C i} (hc : ∀ i, 0 ≤ c i := by cfc_tac) :
+    sqrt c = fun i => sqrt (c i) := by
+  simp only [sqrt_eq_nnrpow]
+  exact nnrpow_map_pi
+
 end sqrt
 
 end NonUnital
@@ -220,6 +262,15 @@ section Unital
 variable {A : Type*} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A]
   [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ≥0 A (0 ≤ ·)]
 
+variable {B : Type*} [PartialOrder B] [Ring B] [StarRing B] [TopologicalSpace B]
+  [Algebra ℝ B] [ContinuousFunctionalCalculus ℝ≥0 B (0 ≤ ·)]
+  [ContinuousFunctionalCalculus ℝ≥0 (A × B) (0 ≤ ·)]
+
+variable {ι : Type*} {C : ι → Type*} [∀ i, PartialOrder (C i)] [∀ i, Ring (C i)]
+  [∀ i, StarRing (C i)] [∀ i, TopologicalSpace (C i)]
+  [∀ i, Algebra ℝ (C i)] [∀ i, ContinuousFunctionalCalculus ℝ≥0 (C i) (0 ≤ ·)]
+  [ContinuousFunctionalCalculus ℝ≥0 (∀ i, C i) (0 ≤ ·)]
+
 /- ## `rpow` -/
 
 /-- Real powers of operators, based on the unital continuous functional calculus. -/
@@ -319,6 +370,33 @@ lemma rpow_intCast (a : Aˣ) (n : ℤ) (ha : (0 : A) ≤ a := by cfc_tac) :
   refine cfc_congr fun _ _ => ?_
   simp
 
+section prod_pi
+
+variable [IsTopologicalRing A] [T2Space A] [IsTopologicalRing B] [T2Space B]
+  [∀ i, IsTopologicalRing (C i)] [∀ i, T2Space (C i)]
+
+/- Note that there is higher-priority instance of `Pow (A × B) ℝ` coming from the `Pow` instance for
+products, hence the direct use of `rpow` here. -/
+lemma rpow_map_prod {a : A} {b : B} {x : ℝ} (ha : 0 ∉ spectrum ℝ≥0 a) (hb : 0 ∉ spectrum ℝ≥0 b)
+    (ha' : 0 ≤ a := by cfc_tac) (hb' : 0 ≤ b := by cfc_tac) :
+    rpow (⟨a, b⟩ : A × B) x = ⟨a ^ x, b ^ x⟩ := by
+  simp only [rpow_def]
+  unfold rpow
+  refine cfc_map_prod (R := ℝ≥0) (S := ℝ) _ a b (by cfc_cont_tac) ?_
+  rw [Prod.le_def]
+  constructor <;> simp [ha', hb']
+
+/- Note that there is a higher-priority instance of `Pow (∀ i, B i) ℝ` coming from the `Pow`
+instance for pi types, hence the direct use of `rpow` here. -/
+lemma rpow_map_pi {c : ∀ i, C i} {x : ℝ} (hc : ∀ i, 0 ∉ spectrum ℝ≥0 (c i))
+    (hc' : ∀ i, 0 ≤ c i := by cfc_tac) :
+    rpow c x = fun i => (c i) ^ x := by
+  simp only [rpow_def]
+  unfold rpow
+  exact cfc_map_pi (S := ℝ) _ c
+
+end prod_pi
+
 section unital_vs_nonunital
 
 variable [IsTopologicalRing A] [T2Space A]
@@ -381,10 +459,10 @@ lemma rpow_sqrt_nnreal {a : A} {x : ℝ≥0}
     (ha : 0 ≤ a := by cfc_tac) : (sqrt a) ^ (x : ℝ) = a ^ (x / 2 : ℝ) := by
   by_cases hx : x = 0
   case pos =>
-    have ha' : 0 ≤ sqrt a := by exact sqrt_nonneg
+    have ha' : 0 ≤ sqrt a := sqrt_nonneg
     simp [hx, rpow_zero _ ha', rpow_zero _ ha]
   case neg =>
-    have h₁ : 0 ≤ (x : ℝ) := by exact NNReal.zero_le_coe
+    have h₁ : 0 ≤ (x : ℝ) := NNReal.zero_le_coe
     rw [sqrt_eq_rpow, rpow_rpow_of_exponent_nonneg _ _ _ (by norm_num) h₁, one_div_mul_eq_div]
 
 end unital_vs_nonunital