diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,673 +1,674 @@ ADS_Functor AI_Planning_Languages_Semantics AODV AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Ackermanns_not_PR Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Blue_Eyes Bondy Boolean_Expression_Checkers Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CISC-Kernel CRDT CSP_RefTK CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Cauchy Cayley_Hamilton Certification_Monads Chandy_Lamport Chord_Segments Circus Clean ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots CryptHOL CryptoBasedCompositionalProperties Cubic_Quartic_Equations DFS_Framework DOM_Components DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Dedekind_Real Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation DiskPaxos Dominance_CHK DynamicArchitectures Dynamic_Tables E_Transcendental Echelon_Form EdmondsKarp_Maxflow Efficient-Mergesort Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Eval_FO Example-Submission Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 FOL_Seq_Calc3 Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier FO_Theory_Rewriting Free-Boolean-Algebra Free-Groups Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL Hyperdual IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IP_Addresses Imperative_Insertion_Sort Impossible_Geometry Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq Isabelle_C Isabelle_Marries_Dirac Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Kleene_Algebra Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lowe_Ontological_Argument Lower_Semicontinuous Lp LP_Duality Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multi_Party_Computation Multirelations Myhill-Nerode Name_Carrying_Type_Inference Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers Nominal2 Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Octonions OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker PAL PCF PLM POPLmark-deBruijn PSemigroupsConvolution Padic_Ints Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Poincare_Bendixson Poincare_Disc Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic QHLProver QR_Decomposition Quantales Quasi_Borel_Spaces Quaternions Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewriting_Z Ribbon_Proofs Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 Safe_Distance Safe_OCL Saturation_Framework Saturation_Framework_Extensions Schutz_Spacetime Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds +Sophomores_Dream Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras SumSquares Sunflowers SuperCalc Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Timed_Automata Topological_Semantics Topology TortoiseHare Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Treaps Tree-Automata Tree_Decomposition Triangle Trie Twelvefold_Way Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith VYDRA_MDL WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeta_3_Irrational Zeta_Function pGCL diff --git a/thys/Sophomores_Dream/ROOT b/thys/Sophomores_Dream/ROOT new file mode 100644 --- /dev/null +++ b/thys/Sophomores_Dream/ROOT @@ -0,0 +1,12 @@ +chapter AFP + +session Sophomores_Dream (AFP) = "HOL-Analysis" + + options [timeout = 900] + sessions + "HOL-Real_Asymp" + theories + Sophomores_Dream + document_files + "root.tex" + "root.bib" + diff --git a/thys/Sophomores_Dream/Sophomores_Dream.thy b/thys/Sophomores_Dream/Sophomores_Dream.thy new file mode 100644 --- /dev/null +++ b/thys/Sophomores_Dream/Sophomores_Dream.thy @@ -0,0 +1,522 @@ +(* + File: Sophomores_Dream.thy + Author: Manuel Eberl, University of Innsbruck +*) +section \The Sophomore's Dream\ +theory Sophomores_Dream + imports "HOL-Analysis.Analysis" "HOL-Real_Asymp.Real_Asymp" +begin + +text \ + This formalisation mostly follows the very clear proof sketch from Wikipedia~\cite{wikipedia}. + That article also provides an interesting historical perspective. A more detailed + exploration of Bernoulli's historical proof can be found in the book by Dunham~\cite{dunham}. + + The name `Sophomore's Dream' apparently comes from a book by Borwein et al., in analogy to + the `Freshman's Dream' equation $(x+y)^n = x^n + y^n$ (which is generally \<^emph>\not\ true except + in rings of characteristic $n$). +\ + +subsection \Auxiliary material\ + +(* TODO: Move to library! *) +lemma integrable_cong: + assumes "\x. x \ A \ f x = g x" + shows "f integrable_on A \ g integrable_on A" + using has_integral_cong [OF assms] by fast + +lemma has_integral_cmul_iff': + assumes "c \ 0" + shows "((\x. c *\<^sub>R f x) has_integral I) A \ (f has_integral I /\<^sub>R c) A" + using assms by (metis divideR_right has_integral_cmul_iff) + +lemma has_integral_Icc_iff_Ioo: + fixes f :: "real \ 'a :: banach" + shows "(f has_integral I) {a..b} \ (f has_integral I) {a<.. {a..b} - {a<.. 0}" + by (rule negligible_subset [of "{a,b}"]) auto + show "negligible {x \ {a<.. 0}" + by (rule negligible_subset [of "{}"]) auto +qed + +lemma integrable_on_Icc_iff_Ioo: + fixes f :: "real \ 'a :: banach" + shows "f integrable_on {a..b} \ f integrable_on {a<.. 'a :: banach" + assumes "summable (\n. norm (f n))" and "f sums S" + shows "has_sum f (UNIV :: nat set) S" + unfolding has_sum_def tendsto_iff eventually_finite_subsets_at_top +proof (safe, goal_cases) + case (1 \) + from assms(1) obtain S' where S': "(\n. norm (f n)) sums S'" + by (auto simp: summable_def) + with 1 obtain N where N: "\n. n \ N \ \S' - (\i < \" + by (auto simp: tendsto_iff eventually_at_top_linorder sums_def dist_norm abs_minus_commute) + + show ?case + proof (rule exI[of _ "{..n. if n \ Y then 0 else f n) sums (S - sum f Y)" + by (intro sums_If_finite_set'[OF \f sums S\]) (auto simp: sum_negf) + hence "S - sum f Y = (\n. if n \ Y then 0 else f n)" + by (simp add: sums_iff) + also have "norm \ \ (\n. norm (if n \ Y then 0 else f n))" + by (rule summable_norm[OF summable_comparison_test'[OF assms(1)]]) auto + also have "\ \ (\n. if n < N then 0 else norm (f n))" + using 2 by (intro suminf_le summable_comparison_test'[OF assms(1)]) auto + also have "(\n. if n \ {..in. if n < N then 0 else norm (f n)) = S' - (\ii \S' - (\i" by simp + also have "\ < \" by (rule N) auto + finally show ?case by (simp add: dist_norm norm_minus_commute) + qed auto +qed + +lemma norm_summable_imp_summable_on: + fixes f :: "nat \ 'a :: banach" + assumes "summable (\n. norm (f n))" + shows "f summable_on UNIV" + using norm_summable_imp_has_sum[OF assms, of "suminf f"] assms + by (auto simp: sums_iff summable_on_def dest: summable_norm_cancel) + +lemma summable_comparison_test_bigo: + fixes f :: "nat \ real" + assumes "summable (\n. norm (g n))" "f \ O(g)" + shows "summable f" +proof - + from \f \ O(g)\ obtain C where C: "eventually (\x. norm (f x) \ C * norm (g x)) at_top" + by (auto elim: landau_o.bigE) + thus ?thesis + by (rule summable_comparison_test_ev) (insert assms, auto intro: summable_mult) +qed + + +subsection \Continuity and bounds for $x \log x$\ + +lemma x_log_x_continuous: "continuous_on {0..1} (\x::real. x * ln x)" +proof - + have "continuous (at x within {0..1}) (\x::real. x * ln x)" if "x \ {0..1}" for x + proof (cases "x = 0") + case True + have "((\x::real. x * ln x) \ 0) (at_right 0)" + by real_asymp + thus ?thesis using True + by (simp add: continuous_def Lim_ident_at at_within_Icc_at_right) + qed (auto intro!: continuous_intros) + thus ?thesis + using continuous_on_eq_continuous_within by blast +qed + +lemma x_log_x_within_01_le: + assumes "x \ {0..(1::real)}" + shows "x * ln x \ {-exp (-1)..0}" +proof - + have "x * ln x \ 0" + using assms by (cases "x = 0") (auto simp: mult_nonneg_nonpos) + let ?f = "\x::real. x * ln x" + have diff: "(?f has_field_derivative (ln x + 1)) (at x)" if "x > 0" for x + using that by (auto intro!: derivative_eq_intros) + have diff': "?f differentiable at x" if "x > 0" for x + using diff[OF that] real_differentiable_def by blast + + consider "x = 0" | "x = 1" | "x = exp (-1)" | "0 < x" "x < exp (-1)" | "exp (-1) < x" "x < 1" + using assms unfolding atLeastAtMost_iff by linarith + hence "x * ln x \ -exp (-1)" + proof cases + assume x: "0 < x" "x < exp (-1)" + have "\l z. x < z \ z < exp (-1) \ (?f has_real_derivative l) (at z) \ + ?f (exp (-1)) - ?f x = (exp (-1) - x) * l" + using x by (intro MVT continuous_on_subset [OF x_log_x_continuous] diff') auto + then obtain l z where lz: + "x < z" "z < exp (-1)" "(?f has_real_derivative l) (at z)" + "?f x = -exp (-1) - (exp (-1) - x) * l" + by (auto simp: algebra_simps) + have [simp]: "l = ln z + 1" + using DERIV_unique[OF diff[of z] lz(3)] lz(1) x by auto + have "ln z \ ln (exp (-1))" + using lz x by (subst ln_le_cancel_iff) auto + hence "(exp (- 1) - x) * l \ 0" + using x lz by (intro mult_nonneg_nonpos) auto + with lz show ?thesis + by linarith + next + assume x: "exp (-1) < x" "x < 1" + have "\l z. exp (-1) < z \ z < x \ (?f has_real_derivative l) (at z) \ + ?f x - ?f (exp (-1)) = (x - exp (-1)) * l" + proof (intro MVT continuous_on_subset [OF x_log_x_continuous] diff') + fix t :: real assume t: "exp (-1) < t" + show "t > 0" + by (rule less_trans [OF _ t]) auto + qed (use x in auto) + then obtain l z where lz: + "exp (-1) < z" "z < x" "(?f has_real_derivative l) (at z)" + "?f x = -exp (-1) - (exp (-1) - x) * l" + by (auto simp: algebra_simps) + have "z > 0" + by (rule less_trans [OF _ lz(1)]) auto + have [simp]: "l = ln z + 1" + using DERIV_unique[OF diff[of z] lz(3)] \z > 0\ by auto + have "ln z \ ln (exp (-1))" + using lz \z > 0\ by (subst ln_le_cancel_iff) auto + hence "(exp (- 1) - x) * l \ 0" + using x lz by (intro mult_nonpos_nonneg) auto + with lz show ?thesis + by linarith + qed auto + + with \x * ln x \ 0\ show ?thesis + by auto +qed + + +subsection \Convergence, Summability, Integrability\ + +text \ + As a first result we can show that the two sums that occur in the two different versions + of the Sophomore's Dream are absolutely summable. This is achieved by a simple comparison + test with the series $\sum_{k=1}^\infty k^{-2}$, as $k^{-k} \in O(k^{-2})$. +\ +theorem abs_summable_sophomores_dream: "summable (\k. 1 / real (k ^ k))" +proof (rule summable_comparison_test_bigo) + show "(\k. 1 / real (k ^ k)) \ O(\k. 1 / real k ^ 2)" + by real_asymp + show "summable (\n. norm (1 / real n ^ 2))" + using inverse_power_summable[of 2, where ?'a = real] by (simp add: field_simps) +qed + +text \ + The existence of the integral is also fairly easy to show since the integrand is continuous + and the integration domain is compact. There is, however, one hiccup: The integrand is not + actually continuous. + + We have $\lim_{x\to 0} x^x = 1$, but in Isabelle $0^0$ is defined as \0\ (for real numbers). + Thus, there is a discontinuity at \x = 0\ + + However, this is a removable discontinuity since for any $x>0$ we have $x^x = e^{x\log x}$, and + as we have just shown, $e^{x \log x}$ \<^emph>\is\ continuous on $[0, 1]$. Since the two integrands + differ only for \x = 0\ (which is negligible), the integral still exists. +\ +theorem integrable_sophomores_dream: "(\x::real. x powr x) integrable_on {0..1}" +proof - + have "(\x::real. exp (x * ln x)) integrable_on {0..1}" + by (intro integrable_continuous_real continuous_on_exp x_log_x_continuous) + also have "?this \ (\x::real. exp (x * ln x)) integrable_on {0<..<1}" + by (simp add: integrable_on_Icc_iff_Ioo) + also have "\ \ (\x::real. x powr x) integrable_on {0<..<1}" + by (intro integrable_cong) (auto simp: powr_def) + also have "\ \ ?thesis" + by (simp add: integrable_on_Icc_iff_Ioo) + finally show ?thesis . +qed + +text \ + Next, we have to show the absolute convergence of the two auxiliary sums that will occur in + our proofs so that we can exchange the order of integration and summation. This is done + with a straightforward application of the Weierstra\ss\ \M\ test. +\ +lemma uniform_limit_sophomores_dream1: + "uniform_limit {0..(1::real)} + (\n x. \kx. \k. (x * ln x) ^ k / fact k) + sequentially" +proof (rule Weierstrass_m_test) + show "summable (\k. exp (-1) ^ k / fact k :: real)" + using summable_exp[of "exp (-1)"] by (simp add: field_simps) +next + fix k :: nat and x :: real + assume x: "x \ {0..1}" + have "norm ((x * ln x) ^ k / fact k) = norm (x * ln x) ^ k / fact k" + by (simp add: power_abs) + also have "\ \ exp (-1) ^ k / fact k" + by (intro divide_right_mono power_mono) (use x_log_x_within_01_le [of x] x in auto) + finally show "norm ((x * ln x) ^ k / fact k) \ exp (- 1) ^ k / fact k" . +qed + +lemma uniform_limit_sophomores_dream2: + "uniform_limit {0..(1::real)} + (\n x. \kx. \k. (-(x * ln x)) ^ k / fact k) + sequentially" +proof (rule Weierstrass_m_test) + show "summable (\k. exp (-1) ^ k / fact k :: real)" + using summable_exp[of "exp (-1)"] by (simp add: field_simps) +next + fix k :: nat and x :: real + assume x: "x \ {0..1}" + have "norm ((-x * ln x) ^ k / fact k) = norm (x * ln x) ^ k / fact k" + by (simp add: power_abs) + also have "\ \ exp (-1) ^ k / fact k" + by (intro divide_right_mono power_mono) (use x_log_x_within_01_le [of x] x in auto) + finally show "norm ((-(x * ln x)) ^ k / fact k) \ exp (- 1) ^ k / fact k" by simp +qed + + +subsection \An auxiliary integral\ + +text \ + Next we compute the integral + \[\int_0^1 (x\log x)^n\,\text{d}x = \frac{(-1)^n\, n!}{(n+1)^{n+1}}\ ,\] + which is a key ingredient in our proof. +\ +lemma sophomores_dream_aux_integral: + "((\x. (x * ln x) ^ n) has_integral (- 1) ^ n * fact n / real ((n + 1) ^ (n + 1))) {0<..<1}" +proof - + have "((\t. t powr real n / exp t) has_integral fact n) {0..}" + using Gamma_integral_real[of "n + 1"] by (auto simp: Gamma_fact powr_realpow) + also have "?this \ ((\t. t powr real n / exp t) has_integral fact n) {0<..}" + proof (rule has_integral_spike_set_eq) + have eq: "{x \ {0<..} - {0..}. x powr real n / exp x \ 0} = {}" + by auto + thus "negligible {x \ {0<..} - {0..}. x powr real n / exp x \ 0}" + by (subst eq) auto + have "{x \ {0..} - {0<..}. x powr real n / exp x \ 0} \ {0}" + by auto + moreover have "negligible {0::real}" + by simp + ultimately show "negligible {x \ {0..} - {0<..}. x powr real n / exp x \ 0}" + by (meson negligible_subset) + qed + also have "\ \ ((\t::real. t ^ n / exp t) has_integral fact n) {0<..}" + by (intro has_integral_spike_eq) (auto simp: powr_realpow) + finally have 1: "((\t::real. t ^ n / exp t) has_integral fact n) {0<..}" . + + have "(\x::real. \x\ ^ n / exp x) integrable_on {0<..} \ + (\x::real. x ^ n / exp x) integrable_on {0<..}" + by (intro integrable_cong) auto + hence 2: "(\t::real. t ^ n / exp t) absolutely_integrable_on {0<..}" + using 1 by (simp add: absolutely_integrable_on_def power_abs has_integral_iff) + + define g :: "real \ real" where "g = (\x. -ln x * (n + 1))" + define g' :: "real \ real" where "g' = (\x. -(n + 1) / x)" + define h :: "real \ real" where "h = (\u. exp (-u / (n + 1)))" + have bij: "bij_betw g {0<..<1} {0<..}" + by (rule bij_betwI[of _ _ _ h]) (auto simp: g_def h_def mult_neg_pos) + have deriv: "(g has_real_derivative g' x) (at x within {0<..<1})" + if "x \ {0<..<1}" for x + unfolding g_def g'_def using that by (auto intro!: derivative_eq_intros simp: field_simps) + + have "(\t::real. t ^ n / exp t) absolutely_integrable_on g ` {0<..<1} \ + integral (g ` {0<..<1}) (\t::real. t ^ n / exp t) = fact n" + using 1 2 bij by (simp add: bij_betw_def has_integral_iff) + also have "?this \ ((\x. \g' x\ *\<^sub>R (g x ^ n / exp (g x))) absolutely_integrable_on {0<..<1} \ + integral {0<..<1} (\x. \g' x\ *\<^sub>R (g x ^ n / exp (g x))) = fact n)" + by (intro has_absolute_integral_change_of_variables_1' [symmetric] deriv) + (auto simp: inj_on_def g_def) + finally have "((\x. \g' x\ *\<^sub>R (g x ^ n / exp (g x))) has_integral fact n) {0<..<1}" + using eq_integralD set_lebesgue_integral_eq_integral(1) by blast + also have "?this \ + ((\x::real. ((-1)^n*(n+1)^(n+1)) *\<^sub>R (ln x ^ n * x ^ n)) has_integral fact n) {0<..<1}" + proof (rule has_integral_cong) + fix x :: real assume x: "x \ {0<..<1}" + have "\g' x\ *\<^sub>R (g x ^ n / exp (g x)) = + (-1) ^ n * (real n + 1) ^ (n + 1) * ln x ^ n * (exp (ln x * (n + 1)) / x)" + using x by (simp add: g_def g'_def exp_minus power_minus' divide_simps add_ac) + also have "exp (ln x * (n + 1)) = x powr real (n + 1)" + using x by (simp add: powr_def) + also have "\ / x = x ^ n" + using x by (subst powr_realpow) auto + finally show "\g' x\ *\<^sub>R (g x ^ n / exp (g x)) = + ((-1)^n*(n+1)^(n+1)) *\<^sub>R (ln x ^ n * x ^ n)" + by (simp add: algebra_simps) + qed + also have "\ \ ((\x::real. ln x ^ n * x ^ n) has_integral + fact n /\<^sub>R real_of_int ((- 1) ^ n * int ((n + 1) ^ (n + 1)))) {0<..<1}" + by (intro has_integral_cmul_iff') (auto simp del: power_Suc) + also have "fact n /\<^sub>R real_of_int ((- 1) ^ n * int ((n + 1) ^ (n + 1))) = + (-1) ^ n * fact n / (n+1) ^ (n+1)" + by (auto simp: divide_simps) + finally show ?thesis + by (simp add: power_mult_distrib mult_ac) +qed + +subsection \Main proofs\ + + +text \ + We can now show the first formula: $\int_0^1 x^{-x}\,\text{d}x = \sum_{n=1}^\infty n^{-n}$ +\ +lemma sophomores_dream_aux1: + "summable (\k. 1 / real ((k+1)^(k+1)))" + "integral {0..1} (\x. x powr (-x)) = (\n. 1 / (n+1)^(n+1))" +proof - + define S where "S = (\x::real. \k. (-(x * ln x)) ^ k / fact k)" + have S_eq: "S x = x powr (-x)" if "x > 0" for x + proof - + have "S x = exp (-x * ln x)" + by (simp add: S_def exp_def field_simps) + also have "\ = x powr (-x)" + using \x > 0\ by (simp add: powr_def) + finally show ?thesis . + qed + + have cont: "continuous_on {0..1} (\x::real. \kn. ((\x. \k J" + using uniform_limit_integral [OF uniform_limit_sophomores_dream2 cont] by (auto simp: S_def) + + note \(S has_integral J) {0..1}\ + also have "(S has_integral J) {0..1} \ (S has_integral J) {0<..<1}" + by (simp add: has_integral_Icc_iff_Ioo) + also have "\ \ ((\x. x powr (-x)) has_integral J) {0<..<1}" + by (intro has_integral_cong) (use S_eq in auto) + also have "\ \ ((\x. x powr (-x)) has_integral J) {0..1}" + by (simp add: has_integral_Icc_iff_Ioo) + finally have integral: "((\x. x powr (-x)) has_integral J) {0..1}" . + + have I_eq: "I = (\n. \kx::real. \kkx::real. \kx::real. \kkkkk. 1 / real ((k + 1) ^ (k + 1))) sums J" + using IJ(3) I_eq by (simp add: sums_def) + + from sums show "summable (\k. 1 / real ((k+1)^(k+1)))" + by (simp add: sums_iff) + from integral sums show "integral {0..1} (\x. x powr (-x)) = (\n. 1 / (n+1)^(n+1))" + by (simp add: sums_iff has_integral_iff) +qed + +theorem sophomores_dream1: + "(\k::nat. norm (k powi (-k))) summable_on {1..}" + "integral {0..1} (\x. x powr (-x)) = (\\<^sub>\ k\{(1::nat)..}. k powi (-k))" +proof - + let ?I = "integral {0..1} (\x. x powr (-x))" + have "(\k::nat. norm (k powi (-k))) summable_on UNIV" + using abs_summable_sophomores_dream + by (intro norm_summable_imp_summable_on) (auto simp: power_int_minus field_simps) + thus "(\k::nat. norm (k powi (-k))) summable_on {1..}" + by (rule summable_on_subset_banach) auto + + have "(\n. 1 / (n+1)^(n+1)) sums ?I" + using sophomores_dream_aux1 by (simp add: sums_iff) + moreover have "summable (\n. norm (1 / real (Suc n ^ Suc n)))" + by (subst summable_Suc_iff) (use abs_summable_sophomores_dream in \auto simp: field_simps\) + ultimately have "has_sum (\n::nat. 1 / (n+1)^(n+1)) UNIV ?I" + by (intro norm_summable_imp_has_sum) auto + also have "?this \ has_sum ((\n::nat. 1 / n^n) \ Suc) UNIV ?I" + by (simp add: o_def field_simps) + also have "\ \ has_sum (\n::nat. 1 / n ^ n) (Suc ` UNIV) ?I" + by (intro has_sum_reindex [symmetric]) auto + also have "Suc ` UNIV = {1..}" + using greaterThan_0 by auto + also have "has_sum (\n::nat. (1 / real (n ^ n))) {1..} ?I \ + has_sum (\n::nat. n powi (-n)) {1..} ?I" + by (intro has_sum_cong) (auto simp: power_int_minus field_simps power_minus') + finally show "integral {0..1} (\x. x powr (-x)) = (\\<^sub>\k\{(1::nat)..}. k powi (-k))" + by (auto dest!: infsumI simp: algebra_simps) +qed + + +text \ + Next, we show the second formula: $\int_0^1 x^x\,\text{d}x = -\sum_{n=1}^\infty (-n)^{-n}$ +\ +lemma sophomores_dream_aux2: + "summable (\k. (-1) ^ k / real ((k+1)^(k+1)))" + "integral {0..1} (\x. x powr x) = (\n. (-1)^n / (n+1)^(n+1))" +proof - + define S where "S = (\x::real. \k. (x * ln x) ^ k / fact k)" + have S_eq: "S x = x powr x" if "x > 0" for x + proof - + have "S x = exp (x * ln x)" + by (simp add: S_def exp_def field_simps) + also have "\ = x powr x" + using \x > 0\ by (simp add: powr_def) + finally show ?thesis . + qed + + have cont: "continuous_on {0..1} (\x::real. \kn. ((\x. \k J" + using uniform_limit_integral [OF uniform_limit_sophomores_dream1 cont] by (auto simp: S_def) + + note \(S has_integral J) {0..1}\ + also have "(S has_integral J) {0..1} \ (S has_integral J) {0<..<1}" + by (simp add: has_integral_Icc_iff_Ioo) + also have "\ \ ((\x. x powr x) has_integral J) {0<..<1}" + by (intro has_integral_cong) (use S_eq in auto) + also have "\ \ ((\x. x powr x) has_integral J) {0..1}" + by (simp add: has_integral_Icc_iff_Ioo) + finally have integral: "((\x. x powr x) has_integral J) {0..1}" . + + have I_eq: "I = (\n. \kx::real. \kkkkkk. (-1) ^ k / real ((k + 1) ^ (k + 1))) sums J" + using IJ(3) I_eq by (simp add: sums_def) + + from sums show "summable (\k. (-1) ^ k / real ((k+1)^(k+1)))" + by (simp add: sums_iff) + from integral sums show "integral {0..1} (\x. x powr x) = (\n. (-1)^n / (n+1)^(n+1))" + by (simp add: sums_iff has_integral_iff) +qed + +theorem sophomores_dream2: + "(\k::nat. norm ((-k) powi (-k))) summable_on {1..}" + "integral {0..1} (\x. x powr x) = -(\\<^sub>\ k\{(1::nat)..}. (-k) powi (-k))" +proof - + let ?I = "integral {0..1} (\x. x powr x)" + have "(\k::nat. norm ((-k) powi (-k))) summable_on UNIV" + using abs_summable_sophomores_dream + by (intro norm_summable_imp_summable_on) (auto simp: power_int_minus field_simps) + thus "(\k::nat. norm ((-k) powi (-k))) summable_on {1..}" + by (rule summable_on_subset_banach) auto + + have "(\n. (-1)^n / (n+1)^(n+1)) sums ?I" + using sophomores_dream_aux2 by (simp add: sums_iff) + moreover have "summable (\n. 1 / real (Suc n ^ Suc n))" + by (subst summable_Suc_iff) (use abs_summable_sophomores_dream in \auto simp: field_simps\) + hence "summable (\n. norm ((- 1) ^ n / real (Suc n ^ Suc n)))" + by simp + ultimately have "has_sum (\n::nat. (-1)^n / (n+1)^(n+1)) UNIV ?I" + by (intro norm_summable_imp_has_sum) auto + also have "?this \ has_sum ((\n::nat. -((-1)^n / n^n)) \ Suc) UNIV ?I" + by (simp add: o_def field_simps) + also have "\ \ has_sum (\n::nat. -((-1)^n / n ^ n)) (Suc ` UNIV) ?I" + by (intro has_sum_reindex [symmetric]) auto + also have "Suc ` UNIV = {1..}" + using greaterThan_0 by auto + also have "has_sum (\n::nat. -((- 1) ^ n / real (n ^ n))) {1..} ?I \ + has_sum (\n::nat. -((-n) powi (-n))) {1..} ?I" + by (intro has_sum_cong) (auto simp: power_int_minus field_simps power_minus') + also have "\ \ has_sum (\n::nat. (-n) powi (-n)) {1..} (-?I)" + by (simp add: has_sum_uminus) + finally show "integral {0..1} (\x. x powr x) = -(\\<^sub>\k\{(1::nat)..}. (-k) powi (-k))" + by (auto dest!: infsumI simp: algebra_simps) +qed + +end \ No newline at end of file diff --git a/thys/Sophomores_Dream/document/root.bib b/thys/Sophomores_Dream/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Sophomores_Dream/document/root.bib @@ -0,0 +1,35 @@ +@book {bernoulli, + title = "Opera omnia", + author = "Johann Bernoulli", + year = 1697, + volume = 3, + pages = {376--381} +} + +@misc{wikipedia, + author = "{Wikipedia contributors}", + title = "Sophomore's dream --- {Wikipedia}{,} The Free Encyclopedia", + year = "2021", + howpublished = "\url{https://en.wikipedia.org/w/index.php?title=Sophomore%27s_dream&oldid=1053905038}", + note = "[Online; accessed 10-April-2022]" +} + +@book{dunham, + title = {The Calculus Gallery: Masterpieces from {N}ewton to {L}ebesgue}, + author = {William Dunham}, + publisher = {Princeton University Press}, + isbn = {9780691095653}, + year = {2004}, + pages = {46--51} +} + +@book{borwein, + title = {Experimentation in Mathematics: Computational Paths to Discovery}, + author = {Jonathan Borwein, David Bailey, Roland Girgensohn}, + publisher = {CRC Press}, + isbn = {9781568811369}, + year = {2004}, + edition = {1}, + pages = {4,44} +} + diff --git a/thys/Sophomores_Dream/document/root.tex b/thys/Sophomores_Dream/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Sophomores_Dream/document/root.tex @@ -0,0 +1,39 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{isabelle,isabellesym} +\usepackage{amsfonts,amsmath,amssymb} +\usepackage{pgfplots} + +% this should be the last package used +\usepackage{pdfsetup} + +% urls in roman style, theory text in math-similar italics +\urlstyle{rm} +\isabellestyle{it} + +\begin{document} + +\title{The Sophomore's Dream} +\author{Manuel Eberl} +\maketitle + +\begin{abstract} +This article provides a brief formalisation of the two equations known as the \emph{Sophomore's Dream}, first discovered by Johann Bernoulli~\cite{bernoulli} in 1697: +\[\int_0^1 x^{-x}\,\text{d}x = \sum_{n=1}^\infty n^{-n} \quad\text{and}\quad \int_0^1 x^x\,\text{d}x = -\sum_{n=1}^\infty (-n)^{-n}\] +\end{abstract} + +\tableofcontents +\parindent 0pt\parskip 0.5ex + +\input{session} + +\nocite{corless96} +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: t +%%% End: