Cover Image

The continuous functional calculus in Lean

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Dedecker, Anatole, Loreaux, Jireh
Format:	Preprint
Published:	2025
Subjects:	Operator Algebras Logic in Computer Science 68V20 (Primary) 47B15, 46L05, 68V35 (Secondary)
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Formalising New Mathematics in Isabelle: Diagonal Ramsey
by: Paulson, Lawrence C
Published: (2025)

Anatomy of a Formal Proof
by: Avigad, Jeremy, et al.
Published: (2024)

Formalizing Pick's Theorem in Isabelle/HOL
by: Binder, Sage, et al.
Published: (2024)

A Formalization of Abstract Rewriting in Agda
by: Arkle, Sam, et al.
Published: (2026)

On preservers of strong Birkhoff-James orthogonality between $C^*$-algebras
by: Kuzma, Bojan, et al.
Published: (2025)

A Modular First Formalisation of Combinatorial Design Theory
by: Edmonds, Chelsea, et al.
Published: (2021)

Universal truth of operator statements via ideal membership
by: Hofstadler, Clemens, et al.
Published: (2022)

An Alternative Approach to Formal Mathematics that Focuses on Communication and Accessibility
by: Farmer, William M.
Published: (2026)

Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma
by: Edmonds, Chelsea, et al.
Published: (2023)

Using Aristotle API for AI-Assisted Theorem Proving in Lean 4: A Formalisation Case Study of the Grasshopper Problem
by: Lau, Gabriel Rongyang
Published: (2026)

Remote Verification System for Mizar Integrated with Emwiki
by: Kai, Toshiki, et al.
Published: (2024)

Rokhkin inclusions with integer and non-integer index
by: Lee, H., et al.
Published: (2024)

On permanence of regularity properties II
by: Lee, Hyun Ho
Published: (2026)

Classification of Certain C*-Algebras Generated by Two Partitions of Unity
by: Schäfer, Björn
Published: (2025)

Hyperrigidity II: $R$-dilations, ideals and decompositions
by: Pietrzycki, Paweł, et al.
Published: (2024)

Kaplansky's problem and unitary orbits in matrix amplifications
by: Marcoux, Laurent W., et al.
Published: (2025)

New insights into linear maps which are anti-derivable at zero
by: Li, Jiankui, et al.
Published: (2025)

Bounded modular functionals and operators on Hilbert C*-modules that are regular
by: Frank, Michael, et al.
Published: (2026)

Algorithm and abstraction in formal mathematics
by: Macbeth, Heather
Published: (2024)

Monoid Theory in Alonzo: A Little Theories Formalization in Simple Type Theory
by: Farmer, William M., et al.
Published: (2023)

Distance to regular elements and polar decompositions in a C*-algebra
by: Thiel, Hannes
Published: (2025)

$M$-ideals, yet again: the case of real JB$^*$-triples
by: Blecher, David P., et al.
Published: (2024)

Singular value functions for C\(^*\)-algebras
by: Fujitsu, Naoto
Published: (2026)

$C^*$-algebras associated to directed graphs of groups, and models of Kirchberg algebras
by: Wu, Victor
Published: (2024)

EP modular operators and their products
by: Sharifi, Kamran
Published: (2014)

Every 2-quasitrace is a trace
by: Gow, Alec
Published: (2025)

Fejér--Riesz factorization for positive noncommutative trigonometric polynomials
by: Klep, Igor, et al.
Published: (2025)

A Higher-Order Vampire (Short Paper)
by: Bhayat, Ahmed, et al.
Published: (2024)

The Free Tangent Law
by: Ejsmont, Wiktor, et al.
Published: (2020)

Decomposition of tracial positive maps and applications in quantum information
by: Dadkha, Ali, et al.
Published: (2022)

Multiplier algebras of $L^p$-operator algebras
by: Blinov, Andrey, et al.
Published: (2024)

Formally Verifying a Transformation from MLTL Formulas to Regular Expressions
by: Wang, Zili, et al.
Published: (2025)

Formalizing MLTL Formula Progression in Isabelle/HOL
by: Kosaian, Katherine, et al.
Published: (2024)

A separation theorem for Hilbert $W^*$-modules
by: Eskandari, Rasoul, et al.
Published: (2024)

On the classification of function algebras on subvarieties of noncommutative operator balls
by: Sampat, Jeet, et al.
Published: (2023)

Orthogonality preserving property for pairs of operators on Hilbert $C^*$-modules
by: Frank, Michael, et al.
Published: (2017)

Wold-type decomposition for doubly twisted left-invertible covariant representations
by: Kumar, Niraj, et al.
Published: (2026)

Twisted crossed products of Banach algebras
by: Delfín, Alonso, et al.
Published: (2025)

$L^p$-modules and $L^p$-correspondences
by: Delfín, Alonso
Published: (2024)

Categories of quantum cpos
by: Kornell, Andre, et al.
Published: (2024)