feat: the cfc_pull tactic

LeanOA.lean

@@ -18,7 +18,6 @@ public import LeanOA.Masa
 public import LeanOA.Mathlib.Algebra.Group.Idempotent
 public import LeanOA.Mathlib.Algebra.Order.Star.Conjugate
 public import LeanOA.Mathlib.Analysis.CStarAlgebra.ApproximateUnit
-public import LeanOA.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
 public import LeanOA.Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
 public import LeanOA.Mathlib.Analysis.CStarAlgebra.Module.Defs
 public import LeanOA.Mathlib.Analysis.CStarAlgebra.MulNonneg
@@ -31,18 +30,25 @@ public import LeanOA.Mathlib.Analysis.LocallyConvex.Polar
 public import LeanOA.Mathlib.Analysis.LocallyConvex.WeakBilin
 public import LeanOA.Mathlib.Analysis.LocallyConvex.WithSeminorms
 public import LeanOA.Mathlib.Analysis.Normed.Group.Uniform
+public import LeanOA.Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.CFCPull.ComplexSqrt
+public import LeanOA.Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.CFCPull.Lemmas
+public import LeanOA.Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.CFCPull.Tags
 public import LeanOA.Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
 public import LeanOA.Mathlib.Data.Real.Archimedean
 public import LeanOA.Mathlib.Data.Set.Function
 public import LeanOA.Mathlib.Misc
 public import LeanOA.Mathlib.Order.Hom.Basic
+public import LeanOA.Mathlib.Tactic.CFCPull
+public import LeanOA.Mathlib.Tactic.CFCPull.Attr
+public import LeanOA.Mathlib.Tactic.CFCPull.Core
 public import LeanOA.Mathlib.Topology.Algebra.Module.LinearMap
 public import LeanOA.Mathlib.Topology.Algebra.Module.PolarTopology
 public import LeanOA.Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
 public import LeanOA.Mathlib.Topology.Algebra.Module.WeakBilin
 public import LeanOA.Mathlib.Topology.Algebra.Module.WeakDual
 public import LeanOA.Mathlib.Topology.Algebra.UniformConvergence
 public import LeanOA.Mathlib.Topology.ContinuousMap.ContinuousMapZero
+public import LeanOA.MathlibTest.CFCPull
 public import LeanOA.Notation
 public import LeanOA.PositiveContinuousLinearMap
 public import LeanOA.TendstoZero.Defs

LeanOA/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/CFCPull/ComplexSqrt.lean

@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2026 Jireh Loreaux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jireh Loreaux
+-/
+module
+
+public import Mathlib.Analysis.Complex.SqrtDeriv
+public import LeanOA.Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.CFCPull.Tags
+public import LeanOA.Mathlib.Tactic.CFCPull
+
+/-!  # `CFC.sqrt` via the complex functional calculus -/
+
+public section
+
+open scoped NNReal
+
+namespace Complex
+
+/-- `Complex.sqrt` is continuous on the closed right half-plane. -/
+lemma continuousOn_sqrt_setOf_re_nonneg : ContinuousOn sqrt {z | 0 ≤ z.re} :=
+  fun _z hz ↦ (continuousAt_sqrt (.inl hz)).continuousWithinAt
+
+end Complex
+
+section NonUnital
+
+variable {A : Type*} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [PartialOrder A]
+  [StarOrderedRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A]
+  [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] [NonnegSpectrumClass ℝ A] {a : A}
+
+/-- The `ℂ`-quasispectrum of a nonnegative element lies in the closed right half-plane, where
+`Complex.sqrt` is continuous. -/
+@[fun_prop]
+lemma Complex.continuousOn_sqrt_quasispectrum (ha : 0 ≤ a) :
+    ContinuousOn Complex.sqrt (quasispectrum ℂ a) := by
+  refine Complex.continuousOn_sqrt_setOf_re_nonneg.mono ?_
+  rw [← ha.isSelfAdjoint.quasispectrumRestricts.algebraMap_image]
+  rintro - ⟨x, hx, rfl⟩
+  simpa using quasispectrum_nonneg_of_nonneg a ha x hx
+
+variable [IsSemitopologicalRing A] [T2Space A]
+
+/-- `CFC.sqrt` is the non-unital calculus over `ℂ` applied to `Complex.sqrt`. This is not
+tagged `@[cfc_pull]` because it could generate side goals involving continuity of `Complex.sqrt`,
+which are not easily discharged by `fun_prop`. -/
+lemma CFC.sqrt_eq_cfcₙ_complex_sqrt (ha : 0 ≤ a) :
+    CFC.sqrt a = cfcₙ (fun x : ℂ ↦ x.sqrt) a := by
+  cfc_pull ℂ a
+  refine cfcₙ_congr ?_
+  rw [← (ha.isSelfAdjoint.quasispectrumRestricts.comp rfl (.nnreal_of_nonneg ha)).algebraMap_image]
+  rintro - ⟨x, hx, rfl⟩
+  rw [IsScalarTower.algebraMap_apply ℝ≥0 ℝ ℂ]
+  aesop (add simp [Complex.sqrt_of_nonneg])
+
+end NonUnital
+
+section Unital
+
+variable {A : Type*} [TopologicalSpace A] [Ring A] [StarRing A] [PartialOrder A]
+  [StarOrderedRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal]
+  [NonnegSpectrumClass ℝ A] {a : A}
+
+/-- The `ℂ`-spectrum of a nonnegative element lies in the closed right half-plane, where
+`Complex.sqrt` is continuous. -/
+@[fun_prop]
+lemma Complex.continuousOn_sqrt_spectrum (ha : 0 ≤ a) :
+    ContinuousOn Complex.sqrt (spectrum ℂ a) := by
+  refine Complex.continuousOn_sqrt_setOf_re_nonneg.mono ?_
+  rw [← ha.isSelfAdjoint.spectrumRestricts.algebraMap_image]
+  rintro - ⟨x, hx, rfl⟩
+  simpa using spectrum_nonneg_of_nonneg ha hx
+
+variable [IsSemitopologicalRing A] [T2Space A]
+
+/-- `CFC.sqrt` is the unital calculus over `ℂ` applied to `Complex.sqrt`. This is not
+tagged `@[cfc_pull]` because it could generate side goals involving continuity of `Complex.sqrt`,
+which are not easily discharged by `fun_prop`. -/
+lemma CFC.sqrt_eq_cfc_complex_sqrt (ha : 0 ≤ a) :
+    CFC.sqrt a = cfc (fun x : ℂ ↦ x.sqrt) a := by
+  cfc_pull -unital [CFC.sqrt_eq_cfcₙ_complex_sqrt] ℂ a
+
+end Unital

LeanOA/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/CFCPull/Lemmas.lean

@@ -0,0 +1,158 @@
+/-
+Copyright (c) 2026 Jireh Loreaux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jireh Loreaux
+-/
+module
+
+public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
+public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
+
+/-!
+# Lemmas needed by the `cfc_pull` tactic
+
+Some lemmas missing from Mathlib needed for the `cfc_pull` tactic.
+-/
+
+@[expose] public section
+
+open scoped NNReal
+open Topology ContinuousMap ContinuousMapZero
+
+section Extend
+
+variable {R A : Type*} {p : A → Prop} [CommSemiring R] [StarRing R] [MetricSpace R]
+  [IsTopologicalSemiring R] [ContinuousStar R] [TopologicalSpace A]
+
+section Unital
+
+variable [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R A p]
+
+/-- The `g := 0` case of `cfcHom_eq_cfc_extend`. -/
+lemma cfcHom_eq_cfc_extend_zero {a : A} (ha : p a) (f : C(spectrum R a, R)) :
+    cfcHom ha f = cfc (Function.extend Subtype.val f 0) a :=
+  cfcHom_eq_cfc_extend 0 ha f
+
+end Unital
+
+section NonUnital
+
+variable [Nontrivial R] [NonUnitalRing A] [StarRing A] [Module R A] [IsScalarTower R A A]
+  [SMulCommClass R A A] [NonUnitalContinuousFunctionalCalculus R A p]
+
+/-- The `g := 0` case of `cfcₙHom_eq_cfcₙ_extend`. -/
+lemma cfcₙHom_eq_cfcₙ_extend_zero {a : A} (ha : p a) (f : C(quasispectrum R a, R)₀) :
+    cfcₙHom ha f = cfcₙ (Function.extend Subtype.val f 0) a :=
+  cfcₙHom_eq_cfcₙ_extend 0 ha f
+
+end NonUnital
+
+end Extend
+
+namespace CFC
+
+section Quasispectrum
+
+-- TODO: these two results and the `grind` pattern should move next to
+-- `NonnegSpectrumClass.quasispectrum_nonneg_of_nonneg`.
+
+lemma quasispectrum_nonpos_of_nonpos {𝕜 A : Type*} [CommRing 𝕜]
+    [PartialOrder 𝕜] [IsOrderedAddMonoid 𝕜] [NonUnitalRing A] [PartialOrder A]
+    [IsOrderedAddMonoid A] [Module 𝕜 A] [NonnegSpectrumClass 𝕜 A]
+    [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] (a : A) (ha : a ≤ 0) :
+    ∀ x ∈ quasispectrum 𝕜 a, x ≤ 0 := by
+  have := quasispectrum_nonneg_of_nonneg (𝕜 := 𝕜) (-a) (by simpa using ha)
+  simpa [Unitization.quasispectrum_eq_spectrum_inr 𝕜, ← spectrum.neg_eq]
+
+lemma nonpos_of_mem_quasispectrum {𝕜 A : Type*} [CommRing 𝕜]
+    [PartialOrder 𝕜] [IsOrderedAddMonoid 𝕜] [NonUnitalRing A] [PartialOrder A]
+    [IsOrderedAddMonoid A] [Module 𝕜 A] [NonnegSpectrumClass 𝕜 A]
+    [IsScalarTower 𝕜 A A] [SMulCommClass 𝕜 A A] {a : A} (ha : a ≤ 0) {x : 𝕜}
+    (hx : x ∈ quasispectrum 𝕜 a) : x ≤ 0 := quasispectrum_nonpos_of_nonpos a ha x hx
+
+grind_pattern nonpos_of_mem_quasispectrum => x ∈ quasispectrum 𝕜 a
+
+end Quasispectrum
+
+section Sqrt
+
+variable {A : Type*} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A]
+  [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A]
+  [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A]
+
+lemma sqrt_def (a : A) : sqrt a = cfcₙ NNReal.sqrt a := rfl
+
+lemma abs_def (a : A) : abs a = cfcₙ NNReal.sqrt (star a * a) := rfl
+
+end Sqrt
+
+section Log
+
+variable {A : Type*} [NormedRing A] [StarRing A] [NormedAlgebra ℝ A]
+  [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
+
+lemma log_def (a : A) : log a = cfc Real.log a := rfl
+
+end Log
+
+end CFC
+
+section Norm
+
+open CFC
+open scoped ComplexOrder
+
+section Unital
+
+variable {A : Type*}
+  [Ring A] [TopologicalSpace A] [StarRing A] [PartialOrder A]
+  [StarOrderedRing A] [IsTopologicalRing A] [T2Space A]
+
+lemma cfc_real_comp_norm [Algebra ℝ A] [NonnegSpectrumClass ℝ A]
+    [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (f : ℝ → ℝ) (a : A)
+    (ha : IsSelfAdjoint a := by cfc_tac)
+    (hf : ContinuousOn f ((‖·‖) '' spectrum ℝ a) := by cfc_cont_tac) :
+    cfc (f ‖·‖) a = cfc f (abs a) :=
+  cfc_comp_norm f a
+
+lemma cfc_complex_comp_norm [Algebra ℂ A] [NonnegSpectrumClass ℝ A]
+    [ContinuousFunctionalCalculus ℂ A IsStarNormal] (f : ℂ → ℂ) (a : A)
+    (ha : IsStarNormal a := by cfc_tac)
+    (hf : ContinuousOn f ((‖·‖) '' spectrum ℂ a) := by cfc_cont_tac) :
+    cfc (f ‖·‖) a = cfc f (abs a) :=
+  cfc_comp_norm f a
+
+end Unital
+
+section NonUnital
+
+variable {A : Type*} [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [PartialOrder A]
+  [StarOrderedRing A] [IsTopologicalRing A] [T2Space A]
+
+lemma cfcₙ_real_comp_norm [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A]
+  [NonnegSpectrumClass ℝ A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
+    (f : ℝ → ℝ) (a : A)
+    (ha : IsSelfAdjoint a := by cfc_tac)
+    (hf : ContinuousOn f ((‖·‖) '' quasispectrum ℝ a) := by cfc_cont_tac) :
+    cfcₙ (f ‖·‖) a = cfcₙ f (abs a) :=
+  cfcₙ_comp_norm f a
+
+lemma cfcₙ_complex_comp_norm [Module ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A]
+    [NonnegSpectrumClass ℝ A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal]
+    (f : ℂ → ℂ) (a : A)
+    (ha : IsStarNormal a := by cfc_tac)
+    (hf : ContinuousOn f ((‖·‖) '' quasispectrum ℂ a) := by cfc_cont_tac) :
+    cfcₙ (f ‖·‖) a = cfcₙ f (abs a) :=
+  cfcₙ_comp_norm f a
+
+end NonUnital
+
+end Norm
+
+@[fun_prop]
+lemma StarAlgHom.continuous_restrictScalars {R S A B : Type*} [TopologicalSpace A]
+    [TopologicalSpace B] [CommSemiring R] [CommSemiring S] [Semiring A] [Semiring B] [Algebra R S]
+    [Algebra S A] [Algebra S B] [Algebra R A] [Algebra R B] [IsScalarTower R S A]
+    [IsScalarTower R S B] [Star A] [Star B] {f : A →⋆ₐ[S] B} (hf : Continuous f) :
+    Continuous (f.restrictScalars R) :=
+  hf