diff --git a/CONTRIBUTORS b/CONTRIBUTORS --- a/CONTRIBUTORS +++ b/CONTRIBUTORS @@ -1,1150 +1,1153 @@ For the purposes of the license agreement in the file COPYRIGHT, a 'contributor' is anybody who is listed in this file (CONTRIBUTORS) or who is listed as an author in one of the source files of this Isabelle distribution. Contributions to Isabelle2024 ----------------------------- * Αpril 2024: Manuel Eberl, Katharina Kreuzer Some material on finite fields and the characteristic of a ring in HOL, HOL-Computational_Algebra, and HOL-Number_Theory. Also a type constructor for the algebraic closure of a field. * March 2024: Manuel Eberl Weierstraß Factorization Theorem in HOL-Complex_Analysis. +* March 2024: Ata Keskin + Analysis lemmas drawn from the Martingales AFP entry. + * March 2024: Anthony Bordg, Manuel Eberl, Wenda Li, Larry Paulson New and more general definition of meromorphicity in HOL-Complex_Analysis. * Feb/March 2024: Simon Wimmer Improvements to HOL-ex.Sketch_and_Explore. * Feb/March 2024: Jonas Stahl Automatic translation of HOL functions into corresponding step-counting running-time functions. * 2023/2024: Makarius Wenzel and Fabian Huch More robust and scalable support for distributed build clusters. * October 2023: Fabian Huch Support for SMTP mailing in Isabelle/Scala. Contributions to Isabelle2023 ----------------------------- * August 2022 - July 2023: Hannah Lachnitt, Stanford and Mathias Fleury, UFR Start work toward reconstructing cvc5 proof in the SMT method. This is currently very experimental and is also changing on the cvc5 side. * October 2022: Jeremy Sylvestre Lemmas for Fun and List. * 2022/2023: Makarius Wenzel Support for interactive document preparation in PIDE, including demo documents for well-known LaTeX styles. * March 2023 - June 2023: Makarius Wenzel ML heap usage and stored heap size has been significantly reduced; based on new command-line tool "isabelle profiling". * 2023: Makarius Wenzel and Fabian Huch Support for distributed build clusters, based on SSH and PostgreSQL. Contributions to Isabelle2022 ----------------------------- * August 2022: Norbert Schirmer, Apple Record simproc that sorts update expressions. * June 2022: Jan van Brügge, TU München Strict cardinality bounds for BNFs. * April - August 2021: Denis Paluca and Fabian Huch, TU München Various improvements to Isabelle/VSCode. * March 2021: Florian Haftmann, TU München More ambitious minimization of case expressions in generated code; code generation: type annotations in pattern bindings are printed in a way suitable for Scala 3. * July 2022: Florian Haftmann, TU München and René Thiemann, UIBK Theory Code_Abstract_Char implements characters by target language integers, sacrificing pattern patching in exchange for dramatically increased performance for comparisions. * November 2021, July - August 2022: Fabian Huch and Makarius Wenzel Improved HTML presentation. Contributions to Isabelle2021-1 ------------------------------- * September / October 2021: Jasmin Blanchette, Martin Desharnais, Mathias Fleury, Makarius Wenzel Upgrade of automatic theorem provers in Sledgehammer and the "smt" proof method. * July - September 2021: Makarius Wenzel Significantly improved Isabelle/Haskell library. * July - September 2021: Jasmin Blanchette, Martin Desharnais Various improvements to Sledgehammer. * September 2021: Dominique Unruh New theory of infinite sums (theory HOL-Analysis.Infinite_Sum), ordering of complex numbers (theory HOL-Library.Complex_Order), and products of uniform spaces (theory HOL-Analysis.Product_Vector). * August 2021: Fabian Huch, TU München Improved HTML presentation: links to formal entities. * November 2020 / July 2021: Norbert Schirmer, Apple Various improvements and cleanup of session "HOL-Statespace". * July 2021: Florian Haftmann Further consolidation of bit operations and word types. * June 2021: Florian Haftmann More context situations susceptible to global_interpretation. * March 2021: Lukas Stevens New order prover. * March 2021: Florian Haftmann Dedicated session for combinatorics. * March 2021: Simon Foster and Leo Freitas More symbol definitions for Z Notation: Isabelle fonts and LaTeX macros. * February 2021: Manuel Eberl New material in sessions HOL-Analysis and HOL-Probability, most notably Hoeffding's inequality and the negative binomial distribution * January 2021: Jakub Kądziołka Some lemmas for HOL-Computational_Algebra. * January 2021: Martin Rasyzk Fast set operations for red-black trees. Contributions to Isabelle2021 ----------------------------- * January 2021: Manuel Eberl Characteristic of a semiring. * January 2021: Manuel Eberl Algebraic integers in HOL-Computational_Algebra. * December 2020: Stepan Holub Contributed lemmas for theory HOL.List. * December 2020: Martin Desharnais Zipperposition 2.0 as external prover for Sledgehammer. * December 2020: Walter Guttmann Extension of session HOL-Hoare with total correctness proof system. * November / December 2020: Makarius Wenzel Improved HTML presentation and PDF document preparation, using mostly Isabelle/Scala instead of Isabelle/ML. * November 2020: Stepan Holub Removed preconditions from lemma comm_append_are_replicate. * November 2020: Florian Haftmann Bundle mixins for locale and class expressions. * November 2020: Jakub Kądziołka Stronger lemmas about orders of group elements (generate_pow_card). * October 2020: Jasmin Blanchette, Martin Desharnais, Mathias Fleury Support veriT as external prover in Sledgehammer. * October 2020: Mathias Fleury Updated proof reconstruction for the SMT solver veriT in the smt method. * October 2020: Jasmin Blanchette, Martin Desharnais Support E prover 2.5 as external prover in Sledgehammer. * September 2020: Florian Haftmann Substantial reworking and modularization of Word library, with generic type conversions. * August 2020: Makarius Wenzel Finally enable PIDE protocol for batch-builds, with various consequences of handling session build databases, Isabelle/Scala within Isabelle/ML etc. * August 2020: Makarius Wenzel Improved monitoring of runtime statistics: ML GC progress and Java. * July 2020: Martin Desharnais Update to Metis 2.4. * June 2020: Makarius Wenzel Batch-builds via "isabelle build" allow to invoke Scala from ML. * June 2020: Florian Haftmann Simproc defined_all for more aggressive substitution with variables from assumptions. * May 2020: Makarius Wenzel Antiquotations for Isabelle systems programming, notably @{scala_function} and @{scala} to invoke Scala from ML. * May 2020: Florian Haftmann Generic algebraically founded bit operations NOT, AND, OR, XOR. Contributions to Isabelle2020 ----------------------------- * February 2020: E. Gunther, M. Pagano and P. Sánchez Terraf Simplified, generalised version of ZF/Constructible. * January 2020: LC Paulson The full finite Ramsey's theorem and elements of finite and infinite Ramsey theory. * December 2019: Basil Fürer, Andreas Lochbihler, Joshua Schneider, Dmitriy Traytel Extension of lift_bnf to support quotient types. * November 2019: Peter Zeller, TU Kaiserslautern Update of Isabelle/VSCode to WebviewPanel API. * October..December 2019: Makarius Wenzel Isabelle/Phabrictor server setup, including Linux platform support in Isabelle/Scala. Client-side tool "isabelle hg_setup". * October 2019: Maximilian Schäffeler Port of the HOL Light decision procedure for metric spaces. * October 2019: Makarius Wenzel More scalable Isabelle dump and underlying headless PIDE session. * August 2019: Makarius Wenzel Better support for proof terms in Isabelle/Pure, notably via method combinator SUBPROOFS (ML) and "subproofs" (Isar). * July 2019: Alexander Krauss, Makarius Wenzel Minimal support for a soft-type system within the Isabelle logical framework. Contributions to Isabelle2019 ----------------------------- * April 2019: LC Paulson Homology and supporting lemmas on topology and group theory * April 2019: Paulo de Vilhena and Martin Baillon Group theory developments, esp. algebraic closure of a field * February/March 2019: Makarius Wenzel Stateless management of export artifacts in the Isabelle/HOL code generator. * February 2019: Manuel Eberl Exponentiation by squaring, used to implement "power" in monoid_mult and fast modular exponentiation. * February 2019: Manuel Eberl Carmichael's function, primitive roots in residue rings, more properties of the order in residue rings. * February 2019: Jeremy Sylvestre Formal Laurent Series and overhaul of Formal power series. * January 2019: Florian Haftmann Clarified syntax and congruence rules for big operators on sets involving the image operator. * January 2019: Florian Haftmann Renovation of code generation, particularly export into session data and proper strings and proper integers based on zarith for OCaml. * January 2019: Andreas Lochbihler New implementation for case_of_simps based on Code_Lazy's pattern matching elimination algorithm. * November/December 2018: Makarius Wenzel Support for Isabelle/Haskell applications of Isabelle/PIDE. * August/September 2018: Makarius Wenzel Improvements of headless Isabelle/PIDE session and server, and systematic exports from theory documents. * December 2018: Florian Haftmann Generic executable sorting algorithms based on executable comparators. * October 2018: Mathias Fleury Proof reconstruction for the SMT solver veriT in the smt method. Contributions to Isabelle2018 ----------------------------- * July 2018: Manuel Eberl "real_asymp" proof method for automatic proofs of real limits, "Big-O" statements, etc. * June 2018: Fabian Immler More tool support for HOL-Types_To_Sets. * June 2018: Martin Baillon and Paulo Emílio de Vilhena A variety of contributions to HOL-Algebra. * June 2018: Wenda Li New/strengthened results involving analysis, topology, etc. * May/June 2018: Makarius Wenzel System infrastructure to export blobs as theory presentation, and to dump PIDE database content in batch mode. * May 2018: Manuel Eberl Landau symbols and asymptotic equivalence (moved from the AFP). * May 2018: Jose Divasón (Universidad de la Rioja), Jesús Aransay (Universidad de la Rioja), Johannes Hölzl (VU Amsterdam), Fabian Immler (TUM) Generalizations in the formalization of linear algebra. * May 2018: Florian Haftmann Consolidation of string-like types in HOL. * May 2018: Andreas Lochbihler (Digital Asset), Pascal Stoop (ETH Zurich) Code generation with lazy evaluation semantics. * March 2018: Florian Haftmann Abstract bit operations push_bit, take_bit, drop_bit, alongside with an algebraic foundation for bit strings and word types in HOL-ex. * March 2018: Viorel Preoteasa Generalisation of complete_distrib_lattice * February 2018: Wenda Li A unified definition for the order of zeros and poles. Improved reasoning around non-essential singularities. * January 2018: Sebastien Gouezel Various small additions to HOL-Analysis * December 2017: Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel A new conditional parametricity prover. * October 2017: Alexander Maletzky Derivation of axiom "iff" in theory HOL.HOL from the other axioms. Contributions to Isabelle2017 ----------------------------- * September 2017: Lawrence Paulson HOL-Analysis, e.g. simplicial complexes, Jordan Curve Theorem. * September 2017: Jasmin Blanchette Further integration of Nunchaku model finder. * November 2016 - June 2017: Makarius Wenzel New Isabelle/VSCode, with underlying restructuring of Isabelle/PIDE. * 2017: Makarius Wenzel Session-qualified theory names (theory imports and ROOT files). Prover IDE improvements. Support for SQL databases in Isabelle/Scala: SQLite and PostgreSQL. * August 2017: Andreas Lochbihler, ETH Zurich type of unordered pairs (HOL-Library.Uprod) * August 2017: Manuel Eberl, TUM HOL-Analysis: infinite products over natural numbers, infinite sums over arbitrary sets, connection between formal power series and analytic complex functions * March 2017: Alasdair Armstrong, University of Sheffield and Simon Foster, University of York Fixed-point theory and Galois Connections in HOL-Algebra. * February 2017: Florian Haftmann, TUM Statically embedded computations implemented by generated code. Contributions to Isabelle2016-1 ------------------------------- * December 2016: Ondřej Kunčar, TUM Types_To_Sets: experimental extension of Higher-Order Logic to allow translation of types to sets. * October 2016: Jasmin Blanchette Integration of Nunchaku model finder. * October 2016: Jaime Mendizabal Roche, TUM Ported remaining theories of session Old_Number_Theory to the new Number_Theory and removed Old_Number_Theory. * September 2016: Sascha Boehme Proof method "argo" based on SMT technology for a combination of quantifier-free propositional logic, equality and linear real arithmetic * July 2016: Daniel Stuewe Height-size proofs in HOL-Data_Structures. * July 2016: Manuel Eberl, TUM Algebraic foundation for primes; generalization from nat to general factorial rings. * June 2016: Andreas Lochbihler, ETH Zurich Formalisation of discrete subprobability distributions. * June 2016: Florian Haftmann, TUM Improvements to code generation: optional timing measurements, more succint closures for static evaluation, less ambiguities concering Scala implicits. * May 2016: Manuel Eberl, TUM Code generation for Probability Mass Functions. * March 2016: Florian Haftmann, TUM Abstract factorial rings with unique factorization. * March 2016: Florian Haftmann, TUM Reworking of the HOL char type as special case of a finite numeral type. * March 2016: Andreas Lochbihler, ETH Zurich Reasoning support for monotonicity, continuity and admissibility in chain-complete partial orders. * February - October 2016: Makarius Wenzel Prover IDE improvements. ML IDE improvements: bootstrap of Pure. Isar language consolidation. Notational modernization of HOL. Tight Poly/ML integration. More Isabelle/Scala system programming modules (e.g. SSH, Mercurial). * Winter 2016: Jasmin Blanchette, Inria & LORIA & MPII, Aymeric Bouzy, Ecole polytechnique, Andreas Lochbihler, ETH Zurich, Andrei Popescu, Middlesex University, and Dmitriy Traytel, ETH Zurich 'corec' command and friends. * January 2016: Florian Haftmann, TUM Abolition of compound operators INFIMUM and SUPREMUM for complete lattices. Contributions to Isabelle2016 ----------------------------- * Winter 2016: Manuel Eberl, TUM Support for real exponentiation ("powr") in the "approximation" method. (This was removed in Isabelle 2015 due to a changed definition of "powr".) * Summer 2015 - Winter 2016: Lawrence C Paulson, Cambridge General, homology form of Cauchy's integral theorem and supporting material (ported from HOL Light). * Winter 2015/16: Gerwin Klein, NICTA New print_record command. * May - December 2015: Makarius Wenzel Prover IDE improvements. More Isar language elements. Document language refinements. Poly/ML debugger integration. Improved multi-platform and multi-architecture support. * Winter 2015: Manuel Eberl, TUM The radius of convergence of power series and various summability tests. Harmonic numbers and the Euler-Mascheroni constant. The Generalised Binomial Theorem. The complex and real Gamma/log-Gamma/Digamma/Polygamma functions and their most important properties. * Autumn 2015: Manuel Eberl, TUM Proper definition of division (with remainder) for formal power series; Euclidean Ring and GCD instance for formal power series. * Autumn 2015: Florian Haftmann, TUM Rewrite definitions for global interpretations and sublocale declarations. * Autumn 2015: Andreas Lochbihler Bourbaki-Witt fixpoint theorem for increasing functions on chain-complete partial orders. * Autumn 2015: Chaitanya Mangla, Lawrence C Paulson, and Manuel Eberl A large number of additional binomial identities. * Summer 2015: Daniel Matichuk, NICTA and Makarius Wenzel Isar subgoal command for proof structure within unstructured proof scripts. * Summer 2015: Florian Haftmann, TUM Generic partial division in rings as inverse operation of multiplication. * Summer 2015: Manuel Eberl and Florian Haftmann, TUM Type class hierarchy with common algebraic notions of integral (semi)domains like units, associated elements and normalization wrt. units. * Summer 2015: Florian Haftmann, TUM Fundamentals of abstract type class for factorial rings. * Summer 2015: Julian Biendarra, TUM and Dmitriy Traytel, ETH Zurich Command to lift a BNF structure on the raw type to the abstract type for typedefs. * Summer 2014: Jeremy Avigad, Luke Serafin, CMU, and Johannes Hölzl, TUM Proof of the central limit theorem: includes weak convergence, characteristic functions, and Levy's uniqueness and continuity theorem. Contributions to Isabelle2015 ----------------------------- * 2014/2015: Daniel Matichuk, Toby Murray, NICTA and Makarius Wenzel The Eisbach proof method language and "match" method. * Winter 2014 and Spring 2015: Ondrej Kuncar, TUM Extension of lift_definition to execute lifted functions that have as a return type a datatype containing a subtype. * March 2015: Jasmin Blanchette, Inria & LORIA & MPII, Mathias Fleury, MPII, and Dmitriy Traytel, TUM More multiset theorems, syntax, and operations. * December 2014: Johannes Hölzl, Manuel Eberl, Sudeep Kanav, TUM, and Jeremy Avigad, Luke Serafin, CMU Various integration theorems: mostly integration on intervals and substitution. * September 2014: Florian Haftmann, TUM Lexicographic order on functions and sum/product over function bodies. * August 2014: Andreas Lochbihler, ETH Zurich Test infrastructure for executing generated code in target languages. * August 2014: Manuel Eberl, TUM Generic euclidean algorithms for GCD et al. Contributions to Isabelle2014 ----------------------------- * July 2014: Thomas Sewell, NICTA Preserve equality hypotheses in "clarify" and friends. New "hypsubst_thin" method configuration option. * Summer 2014: Florian Haftmann, TUM Consolidation and generalization of facts concerning (abelian) semigroups and monoids, particularly products (resp. sums) on finite sets. * Summer 2014: Mathias Fleury, ENS Rennes, and Albert Steckermeier, TUM Work on exotic automatic theorem provers for Sledgehammer (LEO-II, veriT, Waldmeister, etc.). * June 2014: Florian Haftmann, TUM Internal reorganisation of the local theory / named target stack. * June 2014: Sudeep Kanav, TUM, Jeremy Avigad, CMU, and Johannes Hölzl, TUM Various properties of exponentially, Erlang, and normal distributed random variables. * May 2014: Cezary Kaliszyk, University of Innsbruck, and Jasmin Blanchette, TUM SML-based engines for MaSh. * March 2014: René Thiemann Improved code generation for multisets. * February 2014: Florian Haftmann, TUM Permanent interpretation inside theory, locale and class targets with mixin definitions. * Spring 2014: Lawrence C Paulson, Cambridge Theory Complex_Basic_Analysis. Tidying up Number_Theory vs Old_Number_Theory * Winter 2013 and Spring 2014: Ondrej Kuncar, TUM Various improvements to Lifting/Transfer, integration with the BNF package. * Winter 2013 and Spring 2014: Makarius Wenzel, Université Paris-Sud / LRI Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE. * Fall 2013 and Winter 2014: Martin Desharnais, Lorenz Panny, Dmitriy Traytel, and Jasmin Blanchette, TUM Various improvements to the BNF-based (co)datatype package, including a more polished "primcorec" command, optimizations, and integration in the "HOL" session. * Winter/Spring 2014: Sascha Boehme, QAware GmbH, and Jasmin Blanchette, TUM "SMT2" module and "smt2" proof method, based on SMT-LIB 2 and Z3 4.3. * January 2014: Lars Hupel, TUM An improved, interactive simplifier trace with integration into the Isabelle/jEdit Prover IDE. * December 2013: Florian Haftmann, TUM Consolidation of abstract interpretations concerning min and max. * November 2013: Florian Haftmann, TUM Abolition of negative numeral literals in the logic. Contributions to Isabelle2013-1 ------------------------------- * September 2013: Lars Noschinski, TUM Conversion between function definitions as list of equations and case expressions in HOL. New library Simps_Case_Conv with commands case_of_simps, simps_of_case. * September 2013: Nik Sultana, University of Cambridge Improvements to HOL/TPTP parser and import facilities. * September 2013: Johannes Hölzl and Dmitriy Traytel, TUM New "coinduction" method (residing in HOL-BNF) to avoid boilerplate. * Summer 2013: Makarius Wenzel, Université Paris-Sud / LRI Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE. * Summer 2013: Manuel Eberl, TUM Generation of elimination rules in the function package. New command "fun_cases". * Summer 2013: Christian Sternagel, JAIST Improved support for ad hoc overloading of constants, including documentation and examples. * Spring and Summer 2013: Lorenz Panny, Dmitriy Traytel, and Jasmin Blanchette, TUM Various improvements to the BNF-based (co)datatype package, including "primrec_new" and "primcorec" commands and a compatibility layer. * Spring and Summer 2013: Ondrej Kuncar, TUM Various improvements of Lifting and Transfer packages. * Spring 2013: Brian Huffman, Galois Inc. Improvements of the Transfer package. * Summer 2013: Daniel Kühlwein, ICIS, Radboud University Nijmegen Jasmin Blanchette, TUM Various improvements to MaSh, including a server mode. * First half of 2013: Steffen Smolka, TUM Further improvements to Sledgehammer's Isar proof generator. * May 2013: Florian Haftmann, TUM Ephemeral interpretation in local theories. * May 2013: Lukas Bulwahn and Nicolai Schaffroth, TUM Spec_Check: A Quickcheck tool for Isabelle/ML. * April 2013: Stefan Berghofer, secunet Security Networks AG Dmitriy Traytel, TUM Makarius Wenzel, Université Paris-Sud / LRI Case translations as a separate check phase independent of the datatype package. * March 2013: Florian Haftmann, TUM Reform of "big operators" on sets. * March 2013: Florian Haftmann, TUM Algebraic locale hierarchy for orderings and (semi)lattices. * February 2013: Florian Haftmann, TUM Reworking and consolidation of code generation for target language numerals. * February 2013: Florian Haftmann, TUM Sieve of Eratosthenes. Contributions to Isabelle2013 ----------------------------- * 2012: Makarius Wenzel, Université Paris-Sud / LRI Improvements of Isabelle/Scala and Isabelle/jEdit Prover IDE. * Fall 2012: Daniel Kühlwein, ICIS, Radboud University Nijmegen Jasmin Blanchette, TUM Implemented Machine Learning for Sledgehammer (MaSh). * Fall 2012: Steffen Smolka, TUM Various improvements to Sledgehammer's Isar proof generator, including a smart type annotation algorithm and proof shrinking. * December 2012: Alessandro Coglio, Kestrel Contributions to HOL's Lattice library. * November 2012: Fabian Immler, TUM "Symbols" dockable for Isabelle/jEdit. * November 2012: Fabian Immler, TUM Proof of the Daniell-Kolmogorov theorem: the existence of the limit of projective families. * October 2012: Andreas Lochbihler, KIT Efficient construction of red-black trees from sorted associative lists. * September 2012: Florian Haftmann, TUM Lattice instances for type option. * September 2012: Christian Sternagel, JAIST Consolidated HOL/Library (theories: Prefix_Order, Sublist, and Sublist_Order) w.r.t. prefixes, suffixes, and embedding on lists. * August 2012: Dmitriy Traytel, Andrei Popescu, Jasmin Blanchette, TUM New BNF-based (co)datatype package. * August 2012: Andrei Popescu and Dmitriy Traytel, TUM Theories of ordinals and cardinals. * July 2012: Makarius Wenzel, Université Paris-Sud / LRI Advanced support for Isabelle sessions and build management, notably "isabelle build". * June 2012: Felix Kuperjans, Lukas Bulwahn, TUM and Rafal Kolanski, NICTA Simproc for rewriting set comprehensions into pointfree expressions. * May 2012: Andreas Lochbihler, KIT Theory of almost everywhere constant functions. * 2010-2012: Markus Kaiser and Lukas Bulwahn, TUM Graphview in Scala/Swing. Contributions to Isabelle2012 ----------------------------- * April 2012: Johannes Hölzl, TUM Probability: Introduced type to represent measures instead of locales. * April 2012: Johannes Hölzl, Fabian Immler, TUM Float: Moved to Dyadic rationals to represent floating point numers. * April 2012: Thomas Sewell, NICTA and 2010: Sascha Boehme, TUM Theory HOL/Word/WordBitwise: logic/circuit expansion of bitvector equalities/inequalities. * March 2012: Christian Sternagel, JAIST Consolidated theory of relation composition. * March 2012: Nik Sultana, University of Cambridge HOL/TPTP parser and import facilities. * March 2012: Cezary Kaliszyk, University of Innsbruck and Alexander Krauss, QAware GmbH Faster and more scalable Import mechanism for HOL Light proofs. * January 2012: Florian Haftmann, TUM, et al. (Re-)Introduction of the "set" type constructor. * 2012: Ondrej Kuncar, TUM New package Lifting, various improvements and refinements to the Quotient package. * 2011/2012: Jasmin Blanchette, TUM Various improvements to Sledgehammer, notably: tighter integration with SPASS, support for more provers (Alt-Ergo, iProver, iProver-Eq). * 2011/2012: Makarius Wenzel, Université Paris-Sud / LRI Various refinements of local theory infrastructure. Improvements of Isabelle/Scala layer and Isabelle/jEdit Prover IDE. Contributions to Isabelle2011-1 ------------------------------- * September 2011: Peter Gammie Theory HOL/Library/Saturated: numbers with saturated arithmetic. * August 2011: Florian Haftmann, Johannes Hölzl and Lars Noschinski, TUM Refined theory on complete lattices. * August 2011: Brian Huffman, Portland State University Miscellaneous cleanup of Complex_Main and Multivariate_Analysis. * June 2011: Brian Huffman, Portland State University Proof method "countable_datatype" for theory Library/Countable. * 2011: Jasmin Blanchette, TUM Various improvements to Sledgehammer, notably: use of sound translations, support for more provers (Waldmeister, LEO-II, Satallax). Further development of Nitpick and 'try' command. * 2011: Andreas Lochbihler, Karlsruhe Institute of Technology Theory HOL/Library/Cset_Monad allows do notation for computable sets (cset) via the generic monad ad-hoc overloading facility. * 2011: Johannes Hölzl, Armin Heller, TUM and Bogdan Grechuk, University of Edinburgh Theory HOL/Library/Extended_Reals: real numbers extended with plus and minus infinity. * 2011: Makarius Wenzel, Université Paris-Sud / LRI Various building blocks for Isabelle/Scala layer and Isabelle/jEdit Prover IDE. Contributions to Isabelle2011 ----------------------------- * January 2011: Stefan Berghofer, secunet Security Networks AG HOL-SPARK: an interactive prover back-end for SPARK. * October 2010: Bogdan Grechuk, University of Edinburgh Extended convex analysis in Multivariate Analysis. * October 2010: Dmitriy Traytel, TUM Coercive subtyping via subtype constraints. * October 2010: Alexander Krauss, TUM Command partial_function for function definitions based on complete partial orders in HOL. * September 2010: Florian Haftmann, TUM Refined concepts for evaluation, i.e., normalization of terms using different techniques. * September 2010: Florian Haftmann, TUM Code generation for Scala. * August 2010: Johannes Hoelzl, Armin Heller, and Robert Himmelmann, TUM Improved Probability theory in HOL. * July 2010: Florian Haftmann, TUM Reworking and extension of the Imperative HOL framework. * July 2010: Alexander Krauss, TUM and Christian Sternagel, University of Innsbruck Ad-hoc overloading. Generic do notation for monads. Contributions to Isabelle2009-2 ------------------------------- * 2009/2010: Stefan Berghofer, Alexander Krauss, and Andreas Schropp, TUM, Makarius Wenzel, TUM / LRI Elimination of type classes from proof terms. * April 2010: Florian Haftmann, TUM Reorganization of abstract algebra type classes. * April 2010: Florian Haftmann, TUM Code generation for data representations involving invariants; various collections avaiable in theories Fset, Dlist, RBT, Mapping and AssocList. * March 2010: Sascha Boehme, TUM Efficient SHA1 library for Poly/ML. * February 2010: Cezary Kaliszyk and Christian Urban, TUM Quotient type package for Isabelle/HOL. Contributions to Isabelle2009-1 ------------------------------- * November 2009, Brian Huffman, PSU New definitional domain package for HOLCF. * November 2009: Robert Himmelmann, TUM Derivation and Brouwer's fixpoint theorem in Multivariate Analysis. * November 2009: Stefan Berghofer and Lukas Bulwahn, TUM A tabled implementation of the reflexive transitive closure. * November 2009: Lukas Bulwahn, TUM Predicate Compiler: a compiler for inductive predicates to equational specifications. * November 2009: Sascha Boehme, TUM and Burkhart Wolff, LRI Paris HOL-Boogie: an interactive prover back-end for Boogie and VCC. * October 2009: Jasmin Blanchette, TUM Nitpick: yet another counterexample generator for Isabelle/HOL. * October 2009: Sascha Boehme, TUM Extension of SMT method: proof-reconstruction for the SMT solver Z3. * October 2009: Florian Haftmann, TUM Refinement of parts of the HOL datatype package. * October 2009: Florian Haftmann, TUM Generic term styles for term antiquotations. * September 2009: Thomas Sewell, NICTA More efficient HOL/record implementation. * September 2009: Sascha Boehme, TUM SMT method using external SMT solvers. * September 2009: Florian Haftmann, TUM Refinement of sets and lattices. * July 2009: Jeremy Avigad and Amine Chaieb New number theory. * July 2009: Philipp Meyer, TUM HOL/Library/Sum_Of_Squares: functionality to call a remote csdp prover. * July 2009: Florian Haftmann, TUM New quickcheck implementation using new code generator. * July 2009: Florian Haftmann, TUM HOL/Library/Fset: an explicit type of sets; finite sets ready to use for code generation. * June 2009: Florian Haftmann, TUM HOL/Library/Tree: search trees implementing mappings, ready to use for code generation. * March 2009: Philipp Meyer, TUM Minimization tool for results from Sledgehammer. Contributions to Isabelle2009 ----------------------------- * March 2009: Robert Himmelmann, TUM and Amine Chaieb, University of Cambridge Elementary topology in Euclidean space. * March 2009: Johannes Hoelzl, TUM Method "approximation", which proves real valued inequalities by computation. * February 2009: Filip Maric, Univ. of Belgrade A Serbian theory. * February 2009: Jasmin Christian Blanchette, TUM Misc cleanup of HOL/refute. * February 2009: Timothy Bourke, NICTA New find_consts command. * February 2009: Timothy Bourke, NICTA "solves" criterion for find_theorems and auto_solve option * December 2008: Clemens Ballarin, TUM New locale implementation. * December 2008: Armin Heller, TUM and Alexander Krauss, TUM Method "sizechange" for advanced termination proofs. * November 2008: Timothy Bourke, NICTA Performance improvement (factor 50) for find_theorems. * 2008: Florian Haftmann, TUM Various extensions and restructurings in HOL, improvements in evaluation mechanisms, new module binding.ML for name bindings. * October 2008: Fabian Immler, TUM ATP manager for Sledgehammer, based on ML threads instead of Posix processes. Additional ATP wrappers, including remote SystemOnTPTP services. * September 2008: Stefan Berghofer, TUM and Marc Bezem, Univ. Bergen Prover for coherent logic. * August 2008: Fabian Immler, TUM Vampire wrapper script for remote SystemOnTPTP service. Contributions to Isabelle2008 ----------------------------- * 2007/2008: Alexander Krauss, TUM and Florian Haftmann, TUM and Stefan Berghofer, TUM HOL library improvements. * 2007/2008: Brian Huffman, PSU HOLCF library improvements. * 2007/2008: Stefan Berghofer, TUM HOL-Nominal package improvements. * March 2008: Markus Reiter, TUM HOL/Library/RBT: red-black trees. * February 2008: Alexander Krauss, TUM and Florian Haftmann, TUM and Lukas Bulwahn, TUM and John Matthews, Galois: HOL/Library/Imperative_HOL: Haskell-style imperative data structures for HOL. * December 2007: Norbert Schirmer, Uni Saarbruecken Misc improvements of record package in HOL. * December 2007: Florian Haftmann, TUM Overloading and class instantiation target. * December 2007: Florian Haftmann, TUM New version of primrec package for local theories. * December 2007: Alexander Krauss, TUM Method "induction_scheme" in HOL. * November 2007: Peter Lammich, Uni Muenster HOL-Lattice: some more lemmas. Contributions to Isabelle2007 ----------------------------- * October 2007: Norbert Schirmer, TUM / Uni Saarbruecken State Spaces: The Locale Way (in HOL). * October 2007: Mark A. Hillebrand, DFKI Robust sub/superscripts in LaTeX document output. * August 2007: Jeremy Dawson, NICTA and Paul Graunke, Galois and Brian Huffman, PSU and Gerwin Klein, NICTA and John Matthews, Galois HOL-Word: a library for fixed-size machine words in Isabelle. * August 2007: Brian Huffman, PSU HOL/Library/Boolean_Algebra and HOL/Library/Numeral_Type. * June 2007: Amine Chaieb, TUM Semiring normalization and Groebner Bases. Support for dense linear orders. * June 2007: Joe Hurd, Oxford Metis theorem-prover. * 2007: Kong W. Susanto, Cambridge HOL: Metis prover integration. * 2007: Stefan Berghofer, TUM HOL: inductive predicates and sets. * 2007: Norbert Schirmer, TUM HOL/record: misc improvements. * 2006/2007: Alexander Krauss, TUM HOL: function package and related theories on termination. * 2006/2007: Florian Haftmann, TUM Pure: generic code generator framework. Pure: class package. HOL: theory reorganization, code generator setup. * 2006/2007: Christian Urban, TUM and Stefan Berghofer, TUM and Julien Narboux, TUM HOL/Nominal package and related tools. * November 2006: Lukas Bulwahn, TUM HOL: method "lexicographic_order" for function package. * October 2006: Stefan Hohe, TUM HOL-Algebra: ideals and quotients over rings. * August 2006: Amine Chaieb, TUM Experimental support for generic reflection and reification in HOL. * July 2006: Rafal Kolanski, NICTA Hex (0xFF) and binary (0b1011) numerals. * May 2006: Klaus Aehlig, LMU Command 'normal_form': normalization by evaluation. * May 2006: Amine Chaieb, TUM HOL-Complex: Ferrante and Rackoff Algorithm for linear real arithmetic. * February 2006: Benjamin Porter, NICTA HOL and HOL-Complex: generalised mean value theorem, continuum is not denumerable, harmonic and arithmetic series, and denumerability of rationals. * October 2005: Martin Wildmoser, TUM Sketch for Isar 'guess' element. Contributions to Isabelle2005 ----------------------------- * September 2005: Lukas Bulwahn and Bernhard Haeupler, TUM HOL-Complex: Formalization of Taylor series. * September 2005: Stephan Merz, Alwen Tiu, QSL Loria Components for SAT solver method using zChaff. * September 2005: Ning Zhang and Christian Urban, LMU Munich A Chinese theory. * September 2005: Bernhard Haeupler, TUM Method comm_ring for proving equalities in commutative rings. * July/August 2005: Jeremy Avigad, Carnegie Mellon University Various improvements of the HOL and HOL-Complex library. * July 2005: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TUM Some structured proofs about completeness of real numbers. * May 2005: Rafal Kolanski and Gerwin Klein, NICTA Improved retrieval of facts from theory/proof context. * February 2005: Lucas Dixon, University of Edinburgh Improved subst method. * 2005: Brian Huffman, OGI Various improvements of HOLCF. Some improvements of the HOL-Complex library. * 2005: Claire Quigley and Jia Meng, University of Cambridge Some support for asynchronous communication with external provers (experimental). * 2005: Florian Haftmann, TUM Contributions to document 'sugar'. Various ML combinators, notably linear functional transformations. Some cleanup of ML legacy. Additional antiquotations. Improved Isabelle web site. * 2004/2005: David Aspinall, University of Edinburgh Various elements of XML and PGIP based communication with user interfaces (experimental). * 2004/2005: Gerwin Klein, NICTA Contributions to document 'sugar'. Improved Isabelle web site. Improved HTML presentation of theories. * 2004/2005: Clemens Ballarin, TUM Provers: tools for transitive relations and quasi orders. Improved version of locales, notably interpretation of locales. Improved version of HOL-Algebra. * 2004/2005: Amine Chaieb, TUM Improved version of HOL presburger method. * 2004/2005: Steven Obua, TUM Improved version of HOL/Import, support for HOL-Light. Improved version of HOL-Complex-Matrix. Pure/defs: more sophisticated checks on well-formedness of overloading. Pure/Tools: an experimental evaluator for lambda terms. * 2004/2005: Norbert Schirmer, TUM Contributions to document 'sugar'. Improved version of HOL/record. * 2004/2005: Sebastian Skalberg, TUM Improved version of HOL/Import. Some internal ML reorganizations. * 2004/2005: Tjark Weber, TUM SAT solver method using zChaff. Improved version of HOL/refute. :maxLineLen=78: diff --git a/src/HOL/Analysis/Elementary_Metric_Spaces.thy b/src/HOL/Analysis/Elementary_Metric_Spaces.thy --- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy +++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy @@ -1,3332 +1,3333 @@ (* Author: L C Paulson, University of Cambridge Author: Amine Chaieb, University of Cambridge Author: Robert Himmelmann, TU Muenchen Author: Brian Huffman, Portland State University + Author: Ata Keskin, TU Muenchen *) chapter \Elementary Metric Spaces\ theory Elementary_Metric_Spaces imports Abstract_Topology_2 Metric_Arith begin section \Open and closed balls\ definition\<^marker>\tag important\ ball :: "'a::metric_space \ real \ 'a set" where "ball x e = {y. dist x y < e}" definition\<^marker>\tag important\ cball :: "'a::metric_space \ real \ 'a set" where "cball x e = {y. dist x y \ e}" definition\<^marker>\tag important\ sphere :: "'a::metric_space \ real \ 'a set" where "sphere x e = {y. dist x y = e}" lemma mem_ball [simp, metric_unfold]: "y \ ball x e \ dist x y < e" by (simp add: ball_def) lemma mem_cball [simp, metric_unfold]: "y \ cball x e \ dist x y \ e" by (simp add: cball_def) lemma mem_sphere [simp]: "y \ sphere x e \ dist x y = e" by (simp add: sphere_def) lemma ball_trivial [simp]: "ball x 0 = {}" by auto lemma cball_trivial [simp]: "cball x 0 = {x}" by auto lemma sphere_trivial [simp]: "sphere x 0 = {x}" by auto lemma disjoint_ballI: "dist x y \ r+s \ ball x r \ ball y s = {}" using dist_triangle_less_add not_le by fastforce lemma disjoint_cballI: "dist x y > r + s \ cball x r \ cball y s = {}" by (metis add_mono disjoint_iff_not_equal dist_triangle2 dual_order.trans leD mem_cball) lemma sphere_empty [simp]: "r < 0 \ sphere a r = {}" for a :: "'a::metric_space" by auto lemma centre_in_ball [simp]: "x \ ball x e \ 0 < e" by simp lemma centre_in_cball [simp]: "x \ cball x e \ 0 \ e" by simp lemma ball_subset_cball [simp, intro]: "ball x e \ cball x e" by (simp add: subset_eq) lemma mem_ball_imp_mem_cball: "x \ ball y e \ x \ cball y e" by auto lemma sphere_cball [simp,intro]: "sphere z r \ cball z r" by force lemma cball_diff_sphere: "cball a r - sphere a r = ball a r" by auto lemma subset_ball[intro]: "d \ e \ ball x d \ ball x e" by auto lemma subset_cball[intro]: "d \ e \ cball x d \ cball x e" by auto lemma mem_ball_leI: "x \ ball y e \ e \ f \ x \ ball y f" by auto lemma mem_cball_leI: "x \ cball y e \ e \ f \ x \ cball y f" by auto lemma cball_trans: "y \ cball z b \ x \ cball y a \ x \ cball z (b + a)" by metric lemma ball_max_Un: "ball a (max r s) = ball a r \ ball a s" by auto lemma ball_min_Int: "ball a (min r s) = ball a r \ ball a s" by auto lemma cball_max_Un: "cball a (max r s) = cball a r \ cball a s" by auto lemma cball_min_Int: "cball a (min r s) = cball a r \ cball a s" by auto lemma cball_diff_eq_sphere: "cball a r - ball a r = sphere a r" by auto lemma open_ball [intro, simp]: "open (ball x e)" proof - have "open (dist x -` {.. (\x\S. \e>0. ball x e \ S)" by (simp add: open_dist subset_eq Ball_def dist_commute) lemma openI [intro?]: "(\x. x\S \ \e>0. ball x e \ S) \ open S" by (auto simp: open_contains_ball) lemma openE[elim?]: assumes "open S" "x\S" obtains e where "e>0" "ball x e \ S" using assms unfolding open_contains_ball by auto lemma open_contains_ball_eq: "open S \ x\S \ (\e>0. ball x e \ S)" by (metis open_contains_ball subset_eq centre_in_ball) lemma ball_eq_empty[simp]: "ball x e = {} \ e \ 0" unfolding mem_ball set_eq_iff by (simp add: not_less) metric lemma ball_empty: "e \ 0 \ ball x e = {}" by simp lemma closed_cball [iff]: "closed (cball x e)" proof - have "closed (dist x -` {..e})" by (intro closed_vimage closed_atMost continuous_intros) also have "dist x -` {..e} = cball x e" by auto finally show ?thesis . qed lemma open_contains_cball: "open S \ (\x\S. \e>0. cball x e \ S)" proof - { fix x and e::real assume "x\S" "e>0" "ball x e \ S" then have "\d>0. cball x d \ S" unfolding subset_eq by (rule_tac x="e/2" in exI, auto) } moreover { fix x and e::real assume "x\S" "e>0" "cball x e \ S" then have "\d>0. ball x d \ S" using mem_ball_imp_mem_cball by blast } ultimately show ?thesis unfolding open_contains_ball by auto qed lemma open_contains_cball_eq: "open S \ (\x. x \ S \ (\e>0. cball x e \ S))" by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball) lemma eventually_nhds_ball: "d > 0 \ eventually (\x. x \ ball z d) (nhds z)" by (rule eventually_nhds_in_open) simp_all lemma eventually_at_ball: "d > 0 \ eventually (\t. t \ ball z d \ t \ A) (at z within A)" unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute) lemma eventually_at_ball': "d > 0 \ eventually (\t. t \ ball z d \ t \ z \ t \ A) (at z within A)" unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute) lemma at_within_ball: "e > 0 \ dist x y < e \ at y within ball x e = at y" by (subst at_within_open) auto lemma atLeastAtMost_eq_cball: fixes a b::real shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)" by (auto simp: dist_real_def field_simps) lemma cball_eq_atLeastAtMost: fixes a b::real shows "cball a b = {a - b .. a + b}" by (auto simp: dist_real_def) lemma greaterThanLessThan_eq_ball: fixes a b::real shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)" by (auto simp: dist_real_def field_simps) lemma ball_eq_greaterThanLessThan: fixes a b::real shows "ball a b = {a - b <..< a + b}" by (auto simp: dist_real_def) lemma interior_ball [simp]: "interior (ball x e) = ball x e" by (simp add: interior_open) lemma cball_eq_empty [simp]: "cball x e = {} \ e < 0" by (smt (verit, best) Diff_empty ball_eq_empty cball_diff_sphere centre_in_ball centre_in_cball sphere_empty) lemma cball_empty [simp]: "e < 0 \ cball x e = {}" by simp lemma cball_sing: fixes x :: "'a::metric_space" shows "e = 0 \ cball x e = {x}" by simp lemma ball_divide_subset: "d \ 1 \ ball x (e/d) \ ball x e" by (metis ball_eq_empty div_by_1 frac_le linear subset_ball zero_less_one) lemma ball_divide_subset_numeral: "ball x (e / numeral w) \ ball x e" using ball_divide_subset one_le_numeral by blast lemma cball_divide_subset: "d \ 1 \ cball x (e/d) \ cball x e" by (smt (verit, best) cball_empty div_by_1 frac_le subset_cball zero_le_divide_iff) lemma cball_divide_subset_numeral: "cball x (e / numeral w) \ cball x e" using cball_divide_subset one_le_numeral by blast lemma cball_scale: assumes "a \ 0" shows "(\x. a *\<^sub>R x) ` cball c r = cball (a *\<^sub>R c :: 'a :: real_normed_vector) (\a\ * r)" proof - have 1: "(\x. a *\<^sub>R x) ` cball c r \ cball (a *\<^sub>R c) (\a\ * r)" if "a \ 0" for a r and c :: 'a proof safe fix x assume x: "x \ cball c r" have "dist (a *\<^sub>R c) (a *\<^sub>R x) = norm (a *\<^sub>R c - a *\<^sub>R x)" by (auto simp: dist_norm) also have "a *\<^sub>R c - a *\<^sub>R x = a *\<^sub>R (c - x)" by (simp add: algebra_simps) finally show "a *\<^sub>R x \ cball (a *\<^sub>R c) (\a\ * r)" using that x by (auto simp: dist_norm) qed have "cball (a *\<^sub>R c) (\a\ * r) = (\x. a *\<^sub>R x) ` (\x. inverse a *\<^sub>R x) ` cball (a *\<^sub>R c) (\a\ * r)" unfolding image_image using assms by simp also have "\ \ (\x. a *\<^sub>R x) ` cball (inverse a *\<^sub>R (a *\<^sub>R c)) (\inverse a\ * (\a\ * r))" using assms by (intro image_mono 1) auto also have "\ = (\x. a *\<^sub>R x) ` cball c r" using assms by (simp add: algebra_simps) finally have "cball (a *\<^sub>R c) (\a\ * r) \ (\x. a *\<^sub>R x) ` cball c r" . moreover from assms have "(\x. a *\<^sub>R x) ` cball c r \ cball (a *\<^sub>R c) (\a\ * r)" by (intro 1) auto ultimately show ?thesis by blast qed lemma ball_scale: assumes "a \ 0" shows "(\x. a *\<^sub>R x) ` ball c r = ball (a *\<^sub>R c :: 'a :: real_normed_vector) (\a\ * r)" proof - have 1: "(\x. a *\<^sub>R x) ` ball c r \ ball (a *\<^sub>R c) (\a\ * r)" if "a \ 0" for a r and c :: 'a proof safe fix x assume x: "x \ ball c r" have "dist (a *\<^sub>R c) (a *\<^sub>R x) = norm (a *\<^sub>R c - a *\<^sub>R x)" by (auto simp: dist_norm) also have "a *\<^sub>R c - a *\<^sub>R x = a *\<^sub>R (c - x)" by (simp add: algebra_simps) finally show "a *\<^sub>R x \ ball (a *\<^sub>R c) (\a\ * r)" using that x by (auto simp: dist_norm) qed have "ball (a *\<^sub>R c) (\a\ * r) = (\x. a *\<^sub>R x) ` (\x. inverse a *\<^sub>R x) ` ball (a *\<^sub>R c) (\a\ * r)" unfolding image_image using assms by simp also have "\ \ (\x. a *\<^sub>R x) ` ball (inverse a *\<^sub>R (a *\<^sub>R c)) (\inverse a\ * (\a\ * r))" using assms by (intro image_mono 1) auto also have "\ = (\x. a *\<^sub>R x) ` ball c r" using assms by (simp add: algebra_simps) finally have "ball (a *\<^sub>R c) (\a\ * r) \ (\x. a *\<^sub>R x) ` ball c r" . moreover from assms have "(\x. a *\<^sub>R x) ` ball c r \ ball (a *\<^sub>R c) (\a\ * r)" by (intro 1) auto ultimately show ?thesis by blast qed lemma frequently_atE: fixes x :: "'a :: metric_space" assumes "frequently P (at x within s)" shows "\f. filterlim f (at x within s) sequentially \ (\n. P (f n))" proof - have "\y. y \ s \ (ball x (1 / real (Suc n)) - {x}) \ P y" for n proof - have "\z\s. z \ x \ dist z x < (1 / real (Suc n)) \ P z" by (metis assms divide_pos_pos frequently_at of_nat_0_less_iff zero_less_Suc zero_less_one) then show ?thesis by (auto simp: dist_commute conj_commute) qed then obtain f where f: "\n. f n \ s \ (ball x (1 / real (Suc n)) - {x}) \ P (f n)" by metis have "filterlim f (nhds x) sequentially" unfolding tendsto_iff proof clarify fix e :: real assume e: "e > 0" then obtain n where n: "Suc n > 1 / e" by (meson le_nat_floor lessI not_le) have "dist (f k) x < e" if "k \ n" for k proof - have "dist (f k) x < 1 / real (Suc k)" using f[of k] by (auto simp: dist_commute) also have "\ \ 1 / real (Suc n)" using that by (intro divide_left_mono) auto also have "\ < e" using n e by (simp add: field_simps) finally show ?thesis . qed thus "\\<^sub>F k in sequentially. dist (f k) x < e" unfolding eventually_at_top_linorder by blast qed moreover have "f n \ x" for n using f[of n] by auto ultimately have "filterlim f (at x within s) sequentially" using f by (auto simp: filterlim_at) with f show ?thesis by blast qed section \Limit Points\ lemma islimpt_approachable: fixes x :: "'a::metric_space" shows "x islimpt S \ (\e>0. \x'\S. x' \ x \ dist x' x < e)" unfolding islimpt_iff_eventually eventually_at by fast lemma islimpt_approachable_le: "x islimpt S \ (\e>0. \x'\ S. x' \ x \ dist x' x \ e)" for x :: "'a::metric_space" unfolding islimpt_approachable using approachable_lt_le2 [where f="\y. dist y x" and P="\y. y \ S \ y = x" and Q="\x. True"] by auto lemma limpt_of_limpts: "x islimpt {y. y islimpt S} \ x islimpt S" for x :: "'a::metric_space" by (metis islimpt_def islimpt_eq_acc_point mem_Collect_eq) lemma closed_limpts: "closed {x::'a::metric_space. x islimpt S}" using closed_limpt limpt_of_limpts by blast lemma limpt_of_closure: "x islimpt closure S \ x islimpt S" for x :: "'a::metric_space" by (auto simp: closure_def islimpt_Un dest: limpt_of_limpts) lemma islimpt_eq_infinite_ball: "x islimpt S \ (\e>0. infinite(S \ ball x e))" unfolding islimpt_eq_acc_point by (metis open_ball Int_commute Int_mono finite_subset open_contains_ball_eq subset_eq) lemma islimpt_eq_infinite_cball: "x islimpt S \ (\e>0. infinite(S \ cball x e))" unfolding islimpt_eq_infinite_ball by (metis open_ball ball_subset_cball centre_in_ball finite_Int inf.absorb_iff2 inf_assoc open_contains_cball_eq) section \Perfect Metric Spaces\ lemma perfect_choose_dist: "0 < r \ \a. a \ x \ dist a x < r" for x :: "'a::{perfect_space,metric_space}" using islimpt_UNIV [of x] by (simp add: islimpt_approachable) lemma cball_eq_sing: fixes x :: "'a::{metric_space,perfect_space}" shows "cball x e = {x} \ e = 0" by (smt (verit, best) open_ball ball_eq_empty ball_subset_cball cball_empty cball_trivial not_open_singleton subset_singleton_iff) section \Finite and discrete\ lemma finite_ball_include: fixes a :: "'a::metric_space" assumes "finite S" shows "\e>0. S \ ball a e" using assms proof induction case (insert x S) then obtain e0 where "e0>0" and e0:"S \ ball a e0" by auto define e where "e = max e0 (2 * dist a x)" have "e>0" unfolding e_def using \e0>0\ by auto moreover have "insert x S \ ball a e" using e0 \e>0\ unfolding e_def by auto ultimately show ?case by auto qed (auto intro: zero_less_one) lemma finite_set_avoid: fixes a :: "'a::metric_space" assumes "finite S" shows "\d>0. \x\S. x \ a \ d \ dist a x" using assms proof induction case (insert x S) then obtain d where "d > 0" and d: "\x\S. x \ a \ d \ dist a x" by blast show ?case by (smt (verit, del_insts) dist_pos_lt insert.IH insert_iff) qed (auto intro: zero_less_one) lemma discrete_imp_closed: fixes S :: "'a::metric_space set" assumes e: "0 < e" and d: "\x \ S. \y \ S. dist y x < e \ y = x" shows "closed S" proof - have False if C: "\e. e>0 \ \x'\S. x' \ x \ dist x' x < e" for x proof - from e have e2: "e/2 > 0" by arith from C[OF e2] obtain y where y: "y \ S" "y \ x" "dist y x < e/2" by blast from e2 y(2) have mp: "min (e/2) (dist x y) > 0" by simp from d y C[OF mp] show ?thesis by metric qed then show ?thesis by (metis islimpt_approachable closed_limpt [where 'a='a]) qed lemma discrete_imp_not_islimpt: assumes e: "0 < e" and d: "\x y. x \ S \ y \ S \ dist y x < e \ y = x" shows "\ x islimpt S" proof assume "x islimpt S" hence "x islimpt S - {x}" by (meson islimpt_punctured) moreover from assms have "closed (S - {x})" by (intro discrete_imp_closed) auto ultimately show False unfolding closed_limpt by blast qed section \Interior\ lemma mem_interior: "x \ interior S \ (\e>0. ball x e \ S)" using open_contains_ball_eq [where S="interior S"] by (simp add: open_subset_interior) lemma mem_interior_cball: "x \ interior S \ (\e>0. cball x e \ S)" by (meson ball_subset_cball interior_subset mem_interior open_contains_cball open_interior subset_trans) lemma ball_iff_cball: "(\r>0. ball x r \ U) \ (\r>0. cball x r \ U)" by (meson mem_interior mem_interior_cball) section \Frontier\ lemma frontier_straddle: fixes a :: "'a::metric_space" shows "a \ frontier S \ (\e>0. (\x\S. dist a x < e) \ (\x. x \ S \ dist a x < e))" unfolding frontier_def closure_interior by (auto simp: mem_interior subset_eq ball_def) section \Limits\ proposition Lim: "(f \ l) net \ trivial_limit net \ (\e>0. eventually (\x. dist (f x) l < e) net)" by (auto simp: tendsto_iff trivial_limit_eq) text \Show that they yield usual definitions in the various cases.\ proposition Lim_within_le: "(f \ l)(at a within S) \ (\e>0. \d>0. \x\S. 0 < dist x a \ dist x a \ d \ dist (f x) l < e)" by (auto simp: tendsto_iff eventually_at_le) proposition Lim_within: "(f \ l) (at a within S) \ (\e >0. \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" by (auto simp: tendsto_iff eventually_at) corollary Lim_withinI [intro?]: assumes "\e. e > 0 \ \d>0. \x \ S. 0 < dist x a \ dist x a < d \ dist (f x) l \ e" shows "(f \ l) (at a within S)" unfolding Lim_within by (smt (verit, ccfv_SIG) assms zero_less_dist_iff) proposition Lim_at: "(f \ l) (at a) \ (\e >0. \d>0. \x. 0 < dist x a \ dist x a < d \ dist (f x) l < e)" by (auto simp: tendsto_iff eventually_at) lemma Lim_transform_within_set: fixes a :: "'a::metric_space" and l :: "'b::metric_space" shows "\(f \ l) (at a within S); eventually (\x. x \ S \ x \ T) (at a)\ \ (f \ l) (at a within T)" by (simp add: eventually_at Lim_within) (smt (verit, best)) text \Another limit point characterization.\ lemma limpt_sequential_inj: fixes x :: "'a::metric_space" shows "x islimpt S \ (\f. (\n::nat. f n \ S - {x}) \ inj f \ (f \ x) sequentially)" (is "?lhs = ?rhs") proof assume ?lhs then have "\e>0. \x'\S. x' \ x \ dist x' x < e" by (force simp: islimpt_approachable) then obtain y where y: "\e. e>0 \ y e \ S \ y e \ x \ dist (y e) x < e" by metis define f where "f \ rec_nat (y 1) (\n fn. y (min (inverse(2 ^ (Suc n))) (dist fn x)))" have [simp]: "f 0 = y 1" and fSuc: "f(Suc n) = y (min (inverse(2 ^ (Suc n))) (dist (f n) x))" for n by (simp_all add: f_def) have f: "f n \ S \ (f n \ x) \ dist (f n) x < inverse(2 ^ n)" for n proof (induction n) case 0 show ?case by (simp add: y) next case (Suc n) then show ?case by (smt (verit, best) fSuc dist_pos_lt inverse_positive_iff_positive y zero_less_power) qed show ?rhs proof (intro exI conjI allI) show "\n. f n \ S - {x}" using f by blast have "dist (f n) x < dist (f m) x" if "m < n" for m n using that proof (induction n) case 0 then show ?case by simp next case (Suc n) then consider "m < n" | "m = n" using less_Suc_eq by blast then show ?case proof cases assume "m < n" have "dist (f(Suc n)) x = dist (y (min (inverse(2 ^ (Suc n))) (dist (f n) x))) x" by (simp add: fSuc) also have "\ < dist (f n) x" by (metis dist_pos_lt f min.strict_order_iff min_less_iff_conj y) also have "\ < dist (f m) x" using Suc.IH \m < n\ by blast finally show ?thesis . next assume "m = n" then show ?case by (smt (verit, best) dist_pos_lt f fSuc y) qed qed then show "inj f" by (metis less_irrefl linorder_injI) have "\e n. \0 < e; nat \1 / e\ \ n\ \ dist (f n) x < e" apply (rule less_trans [OF f [THEN conjunct2, THEN conjunct2]]) by (simp add: divide_simps order_le_less_trans) then show "f \ x" using lim_sequentially by blast qed next assume ?rhs then show ?lhs by (fastforce simp add: islimpt_approachable lim_sequentially) qed lemma Lim_dist_ubound: assumes "\(trivial_limit net)" and "(f \ l) net" and "eventually (\x. dist a (f x) \ e) net" shows "dist a l \ e" using assms by (fast intro: tendsto_le tendsto_intros) section \Continuity\ text\Derive the epsilon-delta forms, which we often use as "definitions"\ proposition continuous_within_eps_delta: "continuous (at x within s) f \ (\e>0. \d>0. \x'\ s. dist x' x < d --> dist (f x') (f x) < e)" unfolding continuous_within and Lim_within by fastforce corollary continuous_at_eps_delta: "continuous (at x) f \ (\e > 0. \d > 0. \x'. dist x' x < d \ dist (f x') (f x) < e)" using continuous_within_eps_delta [of x UNIV f] by simp lemma continuous_at_right_real_increasing: fixes f :: "real \ real" assumes nondecF: "\x y. x \ y \ f x \ f y" shows "continuous (at_right a) f \ (\e>0. \d>0. f (a + d) - f a < e)" apply (simp add: greaterThan_def dist_real_def continuous_within Lim_within_le) apply (intro all_cong ex_cong) by (smt (verit, best) nondecF) lemma continuous_at_left_real_increasing: assumes nondecF: "\ x y. x \ y \ f x \ ((f y) :: real)" shows "(continuous (at_left (a :: real)) f) \ (\e > 0. \delta > 0. f a - f (a - delta) < e)" apply (simp add: lessThan_def dist_real_def continuous_within Lim_within_le) apply (intro all_cong ex_cong) by (smt (verit) nondecF) text\Versions in terms of open balls.\ lemma continuous_within_ball: "continuous (at x within S) f \ (\e > 0. \d > 0. f ` (ball x d \ S) \ ball (f x) e)" (is "?lhs = ?rhs") proof assume ?lhs { fix e :: real assume "e > 0" then obtain d where "d>0" and d: "\y\S. 0 < dist y x \ dist y x < d \ dist (f y) (f x) < e" using \?lhs\[unfolded continuous_within Lim_within] by auto { fix y assume "y \ f ` (ball x d \ S)" then have "y \ ball (f x) e" using d \e > 0\ by (auto simp: dist_commute) } then have "\d>0. f ` (ball x d \ S) \ ball (f x) e" using \d > 0\ by blast } then show ?rhs by auto next assume ?rhs then show ?lhs apply (simp add: continuous_within Lim_within ball_def subset_eq) by (metis (mono_tags, lifting) Int_iff dist_commute mem_Collect_eq) qed lemma continuous_at_ball: "continuous (at x) f \ (\e>0. \d>0. f ` (ball x d) \ ball (f x) e)" apply (simp add: continuous_at Lim_at subset_eq Ball_def Bex_def image_iff) by (smt (verit, ccfv_threshold) dist_commute dist_self) text\Define setwise continuity in terms of limits within the set.\ lemma continuous_on_iff: "continuous_on s f \ (\x\s. \e>0. \d>0. \x'\s. dist x' x < d \ dist (f x') (f x) < e)" unfolding continuous_on_def Lim_within by (metis dist_pos_lt dist_self) lemma continuous_within_E: assumes "continuous (at x within S) f" "e>0" obtains d where "d>0" "\x'. \x'\ S; dist x' x \ d\ \ dist (f x') (f x) < e" using assms unfolding continuous_within_eps_delta by (metis dense order_le_less_trans) lemma continuous_onI [intro?]: assumes "\x e. \e > 0; x \ S\ \ \d>0. \x'\S. dist x' x < d \ dist (f x') (f x) \ e" shows "continuous_on S f" apply (simp add: continuous_on_iff, clarify) apply (rule ex_forward [OF assms [OF half_gt_zero]], auto) done text\Some simple consequential lemmas.\ lemma continuous_onE: assumes "continuous_on s f" "x\s" "e>0" obtains d where "d>0" "\x'. \x' \ s; dist x' x \ d\ \ dist (f x') (f x) < e" using assms unfolding continuous_on_iff by (metis dense order_le_less_trans) text\The usual transformation theorems.\ lemma continuous_transform_within: fixes f g :: "'a::metric_space \ 'b::topological_space" assumes "continuous (at x within s) f" and "0 < d" and "x \ s" and "\x'. \x' \ s; dist x' x < d\ \ f x' = g x'" shows "continuous (at x within s) g" using assms unfolding continuous_within by (force intro: Lim_transform_within) section \Closure and Limit Characterization\ lemma closure_approachable: fixes S :: "'a::metric_space set" shows "x \ closure S \ (\e>0. \y\S. dist y x < e)" using dist_self by (force simp: closure_def islimpt_approachable) lemma closure_approachable_le: fixes S :: "'a::metric_space set" shows "x \ closure S \ (\e>0. \y\S. dist y x \ e)" unfolding closure_approachable using dense by force lemma closure_approachableD: assumes "x \ closure S" "e>0" shows "\y\S. dist x y < e" using assms unfolding closure_approachable by (auto simp: dist_commute) lemma closed_approachable: fixes S :: "'a::metric_space set" shows "closed S \ (\e>0. \y\S. dist y x < e) \ x \ S" by (metis closure_closed closure_approachable) lemma closure_contains_Inf: fixes S :: "real set" assumes "S \ {}" "bdd_below S" shows "Inf S \ closure S" proof - have *: "\x\S. Inf S \ x" using cInf_lower[of _ S] assms by metis { fix e :: real assume "e > 0" then have "Inf S < Inf S + e" by simp with assms obtain x where "x \ S" "x < Inf S + e" using cInf_lessD by blast with * have "\x\S. dist x (Inf S) < e" using dist_real_def by force } then show ?thesis unfolding closure_approachable by auto qed lemma closure_contains_Sup: fixes S :: "real set" assumes "S \ {}" "bdd_above S" shows "Sup S \ closure S" proof - have *: "\x\S. x \ Sup S" using cSup_upper[of _ S] assms by metis { fix e :: real assume "e > 0" then have "Sup S - e < Sup S" by simp with assms obtain x where "x \ S" "Sup S - e < x" using less_cSupE by blast with * have "\x\S. dist x (Sup S) < e" using dist_real_def by force } then show ?thesis unfolding closure_approachable by auto qed lemma not_trivial_limit_within_ball: "\ trivial_limit (at x within S) \ (\e>0. S \ ball x e - {x} \ {})" (is "?lhs \ ?rhs") proof show ?rhs if ?lhs proof - { fix e :: real assume "e > 0" then obtain y where "y \ S - {x}" and "dist y x < e" using \?lhs\ not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] by auto then have "y \ S \ ball x e - {x}" unfolding ball_def by (simp add: dist_commute) then have "S \ ball x e - {x} \ {}" by blast } then show ?thesis by auto qed show ?lhs if ?rhs proof - { fix e :: real assume "e > 0" then obtain y where "y \ S \ ball x e - {x}" using \?rhs\ by blast then have "y \ S - {x}" and "dist y x < e" unfolding ball_def by (simp_all add: dist_commute) then have "\y \ S - {x}. dist y x < e" by auto } then show ?thesis using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] by auto qed qed section \Boundedness\ (* FIXME: This has to be unified with BSEQ!! *) definition\<^marker>\tag important\ (in metric_space) bounded :: "'a set \ bool" where "bounded S \ (\x e. \y\S. dist x y \ e)" lemma bounded_subset_cball: "bounded S \ (\e x. S \ cball x e \ 0 \ e)" unfolding bounded_def subset_eq by auto (meson order_trans zero_le_dist) lemma bounded_any_center: "bounded S \ (\e. \y\S. dist a y \ e)" unfolding bounded_def by auto (metis add.commute add_le_cancel_right dist_commute dist_triangle_le) lemma bounded_iff: "bounded S \ (\a. \x\S. norm x \ a)" unfolding bounded_any_center [where a=0] by (simp add: dist_norm) lemma bdd_above_norm: "bdd_above (norm ` X) \ bounded X" by (simp add: bounded_iff bdd_above_def) lemma bounded_norm_comp: "bounded ((\x. norm (f x)) ` S) = bounded (f ` S)" by (simp add: bounded_iff) lemma boundedI: assumes "\x. x \ S \ norm x \ B" shows "bounded S" using assms bounded_iff by blast lemma bounded_empty [simp]: "bounded {}" by (simp add: bounded_def) lemma bounded_subset: "bounded T \ S \ T \ bounded S" by (metis bounded_def subset_eq) lemma bounded_interior[intro]: "bounded S \ bounded(interior S)" by (metis bounded_subset interior_subset) lemma bounded_closure[intro]: assumes "bounded S" shows "bounded (closure S)" proof - from assms obtain x and a where a: "\y\S. dist x y \ a" unfolding bounded_def by auto { fix y assume "y \ closure S" then obtain f where f: "\n. f n \ S" "(f \ y) sequentially" unfolding closure_sequential by auto have "\n. f n \ S \ dist x (f n) \ a" using a by simp then have "eventually (\n. dist x (f n) \ a) sequentially" by (simp add: f(1)) then have "dist x y \ a" using Lim_dist_ubound f(2) trivial_limit_sequentially by blast } then show ?thesis unfolding bounded_def by auto qed lemma bounded_closure_image: "bounded (f ` closure S) \ bounded (f ` S)" by (simp add: bounded_subset closure_subset image_mono) lemma bounded_cball[simp,intro]: "bounded (cball x e)" unfolding bounded_def using mem_cball by blast lemma bounded_ball[simp,intro]: "bounded (ball x e)" by (metis ball_subset_cball bounded_cball bounded_subset) lemma bounded_Un[simp]: "bounded (S \ T) \ bounded S \ bounded T" by (auto simp: bounded_def) (metis Un_iff bounded_any_center le_max_iff_disj) lemma bounded_Union[intro]: "finite F \ \S\F. bounded S \ bounded (\F)" by (induct rule: finite_induct[of F]) auto lemma bounded_UN [intro]: "finite A \ \x\A. bounded (B x) \ bounded (\x\A. B x)" by auto lemma bounded_insert [simp]: "bounded (insert x S) \ bounded S" proof - have "\y\{x}. dist x y \ 0" by simp then have "bounded {x}" unfolding bounded_def by fast then show ?thesis by (metis insert_is_Un bounded_Un) qed lemma bounded_subset_ballI: "S \ ball x r \ bounded S" by (meson bounded_ball bounded_subset) lemma bounded_subset_ballD: assumes "bounded S" shows "\r. 0 < r \ S \ ball x r" proof - obtain e::real and y where "S \ cball y e" "0 \ e" using assms by (auto simp: bounded_subset_cball) then show ?thesis by (intro exI[where x="dist x y + e + 1"]) metric qed lemma finite_imp_bounded [intro]: "finite S \ bounded S" by (induct set: finite) simp_all lemma bounded_Int[intro]: "bounded S \ bounded T \ bounded (S \ T)" by (metis Int_lower1 Int_lower2 bounded_subset) lemma bounded_diff[intro]: "bounded S \ bounded (S - T)" by (metis Diff_subset bounded_subset) lemma bounded_dist_comp: assumes "bounded (f ` S)" "bounded (g ` S)" shows "bounded ((\x. dist (f x) (g x)) ` S)" proof - from assms obtain M1 M2 where *: "dist (f x) undefined \ M1" "dist undefined (g x) \ M2" if "x \ S" for x by (auto simp: bounded_any_center[of _ undefined] dist_commute) have "dist (f x) (g x) \ M1 + M2" if "x \ S" for x using *[OF that] by metric then show ?thesis by (auto intro!: boundedI) qed lemma bounded_Times: assumes "bounded s" "bounded t" shows "bounded (s \ t)" proof - obtain x y a b where "\z\s. dist x z \ a" "\z\t. dist y z \ b" using assms [unfolded bounded_def] by auto then have "\z\s \ t. dist (x, y) z \ sqrt (a\<^sup>2 + b\<^sup>2)" by (auto simp: dist_Pair_Pair real_sqrt_le_mono add_mono power_mono) then show ?thesis unfolding bounded_any_center [where a="(x, y)"] by auto qed section \Compactness\ lemma compact_imp_bounded: assumes "compact U" shows "bounded U" proof - have "compact U" "\x\U. open (ball x 1)" "U \ (\x\U. ball x 1)" using assms by auto then obtain D where D: "D \ U" "finite D" "U \ (\x\D. ball x 1)" by (metis compactE_image) from \finite D\ have "bounded (\x\D. ball x 1)" by (simp add: bounded_UN) then show "bounded U" using \U \ (\x\D. ball x 1)\ by (rule bounded_subset) qed lemma continuous_on_compact_bound: assumes "compact A" "continuous_on A f" obtains B where "B \ 0" "\x. x \ A \ norm (f x) \ B" proof - have "compact (f ` A)" by (metis assms compact_continuous_image) then obtain B where "\x\A. norm (f x) \ B" by (auto dest!: compact_imp_bounded simp: bounded_iff) hence "max B 0 \ 0" and "\x\A. norm (f x) \ max B 0" by auto thus ?thesis using that by blast qed lemma closure_Int_ball_not_empty: assumes "S \ closure T" "x \ S" "r > 0" shows "T \ ball x r \ {}" using assms centre_in_ball closure_iff_nhds_not_empty by blast lemma compact_sup_maxdistance: fixes S :: "'a::metric_space set" assumes "compact S" and "S \ {}" shows "\x\S. \y\S. \u\S. \v\S. dist u v \ dist x y" proof - have "compact (S \ S)" using \compact S\ by (intro compact_Times) moreover have "S \ S \ {}" using \S \ {}\ by auto moreover have "continuous_on (S \ S) (\x. dist (fst x) (snd x))" by (intro continuous_at_imp_continuous_on ballI continuous_intros) ultimately show ?thesis using continuous_attains_sup[of "S \ S" "\x. dist (fst x) (snd x)"] by auto qed text \ If \A\ is a compact subset of an open set \B\ in a metric space, then there exists an \\ > 0\ such that the Minkowski sum of \A\ with an open ball of radius \\\ is also a subset of \B\. \ lemma compact_subset_open_imp_ball_epsilon_subset: assumes "compact A" "open B" "A \ B" obtains e where "e > 0" "(\x\A. ball x e) \ B" proof - have "\x\A. \e. e > 0 \ ball x e \ B" using assms unfolding open_contains_ball by blast then obtain e where e: "\x. x \ A \ e x > 0" "\x. x \ A \ ball x (e x) \ B" by metis define C where "C = e ` A" obtain X where X: "X \ A" "finite X" "A \ (\c\X. ball c (e c / 2))" using assms(1) proof (rule compactE_image) show "open (ball x (e x / 2))" if "x \ A" for x by simp show "A \ (\c\A. ball c (e c / 2))" using e by auto qed auto define e' where "e' = Min (insert 1 ((\x. e x / 2) ` X))" have "e' > 0" unfolding e'_def using e X by (subst Min_gr_iff) auto have e': "e' \ e x / 2" if "x \ X" for x using that X unfolding e'_def by (intro Min.coboundedI) auto show ?thesis proof show "e' > 0" by fact next show "(\x\A. ball x e') \ B" proof clarify fix x y assume xy: "x \ A" "y \ ball x e'" from xy(1) X obtain z where z: "z \ X" "x \ ball z (e z / 2)" by auto have "dist y z \ dist x y + dist z x" by (metis dist_commute dist_triangle) also have "dist z x < e z / 2" using xy z by auto also have "dist x y < e'" using xy by auto also have "\ \ e z / 2" using z by (intro e') auto finally have "y \ ball z (e z)" by (simp add: dist_commute) also have "\ \ B" using z X by (intro e) auto finally show "y \ B" . qed qed qed lemma compact_subset_open_imp_cball_epsilon_subset: assumes "compact A" "open B" "A \ B" obtains e where "e > 0" "(\x\A. cball x e) \ B" proof - obtain e where "e > 0" and e: "(\x\A. ball x e) \ B" using compact_subset_open_imp_ball_epsilon_subset [OF assms] by blast then have "(\x\A. cball x (e / 2)) \ (\x\A. ball x e)" by auto with \0 < e\ that show ?thesis by (metis e half_gt_zero_iff order_trans) qed subsubsection\Totally bounded\ proposition seq_compact_imp_totally_bounded: assumes "seq_compact S" shows "\e>0. \k. finite k \ k \ S \ S \ (\x\k. ball x e)" proof - { fix e::real assume "e > 0" assume *: "\k. finite k \ k \ S \ \ S \ (\x\k. ball x e)" let ?Q = "\x n r. r \ S \ (\m < (n::nat). \ (dist (x m) r < e))" have "\x. \n::nat. ?Q x n (x n)" proof (rule dependent_wellorder_choice) fix n x assume "\y. y < n \ ?Q x y (x y)" then have "\ S \ (\x\x ` {0..S" "z \ (\x\x ` {0..r. ?Q x n r" using z by auto qed simp then obtain x where "\n::nat. x n \ S" and x:"\n m. m < n \ \ (dist (x m) (x n) < e)" by blast then obtain l r where "l \ S" and r:"strict_mono r" and "((x \ r) \ l) sequentially" using assms by (metis seq_compact_def) then have "Cauchy (x \ r)" using LIMSEQ_imp_Cauchy by auto then obtain N::nat where "\m n. N \ m \ N \ n \ dist ((x \ r) m) ((x \ r) n) < e" unfolding Cauchy_def using \e > 0\ by blast then have False using x[of "r N" "r (N+1)"] r by (auto simp: strict_mono_def) } then show ?thesis by metis qed subsubsection\Heine-Borel theorem\ proposition seq_compact_imp_Heine_Borel: fixes S :: "'a :: metric_space set" assumes "seq_compact S" shows "compact S" proof - from seq_compact_imp_totally_bounded[OF \seq_compact S\] obtain f where f: "\e>0. finite (f e) \ f e \ S \ S \ (\x\f e. ball x e)" unfolding choice_iff' .. define K where "K = (\(x, r). ball x r) ` ((\e \ \ \ {0 <..}. f e) \ \)" have "countably_compact S" using \seq_compact S\ by (rule seq_compact_imp_countably_compact) then show "compact S" proof (rule countably_compact_imp_compact) show "countable K" unfolding K_def using f by (auto intro: countable_finite countable_subset countable_rat intro!: countable_image countable_SIGMA countable_UN) show "\b\K. open b" by (auto simp: K_def) next fix T x assume T: "open T" "x \ T" and x: "x \ S" from openE[OF T] obtain e where "0 < e" "ball x e \ T" by auto then have "0 < e/2" "ball x (e/2) \ T" by auto from Rats_dense_in_real[OF \0 < e/2\] obtain r where "r \ \" "0 < r" "r < e/2" by auto from f[rule_format, of r] \0 < r\ \x \ S\ obtain k where "k \ f r" "x \ ball k r" by auto from \r \ \\ \0 < r\ \k \ f r\ have "ball k r \ K" by (auto simp: K_def) then show "\b\K. x \ b \ b \ S \ T" proof (rule bexI[rotated], safe) fix y assume "y \ ball k r" with \r < e/2\ \x \ ball k r\ have "dist x y < e" by (intro dist_triangle_half_r [of k _ e]) (auto simp: dist_commute) with \ball x e \ T\ show "y \ T" by auto next show "x \ ball k r" by fact qed qed qed proposition compact_eq_seq_compact_metric: "compact (S :: 'a::metric_space set) \ seq_compact S" using compact_imp_seq_compact seq_compact_imp_Heine_Borel by blast proposition compact_def: \ \this is the definition of compactness in HOL Light\ "compact (S :: 'a::metric_space set) \ (\f. (\n. f n \ S) \ (\l\S. \r::nat\nat. strict_mono r \ (f \ r) \ l))" unfolding compact_eq_seq_compact_metric seq_compact_def by auto subsubsection \Complete the chain of compactness variants\ proposition compact_eq_Bolzano_Weierstrass: fixes S :: "'a::metric_space set" shows "compact S \ (\T. infinite T \ T \ S \ (\x \ S. x islimpt T))" by (meson Bolzano_Weierstrass_imp_seq_compact Heine_Borel_imp_Bolzano_Weierstrass seq_compact_imp_Heine_Borel) proposition Bolzano_Weierstrass_imp_bounded: "(\T. \infinite T; T \ S\ \ (\x \ S. x islimpt T)) \ bounded S" using compact_imp_bounded unfolding compact_eq_Bolzano_Weierstrass by metis section \Banach fixed point theorem\ theorem banach_fix:\ \TODO: rename to \Banach_fix\\ assumes s: "complete s" "s \ {}" and c: "0 \ c" "c < 1" and f: "f ` s \ s" and lipschitz: "\x\s. \y\s. dist (f x) (f y) \ c * dist x y" shows "\!x\s. f x = x" proof - from c have "1 - c > 0" by simp from s(2) obtain z0 where z0: "z0 \ s" by blast define z where "z n = (f ^^ n) z0" for n with f z0 have z_in_s: "z n \ s" for n :: nat by (induct n) auto define d where "d = dist (z 0) (z 1)" have fzn: "f (z n) = z (Suc n)" for n by (simp add: z_def) have cf_z: "dist (z n) (z (Suc n)) \ (c ^ n) * d" for n :: nat proof (induct n) case 0 then show ?case by (simp add: d_def) next case (Suc m) with \0 \ c\ have "c * dist (z m) (z (Suc m)) \ c ^ Suc m * d" using mult_left_mono[of "dist (z m) (z (Suc m))" "c ^ m * d" c] by simp then show ?case using lipschitz[THEN bspec[where x="z m"], OF z_in_s, THEN bspec[where x="z (Suc m)"], OF z_in_s] by (simp add: fzn mult_le_cancel_left) qed have cf_z2: "(1 - c) * dist (z m) (z (m + n)) \ (c ^ m) * d * (1 - c ^ n)" for n m :: nat proof (induct n) case 0 show ?case by simp next case (Suc k) from c have "(1 - c) * dist (z m) (z (m + Suc k)) \ (1 - c) * (dist (z m) (z (m + k)) + dist (z (m + k)) (z (Suc (m + k))))" by (simp add: dist_triangle) also from c cf_z[of "m + k"] have "\ \ (1 - c) * (dist (z m) (z (m + k)) + c ^ (m + k) * d)" by simp also from Suc have "\ \ c ^ m * d * (1 - c ^ k) + (1 - c) * c ^ (m + k) * d" by (simp add: field_simps) also have "\ = (c ^ m) * (d * (1 - c ^ k) + (1 - c) * c ^ k * d)" by (simp add: power_add field_simps) also from c have "\ \ (c ^ m) * d * (1 - c ^ Suc k)" by (simp add: field_simps) finally show ?case by simp qed have "\N. \m n. N \ m \ N \ n \ dist (z m) (z n) < e" if "e > 0" for e proof (cases "d = 0") case True from \1 - c > 0\ have "(1 - c) * x \ 0 \ x \ 0" for x by (simp add: mult_le_0_iff) with c cf_z2[of 0] True have "z n = z0" for n by (simp add: z_def) with \e > 0\ show ?thesis by simp next case False with zero_le_dist[of "z 0" "z 1"] have "d > 0" by (metis d_def less_le) with \1 - c > 0\ \e > 0\ have "0 < e * (1 - c) / d" by simp with c obtain N where N: "c ^ N < e * (1 - c) / d" using real_arch_pow_inv[of "e * (1 - c) / d" c] by auto have *: "dist (z m) (z n) < e" if "m > n" and as: "m \ N" "n \ N" for m n :: nat proof - from c \n \ N\ have *: "c ^ n \ c ^ N" using power_decreasing[OF \n\N\, of c] by simp from c \m > n\ have "1 - c ^ (m - n) > 0" using power_strict_mono[of c 1 "m - n"] by simp with \d > 0\ \0 < 1 - c\ have **: "d * (1 - c ^ (m - n)) / (1 - c) > 0" by simp from cf_z2[of n "m - n"] \m > n\ have "dist (z m) (z n) \ c ^ n * d * (1 - c ^ (m - n)) / (1 - c)" by (simp add: pos_le_divide_eq[OF \1 - c > 0\] mult.commute dist_commute) also have "\ \ c ^ N * d * (1 - c ^ (m - n)) / (1 - c)" using mult_right_mono[OF * order_less_imp_le[OF **]] by (simp add: mult.assoc) also have "\ < (e * (1 - c) / d) * d * (1 - c ^ (m - n)) / (1 - c)" using mult_strict_right_mono[OF N **] by (auto simp: mult.assoc) also from c \d > 0\ \1 - c > 0\ have "\ = e * (1 - c ^ (m - n))" by simp also from c \1 - c ^ (m - n) > 0\ \e > 0\ have "\ \ e" using mult_right_le_one_le[of e "1 - c ^ (m - n)"] by auto finally show ?thesis by simp qed have "dist (z n) (z m) < e" if "N \ m" "N \ n" for m n :: nat proof (cases "n = m") case True with \e > 0\ show ?thesis by simp next case False with *[of n m] *[of m n] and that show ?thesis by (auto simp: dist_commute nat_neq_iff) qed then show ?thesis by auto qed then have "Cauchy z" by (metis metric_CauchyI) then obtain x where "x\s" and x:"(z \ x) sequentially" using s(1)[unfolded compact_def complete_def, THEN spec[where x=z]] and z_in_s by auto define e where "e = dist (f x) x" have "e = 0" proof (rule ccontr) assume "e \ 0" then have "e > 0" unfolding e_def using zero_le_dist[of "f x" x] by (metis dist_eq_0_iff dist_nz e_def) then obtain N where N:"\n\N. dist (z n) x < e/2" using x[unfolded lim_sequentially, THEN spec[where x="e/2"]] by auto then have N':"dist (z N) x < e/2" by auto have *: "c * dist (z N) x \ dist (z N) x" unfolding mult_le_cancel_right2 using zero_le_dist[of "z N" x] and c by (metis dist_eq_0_iff dist_nz order_less_asym less_le) have "dist (f (z N)) (f x) \ c * dist (z N) x" using lipschitz[THEN bspec[where x="z N"], THEN bspec[where x=x]] using z_in_s[of N] \x\s\ using c by auto also have "\ < e/2" using N' and c using * by auto finally show False unfolding fzn using N[THEN spec[where x="Suc N"]] and dist_triangle_half_r[of "z (Suc N)" "f x" e x] unfolding e_def by auto qed then have "f x = x" by (auto simp: e_def) moreover have "y = x" if "f y = y" "y \ s" for y proof - from \x \ s\ \f x = x\ that have "dist x y \ c * dist x y" using lipschitz[THEN bspec[where x=x], THEN bspec[where x=y]] by simp with c and zero_le_dist[of x y] have "dist x y = 0" by (simp add: mult_le_cancel_right1) then show ?thesis by simp qed ultimately show ?thesis using \x\s\ by blast qed section \Edelstein fixed point theorem\ theorem Edelstein_fix: fixes S :: "'a::metric_space set" assumes S: "compact S" "S \ {}" and gs: "(g ` S) \ S" and dist: "\x\S. \y\S. x \ y \ dist (g x) (g y) < dist x y" shows "\!x\S. g x = x" proof - let ?D = "(\x. (x, x)) ` S" have D: "compact ?D" "?D \ {}" by (rule compact_continuous_image) (auto intro!: S continuous_Pair continuous_ident simp: continuous_on_eq_continuous_within) have "\x y e. x \ S \ y \ S \ 0 < e \ dist y x < e \ dist (g y) (g x) < e" using dist by fastforce then have "continuous_on S g" by (auto simp: continuous_on_iff) then have cont: "continuous_on ?D (\x. dist ((g \ fst) x) (snd x))" unfolding continuous_on_eq_continuous_within by (intro continuous_dist ballI continuous_within_compose) (auto intro!: continuous_fst continuous_snd continuous_ident simp: image_image) obtain a where "a \ S" and le: "\x. x \ S \ dist (g a) a \ dist (g x) x" using continuous_attains_inf[OF D cont] by auto have "g a = a" proof (rule ccontr) assume "g a \ a" with \a \ S\ gs have "dist (g (g a)) (g a) < dist (g a) a" by (intro dist[rule_format]) auto moreover have "dist (g a) a \ dist (g (g a)) (g a)" using \a \ S\ gs by (intro le) auto ultimately show False by auto qed moreover have "\x. x \ S \ g x = x \ x = a" using dist[THEN bspec[where x=a]] \g a = a\ and \a\S\ by auto ultimately show "\!x\S. g x = x" using \a \ S\ by blast qed section \The diameter of a set\ definition\<^marker>\tag important\ diameter :: "'a::metric_space set \ real" where "diameter S = (if S = {} then 0 else SUP (x,y)\S\S. dist x y)" lemma diameter_empty [simp]: "diameter{} = 0" by (auto simp: diameter_def) lemma diameter_singleton [simp]: "diameter{x} = 0" by (auto simp: diameter_def) lemma diameter_le: assumes "S \ {} \ 0 \ d" and no: "\x y. \x \ S; y \ S\ \ norm(x - y) \ d" shows "diameter S \ d" using assms by (auto simp: dist_norm diameter_def intro: cSUP_least) lemma diameter_bounded_bound: fixes S :: "'a :: metric_space set" assumes S: "bounded S" "x \ S" "y \ S" shows "dist x y \ diameter S" proof - from S obtain z d where z: "\x. x \ S \ dist z x \ d" unfolding bounded_def by auto have "bdd_above (case_prod dist ` (S\S))" proof (intro bdd_aboveI, safe) fix a b assume "a \ S" "b \ S" with z[of a] z[of b] dist_triangle[of a b z] show "dist a b \ 2 * d" by (simp add: dist_commute) qed moreover have "(x,y) \ S\S" using S by auto ultimately have "dist x y \ (SUP (x,y)\S\S. dist x y)" by (rule cSUP_upper2) simp with \x \ S\ show ?thesis by (auto simp: diameter_def) qed lemma diameter_lower_bounded: fixes S :: "'a :: metric_space set" assumes S: "bounded S" and d: "0 < d" "d < diameter S" shows "\x\S. \y\S. d < dist x y" proof (rule ccontr) assume contr: "\ ?thesis" moreover have "S \ {}" using d by (auto simp: diameter_def) ultimately have "diameter S \ d" by (auto simp: not_less diameter_def intro!: cSUP_least) with \d < diameter S\ show False by auto qed lemma diameter_bounded: assumes "bounded S" shows "\x\S. \y\S. dist x y \ diameter S" and "\d>0. d < diameter S \ (\x\S. \y\S. dist x y > d)" using diameter_bounded_bound[of S] diameter_lower_bounded[of S] assms by auto lemma bounded_two_points: "bounded S \ (\e. \x\S. \y\S. dist x y \ e)" by (meson bounded_def diameter_bounded(1)) lemma diameter_compact_attained: assumes "compact S" and "S \ {}" shows "\x\S. \y\S. dist x y = diameter S" proof - have b: "bounded S" using assms(1) by (rule compact_imp_bounded) then obtain x y where xys: "x\S" "y\S" and xy: "\u\S. \v\S. dist u v \ dist x y" using compact_sup_maxdistance[OF assms] by auto then have "diameter S \ dist x y" unfolding diameter_def by (force intro!: cSUP_least) then show ?thesis by (metis b diameter_bounded_bound order_antisym xys) qed lemma diameter_ge_0: assumes "bounded S" shows "0 \ diameter S" by (metis all_not_in_conv assms diameter_bounded_bound diameter_empty dist_self order_refl) lemma diameter_subset: assumes "S \ T" "bounded T" shows "diameter S \ diameter T" proof (cases "S = {} \ T = {}") case True with assms show ?thesis by (force simp: diameter_ge_0) next case False then have "bdd_above ((\x. case x of (x, xa) \ dist x xa) ` (T \ T))" using \bounded T\ diameter_bounded_bound by (force simp: bdd_above_def) with False \S \ T\ show ?thesis apply (simp add: diameter_def) apply (rule cSUP_subset_mono, auto) done qed lemma diameter_closure: assumes "bounded S" shows "diameter(closure S) = diameter S" proof (rule order_antisym) have "False" if d_less_d: "diameter S < diameter (closure S)" proof - define d where "d = diameter(closure S) - diameter(S)" have "d > 0" using that by (simp add: d_def) then have dle: "diameter(closure(S)) - d / 2 < diameter(closure(S))" by simp have dd: "diameter (closure S) - d / 2 = (diameter(closure(S)) + diameter(S)) / 2" by (simp add: d_def field_split_simps) have bocl: "bounded (closure S)" using assms by blast moreover have "0 \ diameter S" using assms diameter_ge_0 by blast ultimately obtain x y where "x \ closure S" "y \ closure S" and xy: "diameter(closure(S)) - d / 2 < dist x y" by (smt (verit) dle d_less_d d_def dd diameter_lower_bounded) then obtain x' y' where x'y': "x' \ S" "dist x' x < d/4" "y' \ S" "dist y' y < d/4" by (metis \0 < d\ zero_less_divide_iff zero_less_numeral closure_approachable) then have "dist x' y' \ diameter S" using assms diameter_bounded_bound by blast with x'y' have "dist x y \ d / 4 + diameter S + d / 4" by (meson add_mono dist_triangle dist_triangle3 less_eq_real_def order_trans) then show ?thesis using xy d_def by linarith qed then show "diameter (closure S) \ diameter S" by fastforce next show "diameter S \ diameter (closure S)" by (simp add: assms bounded_closure closure_subset diameter_subset) qed proposition Lebesgue_number_lemma: assumes "compact S" "\ \ {}" "S \ \\" and ope: "\B. B \ \ \ open B" obtains \ where "0 < \" "\T. \T \ S; diameter T < \\ \ \B \ \. T \ B" proof (cases "S = {}") case True then show ?thesis by (metis \\ \ {}\ zero_less_one empty_subsetI equals0I subset_trans that) next case False { fix x assume "x \ S" then obtain C where C: "x \ C" "C \ \" using \S \ \\\ by blast then obtain r where r: "r>0" "ball x (2*r) \ C" by (metis mult.commute mult_2_right not_le ope openE field_sum_of_halves zero_le_numeral zero_less_mult_iff) then have "\r C. r > 0 \ ball x (2*r) \ C \ C \ \" using C by blast } then obtain r where r: "\x. x \ S \ r x > 0 \ (\C \ \. ball x (2*r x) \ C)" by metis then have "S \ (\x \ S. ball x (r x))" by auto then obtain \ where "finite \" "S \ \\" and \: "\ \ (\x. ball x (r x)) ` S" by (rule compactE [OF \compact S\]) auto then obtain S0 where "S0 \ S" "finite S0" and S0: "\ = (\x. ball x (r x)) ` S0" by (meson finite_subset_image) then have "S0 \ {}" using False \S \ \\\ by auto define \ where "\ = Inf (r ` S0)" have "\ > 0" using \finite S0\ \S0 \ S\ \S0 \ {}\ r by (auto simp: \_def finite_less_Inf_iff) show ?thesis proof show "0 < \" by (simp add: \0 < \\) show "\B \ \. T \ B" if "T \ S" and dia: "diameter T < \" for T proof (cases "T = {}") case True then show ?thesis using \\ \ {}\ by blast next case False then obtain y where "y \ T" by blast then have "y \ S" using \T \ S\ by auto then obtain x where "x \ S0" and x: "y \ ball x (r x)" using \S \ \\\ S0 that by blast have "ball y \ \ ball y (r x)" by (metis \_def \S0 \ {}\ \finite S0\ \x \ S0\ empty_is_image finite_imageI finite_less_Inf_iff imageI less_irrefl not_le subset_ball) also have "... \ ball x (2*r x)" using x by metric finally obtain C where "C \ \" "ball y \ \ C" by (meson r \S0 \ S\ \x \ S0\ dual_order.trans subsetCE) have "bounded T" using \compact S\ bounded_subset compact_imp_bounded \T \ S\ by blast then have "T \ ball y \" using \y \ T\ dia diameter_bounded_bound by fastforce then show ?thesis by (meson \C \ \\ \ball y \ \ C\ subset_eq) qed qed qed section \Metric spaces with the Heine-Borel property\ text \ A metric space (or topological vector space) is said to have the Heine-Borel property if every closed and bounded subset is compact. \ class heine_borel = metric_space + assumes bounded_imp_convergent_subsequence: "bounded (range f) \ \l r. strict_mono (r::nat\nat) \ ((f \ r) \ l) sequentially" proposition bounded_closed_imp_seq_compact: fixes S::"'a::heine_borel set" assumes "bounded S" and "closed S" shows "seq_compact S" proof (unfold seq_compact_def, clarify) fix f :: "nat \ 'a" assume f: "\n. f n \ S" with \bounded S\ have "bounded (range f)" by (auto intro: bounded_subset) obtain l r where r: "strict_mono (r :: nat \ nat)" and l: "((f \ r) \ l) sequentially" using bounded_imp_convergent_subsequence [OF \bounded (range f)\] by auto from f have fr: "\n. (f \ r) n \ S" by simp show "\l\S. \r. strict_mono r \ (f \ r) \ l" using assms(2) closed_sequentially fr l r by blast qed lemma compact_eq_bounded_closed: fixes S :: "'a::heine_borel set" shows "compact S \ bounded S \ closed S" using bounded_closed_imp_seq_compact compact_eq_seq_compact_metric compact_imp_bounded compact_imp_closed by auto lemma bounded_infinite_imp_islimpt: fixes S :: "'a::heine_borel set" assumes "T \ S" "bounded S" "infinite T" obtains x where "x islimpt S" by (meson assms closed_limpt compact_eq_Bolzano_Weierstrass compact_eq_bounded_closed islimpt_subset) lemma compact_Inter: fixes \ :: "'a :: heine_borel set set" assumes com: "\S. S \ \ \ compact S" and "\ \ {}" shows "compact(\ \)" using assms by (meson Inf_lower all_not_in_conv bounded_subset closed_Inter compact_eq_bounded_closed) lemma compact_closure [simp]: fixes S :: "'a::heine_borel set" shows "compact(closure S) \ bounded S" by (meson bounded_closure bounded_subset closed_closure closure_subset compact_eq_bounded_closed) instance\<^marker>\tag important\ real :: heine_borel proof fix f :: "nat \ real" assume f: "bounded (range f)" obtain r :: "nat \ nat" where r: "strict_mono r" "monoseq (f \ r)" unfolding comp_def by (metis seq_monosub) then have "Bseq (f \ r)" unfolding Bseq_eq_bounded by (metis f BseqI' bounded_iff comp_apply rangeI) with r show "\l r. strict_mono r \ (f \ r) \ l" using Bseq_monoseq_convergent[of "f \ r"] by (auto simp: convergent_def) qed lemma compact_lemma_general: fixes f :: "nat \ 'a" fixes proj::"'a \ 'b \ 'c::heine_borel" (infixl "proj" 60) fixes unproj:: "('b \ 'c) \ 'a" assumes finite_basis: "finite basis" assumes bounded_proj: "\k. k \ basis \ bounded ((\x. x proj k) ` range f)" assumes proj_unproj: "\e k. k \ basis \ (unproj e) proj k = e k" assumes unproj_proj: "\x. unproj (\k. x proj k) = x" shows "\d\basis. \l::'a. \ r::nat\nat. strict_mono r \ (\e>0. eventually (\n. \i\d. dist (f (r n) proj i) (l proj i) < e) sequentially)" proof safe fix d :: "'b set" assume d: "d \ basis" with finite_basis have "finite d" by (blast intro: finite_subset) from this d show "\l::'a. \r::nat\nat. strict_mono r \ (\e>0. eventually (\n. \i\d. dist (f (r n) proj i) (l proj i) < e) sequentially)" proof (induct d) case empty then show ?case unfolding strict_mono_def by auto next case (insert k d) have k[intro]: "k \ basis" using insert by auto have s': "bounded ((\x. x proj k) ` range f)" using k by (rule bounded_proj) obtain l1::"'a" and r1 where r1: "strict_mono r1" and lr1: "\e > 0. \\<^sub>F n in sequentially. \i\d. dist (f (r1 n) proj i) (l1 proj i) < e" using insert by auto have f': "\n. f (r1 n) proj k \ (\x. x proj k) ` range f" by simp have "bounded (range (\i. f (r1 i) proj k))" by (metis (lifting) bounded_subset f' image_subsetI s') then obtain l2 r2 where r2: "strict_mono r2" and lr2: "(\i. f (r1 (r2 i)) proj k) \ l2" using bounded_imp_convergent_subsequence[of "\i. f (r1 i) proj k"] by (auto simp: o_def) define r where "r = r1 \ r2" have r: "strict_mono r" using r1 and r2 unfolding r_def o_def strict_mono_def by auto moreover define l where "l = unproj (\i. if i = k then l2 else l1 proj i)" { fix e::real assume "e > 0" from lr1 \e > 0\ have N1: "\\<^sub>F n in sequentially. \i\d. dist (f (r1 n) proj i) (l1 proj i) < e" by blast from lr2 \e > 0\ have N2: "\\<^sub>F n in sequentially. dist (f (r1 (r2 n)) proj k) l2 < e" by (rule tendstoD) from r2 N1 have N1': "\\<^sub>F n in sequentially. \i\d. dist (f (r1 (r2 n)) proj i) (l1 proj i) < e" by (rule eventually_subseq) have "\\<^sub>F n in sequentially. \i\insert k d. dist (f (r n) proj i) (l proj i) < e" using N1' N2 by eventually_elim (use insert.prems in \auto simp: l_def r_def o_def proj_unproj\) } ultimately show ?case by auto qed qed lemma bounded_fst: "bounded s \ bounded (fst ` s)" unfolding bounded_def by (metis (erased, opaque_lifting) dist_fst_le image_iff order_trans) lemma bounded_snd: "bounded s \ bounded (snd ` s)" unfolding bounded_def by (metis (no_types, opaque_lifting) dist_snd_le image_iff order.trans) instance\<^marker>\tag important\ prod :: (heine_borel, heine_borel) heine_borel proof fix f :: "nat \ 'a \ 'b" assume f: "bounded (range f)" then have "bounded (fst ` range f)" by (rule bounded_fst) then have s1: "bounded (range (fst \ f))" by (simp add: image_comp) obtain l1 r1 where r1: "strict_mono r1" and l1: "(\n. fst (f (r1 n))) \ l1" using bounded_imp_convergent_subsequence [OF s1] unfolding o_def by fast from f have s2: "bounded (range (snd \ f \ r1))" by (auto simp: image_comp intro: bounded_snd bounded_subset) obtain l2 r2 where r2: "strict_mono r2" and l2: "(\n. snd (f (r1 (r2 n)))) \ l2" using bounded_imp_convergent_subsequence [OF s2] unfolding o_def by fast have l1': "((\n. fst (f (r1 (r2 n)))) \ l1) sequentially" using LIMSEQ_subseq_LIMSEQ [OF l1 r2] unfolding o_def . have l: "((f \ (r1 \ r2)) \ (l1, l2)) sequentially" using tendsto_Pair [OF l1' l2] unfolding o_def by simp have r: "strict_mono (r1 \ r2)" using r1 r2 unfolding strict_mono_def by simp show "\l r. strict_mono r \ ((f \ r) \ l) sequentially" using l r by fast qed section \Completeness\ proposition (in metric_space) completeI: assumes "\f. \n. f n \ s \ Cauchy f \ \l\s. f \ l" shows "complete s" using assms unfolding complete_def by fast proposition (in metric_space) completeE: assumes "complete s" and "\n. f n \ s" and "Cauchy f" obtains l where "l \ s" and "f \ l" using assms unfolding complete_def by fast (* TODO: generalize to uniform spaces *) lemma compact_imp_complete: fixes s :: "'a::metric_space set" assumes "compact s" shows "complete s" proof - { fix f assume as: "(\n::nat. f n \ s)" "Cauchy f" from as(1) obtain l r where lr: "l\s" "strict_mono r" "(f \ r) \ l" using assms unfolding compact_def by blast note lr' = seq_suble [OF lr(2)] { fix e :: real assume "e > 0" from as(2) obtain N where N:"\m n. N \ m \ N \ n \ dist (f m) (f n) < e/2" unfolding Cauchy_def using \e > 0\ by (meson half_gt_zero) then obtain M where M:"\n\M. dist ((f \ r) n) l < e/2" by (metis dist_self lim_sequentially lr(3)) { fix n :: nat assume n: "n \ max N M" have "dist ((f \ r) n) l < e/2" using n M by auto moreover have "r n \ N" using lr'[of n] n by auto then have "dist (f n) ((f \ r) n) < e/2" using N and n by auto ultimately have "dist (f n) l < e" using n M by metric } then have "\N. \n\N. dist (f n) l < e" by blast } then have "\l\s. (f \ l) sequentially" using \l\s\ unfolding lim_sequentially by auto } then show ?thesis unfolding complete_def by auto qed proposition compact_eq_totally_bounded: "compact s \ complete s \ (\e>0. \k. finite k \ s \ (\x\k. ball x e))" (is "_ \ ?rhs") proof assume assms: "?rhs" then obtain k where k: "\e. 0 < e \ finite (k e)" "\e. 0 < e \ s \ (\x\k e. ball x e)" by (auto simp: choice_iff') show "compact s" proof cases assume "s = {}" then show "compact s" by (simp add: compact_def) next assume "s \ {}" show ?thesis unfolding compact_def proof safe fix f :: "nat \ 'a" assume f: "\n. f n \ s" define e where "e n = 1 / (2 * Suc n)" for n then have [simp]: "\n. 0 < e n" by auto define B where "B n U = (SOME b. infinite {n. f n \ b} \ (\x. b \ ball x (e n) \ U))" for n U { fix n U assume "infinite {n. f n \ U}" then have "\b\k (e n). infinite {i\{n. f n \ U}. f i \ ball b (e n)}" using k f by (intro pigeonhole_infinite_rel) (auto simp: subset_eq) then obtain a where "a \ k (e n)" "infinite {i \ {n. f n \ U}. f i \ ball a (e n)}" .. then have "\b. infinite {i. f i \ b} \ (\x. b \ ball x (e n) \ U)" by (intro exI[of _ "ball a (e n) \ U"] exI[of _ a]) (auto simp: ac_simps) from someI_ex[OF this] have "infinite {i. f i \ B n U}" "\x. B n U \ ball x (e n) \ U" unfolding B_def by auto } note B = this define F where "F = rec_nat (B 0 UNIV) B" { fix n have "infinite {i. f i \ F n}" by (induct n) (auto simp: F_def B) } then have F: "\n. \x. F (Suc n) \ ball x (e n) \ F n" using B by (simp add: F_def) then have F_dec: "\m n. m \ n \ F n \ F m" using decseq_SucI[of F] by (auto simp: decseq_def) obtain sel where sel: "\k i. i < sel k i" "\k i. f (sel k i) \ F k" proof (atomize_elim, unfold all_conj_distrib[symmetric], intro choice allI) fix k i have "infinite ({n. f n \ F k} - {.. i})" using \infinite {n. f n \ F k}\ by auto from infinite_imp_nonempty[OF this] show "\x>i. f x \ F k" by (simp add: set_eq_iff not_le conj_commute) qed define t where "t = rec_nat (sel 0 0) (\n i. sel (Suc n) i)" have "strict_mono t" unfolding strict_mono_Suc_iff by (simp add: t_def sel) moreover have "\i. (f \ t) i \ s" using f by auto moreover have t: "(f \ t) n \ F n" for n by (cases n) (simp_all add: t_def sel) have "Cauchy (f \ t)" proof (safe intro!: metric_CauchyI exI elim!: nat_approx_posE) fix r :: real and N n m assume "1 / Suc N < r" "Suc N \ n" "Suc N \ m" then have "(f \ t) n \ F (Suc N)" "(f \ t) m \ F (Suc N)" "2 * e N < r" using F_dec t by (auto simp: e_def field_simps) with F[of N] obtain x where "dist x ((f \ t) n) < e N" "dist x ((f \ t) m) < e N" by (auto simp: subset_eq) with \2 * e N < r\ show "dist ((f \ t) m) ((f \ t) n) < r" by metric qed ultimately show "\l\s. \r. strict_mono r \ (f \ r) \ l" using assms unfolding complete_def by blast qed qed qed (metis compact_imp_complete compact_imp_seq_compact seq_compact_imp_totally_bounded) lemma cauchy_imp_bounded: assumes "Cauchy s" shows "bounded (range s)" proof - from assms obtain N :: nat where "\m n. N \ m \ N \ n \ dist (s m) (s n) < 1" by (meson Cauchy_def zero_less_one) then have N:"\n. N \ n \ dist (s N) (s n) < 1" by auto moreover have "bounded (s ` {0..N})" using finite_imp_bounded[of "s ` {1..N}"] by auto then obtain a where a:"\x\s ` {0..N}. dist (s N) x \ a" unfolding bounded_any_center [where a="s N"] by auto ultimately show "?thesis" unfolding bounded_any_center [where a="s N"] apply (rule_tac x="max a 1" in exI, auto) apply (erule_tac x=y in allE) apply (erule_tac x=y in ballE, auto) done qed instance heine_borel < complete_space proof fix f :: "nat \ 'a" assume "Cauchy f" then show "convergent f" unfolding convergent_def using Cauchy_converges_subseq cauchy_imp_bounded bounded_imp_convergent_subsequence by blast qed lemma complete_UNIV: "complete (UNIV :: ('a::complete_space) set)" proof (rule completeI) fix f :: "nat \ 'a" assume "Cauchy f" then show "\l\UNIV. f \ l" using Cauchy_convergent convergent_def by blast qed lemma complete_imp_closed: fixes S :: "'a::metric_space set" shows "complete S \ closed S" by (metis LIMSEQ_imp_Cauchy LIMSEQ_unique closed_sequential_limits completeE) lemma complete_Int_closed: fixes S :: "'a::metric_space set" assumes "complete S" and "closed t" shows "complete (S \ t)" by (metis Int_iff assms closed_sequentially completeE completeI) lemma complete_closed_subset: fixes S :: "'a::metric_space set" assumes "closed S" and "S \ t" and "complete t" shows "complete S" using assms complete_Int_closed [of t S] by (simp add: Int_absorb1) lemma complete_eq_closed: fixes S :: "('a::complete_space) set" shows "complete S \ closed S" proof assume "closed S" then show "complete S" using subset_UNIV complete_UNIV by (rule complete_closed_subset) next assume "complete S" then show "closed S" by (rule complete_imp_closed) qed lemma convergent_eq_Cauchy: fixes S :: "nat \ 'a::complete_space" shows "(\l. (S \ l) sequentially) \ Cauchy S" unfolding Cauchy_convergent_iff convergent_def .. lemma convergent_imp_bounded: fixes S :: "nat \ 'a::metric_space" shows "(S \ l) sequentially \ bounded (range S)" by (intro cauchy_imp_bounded LIMSEQ_imp_Cauchy) lemma frontier_subset_compact: fixes S :: "'a::heine_borel set" shows "compact S \ frontier S \ S" using frontier_subset_closed compact_eq_bounded_closed by blast lemma banach_fix_type: fixes f::"'a::complete_space\'a" assumes c:"0 \ c" "c < 1" and lipschitz:"\x. \y. dist (f x) (f y) \ c * dist x y" shows "\!x. (f x = x)" using assms banach_fix[OF complete_UNIV UNIV_not_empty assms(1,2) subset_UNIV, of f] by auto section \Cauchy continuity\ definition Cauchy_continuous_on where "Cauchy_continuous_on \ \S f. \\. Cauchy \ \ range \ \ S \ Cauchy (f \ \)" lemma continuous_closed_imp_Cauchy_continuous: fixes S :: "('a::complete_space) set" shows "\continuous_on S f; closed S\ \ Cauchy_continuous_on S f" unfolding Cauchy_continuous_on_def by (metis LIMSEQ_imp_Cauchy completeE complete_eq_closed continuous_on_sequentially range_subsetD) lemma uniformly_continuous_imp_Cauchy_continuous: fixes f :: "'a::metric_space \ 'b::metric_space" shows "uniformly_continuous_on S f \ Cauchy_continuous_on S f" by (simp add: uniformly_continuous_on_def Cauchy_continuous_on_def Cauchy_def image_subset_iff) metis lemma Cauchy_continuous_on_imp_continuous: fixes f :: "'a::metric_space \ 'b::metric_space" assumes "Cauchy_continuous_on S f" shows "continuous_on S f" proof - have False if x: "\n. \x'\S. dist x' x < inverse(Suc n) \ \ dist (f x') (f x) < \" "\>0" "x \ S" for x and \::real proof - obtain \ where \: "\n. \ n \ S" and dx: "\n. dist (\ n) x < inverse(Suc n)" and dfx: "\n. \ dist (f (\ n)) (f x) < \" using x by metis define \ where "\ \ \n. if even n then \ n else x" with \ \x \ S\ have "range \ \ S" by auto have "\ \ x" unfolding tendsto_iff proof (intro strip) fix e :: real assume "e>0" then obtain N where "inverse (Suc N) < e" using reals_Archimedean by blast then have "\n. N \ n \ dist (\ n) x < e" by (smt (verit, ccfv_SIG) dx inverse_Suc inverse_less_iff_less inverse_positive_iff_positive of_nat_Suc of_nat_mono) with \e>0\ show "\\<^sub>F n in sequentially. dist (\ n) x < e" by (auto simp add: eventually_sequentially \_def) qed then have "Cauchy \" by (intro LIMSEQ_imp_Cauchy) then have Cf: "Cauchy (f \ \)" by (meson Cauchy_continuous_on_def \range \ \ S\ assms) have "(f \ \) \ f x" unfolding tendsto_iff proof (intro strip) fix e :: real assume "e>0" then obtain N where N: "\m\N. \n\N. dist ((f \ \) m) ((f \ \) n) < e" using Cf unfolding Cauchy_def by presburger moreover have "(f \ \) (Suc(N+N)) = f x" by (simp add: \_def) ultimately have "\n\N. dist ((f \ \) n) (f x) < e" by (metis add_Suc le_add2) then show "\\<^sub>F n in sequentially. dist ((f \ \) n) (f x) < e" using eventually_sequentially by blast qed moreover have "\n. \ dist (f (\ (2*n))) (f x) < \" using dfx by (simp add: \_def) ultimately show False using \\>0\ by (fastforce simp: mult_2 nat_le_iff_add tendsto_iff eventually_sequentially) qed then show ?thesis unfolding continuous_on_iff by (meson inverse_Suc) qed section\<^marker>\tag unimportant\\ Finite intersection property\ text\Also developed in HOL's toplogical spaces theory, but the Heine-Borel type class isn't available there.\ lemma closed_imp_fip: fixes S :: "'a::heine_borel set" assumes "closed S" and T: "T \ \" "bounded T" and clof: "\T. T \ \ \ closed T" and "\\'. \finite \'; \' \ \\ \ S \ \\' \ {}" shows "S \ \\ \ {}" proof - have "compact (S \ T)" using \closed S\ clof compact_eq_bounded_closed T by blast then have "(S \ T) \ \\ \ {}" by (smt (verit, best) Inf_insert Int_assoc assms compact_imp_fip finite_insert insert_subset) then show ?thesis by blast qed lemma closed_imp_fip_compact: fixes S :: "'a::heine_borel set" shows "\closed S; \T. T \ \ \ compact T; \\'. \finite \'; \' \ \\ \ S \ \\' \ {}\ \ S \ \\ \ {}" by (metis closed_imp_fip compact_eq_bounded_closed equals0I finite.emptyI order.refl) lemma closed_fip_Heine_Borel: fixes \ :: "'a::heine_borel set set" assumes "T \ \" "bounded T" and "\T. T \ \ \ closed T" and "\\'. \finite \'; \' \ \\ \ \\' \ {}" shows "\\ \ {}" using closed_imp_fip [OF closed_UNIV] assms by auto lemma compact_fip_Heine_Borel: fixes \ :: "'a::heine_borel set set" assumes clof: "\T. T \ \ \ compact T" and none: "\\'. \finite \'; \' \ \\ \ \\' \ {}" shows "\\ \ {}" by (metis InterI clof closed_fip_Heine_Borel compact_eq_bounded_closed equals0D none) lemma compact_sequence_with_limit: fixes f :: "nat \ 'a::heine_borel" shows "f \ l \ compact (insert l (range f))" by (simp add: closed_limpt compact_eq_bounded_closed convergent_imp_bounded islimpt_insert sequence_unique_limpt) section \Properties of Balls and Spheres\ lemma compact_cball[simp]: fixes x :: "'a::heine_borel" shows "compact (cball x e)" using compact_eq_bounded_closed bounded_cball closed_cball by blast lemma compact_frontier_bounded[intro]: fixes S :: "'a::heine_borel set" shows "bounded S \ compact (frontier S)" unfolding frontier_def using compact_eq_bounded_closed by blast lemma compact_frontier[intro]: fixes S :: "'a::heine_borel set" shows "compact S \ compact (frontier S)" using compact_eq_bounded_closed compact_frontier_bounded by blast lemma no_limpt_imp_countable: assumes "\z. \z islimpt (X :: 'a :: {real_normed_vector, heine_borel} set)" shows "countable X" proof - have "countable (\n. cball 0 (real n) \ X)" proof (intro countable_UN[OF _ countable_finite]) fix n :: nat show "finite (cball 0 (real n) \ X)" using assms by (intro finite_not_islimpt_in_compact) auto qed auto also have "(\n. cball 0 (real n)) = (UNIV :: 'a set)" by (force simp: real_arch_simple) hence "(\n. cball 0 (real n) \ X) = X" by blast finally show "countable X" . qed section \Distance from a Set\ lemma distance_attains_sup: assumes "compact s" "s \ {}" shows "\x\s. \y\s. dist a y \ dist a x" proof (rule continuous_attains_sup [OF assms]) { fix x assume "x\s" have "(dist a \ dist a x) (at x within s)" by (intro tendsto_dist tendsto_const tendsto_ident_at) } then show "continuous_on s (dist a)" unfolding continuous_on .. qed text \For \emph{minimal} distance, we only need closure, not compactness.\ lemma distance_attains_inf: fixes a :: "'a::heine_borel" assumes "closed s" and "s \ {}" obtains x where "x\s" "\y. y \ s \ dist a x \ dist a y" proof - from assms obtain b where "b \ s" by auto let ?B = "s \ cball a (dist b a)" have "?B \ {}" using \b \ s\ by (auto simp: dist_commute) moreover have "continuous_on ?B (dist a)" by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const) moreover have "compact ?B" by (intro closed_Int_compact \closed s\ compact_cball) ultimately obtain x where "x \ ?B" "\y\?B. dist a x \ dist a y" by (metis continuous_attains_inf) with that show ?thesis by fastforce qed section \Infimum Distance\ definition\<^marker>\tag important\ "infdist x A = (if A = {} then 0 else INF a\A. dist x a)" lemma bdd_below_image_dist[intro, simp]: "bdd_below (dist x ` A)" by (auto intro!: zero_le_dist) lemma infdist_notempty: "A \ {} \ infdist x A = (INF a\A. dist x a)" by (simp add: infdist_def) lemma infdist_nonneg: "0 \ infdist x A" by (auto simp: infdist_def intro: cINF_greatest) lemma infdist_le: "a \ A \ infdist x A \ dist x a" by (auto intro: cINF_lower simp add: infdist_def) lemma infdist_le2: "a \ A \ dist x a \ d \ infdist x A \ d" by (auto intro!: cINF_lower2 simp add: infdist_def) lemma infdist_zero[simp]: "a \ A \ infdist a A = 0" by (auto intro!: antisym infdist_nonneg infdist_le2) lemma infdist_Un_min: assumes "A \ {}" "B \ {}" shows "infdist x (A \ B) = min (infdist x A) (infdist x B)" using assms by (simp add: infdist_def cINF_union inf_real_def) lemma infdist_triangle: "infdist x A \ infdist y A + dist x y" proof (cases "A = {}") case True then show ?thesis by (simp add: infdist_def) next case False then obtain a where "a \ A" by auto have "infdist x A \ Inf {dist x y + dist y a |a. a \ A}" proof (rule cInf_greatest) from \A \ {}\ show "{dist x y + dist y a |a. a \ A} \ {}" by simp fix d assume "d \ {dist x y + dist y a |a. a \ A}" then obtain a where d: "d = dist x y + dist y a" "a \ A" by auto show "infdist x A \ d" unfolding infdist_notempty[OF \A \ {}\] proof (rule cINF_lower2) show "a \ A" by fact show "dist x a \ d" unfolding d by (rule dist_triangle) qed simp qed also have "\ = dist x y + infdist y A" proof (rule cInf_eq, safe) fix a assume "a \ A" then show "dist x y + infdist y A \ dist x y + dist y a" by (auto intro: infdist_le) next fix i assume inf: "\d. d \ {dist x y + dist y a |a. a \ A} \ i \ d" then have "i - dist x y \ infdist y A" unfolding infdist_notempty[OF \A \ {}\] using \a \ A\ by (intro cINF_greatest) (auto simp: field_simps) then show "i \ dist x y + infdist y A" by simp qed finally show ?thesis by simp qed lemma infdist_triangle_abs: "\infdist x A - infdist y A\ \ dist x y" by (metis (full_types) abs_diff_le_iff diff_le_eq dist_commute infdist_triangle) lemma in_closure_iff_infdist_zero: assumes "A \ {}" shows "x \ closure A \ infdist x A = 0" proof assume "x \ closure A" show "infdist x A = 0" proof (rule ccontr) assume "infdist x A \ 0" with infdist_nonneg[of x A] have "infdist x A > 0" by auto then have "ball x (infdist x A) \ closure A = {}" by (smt (verit, best) \x \ closure A\ closure_approachableD infdist_le) then have "x \ closure A" by (metis \0 < infdist x A\ centre_in_ball disjoint_iff_not_equal) then show False using \x \ closure A\ by simp qed next assume x: "infdist x A = 0" then obtain a where "a \ A" by atomize_elim (metis all_not_in_conv assms) have False if "e > 0" "\ (\y\A. dist y x < e)" for e proof - have "infdist x A \ e" using \a \ A\ unfolding infdist_def using that by (force simp: dist_commute intro: cINF_greatest) with x \e > 0\ show False by auto qed then show "x \ closure A" using closure_approachable by blast qed lemma in_closed_iff_infdist_zero: assumes "closed A" "A \ {}" shows "x \ A \ infdist x A = 0" proof - have "x \ closure A \ infdist x A = 0" by (simp add: \A \ {}\ in_closure_iff_infdist_zero) with assms show ?thesis by simp qed lemma infdist_pos_not_in_closed: assumes "closed S" "S \ {}" "x \ S" shows "infdist x S > 0" by (smt (verit, best) assms in_closed_iff_infdist_zero infdist_nonneg) lemma infdist_attains_inf: fixes X::"'a::heine_borel set" assumes "closed X" assumes "X \ {}" obtains x where "x \ X" "infdist y X = dist y x" proof - have "bdd_below (dist y ` X)" by auto from distance_attains_inf[OF assms, of y] obtain x where "x \ X" "\z. z \ X \ dist y x \ dist y z" by auto then have "infdist y X = dist y x" by (metis antisym assms(2) cINF_greatest infdist_def infdist_le) with \x \ X\ show ?thesis .. qed text \Every metric space is a T4 space:\ instance metric_space \ t4_space proof fix S T::"'a set" assume H: "closed S" "closed T" "S \ T = {}" consider "S = {}" | "T = {}" | "S \ {} \ T \ {}" by auto then show "\U V. open U \ open V \ S \ U \ T \ V \ U \ V = {}" proof (cases) case 1 then show ?thesis by blast next case 2 then show ?thesis by blast next case 3 define U where "U = (\x\S. ball x ((infdist x T)/2))" have A: "open U" unfolding U_def by auto have "infdist x T > 0" if "x \ S" for x using H that 3 by (auto intro!: infdist_pos_not_in_closed) then have B: "S \ U" unfolding U_def by auto define V where "V = (\x\T. ball x ((infdist x S)/2))" have C: "open V" unfolding V_def by auto have "infdist x S > 0" if "x \ T" for x using H that 3 by (auto intro!: infdist_pos_not_in_closed) then have D: "T \ V" unfolding V_def by auto have "(ball x ((infdist x T)/2)) \ (ball y ((infdist y S)/2)) = {}" if "x \ S" "y \ T" for x y proof auto fix z assume H: "dist x z * 2 < infdist x T" "dist y z * 2 < infdist y S" have "2 * dist x y \ 2 * dist x z + 2 * dist y z" by metric also have "... < infdist x T + infdist y S" using H by auto finally have "dist x y < infdist x T \ dist x y < infdist y S" by auto then show False using infdist_le[OF \x \ S\, of y] infdist_le[OF \y \ T\, of x] by (auto simp add: dist_commute) qed then have E: "U \ V = {}" unfolding U_def V_def by auto show ?thesis using A B C D E by blast qed qed lemma tendsto_infdist [tendsto_intros]: assumes f: "(f \ l) F" shows "((\x. infdist (f x) A) \ infdist l A) F" proof (rule tendstoI) fix e ::real assume "e > 0" from tendstoD[OF f this] show "eventually (\x. dist (infdist (f x) A) (infdist l A) < e) F" proof (eventually_elim) fix x from infdist_triangle[of l A "f x"] infdist_triangle[of "f x" A l] have "dist (infdist (f x) A) (infdist l A) \ dist (f x) l" by (simp add: dist_commute dist_real_def) also assume "dist (f x) l < e" finally show "dist (infdist (f x) A) (infdist l A) < e" . qed qed lemma continuous_infdist[continuous_intros]: assumes "continuous F f" shows "continuous F (\x. infdist (f x) A)" using assms unfolding continuous_def by (rule tendsto_infdist) lemma continuous_on_infdist [continuous_intros]: assumes "continuous_on S f" shows "continuous_on S (\x. infdist (f x) A)" using assms unfolding continuous_on by (auto intro: tendsto_infdist) lemma compact_infdist_le: fixes A::"'a::heine_borel set" assumes "A \ {}" assumes "compact A" assumes "e > 0" shows "compact {x. infdist x A \ e}" proof - from continuous_closed_vimage[of "{0..e}" "\x. infdist x A"] continuous_infdist[OF continuous_ident, of _ UNIV A] have "closed {x. infdist x A \ e}" by (auto simp: vimage_def infdist_nonneg) moreover from assms obtain x0 b where b: "\x. x \ A \ dist x0 x \ b" "closed A" by (auto simp: compact_eq_bounded_closed bounded_def) { fix y assume "infdist y A \ e" moreover from infdist_attains_inf[OF \closed A\ \A \ {}\, of y] obtain z where "z \ A" "infdist y A = dist y z" by blast ultimately have "dist x0 y \ b + e" using b by metric } then have "bounded {x. infdist x A \ e}" by (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + e"]) ultimately show "compact {x. infdist x A \ e}" by (simp add: compact_eq_bounded_closed) qed section \Separation between Points and Sets\ proposition separate_point_closed: fixes S :: "'a::heine_borel set" assumes "closed S" and "a \ S" shows "\d>0. \x\S. d \ dist a x" by (metis assms distance_attains_inf empty_iff gt_ex zero_less_dist_iff) proposition separate_compact_closed: fixes S T :: "'a::heine_borel set" assumes "compact S" and T: "closed T" "S \ T = {}" shows "\d>0. \x\S. \y\T. d \ dist x y" proof cases assume "S \ {} \ T \ {}" then have "S \ {}" "T \ {}" by auto let ?inf = "\x. infdist x T" have "continuous_on S ?inf" by (auto intro!: continuous_at_imp_continuous_on continuous_infdist continuous_ident) then obtain x where x: "x \ S" "\y\S. ?inf x \ ?inf y" using continuous_attains_inf[OF \compact S\ \S \ {}\] by auto then have "0 < ?inf x" using T \T \ {}\ in_closed_iff_infdist_zero by (auto simp: less_le infdist_nonneg) moreover have "\x'\S. \y\T. ?inf x \ dist x' y" using x by (auto intro: order_trans infdist_le) ultimately show ?thesis by auto qed (auto intro!: exI[of _ 1]) proposition separate_closed_compact: fixes S T :: "'a::heine_borel set" assumes S: "closed S" and T: "compact T" and dis: "S \ T = {}" shows "\d>0. \x\S. \y\T. d \ dist x y" by (metis separate_compact_closed[OF T S] dis dist_commute inf_commute) proposition compact_in_open_separated: fixes A::"'a::heine_borel set" assumes A: "A \ {}" "compact A" assumes "open B" assumes "A \ B" obtains e where "e > 0" "{x. infdist x A \ e} \ B" proof atomize_elim have "closed (- B)" "compact A" "- B \ A = {}" using assms by (auto simp: open_Diff compact_eq_bounded_closed) from separate_closed_compact[OF this] obtain d'::real where d': "d'>0" "\x y. x \ B \ y \ A \ d' \ dist x y" by auto define d where "d = d' / 2" hence "d>0" "d < d'" using d' by auto with d' have d: "\x y. x \ B \ y \ A \ d < dist x y" by force show "\e>0. {x. infdist x A \ e} \ B" proof (rule ccontr) assume "\e. 0 < e \ {x. infdist x A \ e} \ B" with \d > 0\ obtain x where x: "infdist x A \ d" "x \ B" by auto then show False by (metis A compact_eq_bounded_closed infdist_attains_inf x d linorder_not_less) qed qed section \Uniform Continuity\ lemma uniformly_continuous_onE: assumes "uniformly_continuous_on s f" "0 < e" obtains d where "d>0" "\x x'. \x\s; x'\s; dist x' x < d\ \ dist (f x') (f x) < e" using assms by (auto simp: uniformly_continuous_on_def) lemma uniformly_continuous_on_sequentially: "uniformly_continuous_on s f \ (\x y. (\n. x n \ s) \ (\n. y n \ s) \ (\n. dist (x n) (y n)) \ 0 \ (\n. dist (f(x n)) (f(y n))) \ 0)" (is "?lhs = ?rhs") proof assume ?lhs { fix x y assume x: "\n. x n \ s" and y: "\n. y n \ s" and xy: "((\n. dist (x n) (y n)) \ 0) sequentially" { fix e :: real assume "e > 0" then obtain d where "d > 0" and d: "\x\s. \x'\s. dist x' x < d \ dist (f x') (f x) < e" by (metis \?lhs\ uniformly_continuous_onE) obtain N where N: "\n\N. dist (x n) (y n) < d" using xy[unfolded lim_sequentially dist_norm] and \d>0\ by auto then have "\N. \n\N. dist (f (x n)) (f (y n)) < e" using d x y by blast } then have "((\n. dist (f(x n)) (f(y n))) \ 0) sequentially" unfolding lim_sequentially and dist_real_def by auto } then show ?rhs by auto next assume ?rhs { assume "\ ?lhs" then obtain e where "e > 0" "\d>0. \x\s. \x'\s. dist x' x < d \ \ dist (f x') (f x) < e" unfolding uniformly_continuous_on_def by auto then obtain fa where fa: "\x. 0 < x \ fst (fa x) \ s \ snd (fa x) \ s \ dist (fst (fa x)) (snd (fa x)) < x \ \ dist (f (fst (fa x))) (f (snd (fa x))) < e" using choice[of "\d x. d>0 \ fst x \ s \ snd x \ s \ dist (snd x) (fst x) < d \ \ dist (f (snd x)) (f (fst x)) < e"] by (auto simp: Bex_def dist_commute) define x where "x n = fst (fa (inverse (real n + 1)))" for n define y where "y n = snd (fa (inverse (real n + 1)))" for n have xyn: "\n. x n \ s \ y n \ s" and xy0: "\n. dist (x n) (y n) < inverse (real n + 1)" and fxy:"\n. \ dist (f (x n)) (f (y n)) < e" unfolding x_def and y_def using fa by auto { fix e :: real assume "e > 0" then obtain N :: nat where "N \ 0" and N: "0 < inverse (real N) \ inverse (real N) < e" unfolding real_arch_inverse[of e] by auto then have "\N. \n\N. dist (x n) (y n) < e" by (smt (verit, ccfv_SIG) inverse_le_imp_le nat_le_real_less of_nat_le_0_iff xy0) } then have "\e>0. \N. \n\N. dist (f (x n)) (f (y n)) < e" using \?rhs\[THEN spec[where x=x], THEN spec[where x=y]] and xyn unfolding lim_sequentially dist_real_def by auto then have False using fxy and \e>0\ by auto } then show ?lhs unfolding uniformly_continuous_on_def by blast qed section \Continuity on a Compact Domain Implies Uniform Continuity\ text\From the proof of the Heine-Borel theorem: Lemma 2 in section 3.7, page 69 of J. C. Burkill and H. Burkill. A Second Course in Mathematical Analysis (CUP, 2002)\ lemma Heine_Borel_lemma: assumes "compact S" and Ssub: "S \ \\" and opn: "\G. G \ \ \ open G" obtains e where "0 < e" "\x. x \ S \ \G \ \. ball x e \ G" proof - have False if neg: "\e. 0 < e \ \x \ S. \G \ \. \ ball x e \ G" proof - have "\x \ S. \G \ \. \ ball x (1 / Suc n) \ G" for n using neg by simp then obtain f where "\n. f n \ S" and fG: "\G n. G \ \ \ \ ball (f n) (1 / Suc n) \ G" by metis then obtain l r where "l \ S" "strict_mono r" and to_l: "(f \ r) \ l" using \compact S\ compact_def that by metis then obtain G where "l \ G" "G \ \" using Ssub by auto then obtain e where "0 < e" and e: "\z. dist z l < e \ z \ G" using opn open_dist by blast obtain N1 where N1: "\n. n \ N1 \ dist (f (r n)) l < e/2" using to_l apply (simp add: lim_sequentially) using \0 < e\ half_gt_zero that by blast obtain N2 where N2: "of_nat N2 > 2/e" using reals_Archimedean2 by blast obtain x where "x \ ball (f (r (max N1 N2))) (1 / real (Suc (r (max N1 N2))))" and "x \ G" using fG [OF \G \ \\, of "r (max N1 N2)"] by blast then have "dist (f (r (max N1 N2))) x < 1 / real (Suc (r (max N1 N2)))" by simp also have "... \ 1 / real (Suc (max N1 N2))" by (meson Suc_le_mono \strict_mono r\ inverse_of_nat_le nat.discI seq_suble) also have "... \ 1 / real (Suc N2)" by (simp add: field_simps) also have "... < e/2" using N2 \0 < e\ by (simp add: field_simps) finally have "dist (f (r (max N1 N2))) x < e/2" . moreover have "dist (f (r (max N1 N2))) l < e/2" using N1 max.cobounded1 by blast ultimately have "dist x l < e" by metric then show ?thesis using e \x \ G\ by blast qed then show ?thesis by (meson that) qed lemma compact_uniformly_equicontinuous: assumes "compact S" and cont: "\x e. \x \ S; 0 < e\ \ \d. 0 < d \ (\f \ \. \x' \ S. dist x' x < d \ dist (f x') (f x) < e)" and "0 < e" obtains d where "0 < d" "\f x x'. \f \ \; x \ S; x' \ S; dist x' x < d\ \ dist (f x') (f x) < e" proof - obtain d where d_pos: "\x e. \x \ S; 0 < e\ \ 0 < d x e" and d_dist : "\x x' e f. \dist x' x < d x e; x \ S; x' \ S; 0 < e; f \ \\ \ dist (f x') (f x) < e" using cont by metis let ?\ = "((\x. ball x (d x (e/2))) ` S)" have Ssub: "S \ \ ?\" using \0 < e\ d_pos by auto then obtain k where "0 < k" and k: "\x. x \ S \ \G \ ?\. ball x k \ G" by (rule Heine_Borel_lemma [OF \compact S\]) auto moreover have "dist (f v) (f u) < e" if "f \ \" "u \ S" "v \ S" "dist v u < k" for f u v proof - obtain G where "G \ ?\" "u \ G" "v \ G" using k that by (metis \dist v u < k\ \u \ S\ \0 < k\ centre_in_ball subsetD dist_commute mem_ball) then obtain w where w: "dist w u < d w (e/2)" "dist w v < d w (e/2)" "w \ S" by auto with that d_dist have "dist (f w) (f v) < e/2" by (metis \0 < e\ dist_commute half_gt_zero) moreover have "dist (f w) (f u) < e/2" using that d_dist w by (metis \0 < e\ dist_commute divide_pos_pos zero_less_numeral) ultimately show ?thesis using dist_triangle_half_r by blast qed ultimately show ?thesis using that by blast qed corollary compact_uniformly_continuous: fixes f :: "'a :: metric_space \ 'b :: metric_space" assumes f: "continuous_on S f" and S: "compact S" shows "uniformly_continuous_on S f" using f unfolding continuous_on_iff uniformly_continuous_on_def by (force intro: compact_uniformly_equicontinuous [OF S, of "{f}"]) section\<^marker>\tag unimportant\\ Theorems relating continuity and uniform continuity to closures\ lemma continuous_on_closure: "continuous_on (closure S) f \ (\x e. x \ closure S \ 0 < e \ (\d. 0 < d \ (\y. y \ S \ dist y x < d \ dist (f y) (f x) < e)))" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs unfolding continuous_on_iff by (metis Un_iff closure_def) next assume R [rule_format]: ?rhs show ?lhs proof fix x and e::real assume "0 < e" and x: "x \ closure S" obtain \::real where "\ > 0" and \: "\y. \y \ S; dist y x < \\ \ dist (f y) (f x) < e/2" using R [of x "e/2"] \0 < e\ x by auto have "dist (f y) (f x) \ e" if y: "y \ closure S" and dyx: "dist y x < \/2" for y proof - obtain \'::real where "\' > 0" and \': "\z. \z \ S; dist z y < \'\ \ dist (f z) (f y) < e/2" using R [of y "e/2"] \0 < e\ y by auto obtain z where "z \ S" and z: "dist z y < min \' \ / 2" using closure_approachable y by (metis \0 < \'\ \0 < \\ divide_pos_pos min_less_iff_conj zero_less_numeral) have "dist (f z) (f y) < e/2" using \' [OF \z \ S\] z \0 < \'\ by metric moreover have "dist (f z) (f x) < e/2" using \[OF \z \ S\] z dyx by metric ultimately show ?thesis by metric qed then show "\d>0. \x'\closure S. dist x' x < d \ dist (f x') (f x) \ e" by (rule_tac x="\/2" in exI) (simp add: \\ > 0\) qed qed lemma continuous_on_closure_sequentially: fixes f :: "'a::metric_space \ 'b :: metric_space" shows "continuous_on (closure S) f \ (\x a. a \ closure S \ (\n. x n \ S) \ x \ a \ (f \ x) \ f a)" (is "?lhs = ?rhs") proof - have "continuous_on (closure S) f \ (\x \ closure S. continuous (at x within S) f)" by (force simp: continuous_on_closure continuous_within_eps_delta) also have "... = ?rhs" by (force simp: continuous_within_sequentially) finally show ?thesis . qed lemma uniformly_continuous_on_closure: fixes f :: "'a::metric_space \ 'b::metric_space" assumes ucont: "uniformly_continuous_on S f" and cont: "continuous_on (closure S) f" shows "uniformly_continuous_on (closure S) f" unfolding uniformly_continuous_on_def proof (intro allI impI) fix e::real assume "0 < e" then obtain d::real where "d>0" and d: "\x x'. \x\S; x'\S; dist x' x < d\ \ dist (f x') (f x) < e/3" using ucont [unfolded uniformly_continuous_on_def, rule_format, of "e/3"] by auto show "\d>0. \x\closure S. \x'\closure S. dist x' x < d \ dist (f x') (f x) < e" proof (rule exI [where x="d/3"], clarsimp simp: \d > 0\) fix x y assume x: "x \ closure S" and y: "y \ closure S" and dyx: "dist y x * 3 < d" obtain d1::real where "d1 > 0" and d1: "\w. \w \ closure S; dist w x < d1\ \ dist (f w) (f x) < e/3" using cont [unfolded continuous_on_iff, rule_format, of "x" "e/3"] \0 < e\ x by auto obtain x' where "x' \ S" and x': "dist x' x < min d1 (d / 3)" using closure_approachable [of x S] by (metis \0 < d1\ \0 < d\ divide_pos_pos min_less_iff_conj x zero_less_numeral) obtain d2::real where "d2 > 0" and d2: "\w \ closure S. dist w y < d2 \ dist (f w) (f y) < e/3" using cont [unfolded continuous_on_iff, rule_format, of "y" "e/3"] \0 < e\ y by auto obtain y' where "y' \ S" and y': "dist y' y < min d2 (d / 3)" using closure_approachable [of y S] by (metis \0 < d2\ \0 < d\ divide_pos_pos min_less_iff_conj y zero_less_numeral) have "dist x' x < d/3" using x' by auto then have "dist x' y' < d" using dyx y' by metric then have "dist (f x') (f y') < e/3" by (rule d [OF \y' \ S\ \x' \ S\]) moreover have "dist (f x') (f x) < e/3" using \x' \ S\ closure_subset x' d1 by (simp add: closure_def) moreover have "dist (f y') (f y) < e/3" using \y' \ S\ closure_subset y' d2 by (simp add: closure_def) ultimately show "dist (f y) (f x) < e" by metric qed qed lemma uniformly_continuous_on_extension_at_closure: fixes f::"'a::metric_space \ 'b::complete_space" assumes uc: "uniformly_continuous_on X f" assumes "x \ closure X" obtains l where "(f \ l) (at x within X)" proof - from assms obtain xs where xs: "xs \ x" "\n. xs n \ X" by (auto simp: closure_sequential) from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF xs] obtain l where l: "(\n. f (xs n)) \ l" by atomize_elim (simp only: convergent_eq_Cauchy) have "(f \ l) (at x within X)" proof (safe intro!: Lim_within_LIMSEQ) fix xs' assume "\n. xs' n \ x \ xs' n \ X" and xs': "xs' \ x" then have "xs' n \ x" "xs' n \ X" for n by auto from uniformly_continuous_on_Cauchy[OF uc LIMSEQ_imp_Cauchy, OF \xs' \ x\ \xs' _ \ X\] obtain l' where l': "(\n. f (xs' n)) \ l'" by atomize_elim (simp only: convergent_eq_Cauchy) show "(\n. f (xs' n)) \ l" proof (rule tendstoI) fix e::real assume "e > 0" define e' where "e' \ e/2" have "e' > 0" using \e > 0\ by (simp add: e'_def) have "\\<^sub>F n in sequentially. dist (f (xs n)) l < e'" by (simp add: \0 < e'\ l tendstoD) moreover from uc[unfolded uniformly_continuous_on_def, rule_format, OF \e' > 0\] obtain d where d: "d > 0" "\x x'. x \ X \ x' \ X \ dist x x' < d \ dist (f x) (f x') < e'" by auto have "\\<^sub>F n in sequentially. dist (xs n) (xs' n) < d" by (auto intro!: \0 < d\ order_tendstoD tendsto_eq_intros xs xs') ultimately show "\\<^sub>F n in sequentially. dist (f (xs' n)) l < e" proof eventually_elim case (elim n) have "dist (f (xs' n)) l \ dist (f (xs n)) (f (xs' n)) + dist (f (xs n)) l" by metric also have "dist (f (xs n)) (f (xs' n)) < e'" by (auto intro!: d xs \xs' _ \ _\ elim) also note \dist (f (xs n)) l < e'\ also have "e' + e' = e" by (simp add: e'_def) finally show ?case by simp qed qed qed thus ?thesis .. qed lemma uniformly_continuous_on_extension_on_closure: fixes f::"'a::metric_space \ 'b::complete_space" assumes uc: "uniformly_continuous_on X f" obtains g where "uniformly_continuous_on (closure X) g" "\x. x \ X \ f x = g x" "\Y h x. X \ Y \ Y \ closure X \ continuous_on Y h \ (\x. x \ X \ f x = h x) \ x \ Y \ h x = g x" proof - from uc have cont_f: "continuous_on X f" by (simp add: uniformly_continuous_imp_continuous) obtain y where y: "(f \ y x) (at x within X)" if "x \ closure X" for x using uniformly_continuous_on_extension_at_closure[OF assms] by meson let ?g = "\x. if x \ X then f x else y x" have "uniformly_continuous_on (closure X) ?g" unfolding uniformly_continuous_on_def proof safe fix e::real assume "e > 0" define e' where "e' \ e / 3" have "e' > 0" using \e > 0\ by (simp add: e'_def) from uc[unfolded uniformly_continuous_on_def, rule_format, OF \0 < e'\] obtain d where "d > 0" and d: "\x x'. x \ X \ x' \ X \ dist x' x < d \ dist (f x') (f x) < e'" by auto define d' where "d' = d / 3" have "d' > 0" using \d > 0\ by (simp add: d'_def) show "\d>0. \x\closure X. \x'\closure X. dist x' x < d \ dist (?g x') (?g x) < e" proof (safe intro!: exI[where x=d'] \d' > 0\) fix x x' assume x: "x \ closure X" and x': "x' \ closure X" and dist: "dist x' x < d'" then obtain xs xs' where xs: "xs \ x" "\n. xs n \ X" and xs': "xs' \ x'" "\n. xs' n \ X" by (auto simp: closure_sequential) have "\\<^sub>F n in sequentially. dist (xs' n) x' < d'" and "\\<^sub>F n in sequentially. dist (xs n) x < d'" by (auto intro!: \0 < d'\ order_tendstoD tendsto_eq_intros xs xs') moreover have "(\x. f (xs x)) \ y x" if "x \ closure X" "x \ X" "xs \ x" "\n. xs n \ X" for xs x using that not_eventuallyD by (force intro!: filterlim_compose[OF y[OF \x \ closure X\]] simp: filterlim_at) then have "(\x. f (xs' x)) \ ?g x'" "(\x. f (xs x)) \ ?g x" using x x' by (auto intro!: continuous_on_tendsto_compose[OF cont_f] simp: xs' xs) then have "\\<^sub>F n in sequentially. dist (f (xs' n)) (?g x') < e'" "\\<^sub>F n in sequentially. dist (f (xs n)) (?g x) < e'" by (auto intro!: \0 < e'\ order_tendstoD tendsto_eq_intros) ultimately have "\\<^sub>F n in sequentially. dist (?g x') (?g x) < e" proof eventually_elim case (elim n) have "dist (?g x') (?g x) \ dist (f (xs' n)) (?g x') + dist (f (xs' n)) (f (xs n)) + dist (f (xs n)) (?g x)" by (metis add.commute add_le_cancel_left dist_commute dist_triangle dist_triangle_le) also from \dist (xs' n) x' < d'\ \dist x' x < d'\ \dist (xs n) x < d'\ have "dist (xs' n) (xs n) < d" unfolding d'_def by metric with \xs _ \ X\ \xs' _ \ X\ have "dist (f (xs' n)) (f (xs n)) < e'" by (rule d) also note \dist (f (xs' n)) (?g x') < e'\ also note \dist (f (xs n)) (?g x) < e'\ finally show ?case by (simp add: e'_def) qed then show "dist (?g x') (?g x) < e" by simp qed qed moreover have "f x = ?g x" if "x \ X" for x using that by simp moreover { fix Y h x assume Y: "x \ Y" "X \ Y" "Y \ closure X" and cont_h: "continuous_on Y h" and extension: "(\x. x \ X \ f x = h x)" { assume "x \ X" have "x \ closure X" using Y by auto then obtain xs where xs: "xs \ x" "\n. xs n \ X" by (auto simp: closure_sequential) from continuous_on_tendsto_compose[OF cont_h xs(1)] xs(2) Y have hx: "(\x. f (xs x)) \ h x" by (auto simp: subsetD extension) then have "(\x. f (xs x)) \ y x" using \x \ X\ not_eventuallyD xs(2) by (force intro!: filterlim_compose[OF y[OF \x \ closure X\]] simp: filterlim_at xs) with hx have "h x = y x" by (rule LIMSEQ_unique) } then have "h x = ?g x" using extension by auto } ultimately show ?thesis .. qed lemma bounded_uniformly_continuous_image: fixes f :: "'a :: heine_borel \ 'b :: heine_borel" assumes "uniformly_continuous_on S f" "bounded S" shows "bounded(f ` S)" by (metis (no_types, lifting) assms bounded_closure_image compact_closure compact_continuous_image compact_eq_bounded_closed image_cong uniformly_continuous_imp_continuous uniformly_continuous_on_extension_on_closure) section \With Abstract Topology (TODO: move and remove dependency?)\ lemma openin_contains_ball: "openin (top_of_set T) S \ S \ T \ (\x \ S. \e. 0 < e \ ball x e \ T \ S)" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (metis IntD2 Int_commute Int_lower1 Int_mono inf.idem openE openin_open) next assume ?rhs then show ?lhs by (smt (verit) open_ball Int_commute Int_iff centre_in_ball in_mono openin_open_Int openin_subopen) qed lemma openin_contains_cball: "openin (top_of_set T) S \ S \ T \ (\x \ S. \e. 0 < e \ cball x e \ T \ S)" (is "?lhs = ?rhs") proof assume ?lhs then show ?rhs by (force simp add: openin_contains_ball intro: exI [where x="_/2"]) next assume ?rhs then show ?lhs by (force simp add: openin_contains_ball) qed section \Closed Nest\ text \Bounded closed nest property (proof does not use Heine-Borel)\ lemma bounded_closed_nest: fixes S :: "nat \ ('a::heine_borel) set" assumes "\n. closed (S n)" and "\n. S n \ {}" and "\m n. m \ n \ S n \ S m" and "bounded (S 0)" obtains a where "\n. a \ S n" proof - from assms(2) obtain x where x: "\n. x n \ S n" using choice[of "\n x. x \ S n"] by auto from assms(4,1) have "seq_compact (S 0)" by (simp add: bounded_closed_imp_seq_compact) then obtain l r where lr: "l \ S 0" "strict_mono r" "(x \ r) \ l" using x and assms(3) unfolding seq_compact_def by blast have "\n. l \ S n" proof fix n :: nat have "closed (S n)" using assms(1) by simp moreover have "\i. (x \ r) i \ S i" using x and assms(3) and lr(2) [THEN seq_suble] by auto then have "\i. (x \ r) (i + n) \ S n" using assms(3) by (fast intro!: le_add2) moreover have "(\i. (x \ r) (i + n)) \ l" using lr(3) by (rule LIMSEQ_ignore_initial_segment) ultimately show "l \ S n" by (metis closed_sequentially) qed then show ?thesis using that by blast qed text \Decreasing case does not even need compactness, just completeness.\ lemma decreasing_closed_nest: fixes S :: "nat \ ('a::complete_space) set" assumes "\n. closed (S n)" "\n. S n \ {}" "\m n. m \ n \ S n \ S m" "\e. e>0 \ \n. \x\S n. \y\S n. dist x y < e" obtains a where "\n. a \ S n" proof - obtain t where t: "\n. t n \ S n" by (meson assms(2) equals0I) { fix e :: real assume "e > 0" then obtain N where N: "\x\S N. \y\S N. dist x y < e" using assms(4) by blast { fix m n :: nat assume "N \ m \ N \ n" then have "t m \ S N" "t n \ S N" using assms(3) t unfolding subset_eq t by blast+ then have "dist (t m) (t n) < e" using N by auto } then have "\N. \m n. N \ m \ N \ n \ dist (t m) (t n) < e" by auto } then have "Cauchy t" by (metis metric_CauchyI) then obtain l where l:"(t \ l) sequentially" using complete_UNIV unfolding complete_def by auto { fix n :: nat { fix e :: real assume "e > 0" then obtain N :: nat where N: "\n\N. dist (t n) l < e" using l[unfolded lim_sequentially] by auto have "t (max n N) \ S n" by (meson assms(3) contra_subsetD max.cobounded1 t) then have "\y\S n. dist y l < e" using N max.cobounded2 by blast } then have "l \ S n" using closed_approachable[of "S n" l] assms(1) by auto } then show ?thesis using that by blast qed text \Strengthen it to the intersection actually being a singleton.\ lemma decreasing_closed_nest_sing: fixes S :: "nat \ 'a::complete_space set" assumes "\n. closed(S n)" "\n. S n \ {}" "\m n. m \ n \ S n \ S m" "\e. e>0 \ \n. \x \ (S n). \ y\(S n). dist x y < e" shows "\a. \(range S) = {a}" proof - obtain a where a: "\n. a \ S n" using decreasing_closed_nest[of S] using assms by auto { fix b assume b: "b \ \(range S)" { fix e :: real assume "e > 0" then have "dist a b < e" using assms(4) and b and a by blast } then have "dist a b = 0" by (metis dist_eq_0_iff dist_nz less_le) } with a have "\(range S) = {a}" unfolding image_def by auto then show ?thesis .. qed section\<^marker>\tag unimportant\ \Making a continuous function avoid some value in a neighbourhood\ lemma continuous_within_avoid: fixes f :: "'a::metric_space \ 'b::t1_space" assumes "continuous (at x within s) f" and "f x \ a" shows "\e>0. \y \ s. dist x y < e --> f y \ a" proof - obtain U where "open U" and "f x \ U" and "a \ U" using t1_space [OF \f x \ a\] by fast have "(f \ f x) (at x within s)" using assms(1) by (simp add: continuous_within) then have "eventually (\y. f y \ U) (at x within s)" using \open U\ and \f x \ U\ unfolding tendsto_def by fast then have "eventually (\y. f y \ a) (at x within s)" using \a \ U\ by (fast elim: eventually_mono) then show ?thesis using \f x \ a\ by (auto simp: dist_commute eventually_at) qed lemma continuous_at_avoid: fixes f :: "'a::metric_space \ 'b::t1_space" assumes "continuous (at x) f" and "f x \ a" shows "\e>0. \y. dist x y < e \ f y \ a" using assms continuous_within_avoid[of x UNIV f a] by simp lemma continuous_on_avoid: fixes f :: "'a::metric_space \ 'b::t1_space" assumes "continuous_on s f" and "x \ s" and "f x \ a" shows "\e>0. \y \ s. dist x y < e \ f y \ a" using assms(1)[unfolded continuous_on_eq_continuous_within, THEN bspec[where x=x], OF assms(2)] continuous_within_avoid[of x s f a] using assms(3) by auto lemma continuous_on_open_avoid: fixes f :: "'a::metric_space \ 'b::t1_space" assumes "continuous_on s f" and "open s" and "x \ s" and "f x \ a" shows "\e>0. \y. dist x y < e \ f y \ a" using assms(1)[unfolded continuous_on_eq_continuous_at[OF assms(2)], THEN bspec[where x=x], OF assms(3)] using continuous_at_avoid[of x f a] assms(4) by auto section \Consequences for Real Numbers\ lemma closed_contains_Inf: fixes S :: "real set" shows "S \ {} \ bdd_below S \ closed S \ Inf S \ S" by (metis closure_contains_Inf closure_closed) lemma closed_subset_contains_Inf: fixes A C :: "real set" shows "closed C \ A \ C \ A \ {} \ bdd_below A \ Inf A \ C" by (metis closure_contains_Inf closure_minimal subset_eq) lemma closed_contains_Sup: fixes S :: "real set" shows "S \ {} \ bdd_above S \ closed S \ Sup S \ S" by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup) lemma closed_subset_contains_Sup: fixes A C :: "real set" shows "closed C \ A \ C \ A \ {} \ bdd_above A \ Sup A \ C" by (metis closure_contains_Sup closure_minimal subset_eq) lemma atLeastAtMost_subset_contains_Inf: fixes A :: "real set" and a b :: real shows "A \ {} \ a \ b \ A \ {a..b} \ Inf A \ {a..b}" by (rule closed_subset_contains_Inf) (auto intro: closed_real_atLeastAtMost intro!: bdd_belowI[of A a]) lemma bounded_real: "bounded (S::real set) \ (\a. \x\S. \x\ \ a)" by (simp add: bounded_iff) lemma bounded_imp_bdd_above: "bounded S \ bdd_above (S :: real set)" by (auto simp: bounded_def bdd_above_def dist_real_def) (metis abs_le_D1 abs_minus_commute diff_le_eq) lemma bounded_imp_bdd_below: "bounded S \ bdd_below (S :: real set)" by (auto simp: bounded_def bdd_below_def dist_real_def) (metis abs_le_D1 add.commute diff_le_eq) lemma bounded_norm_le_SUP_norm: "bounded (range f) \ norm (f x) \ (SUP x. norm (f x))" by (auto intro!: cSUP_upper bounded_imp_bdd_above simp: bounded_norm_comp) lemma bounded_has_Sup: fixes S :: "real set" assumes "bounded S" and "S \ {}" shows "\x\S. x \ Sup S" and "\b. (\x\S. x \ b) \ Sup S \ b" proof show "\b. (\x\S. x \ b) \ Sup S \ b" using assms by (metis cSup_least) qed (metis cSup_upper assms(1) bounded_imp_bdd_above) lemma Sup_insert: fixes S :: "real set" shows "bounded S \ Sup (insert x S) = (if S = {} then x else max x (Sup S))" by (auto simp: bounded_imp_bdd_above sup_max cSup_insert_If) lemma bounded_has_Inf: fixes S :: "real set" assumes "bounded S" and "S \ {}" shows "\x\S. x \ Inf S" and "\b. (\x\S. x \ b) \ Inf S \ b" proof show "\b. (\x\S. x \ b) \ Inf S \ b" using assms by (metis cInf_greatest) qed (metis cInf_lower assms(1) bounded_imp_bdd_below) lemma Inf_insert: fixes S :: "real set" shows "bounded S \ Inf (insert x S) = (if S = {} then x else min x (Inf S))" by (auto simp: bounded_imp_bdd_below inf_min cInf_insert_If) lemma open_real: fixes s :: "real set" shows "open s \ (\x \ s. \e>0. \x'. \x' - x\ < e --> x' \ s)" unfolding open_dist dist_norm by simp lemma islimpt_approachable_real: fixes s :: "real set" shows "x islimpt s \ (\e>0. \x'\ s. x' \ x \ \x' - x\ < e)" unfolding islimpt_approachable dist_norm by simp lemma closed_real: fixes s :: "real set" shows "closed s \ (\x. (\e>0. \x' \ s. x' \ x \ \x' - x\ < e) \ x \ s)" unfolding closed_limpt islimpt_approachable dist_norm by simp lemma continuous_at_real_range: fixes f :: "'a::real_normed_vector \ real" shows "continuous (at x) f \ (\e>0. \d>0. \x'. norm(x' - x) < d --> \f x' - f x\ < e)" by (metis (mono_tags, opaque_lifting) LIM_eq continuous_within norm_eq_zero real_norm_def right_minus_eq) lemma continuous_on_real_range: fixes f :: "'a::real_normed_vector \ real" shows "continuous_on s f \ (\x \ s. \e>0. \d>0. (\x' \ s. norm(x' - x) < d \ \f x' - f x\ < e))" unfolding continuous_on_iff dist_norm by simp lemma continuous_on_closed_Collect_le: fixes f g :: "'a::topological_space \ real" assumes f: "continuous_on s f" and g: "continuous_on s g" and s: "closed s" shows "closed {x \ s. f x \ g x}" proof - have "closed ((\x. g x - f x) -` {0..} \ s)" using closed_real_atLeast continuous_on_diff [OF g f] by (simp add: continuous_on_closed_vimage [OF s]) also have "((\x. g x - f x) -` {0..} \ s) = {x\s. f x \ g x}" by auto finally show ?thesis . qed lemma continuous_le_on_closure: fixes a::real assumes f: "continuous_on (closure s) f" and x: "x \ closure(s)" and xlo: "\x. x \ s ==> f(x) \ a" shows "f(x) \ a" using image_closure_subset [OF f, where T=" {x. x \ a}" ] assms continuous_on_closed_Collect_le[of "UNIV" "\x. x" "\x. a"] by auto lemma continuous_ge_on_closure: fixes a::real assumes f: "continuous_on (closure s) f" and x: "x \ closure(s)" and xlo: "\x. x \ s ==> f(x) \ a" shows "f(x) \ a" using image_closure_subset [OF f, where T=" {x. a \ x}"] assms continuous_on_closed_Collect_le[of "UNIV" "\x. a" "\x. x"] by auto section\The infimum of the distance between two sets\ definition\<^marker>\tag important\ setdist :: "'a::metric_space set \ 'a set \ real" where "setdist s t \ (if s = {} \ t = {} then 0 else Inf {dist x y| x y. x \ s \ y \ t})" lemma setdist_empty1 [simp]: "setdist {} t = 0" by (simp add: setdist_def) lemma setdist_empty2 [simp]: "setdist t {} = 0" by (simp add: setdist_def) lemma setdist_pos_le [simp]: "0 \ setdist s t" by (auto simp: setdist_def ex_in_conv [symmetric] intro: cInf_greatest) lemma le_setdistI: assumes "s \ {}" "t \ {}" "\x y. \x \ s; y \ t\ \ d \ dist x y" shows "d \ setdist s t" using assms by (auto simp: setdist_def Set.ex_in_conv [symmetric] intro: cInf_greatest) lemma setdist_le_dist: "\x \ s; y \ t\ \ setdist s t \ dist x y" unfolding setdist_def by (auto intro!: bdd_belowI [where m=0] cInf_lower) lemma le_setdist_iff: "d \ setdist S T \ (\x \ S. \y \ T. d \ dist x y) \ (S = {} \ T = {} \ d \ 0)" by (smt (verit) le_setdistI setdist_def setdist_le_dist) lemma setdist_ltE: assumes "setdist S T < b" "S \ {}" "T \ {}" obtains x y where "x \ S" "y \ T" "dist x y < b" using assms by (auto simp: not_le [symmetric] le_setdist_iff) lemma setdist_refl: "setdist S S = 0" by (metis dist_eq_0_iff ex_in_conv order_antisym setdist_def setdist_le_dist setdist_pos_le) lemma setdist_sym: "setdist S T = setdist T S" by (force simp: setdist_def dist_commute intro!: arg_cong [where f=Inf]) lemma setdist_triangle: "setdist S T \ setdist S {a} + setdist {a} T" proof (cases "S = {} \ T = {}") case True then show ?thesis using setdist_pos_le by fastforce next case False then have "\x. x \ S \ setdist S T - dist x a \ setdist {a} T" using dist_self dist_triangle3 empty_not_insert le_setdist_iff setdist_le_dist singleton_iff by (smt (verit, best) dist_self dist_triangle3 empty_not_insert le_setdist_iff setdist_le_dist singleton_iff) then have "setdist S T - setdist {a} T \ setdist S {a}" using False by (fastforce intro: le_setdistI) then show ?thesis by (simp add: algebra_simps) qed lemma setdist_singletons [simp]: "setdist {x} {y} = dist x y" by (simp add: setdist_def) lemma setdist_Lipschitz: "\setdist {x} S - setdist {y} S\ \ dist x y" apply (subst setdist_singletons [symmetric]) by (metis abs_diff_le_iff diff_le_eq setdist_triangle setdist_sym) lemma continuous_at_setdist [continuous_intros]: "continuous (at x) (\y. (setdist {y} S))" by (force simp: continuous_at_eps_delta dist_real_def intro: le_less_trans [OF setdist_Lipschitz]) lemma continuous_on_setdist [continuous_intros]: "continuous_on T (\y. (setdist {y} S))" by (metis continuous_at_setdist continuous_at_imp_continuous_on) lemma uniformly_continuous_on_setdist: "uniformly_continuous_on T (\y. (setdist {y} S))" by (force simp: uniformly_continuous_on_def dist_real_def intro: le_less_trans [OF setdist_Lipschitz]) lemma setdist_subset_right: "\T \ {}; T \ u\ \ setdist S u \ setdist S T" by (smt (verit, best) in_mono le_setdist_iff) lemma setdist_subset_left: "\S \ {}; S \ T\ \ setdist T u \ setdist S u" by (metis setdist_subset_right setdist_sym) lemma setdist_closure_1 [simp]: "setdist (closure S) T = setdist S T" proof (cases "S = {} \ T = {}") case True then show ?thesis by force next case False { fix y assume "y \ T" have "continuous_on (closure S) (\a. dist a y)" by (auto simp: continuous_intros dist_norm) then have *: "\x. x \ closure S \ setdist S T \ dist x y" by (fast intro: setdist_le_dist \y \ T\ continuous_ge_on_closure) } then show ?thesis by (metis False antisym closure_eq_empty closure_subset le_setdist_iff setdist_subset_left) qed lemma setdist_closure_2 [simp]: "setdist T (closure S) = setdist T S" by (metis setdist_closure_1 setdist_sym) lemma setdist_eq_0I: "\x \ S; x \ T\ \ setdist S T = 0" by (metis antisym dist_self setdist_le_dist setdist_pos_le) lemma setdist_unique: "\a \ S; b \ T; \x y. x \ S \ y \ T ==> dist a b \ dist x y\ \ setdist S T = dist a b" by (force simp add: setdist_le_dist le_setdist_iff intro: antisym) lemma setdist_le_sing: "x \ S ==> setdist S T \ setdist {x} T" using setdist_subset_left by auto lemma infdist_eq_setdist: "infdist x A = setdist {x} A" by (simp add: infdist_def setdist_def Setcompr_eq_image) lemma setdist_eq_infdist: "setdist A B = (if A = {} then 0 else INF a\A. infdist a B)" proof - have "Inf {dist x y |x y. x \ A \ y \ B} = (INF x\A. Inf (dist x ` B))" if "b \ B" "a \ A" for a b proof (rule order_antisym) have "Inf {dist x y |x y. x \ A \ y \ B} \ Inf (dist x ` B)" if "b \ B" "a \ A" "x \ A" for x proof - have "\b'. b' \ B \ Inf {dist x y |x y. x \ A \ y \ B} \ dist x b'" by (metis (mono_tags, lifting) ex_in_conv setdist_def setdist_le_dist that(3)) then show ?thesis by (smt (verit) cINF_greatest ex_in_conv \b \ B\) qed then show "Inf {dist x y |x y. x \ A \ y \ B} \ (INF x\A. Inf (dist x ` B))" by (metis (mono_tags, lifting) cINF_greatest emptyE that) next have *: "\x y. \b \ B; a \ A; x \ A; y \ B\ \ \a\A. Inf (dist a ` B) \ dist x y" by (meson bdd_below_image_dist cINF_lower) show "(INF x\A. Inf (dist x ` B)) \ Inf {dist x y |x y. x \ A \ y \ B}" proof (rule conditionally_complete_lattice_class.cInf_mono) show "bdd_below ((\x. Inf (dist x ` B)) ` A)" by (metis (no_types, lifting) bdd_belowI2 ex_in_conv infdist_def infdist_nonneg that(1)) qed (use that in \auto simp: *\) qed then show ?thesis by (auto simp: setdist_def infdist_def) qed lemma infdist_mono: assumes "A \ B" "A \ {}" shows "infdist x B \ infdist x A" by (simp add: assms infdist_eq_setdist setdist_subset_right) lemma infdist_singleton [simp]: "infdist x {y} = dist x y" by (simp add: infdist_eq_setdist) proposition setdist_attains_inf: assumes "compact B" "B \ {}" obtains y where "y \ B" "setdist A B = infdist y A" proof (cases "A = {}") case True then show thesis by (metis assms diameter_compact_attained infdist_def setdist_def that) next case False obtain y where "y \ B" and min: "\y'. y' \ B \ infdist y A \ infdist y' A" by (metis continuous_attains_inf [OF assms continuous_on_infdist] continuous_on_id) show thesis proof have "setdist A B = (INF y\B. infdist y A)" by (metis \B \ {}\ setdist_eq_infdist setdist_sym) also have "\ = infdist y A" proof (rule order_antisym) show "(INF y\B. infdist y A) \ infdist y A" by (meson \y \ B\ bdd_belowI2 cInf_lower image_eqI infdist_nonneg) next show "infdist y A \ (INF y\B. infdist y A)" by (simp add: \B \ {}\ cINF_greatest min) qed finally show "setdist A B = infdist y A" . qed (fact \y \ B\) qed section \Diameter Lemma\ text \taken from the AFP entry Martingales, by Ata Keskin, TU München\ lemma diameter_comp_strict_mono: fixes s :: "nat \ 'a :: metric_space" assumes "strict_mono r" "bounded {s i |i. r n \ i}" shows "diameter {s (r i) | i. n \ i} \ diameter {s i | i. r n \ i}" proof (rule diameter_subset) show "{s (r i) | i. n \ i} \ {s i | i. r n \ i}" using assms(1) monotoneD strict_mono_mono by fastforce qed (intro assms(2)) lemma diameter_bounded_bound': fixes S :: "'a :: metric_space set" assumes S: "bdd_above (case_prod dist ` (S\S))" and "x \ S" "y \ S" shows "dist x y \ diameter S" proof - have "(x,y) \ S\S" using assms by auto then have "dist x y \ (SUP (x,y)\S\S. dist x y)" by (metis S cSUP_upper case_prod_conv) with \x \ S\ show ?thesis by (auto simp: diameter_def) qed lemma bounded_imp_dist_bounded: assumes "bounded (range s)" shows "bounded ((\(i, j). dist (s i) (s j)) ` ({n..} \ {n..}))" using bounded_dist_comp[OF bounded_fst bounded_snd, OF bounded_Times(1,1)[OF assms(1,1)]] by (rule bounded_subset, force) text \A sequence is Cauchy, if and only if it is bounded and its diameter tends to zero. The diameter is well-defined only if the sequence is bounded.\ lemma cauchy_iff_diameter_tends_to_zero_and_bounded: fixes s :: "nat \ 'a :: metric_space" shows "Cauchy s \ ((\n. diameter {s i | i. i \ n}) \ 0 \ bounded (range s))" proof - have "{s i |i. N \ i} \ {}" for N by blast hence diameter_SUP: "diameter {s i |i. N \ i} = (SUP (i, j) \ {N..} \ {N..}. dist (s i) (s j))" for N unfolding diameter_def by (auto intro!: arg_cong[of _ _ Sup]) show ?thesis proof (intro iffI) assume asm: "Cauchy s" have "\N. \n\N. norm (diameter {s i |i. n \ i}) < e" if e_pos: "e > 0" for e proof - obtain N where dist_less: "dist (s n) (s m) < (1/2) * e" if "n \ N" "m \ N" for n m using asm e_pos by (metis Cauchy_def mult_pos_pos zero_less_divide_iff zero_less_numeral zero_less_one) { fix r assume "r \ N" hence "dist (s n) (s m) < (1/2) * e" if "n \ r" "m \ r" for n m using dist_less that by simp hence "(SUP (i, j) \ {r..} \ {r..}. dist (s i) (s j)) \ (1/2) * e" by (intro cSup_least) fastforce+ also have "... < e" using e_pos by simp finally have "diameter {s i |i. r \ i} < e" using diameter_SUP by presburger } moreover have "diameter {s i |i. r \ i} \ 0" for r unfolding diameter_SUP using bounded_imp_dist_bounded[OF cauchy_imp_bounded, THEN bounded_imp_bdd_above, OF asm] by (intro cSup_upper2, auto) ultimately show ?thesis by auto qed thus "(\n. diameter {s i |i. n \ i}) \ 0 \ bounded (range s)" using cauchy_imp_bounded[OF asm] by (simp add: LIMSEQ_iff) next assume asm: "(\n. diameter {s i |i. n \ i}) \ 0 \ bounded (range s)" have "\N. \n\N. \m\N. dist (s n) (s m) < e" if e_pos: "e > 0" for e proof - obtain N where diam_less: "diameter {s i |i. r \ i} < e" if "r \ N" for r using LIMSEQ_D asm(1) e_pos by fastforce { fix n m assume "n \ N" "m \ N" hence "dist (s n) (s m) < e" using cSUP_lessD[OF bounded_imp_dist_bounded[THEN bounded_imp_bdd_above], OF _ diam_less[unfolded diameter_SUP]] asm by auto } thus ?thesis by blast qed then show "Cauchy s" by (simp add: Cauchy_def) qed qed end diff --git a/src/HOL/Analysis/Set_Integral.thy b/src/HOL/Analysis/Set_Integral.thy --- a/src/HOL/Analysis/Set_Integral.thy +++ b/src/HOL/Analysis/Set_Integral.thy @@ -1,1951 +1,1952 @@ (* Title: HOL/Analysis/Set_Integral.thy Author: Jeremy Avigad (CMU), Johannes Hölzl (TUM), Luke Serafin (CMU) Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr + Author: Ata Keskin, TU Muenchen Notation and useful facts for working with integrals over a set. TODO: keep all these? Need unicode translations as well. *) chapter \Integrals over a Set\ theory Set_Integral imports Radon_Nikodym begin section \Notation\ definition\<^marker>\tag important\ "set_borel_measurable M A f \ (\x. indicator A x *\<^sub>R f x) \ borel_measurable M" definition\<^marker>\tag important\ "set_integrable M A f \ integrable M (\x. indicator A x *\<^sub>R f x)" definition\<^marker>\tag important\ "set_lebesgue_integral M A f \ lebesgue_integral M (\x. indicator A x *\<^sub>R f x)" syntax "_ascii_set_lebesgue_integral" :: "pttrn \ 'a set \ 'a measure \ real \ real" ("(4LINT (_):(_)/|(_)./ _)" [0,0,0,10] 10) translations "LINT x:A|M. f" == "CONST set_lebesgue_integral M A (\x. f)" (* Notation for integration wrt lebesgue measure on the reals: LBINT x. f LBINT x : A. f TODO: keep all these? Need unicode. *) syntax "_lebesgue_borel_integral" :: "pttrn \ real \ real" ("(2LBINT _./ _)" [0,10] 10) syntax "_set_lebesgue_borel_integral" :: "pttrn \ real set \ real \ real" ("(3LBINT _:_./ _)" [0,0,10] 10) section \Basic properties\ (* lemma indicator_abs_eq: "\A x. \indicator A x\ = ((indicator A x) :: real)" by (auto simp add: indicator_def) *) lemma set_integrable_cong: assumes "M = M'" "A = A'" "\x. x \ A \ f x = f' x" shows "set_integrable M A f = set_integrable M' A' f'" proof - have "(\x. indicator A x *\<^sub>R f x) = (\x. indicator A' x *\<^sub>R f' x)" using assms by (auto simp: indicator_def of_bool_def) thus ?thesis by (simp add: set_integrable_def assms) qed lemma set_borel_measurable_sets: fixes f :: "_ \ _::real_normed_vector" assumes "set_borel_measurable M X f" "B \ sets borel" "X \ sets M" shows "f -` B \ X \ sets M" proof - have "f \ borel_measurable (restrict_space M X)" using assms unfolding set_borel_measurable_def by (subst borel_measurable_restrict_space_iff) auto then have "f -` B \ space (restrict_space M X) \ sets (restrict_space M X)" by (rule measurable_sets) fact with \X \ sets M\ show ?thesis by (subst (asm) sets_restrict_space_iff) (auto simp: space_restrict_space) qed lemma set_integrable_bound: fixes f :: "'a \ 'b::{banach, second_countable_topology}" and g :: "'a \ 'c::{banach, second_countable_topology}" assumes "set_integrable M A f" "set_borel_measurable M A g" assumes "AE x in M. x \ A \ norm (g x) \ norm (f x)" shows "set_integrable M A g" unfolding set_integrable_def proof (rule Bochner_Integration.integrable_bound) from assms(1) show "integrable M (\x. indicator A x *\<^sub>R f x)" by (simp add: set_integrable_def) from assms(2) show "(\x. indicat_real A x *\<^sub>R g x) \ borel_measurable M" by (simp add: set_borel_measurable_def) from assms(3) show "AE x in M. norm (indicat_real A x *\<^sub>R g x) \ norm (indicat_real A x *\<^sub>R f x)" by eventually_elim (simp add: indicator_def) qed lemma set_lebesgue_integral_zero [simp]: "set_lebesgue_integral M A (\x. 0) = 0" by (auto simp: set_lebesgue_integral_def) lemma set_lebesgue_integral_cong: assumes "A \ sets M" and "\x. x \ A \ f x = g x" shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)" unfolding set_lebesgue_integral_def using assms by (metis indicator_simps(2) real_vector.scale_zero_left) lemma set_lebesgue_integral_cong_AE: assumes [measurable]: "A \ sets M" "f \ borel_measurable M" "g \ borel_measurable M" assumes "AE x \ A in M. f x = g x" shows "(LINT x:A|M. f x) = (LINT x:A|M. g x)" proof- have "AE x in M. indicator A x *\<^sub>R f x = indicator A x *\<^sub>R g x" using assms by auto thus ?thesis unfolding set_lebesgue_integral_def by (intro integral_cong_AE) auto qed lemma set_integrable_cong_AE: "f \ borel_measurable M \ g \ borel_measurable M \ AE x \ A in M. f x = g x \ A \ sets M \ set_integrable M A f = set_integrable M A g" unfolding set_integrable_def by (rule integrable_cong_AE) auto lemma set_integrable_subset: fixes M A B and f :: "_ \ _ :: {banach, second_countable_topology}" assumes "set_integrable M A f" "B \ sets M" "B \ A" shows "set_integrable M B f" proof - have "set_integrable M B (\x. indicator A x *\<^sub>R f x)" using assms integrable_mult_indicator set_integrable_def by blast with \B \ A\ show ?thesis unfolding set_integrable_def by (simp add: indicator_inter_arith[symmetric] Int_absorb2) qed lemma set_integrable_restrict_space: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes f: "set_integrable M S f" and T: "T \ sets (restrict_space M S)" shows "set_integrable M T f" proof - obtain T' where T_eq: "T = S \ T'" and "T' \ sets M" using T by (auto simp: sets_restrict_space) have \integrable M (\x. indicator T' x *\<^sub>R (indicator S x *\<^sub>R f x))\ using \T' \ sets M\ f integrable_mult_indicator set_integrable_def by blast then show ?thesis unfolding set_integrable_def unfolding T_eq indicator_inter_arith by (simp add: ac_simps) qed (* TODO: integral_cmul_indicator should be named set_integral_const *) (* TODO: borel_integrable_atLeastAtMost should be named something like set_integrable_Icc_isCont *) lemma set_integral_scaleR_left: assumes "A \ sets M" "c \ 0 \ integrable M f" shows "(LINT t:A|M. f t *\<^sub>R c) = (LINT t:A|M. f t) *\<^sub>R c" unfolding set_lebesgue_integral_def using integrable_mult_indicator[OF assms] by (subst integral_scaleR_left[symmetric], auto) lemma set_integral_scaleR_right [simp]: "(LINT t:A|M. a *\<^sub>R f t) = a *\<^sub>R (LINT t:A|M. f t)" unfolding set_lebesgue_integral_def by (subst integral_scaleR_right[symmetric]) (auto intro!: Bochner_Integration.integral_cong) lemma set_integral_mult_right [simp]: fixes a :: "'a::{real_normed_field, second_countable_topology}" shows "(LINT t:A|M. a * f t) = a * (LINT t:A|M. f t)" unfolding set_lebesgue_integral_def by (subst integral_mult_right_zero[symmetric]) auto lemma set_integral_mult_left [simp]: fixes a :: "'a::{real_normed_field, second_countable_topology}" shows "(LINT t:A|M. f t * a) = (LINT t:A|M. f t) * a" unfolding set_lebesgue_integral_def by (subst integral_mult_left_zero[symmetric]) auto lemma set_integral_divide_zero [simp]: fixes a :: "'a::{real_normed_field, field, second_countable_topology}" shows "(LINT t:A|M. f t / a) = (LINT t:A|M. f t) / a" unfolding set_lebesgue_integral_def by (subst integral_divide_zero[symmetric], intro Bochner_Integration.integral_cong) (auto split: split_indicator) lemma set_integrable_scaleR_right [simp, intro]: shows "(a \ 0 \ set_integrable M A f) \ set_integrable M A (\t. a *\<^sub>R f t)" unfolding set_integrable_def unfolding scaleR_left_commute by (rule integrable_scaleR_right) lemma set_integrable_scaleR_left [simp, intro]: fixes a :: "_ :: {banach, second_countable_topology}" shows "(a \ 0 \ set_integrable M A f) \ set_integrable M A (\t. f t *\<^sub>R a)" unfolding set_integrable_def using integrable_scaleR_left[of a M "\x. indicator A x *\<^sub>R f x"] by simp lemma set_integrable_mult_right [simp, intro]: fixes a :: "'a::{real_normed_field, second_countable_topology}" shows "(a \ 0 \ set_integrable M A f) \ set_integrable M A (\t. a * f t)" unfolding set_integrable_def using integrable_mult_right[of a M "\x. indicator A x *\<^sub>R f x"] by simp lemma set_integrable_mult_right_iff [simp]: fixes a :: "'a::{real_normed_field, second_countable_topology}" assumes "a \ 0" shows "set_integrable M A (\t. a * f t) \ set_integrable M A f" proof assume "set_integrable M A (\t. a * f t)" then have "set_integrable M A (\t. 1/a * (a * f t))" using set_integrable_mult_right by blast then show "set_integrable M A f" using assms by auto qed auto lemma set_integrable_mult_left [simp, intro]: fixes a :: "'a::{real_normed_field, second_countable_topology}" shows "(a \ 0 \ set_integrable M A f) \ set_integrable M A (\t. f t * a)" unfolding set_integrable_def using integrable_mult_left[of a M "\x. indicator A x *\<^sub>R f x"] by simp lemma set_integrable_mult_left_iff [simp]: fixes a :: "'a::{real_normed_field, second_countable_topology}" assumes "a \ 0" shows "set_integrable M A (\t. f t * a) \ set_integrable M A f" using assms by (subst set_integrable_mult_right_iff [symmetric]) (auto simp: mult.commute) lemma set_integrable_divide [simp, intro]: fixes a :: "'a::{real_normed_field, field, second_countable_topology}" assumes "a \ 0 \ set_integrable M A f" shows "set_integrable M A (\t. f t / a)" proof - have "integrable M (\x. indicator A x *\<^sub>R f x / a)" using assms unfolding set_integrable_def by (rule integrable_divide_zero) also have "(\x. indicator A x *\<^sub>R f x / a) = (\x. indicator A x *\<^sub>R (f x / a))" by (auto split: split_indicator) finally show ?thesis unfolding set_integrable_def . qed lemma set_integrable_mult_divide_iff [simp]: fixes a :: "'a::{real_normed_field, second_countable_topology}" assumes "a \ 0" shows "set_integrable M A (\t. f t / a) \ set_integrable M A f" by (simp add: divide_inverse assms) lemma set_integral_add [simp, intro]: fixes f g :: "_ \ _ :: {banach, second_countable_topology}" assumes "set_integrable M A f" "set_integrable M A g" shows "set_integrable M A (\x. f x + g x)" and "(LINT x:A|M. f x + g x) = (LINT x:A|M. f x) + (LINT x:A|M. g x)" using assms unfolding set_integrable_def set_lebesgue_integral_def by (simp_all add: scaleR_add_right) lemma set_integral_diff [simp, intro]: assumes "set_integrable M A f" "set_integrable M A g" shows "set_integrable M A (\x. f x - g x)" and "(LINT x:A|M. f x - g x) = (LINT x:A|M. f x) - (LINT x:A|M. g x)" using assms unfolding set_integrable_def set_lebesgue_integral_def by (simp_all add: scaleR_diff_right) lemma set_integral_uminus: "set_integrable M A f \ (LINT x:A|M. - f x) = - (LINT x:A|M. f x)" unfolding set_integrable_def set_lebesgue_integral_def by (subst integral_minus[symmetric]) simp_all lemma set_integral_complex_of_real: "(LINT x:A|M. complex_of_real (f x)) = of_real (LINT x:A|M. f x)" unfolding set_lebesgue_integral_def by (subst integral_complex_of_real[symmetric]) (auto intro!: Bochner_Integration.integral_cong split: split_indicator) lemma set_integral_mono: fixes f g :: "_ \ real" assumes "set_integrable M A f" "set_integrable M A g" "\x. x \ A \ f x \ g x" shows "(LINT x:A|M. f x) \ (LINT x:A|M. g x)" using assms unfolding set_integrable_def set_lebesgue_integral_def by (auto intro: integral_mono split: split_indicator) lemma set_integral_mono_AE: fixes f g :: "_ \ real" assumes "set_integrable M A f" "set_integrable M A g" "AE x \ A in M. f x \ g x" shows "(LINT x:A|M. f x) \ (LINT x:A|M. g x)" using assms unfolding set_integrable_def set_lebesgue_integral_def by (auto intro: integral_mono_AE split: split_indicator) lemma set_integrable_abs: "set_integrable M A f \ set_integrable M A (\x. \f x\ :: real)" using integrable_abs[of M "\x. f x * indicator A x"]unfolding set_integrable_def by (simp add: abs_mult ac_simps) lemma set_integrable_abs_iff: fixes f :: "_ \ real" shows "set_borel_measurable M A f \ set_integrable M A (\x. \f x\) = set_integrable M A f" unfolding set_integrable_def set_borel_measurable_def by (subst (2) integrable_abs_iff[symmetric]) (simp_all add: abs_mult ac_simps) lemma set_integrable_abs_iff': fixes f :: "_ \ real" shows "f \ borel_measurable M \ A \ sets M \ set_integrable M A (\x. \f x\) = set_integrable M A f" by (simp add: set_borel_measurable_def set_integrable_abs_iff) lemma set_integrable_discrete_difference: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes "countable X" assumes diff: "(A - B) \ (B - A) \ X" assumes "\x. x \ X \ emeasure M {x} = 0" "\x. x \ X \ {x} \ sets M" shows "set_integrable M A f \ set_integrable M B f" unfolding set_integrable_def proof (rule integrable_discrete_difference[where X=X]) show "\x. x \ space M \ x \ X \ indicator A x *\<^sub>R f x = indicator B x *\<^sub>R f x" using diff by (auto split: split_indicator) qed fact+ lemma set_integral_discrete_difference: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes "countable X" assumes diff: "(A - B) \ (B - A) \ X" assumes "\x. x \ X \ emeasure M {x} = 0" "\x. x \ X \ {x} \ sets M" shows "set_lebesgue_integral M A f = set_lebesgue_integral M B f" unfolding set_lebesgue_integral_def proof (rule integral_discrete_difference[where X=X]) show "\x. x \ space M \ x \ X \ indicator A x *\<^sub>R f x = indicator B x *\<^sub>R f x" using diff by (auto split: split_indicator) qed fact+ lemma set_integrable_Un: fixes f g :: "_ \ _ :: {banach, second_countable_topology}" assumes f_A: "set_integrable M A f" and f_B: "set_integrable M B f" and [measurable]: "A \ sets M" "B \ sets M" shows "set_integrable M (A \ B) f" proof - have "set_integrable M (A - B) f" using f_A by (rule set_integrable_subset) auto with f_B have "integrable M (\x. indicator (A - B) x *\<^sub>R f x + indicator B x *\<^sub>R f x)" unfolding set_integrable_def using integrable_add by blast then show ?thesis unfolding set_integrable_def by (rule integrable_cong[THEN iffD1, rotated 2]) (auto split: split_indicator) qed lemma set_integrable_empty [simp]: "set_integrable M {} f" by (auto simp: set_integrable_def) lemma set_integrable_UN: fixes f :: "_ \ _ :: {banach, second_countable_topology}" assumes "finite I" "\i. i\I \ set_integrable M (A i) f" "\i. i\I \ A i \ sets M" shows "set_integrable M (\i\I. A i) f" using assms by (induct I) (auto simp: set_integrable_Un sets.finite_UN) lemma set_integral_Un: fixes f :: "_ \ _ :: {banach, second_countable_topology}" assumes "A \ B = {}" and "set_integrable M A f" and "set_integrable M B f" shows "(LINT x:A\B|M. f x) = (LINT x:A|M. f x) + (LINT x:B|M. f x)" using assms unfolding set_integrable_def set_lebesgue_integral_def by (auto simp add: indicator_union_arith indicator_inter_arith[symmetric] scaleR_add_left) lemma set_integral_cong_set: fixes f :: "_ \ _ :: {banach, second_countable_topology}" assumes "set_borel_measurable M A f" "set_borel_measurable M B f" and ae: "AE x in M. x \ A \ x \ B" shows "(LINT x:B|M. f x) = (LINT x:A|M. f x)" unfolding set_lebesgue_integral_def proof (rule integral_cong_AE) show "AE x in M. indicator B x *\<^sub>R f x = indicator A x *\<^sub>R f x" using ae by (auto simp: subset_eq split: split_indicator) qed (use assms in \auto simp: set_borel_measurable_def\) proposition set_borel_measurable_subset: fixes f :: "_ \ _ :: {banach, second_countable_topology}" assumes [measurable]: "set_borel_measurable M A f" "B \ sets M" and "B \ A" shows "set_borel_measurable M B f" proof- have "set_borel_measurable M B (\x. indicator A x *\<^sub>R f x)" using assms unfolding set_borel_measurable_def using borel_measurable_indicator borel_measurable_scaleR by blast moreover have "(\x. indicator B x *\<^sub>R indicator A x *\<^sub>R f x) = (\x. indicator B x *\<^sub>R f x)" using \B \ A\ by (auto simp: fun_eq_iff split: split_indicator) ultimately show ?thesis unfolding set_borel_measurable_def by simp qed lemma set_integral_Un_AE: fixes f :: "_ \ _ :: {banach, second_countable_topology}" assumes ae: "AE x in M. \ (x \ A \ x \ B)" and [measurable]: "A \ sets M" "B \ sets M" and "set_integrable M A f" and "set_integrable M B f" shows "(LINT x:A\B|M. f x) = (LINT x:A|M. f x) + (LINT x:B|M. f x)" proof - have f: "set_integrable M (A \ B) f" by (intro set_integrable_Un assms) then have f': "set_borel_measurable M (A \ B) f" using integrable_iff_bounded set_borel_measurable_def set_integrable_def by blast have "(LINT x:A\B|M. f x) = (LINT x:(A - A \ B) \ (B - A \ B)|M. f x)" proof (rule set_integral_cong_set) show "AE x in M. (x \ A - A \ B \ (B - A \ B)) = (x \ A \ B)" using ae by auto show "set_borel_measurable M (A - A \ B \ (B - A \ B)) f" using f' by (rule set_borel_measurable_subset) auto qed fact also have "\ = (LINT x:(A - A \ B)|M. f x) + (LINT x:(B - A \ B)|M. f x)" by (auto intro!: set_integral_Un set_integrable_subset[OF f]) also have "\ = (LINT x:A|M. f x) + (LINT x:B|M. f x)" using ae by (intro arg_cong2[where f="(+)"] set_integral_cong_set) (auto intro!: set_borel_measurable_subset[OF f']) finally show ?thesis . qed lemma set_integral_finite_Union: fixes f :: "_ \ _ :: {banach, second_countable_topology}" assumes "finite I" "disjoint_family_on A I" and "\i. i \ I \ set_integrable M (A i) f" "\i. i \ I \ A i \ sets M" shows "(LINT x:(\i\I. A i)|M. f x) = (\i\I. LINT x:A i|M. f x)" using assms proof induction case (insert x F) then have "A x \ \(A ` F) = {}" by (meson disjoint_family_on_insert) with insert show ?case by (simp add: set_integral_Un set_integrable_Un set_integrable_UN disjoint_family_on_insert) qed (simp add: set_lebesgue_integral_def) (* TODO: find a better name? *) lemma pos_integrable_to_top: fixes l::real assumes "\i. A i \ sets M" "mono A" assumes nneg: "\x i. x \ A i \ 0 \ f x" and intgbl: "\i::nat. set_integrable M (A i) f" and lim: "(\i::nat. LINT x:A i|M. f x) \ l" shows "set_integrable M (\i. A i) f" unfolding set_integrable_def apply (rule integrable_monotone_convergence[where f = "\i::nat. \x. indicator (A i) x *\<^sub>R f x" and x = l]) apply (rule intgbl [unfolded set_integrable_def]) prefer 3 apply (rule lim [unfolded set_lebesgue_integral_def]) apply (rule AE_I2) using \mono A\ apply (auto simp: mono_def nneg split: split_indicator) [] proof (rule AE_I2) { fix x assume "x \ space M" show "(\i. indicator (A i) x *\<^sub>R f x) \ indicator (\i. A i) x *\<^sub>R f x" proof cases assume "\i. x \ A i" then obtain i where "x \ A i" .. then have "\\<^sub>F i in sequentially. x \ A i" using \x \ A i\ \mono A\ by (auto simp: eventually_sequentially mono_def) with eventually_mono have "\\<^sub>F i in sequentially. indicat_real (A i) x *\<^sub>R f x = indicat_real (\ (range A)) x *\<^sub>R f x" by fastforce then show ?thesis by (intro tendsto_eventually) qed auto } then show "(\x. indicator (\i. A i) x *\<^sub>R f x) \ borel_measurable M" apply (rule borel_measurable_LIMSEQ_real) apply assumption using intgbl set_integrable_def by blast qed text \Proof from Royden, \emph{Real Analysis}, p. 91.\ lemma lebesgue_integral_countable_add: fixes f :: "_ \ 'a :: {banach, second_countable_topology}" assumes meas[intro]: "\i::nat. A i \ sets M" and disj: "\i j. i \ j \ A i \ A j = {}" and intgbl: "set_integrable M (\i. A i) f" shows "(LINT x:(\i. A i)|M. f x) = (\i. (LINT x:(A i)|M. f x))" unfolding set_lebesgue_integral_def proof (subst integral_suminf[symmetric]) show int_A: "integrable M (\x. indicat_real (A i) x *\<^sub>R f x)" for i using intgbl unfolding set_integrable_def [symmetric] by (rule set_integrable_subset) auto { fix x assume "x \ space M" have "(\i. indicator (A i) x *\<^sub>R f x) sums (indicator (\i. A i) x *\<^sub>R f x)" by (intro sums_scaleR_left indicator_sums) fact } note sums = this have norm_f: "\i. set_integrable M (A i) (\x. norm (f x))" using int_A[THEN integrable_norm] unfolding set_integrable_def by auto show "AE x in M. summable (\i. norm (indicator (A i) x *\<^sub>R f x))" using disj by (intro AE_I2) (auto intro!: summable_mult2 sums_summable[OF indicator_sums]) show "summable (\i. LINT x|M. norm (indicator (A i) x *\<^sub>R f x))" proof (rule summableI_nonneg_bounded) fix n show "0 \ LINT x|M. norm (indicator (A n) x *\<^sub>R f x)" using norm_f by (auto intro!: integral_nonneg_AE) have "(\iR f x)) = (\i = set_lebesgue_integral M (\ix. norm (f x))" using norm_f by (subst set_integral_finite_Union) (auto simp: disjoint_family_on_def disj) also have "\ \ set_lebesgue_integral M (\i. A i) (\x. norm (f x))" using intgbl[unfolded set_integrable_def, THEN integrable_norm] norm_f unfolding set_lebesgue_integral_def set_integrable_def apply (intro integral_mono set_integrable_UN[of "{..iR f x)) \ set_lebesgue_integral M (\i. A i) (\x. norm (f x))" by simp qed show "LINT x|M. indicator (\(A ` UNIV)) x *\<^sub>R f x = LINT x|M. (\i. indicator (A i) x *\<^sub>R f x)" by (metis (no_types, lifting) integral_cong sums sums_unique) qed lemma set_integral_cont_up: fixes f :: "_ \ 'a :: {banach, second_countable_topology}" assumes [measurable]: "\i. A i \ sets M" and A: "incseq A" and intgbl: "set_integrable M (\i. A i) f" shows "(\i. LINT x:(A i)|M. f x) \ (LINT x:(\i. A i)|M. f x)" unfolding set_lebesgue_integral_def proof (intro integral_dominated_convergence[where w="\x. indicator (\i. A i) x *\<^sub>R norm (f x)"]) have int_A: "\i. set_integrable M (A i) f" using intgbl by (rule set_integrable_subset) auto show "\i. (\x. indicator (A i) x *\<^sub>R f x) \ borel_measurable M" using int_A integrable_iff_bounded set_integrable_def by blast show "(\x. indicator (\(A ` UNIV)) x *\<^sub>R f x) \ borel_measurable M" using integrable_iff_bounded intgbl set_integrable_def by blast show "integrable M (\x. indicator (\i. A i) x *\<^sub>R norm (f x))" using int_A intgbl integrable_norm unfolding set_integrable_def by fastforce { fix x i assume "x \ A i" with A have "(\xa. indicator (A xa) x::real) \ 1 \ (\xa. 1::real) \ 1" by (intro filterlim_cong refl) (fastforce simp: eventually_sequentially incseq_def subset_eq intro!: exI[of _ i]) } then show "AE x in M. (\i. indicator (A i) x *\<^sub>R f x) \ indicator (\i. A i) x *\<^sub>R f x" by (intro AE_I2 tendsto_intros) (auto split: split_indicator) qed (auto split: split_indicator) (* Can the int0 hypothesis be dropped? *) lemma set_integral_cont_down: fixes f :: "_ \ 'a :: {banach, second_countable_topology}" assumes [measurable]: "\i. A i \ sets M" and A: "decseq A" and int0: "set_integrable M (A 0) f" shows "(\i::nat. LINT x:(A i)|M. f x) \ (LINT x:(\i. A i)|M. f x)" unfolding set_lebesgue_integral_def proof (rule integral_dominated_convergence) have int_A: "\i. set_integrable M (A i) f" using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def) have "integrable M (\c. norm (indicat_real (A 0) c *\<^sub>R f c))" by (metis (no_types) int0 integrable_norm set_integrable_def) then show "integrable M (\x. indicator (A 0) x *\<^sub>R norm (f x))" by force have "set_integrable M (\i. A i) f" using int0 by (rule set_integrable_subset) (insert A, auto simp: decseq_def) with int_A show "(\x. indicat_real (\(A ` UNIV)) x *\<^sub>R f x) \ borel_measurable M" "\i. (\x. indicat_real (A i) x *\<^sub>R f x) \ borel_measurable M" by (auto simp: set_integrable_def) show "\i. AE x in M. norm (indicator (A i) x *\<^sub>R f x) \ indicator (A 0) x *\<^sub>R norm (f x)" using A by (auto split: split_indicator simp: decseq_def) { fix x i assume "x \ space M" "x \ A i" with A have "(\i. indicator (A i) x::real) \ 0 \ (\i. 0::real) \ 0" by (intro filterlim_cong refl) (auto split: split_indicator simp: eventually_sequentially decseq_def intro!: exI[of _ i]) } then show "AE x in M. (\i. indicator (A i) x *\<^sub>R f x) \ indicator (\i. A i) x *\<^sub>R f x" by (intro AE_I2 tendsto_intros) (auto split: split_indicator) qed lemma set_integral_at_point: fixes a :: real assumes "set_integrable M {a} f" and [simp]: "{a} \ sets M" and "(emeasure M) {a} \ \" shows "(LINT x:{a} | M. f x) = f a * measure M {a}" proof- have "set_lebesgue_integral M {a} f = set_lebesgue_integral M {a} (%x. f a)" by (intro set_lebesgue_integral_cong) simp_all then show ?thesis using assms unfolding set_lebesgue_integral_def by simp qed section \Complex integrals\ abbreviation complex_integrable :: "'a measure \ ('a \ complex) \ bool" where "complex_integrable M f \ integrable M f" abbreviation complex_lebesgue_integral :: "'a measure \ ('a \ complex) \ complex" ("integral\<^sup>C") where "integral\<^sup>C M f == integral\<^sup>L M f" syntax "_complex_lebesgue_integral" :: "pttrn \ complex \ 'a measure \ complex" ("\\<^sup>C _. _ \_" [0,0] 110) translations "\\<^sup>Cx. f \M" == "CONST complex_lebesgue_integral M (\x. f)" syntax "_ascii_complex_lebesgue_integral" :: "pttrn \ 'a measure \ real \ real" ("(3CLINT _|_. _)" [0,0,10] 10) translations "CLINT x|M. f" == "CONST complex_lebesgue_integral M (\x. f)" lemma complex_integrable_cnj [simp]: "complex_integrable M (\x. cnj (f x)) \ complex_integrable M f" proof assume "complex_integrable M (\x. cnj (f x))" then have "complex_integrable M (\x. cnj (cnj (f x)))" by (rule integrable_cnj) then show "complex_integrable M f" by simp qed simp lemma complex_of_real_integrable_eq: "complex_integrable M (\x. complex_of_real (f x)) \ integrable M f" proof assume "complex_integrable M (\x. complex_of_real (f x))" then have "integrable M (\x. Re (complex_of_real (f x)))" by (rule integrable_Re) then show "integrable M f" by simp qed simp abbreviation complex_set_integrable :: "'a measure \ 'a set \ ('a \ complex) \ bool" where "complex_set_integrable M A f \ set_integrable M A f" abbreviation complex_set_lebesgue_integral :: "'a measure \ 'a set \ ('a \ complex) \ complex" where "complex_set_lebesgue_integral M A f \ set_lebesgue_integral M A f" syntax "_ascii_complex_set_lebesgue_integral" :: "pttrn \ 'a set \ 'a measure \ real \ real" ("(4CLINT _:_|_. _)" [0,0,0,10] 10) translations "CLINT x:A|M. f" == "CONST complex_set_lebesgue_integral M A (\x. f)" lemma set_measurable_continuous_on_ivl: assumes "continuous_on {a..b} (f :: real \ real)" shows "set_borel_measurable borel {a..b} f" unfolding set_borel_measurable_def by (rule borel_measurable_continuous_on_indicator[OF _ assms]) simp section \NN Set Integrals\ text\This notation is from Sébastien Gouëzel: His use is not directly in line with the notations in this file, they are more in line with sum, and more readable he thinks.\ abbreviation "set_nn_integral M A f \ nn_integral M (\x. f x * indicator A x)" syntax "_set_nn_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal" ("(\\<^sup>+((_)\(_)./ _)/\_)" [0,0,0,110] 10) "_set_lebesgue_integral" :: "pttrn => 'a set => 'a measure => ereal => ereal" ("(\((_)\(_)./ _)/\_)" [0,0,0,110] 10) translations "\\<^sup>+x \ A. f \M" == "CONST set_nn_integral M A (\x. f)" "\x \ A. f \M" == "CONST set_lebesgue_integral M A (\x. f)" lemma set_nn_integral_cong: assumes "M = M'" "A = B" "\x. x \ space M \ A \ f x = g x" shows "set_nn_integral M A f = set_nn_integral M' B g" by (metis (mono_tags, lifting) IntI assms indicator_simps(2) mult_eq_0_iff nn_integral_cong) lemma nn_integral_disjoint_pair: assumes [measurable]: "f \ borel_measurable M" "B \ sets M" "C \ sets M" "B \ C = {}" shows "(\\<^sup>+x \ B \ C. f x \M) = (\\<^sup>+x \ B. f x \M) + (\\<^sup>+x \ C. f x \M)" proof - have mes: "\D. D \ sets M \ (\x. f x * indicator D x) \ borel_measurable M" by simp have pos: "\D. AE x in M. f x * indicator D x \ 0" using assms(2) by auto have "\x. f x * indicator (B \ C) x = f x * indicator B x + f x * indicator C x" using assms(4) by (auto split: split_indicator) then have "(\\<^sup>+x. f x * indicator (B \ C) x \M) = (\\<^sup>+x. f x * indicator B x + f x * indicator C x \M)" by simp also have "\ = (\\<^sup>+x. f x * indicator B x \M) + (\\<^sup>+x. f x * indicator C x \M)" by (rule nn_integral_add) (auto simp add: assms mes pos) finally show ?thesis by simp qed lemma nn_integral_disjoint_pair_countspace: assumes "B \ C = {}" shows "(\\<^sup>+x \ B \ C. f x \count_space UNIV) = (\\<^sup>+x \ B. f x \count_space UNIV) + (\\<^sup>+x \ C. f x \count_space UNIV)" by (rule nn_integral_disjoint_pair) (simp_all add: assms) lemma nn_integral_null_delta: assumes "A \ sets M" "B \ sets M" "(A - B) \ (B - A) \ null_sets M" shows "(\\<^sup>+x \ A. f x \M) = (\\<^sup>+x \ B. f x \M)" proof (rule nn_integral_cong_AE) have *: "AE a in M. a \ (A - B) \ (B - A)" using assms(3) AE_not_in by blast then show \AE x in M. f x * indicator A x = f x * indicator B x\ by auto qed proposition nn_integral_disjoint_family: assumes [measurable]: "f \ borel_measurable M" "\(n::nat). B n \ sets M" and "disjoint_family B" shows "(\\<^sup>+x \ (\n. B n). f x \M) = (\n. (\\<^sup>+x \ B n. f x \M))" proof - have "(\\<^sup>+ x. (\n. f x * indicator (B n) x) \M) = (\n. (\\<^sup>+ x. f x * indicator (B n) x \M))" by (rule nn_integral_suminf) simp moreover have "(\n. f x * indicator (B n) x) = f x * indicator (\n. B n) x" for x proof (cases) assume "x \ (\n. B n)" then obtain n where "x \ B n" by blast have a: "finite {n}" by simp have "\i. i \ n \ x \ B i" using \x \ B n\ assms(3) disjoint_family_on_def by (metis IntI UNIV_I empty_iff) then have "\i. i \ {n} \ indicator (B i) x = (0::ennreal)" using indicator_def by simp then have b: "\i. i \ {n} \ f x * indicator (B i) x = (0::ennreal)" by simp define h where "h = (\i. f x * indicator (B i) x)" then have "\i. i \ {n} \ h i = 0" using b by simp then have "(\i. h i) = (\i\{n}. h i)" by (metis sums_unique[OF sums_finite[OF a]]) then have "(\i. h i) = h n" by simp then have "(\n. f x * indicator (B n) x) = f x * indicator (B n) x" using h_def by simp then have "(\n. f x * indicator (B n) x) = f x" using \x \ B n\ indicator_def by simp then show ?thesis using \x \ (\n. B n)\ by auto next assume "x \ (\n. B n)" then have "\n. f x * indicator (B n) x = 0" by simp have "(\n. f x * indicator (B n) x) = 0" by (simp add: \\n. f x * indicator (B n) x = 0\) then show ?thesis using \x \ (\n. B n)\ by auto qed ultimately show ?thesis by simp qed lemma nn_set_integral_add: assumes [measurable]: "f \ borel_measurable M" "g \ borel_measurable M" "A \ sets M" shows "(\\<^sup>+x \ A. (f x + g x) \M) = (\\<^sup>+x \ A. f x \M) + (\\<^sup>+x \ A. g x \M)" proof - have "(\\<^sup>+x \ A. (f x + g x) \M) = (\\<^sup>+x. (f x * indicator A x + g x * indicator A x) \M)" by (auto simp add: indicator_def intro!: nn_integral_cong) also have "\ = (\\<^sup>+x. f x * indicator A x \M) + (\\<^sup>+x. g x * indicator A x \M)" apply (rule nn_integral_add) using assms(1) assms(2) by auto finally show ?thesis by simp qed lemma nn_set_integral_cong: assumes "AE x in M. f x = g x" shows "(\\<^sup>+x \ A. f x \M) = (\\<^sup>+x \ A. g x \M)" apply (rule nn_integral_cong_AE) using assms(1) by auto lemma nn_set_integral_set_mono: "A \ B \ (\\<^sup>+ x \ A. f x \M) \ (\\<^sup>+ x \ B. f x \M)" by (auto intro!: nn_integral_mono split: split_indicator) lemma nn_set_integral_mono: assumes [measurable]: "f \ borel_measurable M" "g \ borel_measurable M" "A \ sets M" and "AE x\A in M. f x \ g x" shows "(\\<^sup>+x \ A. f x \M) \ (\\<^sup>+x \ A. g x \M)" by (auto intro!: nn_integral_mono_AE split: split_indicator simp: assms) lemma nn_set_integral_space [simp]: shows "(\\<^sup>+ x \ space M. f x \M) = (\\<^sup>+x. f x \M)" by (metis (mono_tags, lifting) indicator_simps(1) mult.right_neutral nn_integral_cong) lemma nn_integral_count_compose_inj: assumes "inj_on g A" shows "(\\<^sup>+x \ A. f (g x) \count_space UNIV) = (\\<^sup>+y \ g`A. f y \count_space UNIV)" proof - have "(\\<^sup>+x \ A. f (g x) \count_space UNIV) = (\\<^sup>+x. f (g x) \count_space A)" by (auto simp add: nn_integral_count_space_indicator[symmetric]) also have "\ = (\\<^sup>+y. f y \count_space (g`A))" by (simp add: assms nn_integral_bij_count_space inj_on_imp_bij_betw) also have "\ = (\\<^sup>+y \ g`A. f y \count_space UNIV)" by (auto simp add: nn_integral_count_space_indicator[symmetric]) finally show ?thesis by simp qed lemma nn_integral_count_compose_bij: assumes "bij_betw g A B" shows "(\\<^sup>+x \ A. f (g x) \count_space UNIV) = (\\<^sup>+y \ B. f y \count_space UNIV)" proof - have "inj_on g A" using assms bij_betw_def by auto then have "(\\<^sup>+x \ A. f (g x) \count_space UNIV) = (\\<^sup>+y \ g`A. f y \count_space UNIV)" by (rule nn_integral_count_compose_inj) then show ?thesis using assms by (simp add: bij_betw_def) qed lemma set_integral_null_delta: fixes f::"_ \ _ :: {banach, second_countable_topology}" assumes [measurable]: "integrable M f" "A \ sets M" "B \ sets M" and null: "(A - B) \ (B - A) \ null_sets M" shows "(\x \ A. f x \M) = (\x \ B. f x \M)" proof (rule set_integral_cong_set) have *: "AE a in M. a \ (A - B) \ (B - A)" using null AE_not_in by blast then show "AE x in M. (x \ B) = (x \ A)" by auto qed (simp_all add: set_borel_measurable_def) lemma set_integral_space: assumes "integrable M f" shows "(\x \ space M. f x \M) = (\x. f x \M)" by (metis (no_types, lifting) indicator_simps(1) integral_cong scaleR_one set_lebesgue_integral_def) lemma null_if_pos_func_has_zero_nn_int: fixes f::"'a \ ennreal" assumes [measurable]: "f \ borel_measurable M" "A \ sets M" and "AE x\A in M. f x > 0" "(\\<^sup>+x\A. f x \M) = 0" shows "A \ null_sets M" proof - have "AE x in M. f x * indicator A x = 0" by (subst nn_integral_0_iff_AE[symmetric], auto simp add: assms(4)) then have "AE x\A in M. False" using assms(3) by auto then show "A \ null_sets M" using assms(2) by (simp add: AE_iff_null_sets) qed lemma null_if_pos_func_has_zero_int: assumes [measurable]: "integrable M f" "A \ sets M" and "AE x\A in M. f x > 0" "(\x\A. f x \M) = (0::real)" shows "A \ null_sets M" proof - have "AE x in M. indicator A x * f x = 0" apply (subst integral_nonneg_eq_0_iff_AE[symmetric]) using assms integrable_mult_indicator[OF \A \ sets M\ assms(1)] by (auto simp: set_lebesgue_integral_def) then have "AE x\A in M. f x = 0" by auto then have "AE x\A in M. False" using assms(3) by auto then show "A \ null_sets M" using assms(2) by (simp add: AE_iff_null_sets) qed text\The next lemma is a variant of \density_unique\. Note that it uses the notation for nonnegative set integrals introduced earlier.\ lemma (in sigma_finite_measure) density_unique2: assumes [measurable]: "f \ borel_measurable M" "f' \ borel_measurable M" assumes density_eq: "\A. A \ sets M \ (\\<^sup>+ x \ A. f x \M) = (\\<^sup>+ x \ A. f' x \M)" shows "AE x in M. f x = f' x" proof (rule density_unique) show "density M f = density M f'" by (intro measure_eqI) (auto simp: emeasure_density intro!: density_eq) qed (auto simp add: assms) text \The next lemma implies the same statement for Banach-space valued functions using Hahn-Banach theorem and linear forms. Since they are not yet easily available, I only formulate it for real-valued functions.\ lemma density_unique_real: fixes f f'::"_ \ real" assumes M[measurable]: "integrable M f" "integrable M f'" assumes density_eq: "\A. A \ sets M \ (\x \ A. f x \M) = (\x \ A. f' x \M)" shows "AE x in M. f x = f' x" proof - define A where "A = {x \ space M. f x < f' x}" then have [measurable]: "A \ sets M" by simp have "(\x \ A. (f' x - f x) \M) = (\x \ A. f' x \M) - (\x \ A. f x \M)" using \A \ sets M\ M integrable_mult_indicator set_integrable_def by blast then have "(\x \ A. (f' x - f x) \M) = 0" using assms(3) by simp then have "A \ null_sets M" using A_def null_if_pos_func_has_zero_int[where ?f = "\x. f' x - f x" and ?A = A] assms by auto then have "AE x in M. x \ A" by (simp add: AE_not_in) then have *: "AE x in M. f' x \ f x" unfolding A_def by auto define B where "B = {x \ space M. f' x < f x}" then have [measurable]: "B \ sets M" by simp have "(\x \ B. (f x - f' x) \M) = (\x \ B. f x \M) - (\x \ B. f' x \M)" using \B \ sets M\ M integrable_mult_indicator set_integrable_def by blast then have "(\x \ B. (f x - f' x) \M) = 0" using assms(3) by simp then have "B \ null_sets M" using B_def null_if_pos_func_has_zero_int[where ?f = "\x. f x - f' x" and ?A = B] assms by auto then have "AE x in M. x \ B" by (simp add: AE_not_in) then have "AE x in M. f' x \ f x" unfolding B_def by auto then show ?thesis using * by auto qed section \Scheffé's lemma\ text \The next lemma shows that \L\<^sup>1\ convergence of a sequence of functions follows from almost everywhere convergence and the weaker condition of the convergence of the integrated norms (or even just the nontrivial inequality about them). Useful in a lot of contexts! This statement (or its variations) are known as Scheffe lemma. The formalization is more painful as one should jump back and forth between reals and ereals and justify all the time positivity or integrability (thankfully, measurability is handled more or less automatically).\ proposition Scheffe_lemma1: assumes "\n. integrable M (F n)" "integrable M f" "AE x in M. (\n. F n x) \ f x" "limsup (\n. \\<^sup>+ x. norm(F n x) \M) \ (\\<^sup>+ x. norm(f x) \M)" shows "(\n. \\<^sup>+ x. norm(F n x - f x) \M) \ 0" proof - have [measurable]: "\n. F n \ borel_measurable M" "f \ borel_measurable M" using assms(1) assms(2) by simp_all define G where "G = (\n x. norm(f x) + norm(F n x) - norm(F n x - f x))" have [measurable]: "\n. G n \ borel_measurable M" unfolding G_def by simp have G_pos[simp]: "\n x. G n x \ 0" unfolding G_def by (metis ge_iff_diff_ge_0 norm_minus_commute norm_triangle_ineq4) have finint: "(\\<^sup>+ x. norm(f x) \M) \ \" using has_bochner_integral_implies_finite_norm[OF has_bochner_integral_integrable[OF \integrable M f\]] by simp then have fin2: "2 * (\\<^sup>+ x. norm(f x) \M) \ \" by (auto simp: ennreal_mult_eq_top_iff) { fix x assume *: "(\n. F n x) \ f x" then have "(\n. norm(F n x)) \ norm(f x)" using tendsto_norm by blast moreover have "(\n. norm(F n x - f x)) \ 0" using * Lim_null tendsto_norm_zero_iff by fastforce ultimately have a: "(\n. norm(F n x) - norm(F n x - f x)) \ norm(f x)" using tendsto_diff by fastforce have "(\n. norm(f x) + (norm(F n x) - norm(F n x - f x))) \ norm(f x) + norm(f x)" by (rule tendsto_add) (auto simp add: a) moreover have "\n. G n x = norm(f x) + (norm(F n x) - norm(F n x - f x))" unfolding G_def by simp ultimately have "(\n. G n x) \ 2 * norm(f x)" by simp then have "(\n. ennreal(G n x)) \ ennreal(2 * norm(f x))" by simp then have "liminf (\n. ennreal(G n x)) = ennreal(2 * norm(f x))" using sequentially_bot tendsto_iff_Liminf_eq_Limsup by blast } then have "AE x in M. liminf (\n. ennreal(G n x)) = ennreal(2 * norm(f x))" using assms(3) by auto then have "(\\<^sup>+ x. liminf (\n. ennreal (G n x)) \M) = (\\<^sup>+ x. 2 * ennreal(norm(f x)) \M)" by (simp add: nn_integral_cong_AE ennreal_mult) also have "\ = 2 * (\\<^sup>+ x. norm(f x) \M)" by (rule nn_integral_cmult) auto finally have int_liminf: "(\\<^sup>+ x. liminf (\n. ennreal (G n x)) \M) = 2 * (\\<^sup>+ x. norm(f x) \M)" by simp have "(\\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \M) = (\\<^sup>+x. norm(f x) \M) + (\\<^sup>+x. norm(F n x) \M)" for n by (rule nn_integral_add) (auto simp add: assms) then have "limsup (\n. (\\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \M)) = limsup (\n. (\\<^sup>+x. norm(f x) \M) + (\\<^sup>+x. norm(F n x) \M))" by simp also have "\ = (\\<^sup>+x. norm(f x) \M) + limsup (\n. (\\<^sup>+x. norm(F n x) \M))" by (rule Limsup_const_add, auto simp add: finint) also have "\ \ (\\<^sup>+x. norm(f x) \M) + (\\<^sup>+x. norm(f x) \M)" using assms(4) by (simp add: add_left_mono) also have "\ = 2 * (\\<^sup>+x. norm(f x) \M)" unfolding one_add_one[symmetric] distrib_right by simp ultimately have a: "limsup (\n. (\\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \M)) \ 2 * (\\<^sup>+x. norm(f x) \M)" by simp have le: "ennreal (norm (F n x - f x)) \ ennreal (norm (f x)) + ennreal (norm (F n x))" for n x by (simp add: norm_minus_commute norm_triangle_ineq4 ennreal_minus flip: ennreal_plus) then have le2: "(\\<^sup>+ x. ennreal (norm (F n x - f x)) \M) \ (\\<^sup>+ x. ennreal (norm (f x)) + ennreal (norm (F n x)) \M)" for n by (rule nn_integral_mono) have "2 * (\\<^sup>+ x. norm(f x) \M) = (\\<^sup>+ x. liminf (\n. ennreal (G n x)) \M)" by (simp add: int_liminf) also have "\ \ liminf (\n. (\\<^sup>+x. G n x \M))" by (rule nn_integral_liminf) auto also have "liminf (\n. (\\<^sup>+x. G n x \M)) = liminf (\n. (\\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \M) - (\\<^sup>+x. norm(F n x - f x) \M))" proof (intro arg_cong[where f=liminf] ext) fix n have "\x. ennreal(G n x) = ennreal(norm(f x)) + ennreal(norm(F n x)) - ennreal(norm(F n x - f x))" unfolding G_def by (simp add: ennreal_minus flip: ennreal_plus) moreover have "(\\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) - ennreal(norm(F n x - f x)) \M) = (\\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \M) - (\\<^sup>+x. norm(F n x - f x) \M)" proof (rule nn_integral_diff) from le show "AE x in M. ennreal (norm (F n x - f x)) \ ennreal (norm (f x)) + ennreal (norm (F n x))" by simp from le2 have "(\\<^sup>+x. ennreal (norm (F n x - f x)) \M) < \" using assms(1) assms(2) by (metis has_bochner_integral_implies_finite_norm integrable.simps Bochner_Integration.integrable_diff) then show "(\\<^sup>+x. ennreal (norm (F n x - f x)) \M) \ \" by simp qed (auto simp add: assms) ultimately show "(\\<^sup>+x. G n x \M) = (\\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \M) - (\\<^sup>+x. norm(F n x - f x) \M)" by simp qed finally have "2 * (\\<^sup>+ x. norm(f x) \M) + limsup (\n. (\\<^sup>+x. norm(F n x - f x) \M)) \ liminf (\n. (\\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \M) - (\\<^sup>+x. norm(F n x - f x) \M)) + limsup (\n. (\\<^sup>+x. norm(F n x - f x) \M))" by (intro add_mono) auto also have "\ \ (limsup (\n. \\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \M) - limsup (\n. \\<^sup>+x. norm (F n x - f x) \M)) + limsup (\n. (\\<^sup>+x. norm(F n x - f x) \M))" by (intro add_mono liminf_minus_ennreal le2) auto also have "\ = limsup (\n. (\\<^sup>+x. ennreal(norm(f x)) + ennreal(norm(F n x)) \M))" by (intro diff_add_cancel_ennreal Limsup_mono always_eventually allI le2) also have "\ \ 2 * (\\<^sup>+x. norm(f x) \M)" by fact finally have "limsup (\n. (\\<^sup>+x. norm(F n x - f x) \M)) = 0" using fin2 by simp then show ?thesis by (rule tendsto_0_if_Limsup_eq_0_ennreal) qed proposition Scheffe_lemma2: fixes F::"nat \ 'a \ 'b::{banach, second_countable_topology}" assumes "\ n::nat. F n \ borel_measurable M" "integrable M f" "AE x in M. (\n. F n x) \ f x" "\n. (\\<^sup>+ x. norm(F n x) \M) \ (\\<^sup>+ x. norm(f x) \M)" shows "(\n. \\<^sup>+ x. norm(F n x - f x) \M) \ 0" proof (rule Scheffe_lemma1) fix n::nat have "(\\<^sup>+ x. norm(f x) \M) < \" using assms(2) by (metis has_bochner_integral_implies_finite_norm integrable.cases) then have "(\\<^sup>+ x. norm(F n x) \M) < \" using assms(4)[of n] by auto then show "integrable M (F n)" by (subst integrable_iff_bounded, simp add: assms(1)[of n]) qed (auto simp add: assms Limsup_bounded) lemma tendsto_set_lebesgue_integral_at_right: fixes a b :: real and f :: "real \ 'a :: {banach,second_countable_topology}" assumes "a < b" and sets: "\a'. a' \ {a<..b} \ {a'..b} \ sets M" and "set_integrable M {a<..b} f" shows "((\a'. set_lebesgue_integral M {a'..b} f) \ set_lebesgue_integral M {a<..b} f) (at_right a)" proof (rule tendsto_at_right_sequentially[OF assms(1)], goal_cases) case (1 S) have eq: "(\n. {S n..b}) = {a<..b}" proof safe fix x n assume "x \ {S n..b}" with 1(1,2)[of n] show "x \ {a<..b}" by auto next fix x assume "x \ {a<..b}" with order_tendstoD[OF \S \ a\, of x] show "x \ (\n. {S n..b})" by (force simp: eventually_at_top_linorder dest: less_imp_le) qed have "(\n. set_lebesgue_integral M {S n..b} f) \ set_lebesgue_integral M (\n. {S n..b}) f" by (rule set_integral_cont_up) (insert assms 1, auto simp: eq incseq_def decseq_def less_imp_le) with eq show ?case by simp qed section \Convergence of integrals over an interval\ text \ The next lemmas relate convergence of integrals over an interval to improper integrals. \ lemma tendsto_set_lebesgue_integral_at_left: fixes a b :: real and f :: "real \ 'a :: {banach,second_countable_topology}" assumes "a < b" and sets: "\b'. b' \ {a.. {a..b'} \ sets M" and "set_integrable M {a..b'. set_lebesgue_integral M {a..b'} f) \ set_lebesgue_integral M {a..n. {a..S n}) = {a.. {a..S n}" with 1(1,2)[of n] show "x \ {a.. {a..S \ b\, of x] show "x \ (\n. {a..S n})" by (force simp: eventually_at_top_linorder dest: less_imp_le) qed have "(\n. set_lebesgue_integral M {a..S n} f) \ set_lebesgue_integral M (\n. {a..S n}) f" by (rule set_integral_cont_up) (insert assms 1, auto simp: eq incseq_def decseq_def less_imp_le) with eq show ?case by simp qed proposition tendsto_set_lebesgue_integral_at_top: fixes f :: "real \ 'a::{banach, second_countable_topology}" assumes sets: "\b. b \ a \ {a..b} \ sets M" and int: "set_integrable M {a..} f" shows "((\b. set_lebesgue_integral M {a..b} f) \ set_lebesgue_integral M {a..} f) at_top" proof (rule tendsto_at_topI_sequentially) fix X :: "nat \ real" assume "filterlim X at_top sequentially" show "(\n. set_lebesgue_integral M {a..X n} f) \ set_lebesgue_integral M {a..} f" unfolding set_lebesgue_integral_def proof (rule integral_dominated_convergence) show "integrable M (\x. indicat_real {a..} x *\<^sub>R norm (f x))" using integrable_norm[OF int[unfolded set_integrable_def]] by simp show "AE x in M. (\n. indicator {a..X n} x *\<^sub>R f x) \ indicat_real {a..} x *\<^sub>R f x" proof fix x from \filterlim X at_top sequentially\ have "eventually (\n. x \ X n) sequentially" unfolding filterlim_at_top_ge[where c=x] by auto then show "(\n. indicator {a..X n} x *\<^sub>R f x) \ indicat_real {a..} x *\<^sub>R f x" by (intro tendsto_eventually) (auto split: split_indicator elim!: eventually_mono) qed fix n show "AE x in M. norm (indicator {a..X n} x *\<^sub>R f x) \ indicator {a..} x *\<^sub>R norm (f x)" by (auto split: split_indicator) next from int show "(\x. indicat_real {a..} x *\<^sub>R f x) \ borel_measurable M" by (simp add: set_integrable_def) next fix n :: nat from sets have "{a..X n} \ sets M" by (cases "X n \ a") auto with int have "set_integrable M {a..X n} f" by (rule set_integrable_subset) auto thus "(\x. indicat_real {a..X n} x *\<^sub>R f x) \ borel_measurable M" by (simp add: set_integrable_def) qed qed proposition tendsto_set_lebesgue_integral_at_bot: fixes f :: "real \ 'a::{banach, second_countable_topology}" assumes sets: "\a. a \ b \ {a..b} \ sets M" and int: "set_integrable M {..b} f" shows "((\a. set_lebesgue_integral M {a..b} f) \ set_lebesgue_integral M {..b} f) at_bot" proof (rule tendsto_at_botI_sequentially) fix X :: "nat \ real" assume "filterlim X at_bot sequentially" show "(\n. set_lebesgue_integral M {X n..b} f) \ set_lebesgue_integral M {..b} f" unfolding set_lebesgue_integral_def proof (rule integral_dominated_convergence) show "integrable M (\x. indicat_real {..b} x *\<^sub>R norm (f x))" using integrable_norm[OF int[unfolded set_integrable_def]] by simp show "AE x in M. (\n. indicator {X n..b} x *\<^sub>R f x) \ indicat_real {..b} x *\<^sub>R f x" proof fix x from \filterlim X at_bot sequentially\ have "eventually (\n. x \ X n) sequentially" unfolding filterlim_at_bot_le[where c=x] by auto then show "(\n. indicator {X n..b} x *\<^sub>R f x) \ indicat_real {..b} x *\<^sub>R f x" by (intro tendsto_eventually) (auto split: split_indicator elim!: eventually_mono) qed fix n show "AE x in M. norm (indicator {X n..b} x *\<^sub>R f x) \ indicator {..b} x *\<^sub>R norm (f x)" by (auto split: split_indicator) next from int show "(\x. indicat_real {..b} x *\<^sub>R f x) \ borel_measurable M" by (simp add: set_integrable_def) next fix n :: nat from sets have "{X n..b} \ sets M" by (cases "X n \ b") auto with int have "set_integrable M {X n..b} f" by (rule set_integrable_subset) auto thus "(\x. indicat_real {X n..b} x *\<^sub>R f x) \ borel_measurable M" by (simp add: set_integrable_def) qed qed theorem integral_Markov_inequality': fixes u :: "'a \ real" assumes [measurable]: "set_integrable M A u" and "A \ sets M" assumes "AE x in M. x \ A \ u x \ 0" and "0 < (c::real)" shows "emeasure M {x\A. u x \ c} \ (1/c::real) * (\x\A. u x \M)" proof - have "(\x. u x * indicator A x) \ borel_measurable M" using assms by (auto simp: set_integrable_def mult_ac) hence "(\x. ennreal (u x * indicator A x)) \ borel_measurable M" by measurable also have "(\x. ennreal (u x * indicator A x)) = (\x. ennreal (u x) * indicator A x)" by (intro ext) (auto simp: indicator_def) finally have meas: "\ \ borel_measurable M" . from assms(3) have AE: "AE x in M. 0 \ u x * indicator A x" by eventually_elim (auto simp: indicator_def) have nonneg: "set_lebesgue_integral M A u \ 0" unfolding set_lebesgue_integral_def by (intro Bochner_Integration.integral_nonneg_AE eventually_mono[OF AE]) (auto simp: mult_ac) have A: "A \ space M" using \A \ sets M\ by (simp add: sets.sets_into_space) have "{x \ A. u x \ c} = {x \ A. ennreal(1/c) * u x \ 1}" using \c>0\ A by (auto simp: ennreal_mult'[symmetric]) then have "emeasure M {x \ A. u x \ c} = emeasure M ({x \ A. ennreal(1/c) * u x \ 1})" by simp also have "\ \ ennreal(1/c) * (\\<^sup>+ x. ennreal(u x) * indicator A x \M)" by (intro nn_integral_Markov_inequality meas assms) also have "(\\<^sup>+ x. ennreal(u x) * indicator A x \M) = ennreal (set_lebesgue_integral M A u)" unfolding set_lebesgue_integral_def nn_integral_set_ennreal using assms AE by (subst nn_integral_eq_integral) (simp_all add: mult_ac set_integrable_def) finally show ?thesis using \c > 0\ nonneg by (subst ennreal_mult) auto qed theorem integral_Markov_inequality'_measure: assumes [measurable]: "set_integrable M A u" and "A \ sets M" and "AE x in M. x \ A \ 0 \ u x" "0 < (c::real)" shows "measure M {x\A. u x \ c} \ (\x\A. u x \M) / c" proof - have nonneg: "set_lebesgue_integral M A u \ 0" unfolding set_lebesgue_integral_def by (intro Bochner_Integration.integral_nonneg_AE eventually_mono[OF assms(3)]) (auto simp: mult_ac) have le: "emeasure M {x\A. u x \ c} \ ennreal ((1/c) * (\x\A. u x \M))" by (rule integral_Markov_inequality') (use assms in auto) also have "\ < top" by auto finally have "ennreal (measure M {x\A. u x \ c}) = emeasure M {x\A. u x \ c}" by (intro emeasure_eq_ennreal_measure [symmetric]) auto also note le finally show ?thesis using nonneg by (subst (asm) ennreal_le_iff) (auto intro!: divide_nonneg_pos Bochner_Integration.integral_nonneg_AE assms) qed theorem%important (in finite_measure) Chernoff_ineq_ge: assumes s: "s > 0" assumes integrable: "set_integrable M A (\x. exp (s * f x))" and "A \ sets M" shows "measure M {x\A. f x \ a} \ exp (-s * a) * (\x\A. exp (s * f x) \M)" proof - have "{x\A. f x \ a} = {x\A. exp (s * f x) \ exp (s * a)}" using s by auto also have "measure M \ \ set_lebesgue_integral M A (\x. exp (s * f x)) / exp (s * a)" by (intro integral_Markov_inequality'_measure assms) auto finally show ?thesis by (simp add: exp_minus field_simps) qed theorem%important (in finite_measure) Chernoff_ineq_le: assumes s: "s > 0" assumes integrable: "set_integrable M A (\x. exp (-s * f x))" and "A \ sets M" shows "measure M {x\A. f x \ a} \ exp (s * a) * (\x\A. exp (-s * f x) \M)" proof - have "{x\A. f x \ a} = {x\A. exp (-s * f x) \ exp (-s * a)}" using s by auto also have "measure M \ \ set_lebesgue_integral M A (\x. exp (-s * f x)) / exp (-s * a)" by (intro integral_Markov_inequality'_measure assms) auto finally show ?thesis by (simp add: exp_minus field_simps) qed section \Integrable Simple Functions\ text \This section is from the Martingales AFP entry, by Ata Keskin, TU München\ text \We restate some basic results concerning Bochner-integrable functions.\ lemma integrable_implies_simple_function_sequence: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes "integrable M f" obtains s where "\i. simple_function M (s i)" and "\i. emeasure M {y \ space M. s i y \ 0} \ \" and "\x. x \ space M \ (\i. s i x) \ f x" and "\x i. x \ space M \ norm (s i x) \ 2 * norm (f x)" proof- have f: "f \ borel_measurable M" "(\\<^sup>+x. norm (f x) \M) < \" using assms unfolding integrable_iff_bounded by auto obtain s where s: "\i. simple_function M (s i)" "\x. x \ space M \ (\i. s i x) \ f x" "\i x. x \ space M \ norm (s i x) \ 2 * norm (f x)" using borel_measurable_implies_sequence_metric[OF f(1)] unfolding norm_conv_dist by metis { fix i have "(\\<^sup>+x. norm (s i x) \M) \ (\\<^sup>+x. ennreal (2 * norm (f x)) \M)" using s by (intro nn_integral_mono, auto) also have "\ < \" using f by (simp add: nn_integral_cmult ennreal_mult_less_top ennreal_mult) finally have sbi: "Bochner_Integration.simple_bochner_integrable M (s i)" using s by (intro simple_bochner_integrableI_bounded) auto hence "emeasure M {y \ space M. s i y \ 0} \ \" by (auto intro: integrableI_simple_bochner_integrable simple_bochner_integrable.cases) } thus ?thesis using that s by blast qed text \Simple functions can be represented by sums of indicator functions.\ lemma simple_function_indicator_representation_banach: fixes f ::"'a \ 'b :: {second_countable_topology, banach}" assumes "simple_function M f" "x \ space M" shows "f x = (\y \ f ` space M. indicator (f -` {y} \ space M) x *\<^sub>R y)" (is "?l = ?r") proof - have "?r = (\y \ f ` space M. (if y = f x then indicator (f -` {y} \ space M) x *\<^sub>R y else 0))" by (auto intro!: sum.cong) also have "\ = indicator (f -` {f x} \ space M) x *\<^sub>R f x" using assms by (auto dest: simple_functionD) also have "\ = f x" using assms by (auto simp: indicator_def) finally show ?thesis by auto qed lemma simple_function_indicator_representation_AE: fixes f ::"'a \ 'b :: {second_countable_topology, banach}" assumes "simple_function M f" shows "AE x in M. f x = (\y \ f ` space M. indicator (f -` {y} \ space M) x *\<^sub>R y)" by (metis (mono_tags, lifting) AE_I2 simple_function_indicator_representation_banach assms) lemmas simple_function_scaleR[intro] = simple_function_compose2[where h="(*\<^sub>R)"] lemmas integrable_simple_function = simple_bochner_integrable.intros[THEN has_bochner_integral_simple_bochner_integrable, THEN integrable.intros] text \Induction rule for simple integrable functions.\ lemma\<^marker>\tag important\ integrable_simple_function_induct[consumes 2, case_names cong indicator add, induct set: simple_function]: fixes f :: "'a \ 'b :: {second_countable_topology, banach}" assumes f: "simple_function M f" "emeasure M {y \ space M. f y \ 0} \ \" assumes cong: "\f g. simple_function M f \ emeasure M {y \ space M. f y \ 0} \ \ \ simple_function M g \ emeasure M {y \ space M. g y \ 0} \ \ \ (\x. x \ space M \ f x = g x) \ P f \ P g" assumes indicator: "\A y. A \ sets M \ emeasure M A < \ \ P (\x. indicator A x *\<^sub>R y)" assumes add: "\f g. simple_function M f \ emeasure M {y \ space M. f y \ 0} \ \ \ simple_function M g \ emeasure M {y \ space M. g y \ 0} \ \ \ (\z. z \ space M \ norm (f z + g z) = norm (f z) + norm (g z)) \ P f \ P g \ P (\x. f x + g x)" shows "P f" proof- let ?f = "\x. (\y\f ` space M. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" have f_ae_eq: "f x = ?f x" if "x \ space M" for x using simple_function_indicator_representation_banach[OF f(1) that] . moreover have "emeasure M {y \ space M. ?f y \ 0} \ \" by (metis (no_types, lifting) Collect_cong calculation f(2)) moreover have "P (\x. \y\S. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" "simple_function M (\x. \y\S. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" "emeasure M {y \ space M. (\x\S. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} \ \" if "S \ f ` space M" for S using simple_functionD(1)[OF assms(1), THEN rev_finite_subset, OF that] that proof (induction rule: finite_induct) case empty { case 1 then show ?case using indicator[of "{}"] by force next case 2 then show ?case by force next case 3 then show ?case by force } next case (insert x F) have "(f -` {x} \ space M) \ {y \ space M. f y \ 0}" if "x \ 0" using that by blast moreover have "{y \ space M. f y \ 0} = space M - (f -` {0} \ space M)" by blast moreover have "space M - (f -` {0} \ space M) \ sets M" using simple_functionD(2)[OF f(1)] by blast ultimately have fin_0: "emeasure M (f -` {x} \ space M) < \" if "x \ 0" using that by (metis emeasure_mono f(2) infinity_ennreal_def top.not_eq_extremum top_unique) hence fin_1: "emeasure M {y \ space M. indicat_real (f -` {x} \ space M) y *\<^sub>R x \ 0} \ \" if "x \ 0" by (metis (mono_tags, lifting) emeasure_mono f(1) indicator_simps(2) linorder_not_less mem_Collect_eq scaleR_eq_0_iff simple_functionD(2) subsetI that) have *: "(\y\insert x F. indicat_real (f -` {y} \ space M) xa *\<^sub>R y) = (\y\F. indicat_real (f -` {y} \ space M) xa *\<^sub>R y) + indicat_real (f -` {x} \ space M) xa *\<^sub>R x" for xa by (metis (no_types, lifting) Diff_empty Diff_insert0 add.commute insert.hyps(1) insert.hyps(2) sum.insert_remove) have **: "{y \ space M. (\x\insert x F. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} \ {y \ space M. (\x\F. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} \ {y \ space M. indicat_real (f -` {x} \ space M) y *\<^sub>R x \ 0}" unfolding * by fastforce { case 1 hence x: "x \ f ` space M" and F: "F \ f ` space M" by auto show ?case proof (cases "x = 0") case True then show ?thesis unfolding * using insert(3)[OF F] by simp next case False have norm_argument: "norm ((\y\F. indicat_real (f -` {y} \ space M) z *\<^sub>R y) + indicat_real (f -` {x} \ space M) z *\<^sub>R x) = norm (\y\F. indicat_real (f -` {y} \ space M) z *\<^sub>R y) + norm (indicat_real (f -` {x} \ space M) z *\<^sub>R x)" if z: "z \ space M" for z proof (cases "f z = x") case True have "indicat_real (f -` {y} \ space M) z *\<^sub>R y = 0" if "y \ F" for y using True insert(2) z that 1 unfolding indicator_def by force hence "(\y\F. indicat_real (f -` {y} \ space M) z *\<^sub>R y) = 0" by (meson sum.neutral) then show ?thesis by force next case False then show ?thesis by force qed show ?thesis using False simple_functionD(2)[OF f(1)] insert(3,5)[OF F] simple_function_scaleR fin_0 fin_1 by (subst *, subst add, subst simple_function_sum) (blast intro: norm_argument indicator)+ qed next case 2 hence x: "x \ f ` space M" and F: "F \ f ` space M" by auto show ?case proof (cases "x = 0") case True then show ?thesis unfolding * using insert(4)[OF F] by simp next case False then show ?thesis unfolding * using insert(4)[OF F] simple_functionD(2)[OF f(1)] by fast qed next case 3 hence x: "x \ f ` space M" and F: "F \ f ` space M" by auto show ?case proof (cases "x = 0") case True then show ?thesis unfolding * using insert(5)[OF F] by simp next case False have "emeasure M {y \ space M. (\x\insert x F. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} \ emeasure M ({y \ space M. (\x\F. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} \ {y \ space M. indicat_real (f -` {x} \ space M) y *\<^sub>R x \ 0})" using ** simple_functionD(2)[OF insert(4)[OF F]] simple_functionD(2)[OF f(1)] by (intro emeasure_mono, force+) also have "\ \ emeasure M {y \ space M. (\x\F. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} + emeasure M {y \ space M. indicat_real (f -` {x} \ space M) y *\<^sub>R x \ 0}" using simple_functionD(2)[OF insert(4)[OF F]] simple_functionD(2)[OF f(1)] by (intro emeasure_subadditive, force+) also have "\ < \" using insert(5)[OF F] fin_1[OF False] by (simp add: less_top) finally show ?thesis by simp qed } qed moreover have "simple_function M (\x. \y\f ` space M. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" using calculation by blast moreover have "P (\x. \y\f ` space M. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" using calculation by blast ultimately show ?thesis by (intro cong[OF _ _ f(1,2)], blast, presburger+) qed text \Induction rule for non-negative simple integrable functions\ lemma\<^marker>\tag important\ integrable_simple_function_induct_nn[consumes 3, case_names cong indicator add, induct set: simple_function]: fixes f :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" assumes f: "simple_function M f" "emeasure M {y \ space M. f y \ 0} \ \" "\x. x \ space M \ f x \ 0" assumes cong: "\f g. simple_function M f \ emeasure M {y \ space M. f y \ 0} \ \ \ (\x. x \ space M \ f x \ 0) \ simple_function M g \ emeasure M {y \ space M. g y \ 0} \ \ \ (\x. x \ space M \ g x \ 0) \ (\x. x \ space M \ f x = g x) \ P f \ P g" assumes indicator: "\A y. y \ 0 \ A \ sets M \ emeasure M A < \ \ P (\x. indicator A x *\<^sub>R y)" assumes add: "\f g. (\x. x \ space M \ f x \ 0) \ simple_function M f \ emeasure M {y \ space M. f y \ 0} \ \ \ (\x. x \ space M \ g x \ 0) \ simple_function M g \ emeasure M {y \ space M. g y \ 0} \ \ \ (\z. z \ space M \ norm (f z + g z) = norm (f z) + norm (g z)) \ P f \ P g \ P (\x. f x + g x)" shows "P f" proof- let ?f = "\x. (\y\f ` space M. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" have f_ae_eq: "f x = ?f x" if "x \ space M" for x using simple_function_indicator_representation_banach[OF f(1) that] . moreover have "emeasure M {y \ space M. ?f y \ 0} \ \" by (metis (no_types, lifting) Collect_cong calculation f(2)) moreover have "P (\x. \y\S. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" "simple_function M (\x. \y\S. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" "emeasure M {y \ space M. (\x\S. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} \ \" "\x. x \ space M \ 0 \ (\y\S. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" if "S \ f ` space M" for S using simple_functionD(1)[OF assms(1), THEN rev_finite_subset, OF that] that proof (induction rule: finite_subset_induct') case empty { case 1 then show ?case using indicator[of 0 "{}"] by force next case 2 then show ?case by force next case 3 then show ?case by force next case 4 then show ?case by force } next case (insert x F) have "(f -` {x} \ space M) \ {y \ space M. f y \ 0}" if "x \ 0" using that by blast moreover have "{y \ space M. f y \ 0} = space M - (f -` {0} \ space M)" by blast moreover have "space M - (f -` {0} \ space M) \ sets M" using simple_functionD(2)[OF f(1)] by blast ultimately have fin_0: "emeasure M (f -` {x} \ space M) < \" if "x \ 0" using that by (metis emeasure_mono f(2) infinity_ennreal_def top.not_eq_extremum top_unique) hence fin_1: "emeasure M {y \ space M. indicat_real (f -` {x} \ space M) y *\<^sub>R x \ 0} \ \" if "x \ 0" by (metis (mono_tags, lifting) emeasure_mono f(1) indicator_simps(2) linorder_not_less mem_Collect_eq scaleR_eq_0_iff simple_functionD(2) subsetI that) have nonneg_x: "x \ 0" using insert f by blast have *: "(\y\insert x F. indicat_real (f -` {y} \ space M) xa *\<^sub>R y) = (\y\F. indicat_real (f -` {y} \ space M) xa *\<^sub>R y) + indicat_real (f -` {x} \ space M) xa *\<^sub>R x" for xa by (metis (no_types, lifting) add.commute insert.hyps(1) insert.hyps(4) sum.insert) have **: "{y \ space M. (\x\insert x F. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} \ {y \ space M. (\x\F. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} \ {y \ space M. indicat_real (f -` {x} \ space M) y *\<^sub>R x \ 0}" unfolding * by fastforce { case 1 show ?case proof (cases "x = 0") case True then show ?thesis unfolding * using insert by simp next case False have norm_argument: "norm ((\y\F. indicat_real (f -` {y} \ space M) z *\<^sub>R y) + indicat_real (f -` {x} \ space M) z *\<^sub>R x) = norm (\y\F. indicat_real (f -` {y} \ space M) z *\<^sub>R y) + norm (indicat_real (f -` {x} \ space M) z *\<^sub>R x)" if z: "z \ space M" for z proof (cases "f z = x") case True have "indicat_real (f -` {y} \ space M) z *\<^sub>R y = 0" if "y \ F" for y using True insert z that 1 unfolding indicator_def by force hence "(\y\F. indicat_real (f -` {y} \ space M) z *\<^sub>R y) = 0" by (meson sum.neutral) thus ?thesis by force qed (force) show ?thesis using False fin_0 fin_1 f norm_argument by (subst *, subst add, presburger add: insert, intro insert, intro insert, fastforce simp add: indicator_def intro!: insert(2) f(3), auto intro!: indicator insert nonneg_x) qed next case 2 show ?case proof (cases "x = 0") case True then show ?thesis unfolding * using insert by simp next case False then show ?thesis unfolding * using insert simple_functionD(2)[OF f(1)] by fast qed next case 3 show ?case proof (cases "x = 0") case True then show ?thesis unfolding * using insert by simp next case False have "emeasure M {y \ space M. (\x\insert x F. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} \ emeasure M ({y \ space M. (\x\F. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} \ {y \ space M. indicat_real (f -` {x} \ space M) y *\<^sub>R x \ 0})" using ** simple_functionD(2)[OF insert(6)] simple_functionD(2)[OF f(1)] insert.IH(2) by (intro emeasure_mono, blast, simp) also have "\ \ emeasure M {y \ space M. (\x\F. indicat_real (f -` {x} \ space M) y *\<^sub>R x) \ 0} + emeasure M {y \ space M. indicat_real (f -` {x} \ space M) y *\<^sub>R x \ 0}" using simple_functionD(2)[OF insert(6)] simple_functionD(2)[OF f(1)] by (intro emeasure_subadditive, force+) also have "\ < \" using insert(7) fin_1[OF False] by (simp add: less_top) finally show ?thesis by simp qed next case (4 \) thus ?case using insert nonneg_x f(3) by (auto simp add: scaleR_nonneg_nonneg intro: sum_nonneg) } qed moreover have "simple_function M (\x. \y\f ` space M. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" using calculation by blast moreover have "P (\x. \y\f ` space M. indicat_real (f -` {y} \ space M) x *\<^sub>R y)" using calculation by blast moreover have "\x. x \ space M \ 0 \ f x" using f(3) by simp ultimately show ?thesis by (smt (verit) Collect_cong f(1) local.cong) qed lemma finite_nn_integral_imp_ae_finite: fixes f :: "'a \ ennreal" assumes "f \ borel_measurable M" "(\\<^sup>+x. f x \M) < \" shows "AE x in M. f x < \" proof (rule ccontr, goal_cases) case 1 let ?A = "space M \ {x. f x = \}" have *: "emeasure M ?A > 0" using 1 assms(1) by (metis (mono_tags, lifting) assms(2) eventually_mono infinity_ennreal_def nn_integral_noteq_infinite top.not_eq_extremum) have "(\\<^sup>+x. f x * indicator ?A x \M) = (\\<^sup>+x. \ * indicator ?A x \M)" by (metis (mono_tags, lifting) indicator_inter_arith indicator_simps(2) mem_Collect_eq mult_eq_0_iff) also have "\ = \ * emeasure M ?A" using assms(1) by (intro nn_integral_cmult_indicator, simp) also have "\ = \" using * by fastforce finally have "(\\<^sup>+x. f x * indicator ?A x \M) = \" . moreover have "(\\<^sup>+x. f x * indicator ?A x \M) \ (\\<^sup>+x. f x \M)" by (intro nn_integral_mono, simp add: indicator_def) ultimately show ?case using assms(2) by simp qed text \Convergence in L1-Norm implies existence of a subsequence which convergences almost everywhere. This lemma is easier to use than the existing one in \<^theory>\HOL-Analysis.Bochner_Integration\\ lemma cauchy_L1_AE_cauchy_subseq: fixes s :: "nat \ 'a \ 'b::{banach, second_countable_topology}" assumes [measurable]: "\n. integrable M (s n)" and "\e. e > 0 \ \N. \i\N. \j\N. LINT x|M. norm (s i x - s j x) < e" obtains r where "strict_mono r" "AE x in M. Cauchy (\i. s (r i) x)" proof- have "\r. \n. (\i\r n. \j\ r n. LINT x|M. norm (s i x - s j x) < (1 / 2) ^ n) \ (r (Suc n) > r n)" proof (intro dependent_nat_choice, goal_cases) case 1 then show ?case using assms(2) by presburger next case (2 x n) obtain N where *: "LINT x|M. norm (s i x - s j x) < (1 / 2) ^ Suc n" if "i \ N" "j \ N" for i j using assms(2)[of "(1 / 2) ^ Suc n"] by auto { fix i j assume "i \ max N (Suc x)" "j \ max N (Suc x)" hence "integral\<^sup>L M (\x. norm (s i x - s j x)) < (1 / 2) ^ Suc n" using * by fastforce } then show ?case by fastforce qed then obtain r where strict_mono: "strict_mono r" and "\i\r n. \j\ r n. LINT x|M. norm (s i x - s j x) < (1 / 2) ^ n" for n using strict_mono_Suc_iff by blast hence r_is: "LINT x|M. norm (s (r (Suc n)) x - s (r n) x) < (1 / 2) ^ n" for n by (simp add: strict_mono_leD) define g where "g = (\n x. (\i\n. ennreal (norm (s (r (Suc i)) x - s (r i) x))))" define g' where "g' = (\x. \i. ennreal (norm (s (r (Suc i)) x - s (r i) x)))" have integrable_g: "(\\<^sup>+ x. g n x \M) < 2" for n proof - have "(\\<^sup>+ x. g n x \M) = (\\<^sup>+ x. (\i\n. ennreal (norm (s (r (Suc i)) x - s (r i) x))) \M)" using g_def by simp also have "\ = (\i\n. (\\<^sup>+ x. ennreal (norm (s (r (Suc i)) x - s (r i) x)) \M))" by (intro nn_integral_sum, simp) also have "\ = (\i\n. LINT x|M. norm (s (r (Suc i)) x - s (r i) x))" unfolding dist_norm using assms(1) by (subst nn_integral_eq_integral[OF integrable_norm], auto) also have "\ < ennreal (\i\n. (1 / 2) ^ i)" by (intro ennreal_lessI[OF sum_pos sum_strict_mono[OF finite_atMost _ r_is]], auto) also have "\ \ ennreal 2" unfolding sum_gp0[of "1 / 2" n] by (intro ennreal_leI, auto) finally show "(\\<^sup>+ x. g n x \M) < 2" by simp qed have integrable_g': "(\\<^sup>+ x. g' x \M) \ 2" proof - have "incseq (\n. g n x)" for x by (intro incseq_SucI, auto simp add: g_def ennreal_leI) hence "convergent (\n. g n x)" for x unfolding convergent_def using LIMSEQ_incseq_SUP by fast hence "(\n. g n x) \ g' x" for x unfolding g_def g'_def by (intro summable_iff_convergent'[THEN iffD2, THEN summable_LIMSEQ'], blast) hence "(\\<^sup>+ x. g' x \M) = (\\<^sup>+ x. liminf (\n. g n x) \M)" by (metis lim_imp_Liminf trivial_limit_sequentially) also have "\ \ liminf (\n. \\<^sup>+ x. g n x \M)" by (intro nn_integral_liminf, simp add: g_def) also have "\ \ liminf (\n. 2)" using integrable_g by (intro Liminf_mono) (simp add: order_le_less) also have "\ = 2" using sequentially_bot tendsto_iff_Liminf_eq_Limsup by blast finally show ?thesis . qed hence "AE x in M. g' x < \" by (intro finite_nn_integral_imp_ae_finite) (auto simp add: order_le_less_trans g'_def) moreover have "summable (\i. norm (s (r (Suc i)) x - s (r i) x))" if "g' x \ \" for x using that unfolding g'_def by (intro summable_suminf_not_top) fastforce+ ultimately have ae_summable: "AE x in M. summable (\i. s (r (Suc i)) x - s (r i) x)" using summable_norm_cancel unfolding dist_norm by force { fix x assume "summable (\i. s (r (Suc i)) x - s (r i) x)" hence "(\n. \i (\i. s (r (Suc i)) x - s (r i) x)" using summable_LIMSEQ by blast moreover have "(\n. (\in. s (r n) x - s (r 0) x)" using sum_lessThan_telescope by fastforce ultimately have "(\n. s (r n) x - s (r 0) x) \ (\i. s (r (Suc i)) x - s (r i) x)" by argo hence "(\n. s (r n) x - s (r 0) x + s (r 0) x) \ (\i. s (r (Suc i)) x - s (r i) x) + s (r 0) x" by (intro isCont_tendsto_compose[of _ "\z. z + s (r 0) x"], auto) hence "Cauchy (\n. s (r n) x)" by (simp add: LIMSEQ_imp_Cauchy) } hence "AE x in M. Cauchy (\i. s (r i) x)" using ae_summable by fast thus ?thesis by (rule that[OF strict_mono(1)]) qed subsection \Totally Ordered Banach Spaces\ lemma integrable_max[simp, intro]: fixes f :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology}" assumes fg[measurable]: "integrable M f" "integrable M g" shows "integrable M (\x. max (f x) (g x))" proof (rule Bochner_Integration.integrable_bound) { fix x y :: 'b have "norm (max x y) \ max (norm x) (norm y)" by linarith also have "\ \ norm x + norm y" by simp finally have "norm (max x y) \ norm (norm x + norm y)" by simp } thus "AE x in M. norm (max (f x) (g x)) \ norm (norm (f x) + norm (g x))" by simp qed (auto intro: Bochner_Integration.integrable_add[OF integrable_norm[OF fg(1)] integrable_norm[OF fg(2)]]) lemma integrable_min[simp, intro]: fixes f :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology}" assumes [measurable]: "integrable M f" "integrable M g" shows "integrable M (\x. min (f x) (g x))" proof - have "norm (min (f x) (g x)) \ norm (f x) \ norm (min (f x) (g x)) \ norm (g x)" for x by linarith thus ?thesis by (intro integrable_bound[OF integrable_max[OF integrable_norm(1,1), OF assms]], auto) qed text \Restatement of \integral_nonneg_AE\ for functions taking values in a Banach space.\ lemma integral_nonneg_AE_banach: fixes f :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" assumes [measurable]: "f \ borel_measurable M" and nonneg: "AE x in M. 0 \ f x" shows "0 \ integral\<^sup>L M f" proof cases assume integrable: "integrable M f" hence max: "(\x. max 0 (f x)) \ borel_measurable M" "\x. 0 \ max 0 (f x)" "integrable M (\x. max 0 (f x))" by auto hence "0 \ integral\<^sup>L M (\x. max 0 (f x))" proof - obtain s where *: "\i. simple_function M (s i)" "\i. emeasure M {y \ space M. s i y \ 0} \ \" "\x. x \ space M \ (\i. s i x) \ f x" "\x i. x \ space M \ norm (s i x) \ 2 * norm (f x)" using integrable_implies_simple_function_sequence[OF integrable] by blast have simple: "\i. simple_function M (\x. max 0 (s i x))" using * by fast have "\i. {y \ space M. max 0 (s i y) \ 0} \ {y \ space M. s i y \ 0}" unfolding max_def by force moreover have "\i. {y \ space M. s i y \ 0} \ sets M" using * by measurable ultimately have "\i. emeasure M {y \ space M. max 0 (s i y) \ 0} \ emeasure M {y \ space M. s i y \ 0}" by (rule emeasure_mono) hence **:"\i. emeasure M {y \ space M. max 0 (s i y) \ 0} \ \" using *(2) by (auto intro: order.strict_trans1 simp add: top.not_eq_extremum) have "\x. x \ space M \ (\i. max 0 (s i x)) \ max 0 (f x)" using *(3) tendsto_max by blast moreover have "\x i. x \ space M \ norm (max 0 (s i x)) \ norm (2 *\<^sub>R f x)" using *(4) unfolding max_def by auto ultimately have tendsto: "(\i. integral\<^sup>L M (\x. max 0 (s i x))) \ integral\<^sup>L M (\x. max 0 (f x))" using borel_measurable_simple_function simple integrable by (intro integral_dominated_convergence[OF max(1) _ integrable_norm[OF integrable_scaleR_right], of _ 2 f], blast+) { fix h :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" assume "simple_function M h" "emeasure M {y \ space M. h y \ 0} \ \" "\x. x \ space M \ h x \ 0" hence *: "integral\<^sup>L M h \ 0" proof (induct rule: integrable_simple_function_induct_nn) case (cong f g) then show ?case using Bochner_Integration.integral_cong by force next case (indicator A y) hence "A \ {} \ y \ 0" using sets.sets_into_space by fastforce then show ?case using indicator by (cases "A = {}", auto simp add: scaleR_nonneg_nonneg) next case (add f g) then show ?case by (simp add: integrable_simple_function) qed } thus ?thesis using LIMSEQ_le_const[OF tendsto, of 0] ** simple by fastforce qed also have "\ = integral\<^sup>L M f" using nonneg by (auto intro: integral_cong_AE) finally show ?thesis . qed (simp add: not_integrable_integral_eq) lemma integral_mono_AE_banach: fixes f g :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" assumes "integrable M f" "integrable M g" "AE x in M. f x \ g x" shows "integral\<^sup>L M f \ integral\<^sup>L M g" using integral_nonneg_AE_banach[of "\x. g x - f x"] assms Bochner_Integration.integral_diff[OF assms(1,2)] by force lemma integral_mono_banach: fixes f g :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" assumes "integrable M f" "integrable M g" "\x. x \ space M \ f x \ g x" shows "integral\<^sup>L M f \ integral\<^sup>L M g" using integral_mono_AE_banach assms by blast subsection \Auxiliary Lemmas for Set Integrals\ lemma nn_set_integral_eq_set_integral: assumes [measurable]:"integrable M f" and "AE x \ A in M. 0 \ f x" "A \ sets M" shows "(\\<^sup>+x\A. f x \M) = (\ x \ A. f x \M)" proof- have "(\\<^sup>+x. indicator A x *\<^sub>R f x \M) = (\ x \ A. f x \M)" unfolding set_lebesgue_integral_def using assms(2) by (intro nn_integral_eq_integral[of _ "\x. indicat_real A x *\<^sub>R f x"], blast intro: assms integrable_mult_indicator, fastforce) moreover have "(\\<^sup>+x. indicator A x *\<^sub>R f x \M) = (\\<^sup>+x\A. f x \M)" by (metis ennreal_0 indicator_simps(1) indicator_simps(2) mult.commute mult_1 mult_zero_left real_scaleR_def) ultimately show ?thesis by argo qed lemma set_integral_restrict_space: fixes f :: "'a \ 'b::{banach, second_countable_topology}" assumes "\ \ space M \ sets M" shows "set_lebesgue_integral (restrict_space M \) A f = set_lebesgue_integral M A (\x. indicator \ x *\<^sub>R f x)" unfolding set_lebesgue_integral_def by (subst integral_restrict_space, auto intro!: integrable_mult_indicator assms simp: mult.commute) lemma set_integral_const: fixes c :: "'b::{banach, second_countable_topology}" assumes "A \ sets M" "emeasure M A \ \" shows "set_lebesgue_integral M A (\_. c) = measure M A *\<^sub>R c" unfolding set_lebesgue_integral_def using assms by (metis has_bochner_integral_indicator has_bochner_integral_integral_eq infinity_ennreal_def less_top) lemma set_integral_mono_banach: fixes f g :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" assumes "set_integrable M A f" "set_integrable M A g" "\x. x \ A \ f x \ g x" shows "(LINT x:A|M. f x) \ (LINT x:A|M. g x)" using assms unfolding set_integrable_def set_lebesgue_integral_def by (auto intro: integral_mono_banach split: split_indicator) lemma set_integral_mono_AE_banach: fixes f g :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" assumes "set_integrable M A f" "set_integrable M A g" "AE x\A in M. f x \ g x" shows "set_lebesgue_integral M A f \ set_lebesgue_integral M A g" using assms unfolding set_lebesgue_integral_def by (auto simp add: set_integrable_def intro!: integral_mono_AE_banach[of M "\x. indicator A x *\<^sub>R f x" "\x. indicator A x *\<^sub>R g x"], simp add: indicator_def) subsection \Integrability and Measurability of the Diameter\ context fixes s :: "nat \ 'a \ 'b :: {second_countable_topology, banach}" and M assumes bounded: "\x. x \ space M \ bounded (range (\i. s i x))" begin lemma borel_measurable_diameter: assumes [measurable]: "\i. (s i) \ borel_measurable M" shows "(\x. diameter {s i x |i. n \ i}) \ borel_measurable M" proof - have "{s i x |i. N \ i} \ {}" for x N by blast hence diameter_SUP: "diameter {s i x |i. N \ i} = (SUP (i, j) \ {N..} \ {N..}. dist (s i x) (s j x))" for x N unfolding diameter_def by (auto intro!: arg_cong[of _ _ Sup]) have "case_prod dist ` ({s i x |i. n \ i} \ {s i x |i. n \ i}) = ((\(i, j). dist (s i x) (s j x)) ` ({n..} \ {n..}))" for x by fast hence *: "(\x. diameter {s i x |i. n \ i}) = (\x. Sup ((\(i, j). dist (s i x) (s j x)) ` ({n..} \ {n..})))" using diameter_SUP by (simp add: case_prod_beta') have "bounded ((\(i, j). dist (s i x) (s j x)) ` ({n..} \ {n..}))" if "x \ space M" for x by (rule bounded_imp_dist_bounded[OF bounded, OF that]) hence bdd: "bdd_above ((\(i, j). dist (s i x) (s j x)) ` ({n..} \ {n..}))" if "x \ space M" for x using that bounded_imp_bdd_above by presburger have "fst p \ borel_measurable M" "snd p \ borel_measurable M" if "p \ s ` {n..} \ s ` {n..}" for p using that by fastforce+ hence "(\x. fst p x - snd p x) \ borel_measurable M" if "p \ s ` {n..} \ s ` {n..}" for p using that borel_measurable_diff by simp hence "(\x. case p of (f, g) \ dist (f x) (g x)) \ borel_measurable M" if "p \ s ` {n..} \ s ` {n..}" for p unfolding dist_norm using that by measurable moreover have "countable (s ` {n..} \ s ` {n..})" by (intro countable_SIGMA countable_image, auto) ultimately show ?thesis unfolding * by (auto intro!: borel_measurable_cSUP bdd) qed lemma integrable_bound_diameter: fixes f :: "'a \ real" assumes "integrable M f" and [measurable]: "\i. (s i) \ borel_measurable M" and "\x i. x \ space M \ norm (s i x) \ f x" shows "integrable M (\x. diameter {s i x |i. n \ i})" proof - have "{s i x |i. N \ i} \ {}" for x N by blast hence diameter_SUP: "diameter {s i x |i. N \ i} = (SUP (i, j) \ {N..} \ {N..}. dist (s i x) (s j x))" for x N unfolding diameter_def by (auto intro!: arg_cong[of _ _ Sup]) { fix x assume x: "x \ space M" let ?S = "(\(i, j). dist (s i x) (s j x)) ` ({n..} \ {n..})" have "case_prod dist ` ({s i x |i. n \ i} \ {s i x |i. n \ i}) = (\(i, j). dist (s i x) (s j x)) ` ({n..} \ {n..})" by fast hence *: "diameter {s i x |i. n \ i} = Sup ?S" using diameter_SUP by (simp add: case_prod_beta') have "bounded ?S" by (rule bounded_imp_dist_bounded[OF bounded[OF x]]) hence Sup_S_nonneg:"0 \ Sup ?S" by (auto intro!: cSup_upper2 x bounded_imp_bdd_above) have "dist (s i x) (s j x) \ 2 * f x" for i j by (intro dist_triangle2[THEN order_trans, of _ 0]) (metis norm_conv_dist assms(3) x add_mono mult_2) hence "\c \ ?S. c \ 2 * f x" by force hence "Sup ?S \ 2 * f x" by (intro cSup_least, auto) hence "norm (Sup ?S) \ 2 * norm (f x)" using Sup_S_nonneg by auto also have "\ = norm (2 *\<^sub>R f x)" by simp finally have "norm (diameter {s i x |i. n \ i}) \ norm (2 *\<^sub>R f x)" unfolding * . } hence "AE x in M. norm (diameter {s i x |i. n \ i}) \ norm (2 *\<^sub>R f x)" by blast thus "integrable M (\x. diameter {s i x |i. n \ i})" using borel_measurable_diameter by (intro Bochner_Integration.integrable_bound[OF assms(1)[THEN integrable_scaleR_right[of 2]]], measurable) qed end subsection \Averaging Theorem\ text \We aim to lift results from the real case to arbitrary Banach spaces. Our fundamental tool in this regard will be the averaging theorem. The proof of this theorem is due to Serge Lang (Real and Functional Analysis) \<^cite>\"Lang_1993"\. The theorem allows us to make statements about a function's value almost everywhere, depending on the value its integral takes on various sets of the measure space.\ text \Before we introduce and prove the averaging theorem, we will first show the following lemma which is crucial for our proof. While not stated exactly in this manner, our proof makes use of the characterization of second-countable topological spaces given in the book General Topology by Ryszard Engelking (Theorem 4.1.15) \<^cite>\"engelking_1989"\. (Engelking's book \emph{General Topology})\ lemma balls_countable_basis: obtains D :: "'a :: {metric_space, second_countable_topology} set" where "topological_basis (case_prod ball ` (D \ (\ \ {0<..})))" and "countable D" and "D \ {}" proof - obtain D :: "'a set" where dense_subset: "countable D" "D \ {}" "\open U; U \ {}\ \ \y \ D. y \ U" for U using countable_dense_exists by blast have "topological_basis (case_prod ball ` (D \ (\ \ {0<..})))" proof (intro topological_basis_iff[THEN iffD2], fast, clarify) fix U and x :: 'a assume asm: "open U" "x \ U" obtain e where e: "e > 0" "ball x e \ U" using asm openE by blast obtain y where y: "y \ D" "y \ ball x (e / 3)" using dense_subset(3)[OF open_ball, of x "e / 3"] centre_in_ball[THEN iffD2, OF divide_pos_pos[OF e(1), of 3]] by force obtain r where r: "r \ \ \ {e/3<.. ball y r" using r y by (simp add: dist_commute) hence "ball y r \ U" using r by (intro order_trans[OF _ e(2)], simp, metric) moreover have "ball y r \ (case_prod ball ` (D \ (\ \ {0<..})))" using y(1) r by force ultimately show "\B'\(case_prod ball ` (D \ (\ \ {0<..}))). x \ B' \ B' \ U" using * by meson qed thus ?thesis using that dense_subset by blast qed context sigma_finite_measure begin text \To show statements concerning \\\-finite measure spaces, one usually shows the statement for finite measure spaces and uses a limiting argument to show it for the \\\-finite case. The following induction scheme formalizes this.\ lemma sigma_finite_measure_induct[case_names finite_measure, consumes 0]: assumes "\(N :: 'a measure) \. finite_measure N \ N = restrict_space M \ \ \ \ sets M \ emeasure N \ \ \ \ emeasure N \ \ 0 \ almost_everywhere N Q" and [measurable]: "Measurable.pred M Q" shows "almost_everywhere M Q" proof - have *: "almost_everywhere N Q" if "finite_measure N" "N = restrict_space M \" "\ \ sets M" "emeasure N \ \ \" for N \ using that by (cases "emeasure N \ = 0", auto intro: emeasure_0_AE assms(1)) obtain A :: "nat \ 'a set" where A: "range A \ sets M" "(\i. A i) = space M" and emeasure_finite: "emeasure M (A i) \ \" for i using sigma_finite by metis note A(1)[measurable] have space_restr: "space (restrict_space M (A i)) = A i" for i unfolding space_restrict_space by simp { fix i have *: "{x \ A i \ space M. Q x} = {x \ space M. Q x} \ (A i)" by fast have "Measurable.pred (restrict_space M (A i)) Q" using A by (intro measurableI, auto simp add: space_restr intro!: sets_restrict_space_iff[THEN iffD2], measurable, auto) } note this[measurable] { fix i have "finite_measure (restrict_space M (A i))" using emeasure_finite by (intro finite_measureI, subst space_restr, subst emeasure_restrict_space, auto) hence "emeasure (restrict_space M (A i)) {x \ A i. \Q x} = 0" using emeasure_finite by (intro AE_iff_measurable[THEN iffD1, OF _ _ *], measurable, subst space_restr[symmetric], intro sets.top, auto simp add: emeasure_restrict_space) hence "emeasure M {x \ A i. \ Q x} = 0" by (subst emeasure_restrict_space[symmetric], auto) } hence "emeasure M (\i. {x \ A i. \ Q x}) = 0" by (intro emeasure_UN_eq_0, auto) moreover have "(\i. {x \ A i. \ Q x}) = {x \ space M. \ Q x}" using A by auto ultimately show ?thesis by (intro AE_iff_measurable[THEN iffD2], auto) qed text \Real Functional Analysis - Lang\ text \The Averaging Theorem allows us to make statements concerning how a function behaves almost everywhere, depending on its behaviour on average.\ lemma averaging_theorem: fixes f::"_ \ 'b::{second_countable_topology, banach}" assumes [measurable]: "integrable M f" and closed: "closed S" and "\A. A \ sets M \ measure M A > 0 \ (1 / measure M A) *\<^sub>R set_lebesgue_integral M A f \ S" shows "AE x in M. f x \ S" proof (induct rule: sigma_finite_measure_induct) case (finite_measure N \) interpret finite_measure N by (rule finite_measure) have integrable[measurable]: "integrable N f" using assms finite_measure by (auto simp: integrable_restrict_space integrable_mult_indicator) have average: "(1 / Sigma_Algebra.measure N A) *\<^sub>R set_lebesgue_integral N A f \ S" if "A \ sets N" "measure N A > 0" for A proof - have *: "A \ sets M" using that by (simp add: sets_restrict_space_iff finite_measure) have "A = A \ \" by (metis finite_measure(2,3) inf.orderE sets.sets_into_space space_restrict_space that(1)) hence "set_lebesgue_integral N A f = set_lebesgue_integral M A f" unfolding finite_measure by (subst set_integral_restrict_space, auto simp add: finite_measure set_lebesgue_integral_def indicator_inter_arith[symmetric]) moreover have "measure N A = measure M A" using that by (auto intro!: measure_restrict_space simp add: finite_measure sets_restrict_space_iff) ultimately show ?thesis using that * assms(3) by presburger qed obtain D :: "'b set" where balls_basis: "topological_basis (case_prod ball ` (D \ (\ \ {0<..})))" and countable_D: "countable D" using balls_countable_basis by blast have countable_balls: "countable (case_prod ball ` (D \ (\ \ {0<..})))" using countable_rat countable_D by blast obtain B where B_balls: "B \ case_prod ball ` (D \ (\ \ {0<..}))" "\B = -S" using topological_basis[THEN iffD1, OF balls_basis] open_Compl[OF assms(2)] by meson hence countable_B: "countable B" using countable_balls countable_subset by fast define b where "b = from_nat_into (B \ {{}})" have "B \ {{}} \ {}" by simp have range_b: "range b = B \ {{}}" using countable_B by (auto simp add: b_def intro!: range_from_nat_into) have open_b: "open (b i)" for i unfolding b_def using B_balls open_ball from_nat_into[of "B \ {{}}" i] by force have Union_range_b: "\(range b) = -S" using B_balls range_b by simp { fix v r assume ball_in_Compl: "ball v r \ -S" define A where "A = f -` ball v r \ space N" have dist_less: "dist (f x) v < r" if "x \ A" for x using that unfolding A_def vimage_def by (simp add: dist_commute) hence AE_less: "AE x \ A in N. norm (f x - v) < r" by (auto simp add: dist_norm) have *: "A \ sets N" unfolding A_def by simp have "emeasure N A = 0" proof - { assume asm: "emeasure N A > 0" hence measure_pos: "measure N A > 0" unfolding emeasure_eq_measure by simp hence "(1 / measure N A) *\<^sub>R set_lebesgue_integral N A f - v = (1 / measure N A) *\<^sub>R set_lebesgue_integral N A (\x. f x - v)" using integrable integrable_const * by (subst set_integral_diff(2), auto simp add: set_integrable_def set_integral_const[OF *] algebra_simps intro!: integrable_mult_indicator) moreover have "norm (\x\A. (f x - v)\N) \ (\x\A. norm (f x - v)\N)" using * by (auto intro!: integral_norm_bound[of N "\x. indicator A x *\<^sub>R (f x - v)", THEN order_trans] integrable_mult_indicator integrable simp add: set_lebesgue_integral_def) ultimately have "norm ((1 / measure N A) *\<^sub>R set_lebesgue_integral N A f - v) \ set_lebesgue_integral N A (\x. norm (f x - v)) / measure N A" using asm by (auto intro: divide_right_mono) also have "\ < set_lebesgue_integral N A (\x. r) / measure N A" unfolding set_lebesgue_integral_def using asm * integrable integrable_const AE_less measure_pos by (intro divide_strict_right_mono integral_less_AE[of _ _ A] integrable_mult_indicator) (fastforce simp add: dist_less dist_norm indicator_def)+ also have "\ = r" using * measure_pos by (simp add: set_integral_const) finally have "dist ((1 / measure N A) *\<^sub>R set_lebesgue_integral N A f) v < r" by (subst dist_norm) hence "False" using average[OF * measure_pos] by (metis ComplD dist_commute in_mono mem_ball ball_in_Compl) } thus ?thesis by fastforce qed } note * = this { fix b' assume "b' \ B" hence ball_subset_Compl: "b' \ -S" and ball_radius_pos: "\v \ D. \r>0. b' = ball v r" using B_balls by (blast, fast) } note ** = this hence "emeasure N (f -` b i \ space N) = 0" for i by (cases "b i = {}", simp) (metis UnE singletonD * range_b[THEN eq_refl, THEN range_subsetD]) hence "emeasure N (\i. f -` b i \ space N) = 0" using open_b by (intro emeasure_UN_eq_0) fastforce+ moreover have "(\i. f -` b i \ space N) = f -` (\(range b)) \ space N" by blast ultimately have "emeasure N (f -` (-S) \ space N) = 0" using Union_range_b by argo hence "AE x in N. f x \ -S" using open_Compl[OF assms(2)] by (intro AE_iff_measurable[THEN iffD2], auto) thus ?case by force qed (simp add: pred_sets2[OF borel_closed] assms(2)) lemma density_zero: fixes f::"'a \ 'b::{second_countable_topology, banach}" assumes "integrable M f" and density_0: "\A. A \ sets M \ set_lebesgue_integral M A f = 0" shows "AE x in M. f x = 0" using averaging_theorem[OF assms(1), of "{0}"] assms(2) by (simp add: scaleR_nonneg_nonneg) text \The following lemma shows that densities are unique in Banach spaces.\ lemma density_unique_banach: fixes f f'::"'a \ 'b::{second_countable_topology, banach}" assumes "integrable M f" "integrable M f'" and density_eq: "\A. A \ sets M \ set_lebesgue_integral M A f = set_lebesgue_integral M A f'" shows "AE x in M. f x = f' x" proof- { fix A assume asm: "A \ sets M" hence "LINT x|M. indicat_real A x *\<^sub>R (f x - f' x) = 0" using density_eq assms(1,2) by (simp add: set_lebesgue_integral_def algebra_simps Bochner_Integration.integral_diff[OF integrable_mult_indicator(1,1)]) } thus ?thesis using density_zero[OF Bochner_Integration.integrable_diff[OF assms(1,2)]] by (simp add: set_lebesgue_integral_def) qed lemma density_nonneg: fixes f::"_ \ 'b::{second_countable_topology, banach, linorder_topology, ordered_real_vector}" assumes "integrable M f" and "\A. A \ sets M \ set_lebesgue_integral M A f \ 0" shows "AE x in M. f x \ 0" using averaging_theorem[OF assms(1), of "{0..}", OF closed_atLeast] assms(2) by (simp add: scaleR_nonneg_nonneg) corollary integral_nonneg_eq_0_iff_AE_banach: fixes f :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" assumes f[measurable]: "integrable M f" and nonneg: "AE x in M. 0 \ f x" shows "integral\<^sup>L M f = 0 \ (AE x in M. f x = 0)" proof assume *: "integral\<^sup>L M f = 0" { fix A assume asm: "A \ sets M" have "0 \ integral\<^sup>L M (\x. indicator A x *\<^sub>R f x)" using nonneg by (subst integral_zero[of M, symmetric], intro integral_mono_AE_banach integrable_mult_indicator asm f integrable_zero, auto simp add: indicator_def) moreover have "\ \ integral\<^sup>L M f" using nonneg by (intro integral_mono_AE_banach integrable_mult_indicator asm f, auto simp add: indicator_def) ultimately have "set_lebesgue_integral M A f = 0" unfolding set_lebesgue_integral_def using * by force } thus "AE x in M. f x = 0" by (intro density_zero f, blast) qed (auto simp add: integral_eq_zero_AE) corollary integral_eq_mono_AE_eq_AE: fixes f g :: "'a \ 'b :: {second_countable_topology, banach, linorder_topology, ordered_real_vector}" assumes "integrable M f" "integrable M g" "integral\<^sup>L M f = integral\<^sup>L M g" "AE x in M. f x \ g x" shows "AE x in M. f x = g x" proof - define h where "h = (\x. g x - f x)" have "AE x in M. h x = 0" unfolding h_def using assms by (subst integral_nonneg_eq_0_iff_AE_banach[symmetric]) auto then show ?thesis unfolding h_def by auto qed end end