diff --git a/web/entries/Banach_Steinhaus.html b/web/entries/Banach_Steinhaus.html --- a/web/entries/Banach_Steinhaus.html +++ b/web/entries/Banach_Steinhaus.html @@ -1,186 +1,186 @@ Banach-Steinhaus Theorem - Archive of Formal Proofs

Banach-Steinhaus Theorem

Title:	Banach-Steinhaus Theorem
Authors:	Dominique Unruh and Jose Manuel Rodriguez Caballero
Submission date:	2020-05-02
Abstract:	-We formalize is Isabelle/HOL a result -due to S. Banach and H. Steinhaus, known as -the Banach-Steinhaus theorem or Uniform boundedness principle: A +We formalize in Isabelle/HOL a result +due to S. Banach and H. Steinhaus known as +the Banach-Steinhaus theorem or Uniform boundedness principle: a pointwise-bounded family of continuous linear operators from a Banach space to a normed space is uniformly bounded. Our approach is an adaptation to Isabelle/HOL of a proof due to A. Sokal.
BibTeX:	@article{Banach_Steinhaus-AFP, author = {Dominique Unruh and Jose Manuel Rodriguez Caballero}, title = {Banach-Steinhaus Theorem}, journal = {Archive of Formal Proofs}, month = may, year = 2020, note = {\url{http://isa-afp.org/entries/Banach_Steinhaus.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License

Proof outline
Proof document

Browse theories

Download this entry

Older releases: None

\ No newline at end of file diff --git a/web/rss.xml b/web/rss.xml --- a/web/rss.xml +++ b/web/rss.xml @@ -1,594 +1,594 @@ Archive of Formal Proofs https://www.isa-afp.org The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle. 08 May 2020 00:00:00 +0000 An Efficient Normalisation Procedure for Linear Temporal Logic: Isabelle/HOL Formalisation https://www.isa-afp.org/entries/LTL_Normal_Form.html https://www.isa-afp.org/entries/LTL_Normal_Form.html Salomon Sickert 08 May 2020 00:00:00 +0000 In the mid 80s, Lichtenstein, Pnueli, and Zuck proved a classical theorem stating that every formula of Past LTL (the extension of LTL with past operators) is equivalent to a formula of the form $\bigwedge_{i=1}^n \mathbf{G}\mathbf{F} \varphi_i \vee \mathbf{F}\mathbf{G} \psi_i$, where $\varphi_i$ and $\psi_i$ contain only past operators. Some years later, Chang, Manna, and Pnueli built on this result to derive a similar normal form for LTL. Both normalisation procedures have a non-elementary worst-case blow-up, and follow an involved path from formulas to counter-free automata to star-free regular expressions and back to formulas. We improve on both points. We present an executable formalisation of a direct and purely syntactic normalisation procedure for LTL yielding a normal form, comparable to the one by Chang, Manna, and Pnueli, that has only a single exponential blow-up. Formalization of Forcing in Isabelle/ZF https://www.isa-afp.org/entries/Forcing.html https://www.isa-afp.org/entries/Forcing.html Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf 06 May 2020 00:00:00 +0000 We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct a proper generic extension and show that the latter also satisfies ZFC. Banach-Steinhaus Theorem https://www.isa-afp.org/entries/Banach_Steinhaus.html https://www.isa-afp.org/entries/Banach_Steinhaus.html Dominique Unruh, Jose Manuel Rodriguez Caballero 02 May 2020 00:00:00 +0000 -We formalize is Isabelle/HOL a result -due to S. Banach and H. Steinhaus, known as -the Banach-Steinhaus theorem or Uniform boundedness principle: A +We formalize in Isabelle/HOL a result +due to S. Banach and H. Steinhaus known as +the Banach-Steinhaus theorem or Uniform boundedness principle: a pointwise-bounded family of continuous linear operators from a Banach space to a normed space is uniformly bounded. Our approach is an adaptation to Isabelle/HOL of a proof due to A. Sokal. Attack Trees in Isabelle for GDPR compliance of IoT healthcare systems https://www.isa-afp.org/entries/Attack_Trees.html https://www.isa-afp.org/entries/Attack_Trees.html Florian Kammueller 27 Apr 2020 00:00:00 +0000 In this article, we present a proof theory for Attack Trees. Attack Trees are a well established and useful model for the construction of attacks on systems since they allow a stepwise exploration of high level attacks in application scenarios. Using the expressiveness of Higher Order Logic in Isabelle, we develop a generic theory of Attack Trees with a state-based semantics based on Kripke structures and CTL. The resulting framework allows mechanically supported logic analysis of the meta-theory of the proof calculus of Attack Trees and at the same time the developed proof theory enables application to case studies. A central correctness and completeness result proved in Isabelle establishes a connection between the notion of Attack Tree validity and CTL. The application is illustrated on the example of a healthcare IoT system and GDPR compliance verification. Power Sum Polynomials https://www.isa-afp.org/entries/Power_Sum_Polynomials.html https://www.isa-afp.org/entries/Power_Sum_Polynomials.html Manuel Eberl 24 Apr 2020 00:00:00 +0000 This article provides a formalisation of the symmetric multivariate polynomials known as power sum polynomials. These are of the form pn(X1,…, Xk) = X1n + … + Xkn. A formal proof of the Girard–Newton Theorem is also given. This theorem relates the power sum polynomials to the elementary symmetric polynomials sk in the form of a recurrence relation (-1)k k sk = ∑i&isinv;[0,k) (-1)i si pk-i . As an application, this is then used to solve a generalised form of a puzzle given as an exercise in Dummit and Foote's Abstract Algebra: For k complex unknowns x1, …, xk, define pj := x1j + … + xkj. Then for each vector a &isinv; ℂk, show that there is exactly one solution to the system p1 = a1, …, pk = ak up to permutation of the xi and determine the value of pi for i>k. The Lambert W Function on the Reals https://www.isa-afp.org/entries/Lambert_W.html https://www.isa-afp.org/entries/Lambert_W.html Manuel Eberl 24 Apr 2020 00:00:00 +0000 The Lambert W function is a multi-valued function defined as the inverse function of x ↦ x ex. Besides numerous applications in combinatorics, physics, and engineering, it also frequently occurs when solving equations containing both ex and x, or both x and log x. This article provides a definition of the two real-valued branches W0(x) and W-1(x) and proves various properties such as basic identities and inequalities, monotonicity, differentiability, asymptotic expansions, and the MacLaurin series of W0(x) at x = 0. Gaussian Integers https://www.isa-afp.org/entries/Gaussian_Integers.html https://www.isa-afp.org/entries/Gaussian_Integers.html Manuel Eberl 24 Apr 2020 00:00:00 +0000 The Gaussian integers are the subring ℤ[i] of the complex numbers, i. e. the ring of all complex numbers with integral real and imaginary part. This article provides a definition of this ring as well as proofs of various basic properties, such as that they form a Euclidean ring and a full classification of their primes. An executable (albeit not very efficient) factorisation algorithm is also provided. Lastly, this Gaussian integer formalisation is used in two short applications: <ol> <li> The characterisation of all positive integers that can be written as sums of two squares</li> <li> Euclid's formula for primitive Pythagorean triples</li> </ol> While elementary proofs for both of these are already available in the AFP, the theory of Gaussian integers provides more concise proofs and a more high-level view. Matrices for ODEs https://www.isa-afp.org/entries/Matrices_for_ODEs.html https://www.isa-afp.org/entries/Matrices_for_ODEs.html Jonathan Julian Huerta y Munive 19 Apr 2020 00:00:00 +0000 Our theories formalise various matrix properties that serve to establish existence, uniqueness and characterisation of the solution to affine systems of ordinary differential equations (ODEs). In particular, we formalise the operator and maximum norm of matrices. Then we use them to prove that square matrices form a Banach space, and in this setting, we show an instance of Picard-Lindelöf’s theorem for affine systems of ODEs. Finally, we use this formalisation to verify three simple hybrid programs. Authenticated Data Structures As Functors https://www.isa-afp.org/entries/ADS_Functor.html https://www.isa-afp.org/entries/ADS_Functor.html Andreas Lochbihler, Ognjen Marić 16 Apr 2020 00:00:00 +0000 Authenticated data structures allow several systems to convince each other that they are referring to the same data structure, even if each of them knows only a part of the data structure. Using inclusion proofs, knowledgeable systems can selectively share their knowledge with other systems and the latter can verify the authenticity of what is being shared. In this article, we show how to modularly define authenticated data structures, their inclusion proofs, and operations thereon as datatypes in Isabelle/HOL, using a shallow embedding. Modularity allows us to construct complicated trees from reusable building blocks, which we call Merkle functors. Merkle functors include sums, products, and function spaces and are closed under composition and least fixpoints. As a practical application, we model the hierarchical transactions of <a href="https://www.canton.io">Canton</a>, a practical interoperability protocol for distributed ledgers, as authenticated data structures. This is a first step towards formalizing the Canton protocol and verifying its integrity and security guarantees. Formalization of an Algorithm for Greedily Computing Associative Aggregations on Sliding Windows https://www.isa-afp.org/entries/Sliding_Window_Algorithm.html https://www.isa-afp.org/entries/Sliding_Window_Algorithm.html Lukas Heimes, Dmitriy Traytel, Joshua Schneider 10 Apr 2020 00:00:00 +0000 Basin et al.'s <a href="https://doi.org/10.1016/j.ipl.2014.09.009">sliding window algorithm (SWA)</a> is an algorithm for combining the elements of subsequences of a sequence with an associative operator. It is greedy and minimizes the number of operator applications. We formalize the algorithm and verify its functional correctness. We extend the algorithm with additional operations and provide an alternative interface to the slide operation that does not require the entire input sequence. A Comprehensive Framework for Saturation Theorem Proving https://www.isa-afp.org/entries/Saturation_Framework.html https://www.isa-afp.org/entries/Saturation_Framework.html Sophie Tourret 09 Apr 2020 00:00:00 +0000 This Isabelle/HOL formalization is the companion of the technical report “A comprehensive framework for saturation theorem proving”, itself companion of the eponym IJCAR 2020 paper, written by Uwe Waldmann, Sophie Tourret, Simon Robillard and Jasmin Blanchette. It verifies a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution or superposition, and allows to model entire prover architectures in such a way that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of a prover implementing the calculus using a variant of the given clause loop. The technical report “A comprehensive framework for saturation theorem proving” is available <a href="http://matryoshka.gforge.inria.fr/pubs/satur_report.pdf">on the Matryoshka website</a>. The names of the Isabelle lemmas and theorems corresponding to the results in the report are indicated in the margin of the report. Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations https://www.isa-afp.org/entries/MFODL_Monitor_Optimized.html https://www.isa-afp.org/entries/MFODL_Monitor_Optimized.html Thibault Dardinier, Lukas Heimes, Martin Raszyk, Joshua Schneider, Dmitriy Traytel 09 Apr 2020 00:00:00 +0000 A monitor is a runtime verification tool that solves the following problem: Given a stream of time-stamped events and a policy formulated in a specification language, decide whether the policy is satisfied at every point in the stream. We verify the correctness of an executable monitor for specifications given as formulas in metric first-order dynamic logic (MFODL), which combines the features of metric first-order temporal logic (MFOTL) and metric dynamic logic. Thus, MFODL supports real-time constraints, first-order parameters, and regular expressions. Additionally, the monitor supports aggregation operations such as count and sum. This formalization, which is described in a <a href="http://people.inf.ethz.ch/trayteld/papers/ijcar20-verimonplus/verimonplus.pdf"> forthcoming paper at IJCAR 2020</a>, significantly extends <a href="https://www.isa-afp.org/entries/MFOTL_Monitor.html">previous work on a verified monitor</a> for MFOTL. Apart from the addition of regular expressions and aggregations, we implemented <a href="https://www.isa-afp.org/entries/Generic_Join.html">multi-way joins</a> and a specialized sliding window algorithm to further optimize the monitor. Lucas's Theorem https://www.isa-afp.org/entries/Lucas_Theorem.html https://www.isa-afp.org/entries/Lucas_Theorem.html Chelsea Edmonds 07 Apr 2020 00:00:00 +0000 This work presents a formalisation of a generating function proof for Lucas's theorem. We first outline extensions to the existing Formal Power Series (FPS) library, including an equivalence relation for coefficients modulo n, an alternate binomial theorem statement, and a formalised proof of the Freshman's dream (mod p) lemma. The second part of the work presents the formal proof of Lucas's Theorem. Working backwards, the formalisation first proves a well known corollary of the theorem which is easier to formalise, and then applies induction to prove the original theorem statement. The proof of the corollary aims to provide a good example of a formalised generating function equivalence proof using the FPS library. The final theorem statement is intended to be integrated into the formalised proof of Hilbert's 10th Problem. Strong Eventual Consistency of the Collaborative Editing Framework WOOT https://www.isa-afp.org/entries/WOOT_Strong_Eventual_Consistency.html https://www.isa-afp.org/entries/WOOT_Strong_Eventual_Consistency.html Emin Karayel, Edgar Gonzàlez 25 Mar 2020 00:00:00 +0000 Commutative Replicated Data Types (CRDTs) are a promising new class of data structures for large-scale shared mutable content in applications that only require eventual consistency. The WithOut Operational Transforms (WOOT) framework is a CRDT for collaborative text editing introduced by Oster et al. (CSCW 2006) for which the eventual consistency property was verified only for a bounded model to date. We contribute a formal proof for WOOTs strong eventual consistency. Furstenberg's topology and his proof of the infinitude of primes https://www.isa-afp.org/entries/Furstenberg_Topology.html https://www.isa-afp.org/entries/Furstenberg_Topology.html Manuel Eberl 22 Mar 2020 00:00:00 +0000 This article gives a formal version of Furstenberg's topological proof of the infinitude of primes. He defines a topology on the integers based on arithmetic progressions (or, equivalently, residue classes). Using some fairly obvious properties of this topology, the infinitude of primes is then easily obtained. Apart from this, this topology is also fairly ‘nice’ in general: it is second countable, metrizable, and perfect. All of these (well-known) facts are formally proven, including an explicit metric for the topology given by Zulfeqarr. An Under-Approximate Relational Logic https://www.isa-afp.org/entries/Relational-Incorrectness-Logic.html https://www.isa-afp.org/entries/Relational-Incorrectness-Logic.html Toby Murray 12 Mar 2020 00:00:00 +0000 Recently, authors have proposed under-approximate logics for reasoning about programs. So far, all such logics have been confined to reasoning about individual program behaviours. Yet there exist many over-approximate relational logics for reasoning about pairs of programs and relating their behaviours. We present the first under-approximate relational logic, for the simple imperative language IMP. We prove our logic is both sound and complete. Additionally, we show how reasoning in this logic can be decomposed into non-relational reasoning in an under-approximate Hoare logic, mirroring Beringer’s result for over-approximate relational logics. We illustrate the application of our logic on some small examples in which we provably demonstrate the presence of insecurity. Hello World https://www.isa-afp.org/entries/Hello_World.html https://www.isa-afp.org/entries/Hello_World.html Cornelius Diekmann, Lars Hupel 07 Mar 2020 00:00:00 +0000 In this article, we present a formalization of the well-known "Hello, World!" code, including a formal framework for reasoning about IO. Our model is inspired by the handling of IO in Haskell. We start by formalizing the 🌍 and embrace the IO monad afterwards. Then we present a sample main :: IO (), followed by its proof of correctness. Implementing the Goodstein Function in λ-Calculus https://www.isa-afp.org/entries/Goodstein_Lambda.html https://www.isa-afp.org/entries/Goodstein_Lambda.html Bertram Felgenhauer 21 Feb 2020 00:00:00 +0000 In this formalization, we develop an implementation of the Goodstein function G in plain λ-calculus, linked to a concise, self-contained specification. The implementation works on a Church-encoded representation of countable ordinals. The initial conversion to hereditary base 2 is not covered, but the material is sufficient to compute the particular value G(16), and easily extends to other fixed arguments. A Generic Framework for Verified Compilers https://www.isa-afp.org/entries/VeriComp.html https://www.isa-afp.org/entries/VeriComp.html Martin Desharnais 10 Feb 2020 00:00:00 +0000 This is a generic framework for formalizing compiler transformations. It leverages Isabelle/HOL’s locales to abstract over concrete languages and transformations. It states common definitions for language semantics, program behaviours, forward and backward simulations, and compilers. We provide generic operations, such as simulation and compiler composition, and prove general (partial) correctness theorems, resulting in reusable proof components. Arithmetic progressions and relative primes https://www.isa-afp.org/entries/Arith_Prog_Rel_Primes.html https://www.isa-afp.org/entries/Arith_Prog_Rel_Primes.html José Manuel Rodríguez Caballero 01 Feb 2020 00:00:00 +0000 This article provides a formalization of the solution obtained by the author of the Problem “ARITHMETIC PROGRESSIONS” from the <a href="https://www.ocf.berkeley.edu/~wwu/riddles/putnam.shtml"> Putnam exam problems of 2002</a>. The statement of the problem is as follows: For which integers n > 1 does the set of positive integers less than and relatively prime to n constitute an arithmetic progression? A Hierarchy of Algebras for Boolean Subsets https://www.isa-afp.org/entries/Subset_Boolean_Algebras.html https://www.isa-afp.org/entries/Subset_Boolean_Algebras.html Walter Guttmann, Bernhard Möller 31 Jan 2020 00:00:00 +0000 We present a collection of axiom systems for the construction of Boolean subalgebras of larger overall algebras. The subalgebras are defined as the range of a complement-like operation on a semilattice. This technique has been used, for example, with the antidomain operation, dynamic negation and Stone algebras. We present a common ground for these constructions based on a new equational axiomatisation of Boolean algebras. Mersenne primes and the Lucas–Lehmer test https://www.isa-afp.org/entries/Mersenne_Primes.html https://www.isa-afp.org/entries/Mersenne_Primes.html Manuel Eberl 17 Jan 2020 00:00:00 +0000 This article provides formal proofs of basic properties of Mersenne numbers, i. e. numbers of the form 2n - 1, and especially of Mersenne primes. In particular, an efficient, verified, and executable version of the Lucas–Lehmer test is developed. This test decides primality for Mersenne numbers in time polynomial in n. Verified Approximation Algorithms https://www.isa-afp.org/entries/Approximation_Algorithms.html https://www.isa-afp.org/entries/Approximation_Algorithms.html Robin Eßmann, Tobias Nipkow, Simon Robillard 16 Jan 2020 00:00:00 +0000 We present the first formal verification of approximation algorithms for NP-complete optimization problems: vertex cover, independent set, load balancing, and bin packing. The proofs correct incompletenesses in existing proofs and improve the approximation ratio in one case. Closest Pair of Points Algorithms https://www.isa-afp.org/entries/Closest_Pair_Points.html https://www.isa-afp.org/entries/Closest_Pair_Points.html Martin Rau, Tobias Nipkow 13 Jan 2020 00:00:00 +0000 This entry provides two related verified divide-and-conquer algorithms solving the fundamental Closest Pair of Points problem in Computational Geometry. Functional correctness and the optimal running time of O(n log n) are proved. Executable code is generated which is empirically competitive with handwritten reference implementations. Skip Lists https://www.isa-afp.org/entries/Skip_Lists.html https://www.isa-afp.org/entries/Skip_Lists.html Max W. Haslbeck, Manuel Eberl 09 Jan 2020 00:00:00 +0000 Skip lists are sorted linked lists enhanced with shortcuts and are an alternative to binary search trees. A skip lists consists of multiple levels of sorted linked lists where a list on level n is a subsequence of the list on level n − 1. In the ideal case, elements are skipped in such a way that a lookup in a skip lists takes O(log n) time. In a randomised skip list the skipped elements are choosen randomly. This entry contains formalized proofs of the textbook results about the expected height and the expected length of a search path in a randomised skip list. Bicategories https://www.isa-afp.org/entries/Bicategory.html https://www.isa-afp.org/entries/Bicategory.html Eugene W. Stark 06 Jan 2020 00:00:00 +0000 Taking as a starting point the author's previous work on developing aspects of category theory in Isabelle/HOL, this article gives a compatible formalization of the notion of "bicategory" and develops a framework within which formal proofs of facts about bicategories can be given. The framework includes a number of basic results, including the Coherence Theorem, the Strictness Theorem, pseudofunctors and biequivalence, and facts about internal equivalences and adjunctions in a bicategory. As a driving application and demonstration of the utility of the framework, it is used to give a formal proof of a theorem, due to Carboni, Kasangian, and Street, that characterizes up to biequivalence the bicategories of spans in a category with pullbacks. The formalization effort necessitated the filling-in of many details that were not evident from the brief presentation in the original paper, as well as identifying a few minor corrections along the way. The Irrationality of ζ(3) https://www.isa-afp.org/entries/Zeta_3_Irrational.html https://www.isa-afp.org/entries/Zeta_3_Irrational.html Manuel Eberl 27 Dec 2019 00:00:00 +0000 This article provides a formalisation of Beukers's straightforward analytic proof that ζ(3) is irrational. This was first proven by Apéry (which is why this result is also often called ‘Apéry's Theorem’) using a more algebraic approach. This formalisation follows <a href="http://people.math.sc.edu/filaseta/gradcourses/Math785/Math785Notes4.pdf">Filaseta's presentation</a> of Beukers's proof. Formalizing a Seligman-Style Tableau System for Hybrid Logic https://www.isa-afp.org/entries/Hybrid_Logic.html https://www.isa-afp.org/entries/Hybrid_Logic.html Asta Halkjær From 20 Dec 2019 00:00:00 +0000 This work is a formalization of soundness and completeness proofs for a Seligman-style tableau system for hybrid logic. The completeness result is obtained via a synthetic approach using maximally consistent sets of tableau blocks. The formalization differs from the cited work in a few ways. First, to avoid the need to backtrack in the construction of a tableau, the formalized system has no unnamed initial segment, and therefore no Name rule. Second, I show that the full Bridge rule is admissible in the system. Third, I start from rules restricted to only extend the branch with new formulas, including only witnessing diamonds that are not already witnessed, and show that the unrestricted rules are admissible. Similarly, I start from simpler versions of the @-rules and show the general ones admissible. Finally, the GoTo rule is restricted using a notion of coins such that each application consumes a coin and coins are earned through applications of the remaining rules. I show that if a branch can be closed then it can be closed starting from a single coin. These restrictions are imposed to rule out some means of nontermination. The Poincaré-Bendixson Theorem https://www.isa-afp.org/entries/Poincare_Bendixson.html https://www.isa-afp.org/entries/Poincare_Bendixson.html Fabian Immler, Yong Kiam Tan 18 Dec 2019 00:00:00 +0000 The Poincaré-Bendixson theorem is a classical result in the study of (continuous) dynamical systems. Colloquially, it restricts the possible behaviors of planar dynamical systems: such systems cannot be chaotic. In practice, it is a useful tool for proving the existence of (limiting) periodic behavior in planar systems. The theorem is an interesting and challenging benchmark for formalized mathematics because proofs in the literature rely on geometric sketches and only hint at symmetric cases. It also requires a substantial background of mathematical theories, e.g., the Jordan curve theorem, real analysis, ordinary differential equations, and limiting (long-term) behavior of dynamical systems. Poincaré Disc Model https://www.isa-afp.org/entries/Poincare_Disc.html https://www.isa-afp.org/entries/Poincare_Disc.html Danijela Simić, Filip Marić, Pierre Boutry 16 Dec 2019 00:00:00 +0000 We describe formalization of the Poincaré disc model of hyperbolic geometry within the Isabelle/HOL proof assistant. The model is defined within the extended complex plane (one dimensional complex projectives space ℂP1), formalized in the AFP entry “Complex Geometry”. Points, lines, congruence of pairs of points, betweenness of triples of points, circles, and isometries are defined within the model. It is shown that the model satisfies all Tarski's axioms except the Euclid's axiom. It is shown that it satisfies its negation and the limiting parallels axiom (which proves it to be a model of hyperbolic geometry).