diff --git a/thys/Example-Submission/ROOT b/thys/Example-Submission/ROOT --- a/thys/Example-Submission/ROOT +++ b/thys/Example-Submission/ROOT @@ -1,33 +1,33 @@ (* All sessions must be in chapter AFP *) chapter AFP (* There must be one session with the (short) name of the entry. This session generates the web document and HTML files. - It is strongly encouraged to have precisely one session, but it + It is strongly encouraged to have precisely one session, but if needed, further sessions are permitted. Every theory must be included in at least one of the sessions. *) (* Session name, list base session: *) session "Example-Submission" = HOL + (* Timeout (in sec) in case of non-termination problems *) options [timeout = 600] (* To suppress document generation of some theories: *) (* theories [document = false] This_Theory That_Theory *) (* The top-level theories of the submission: *) theories Submission (* Dependencies on document source files: *) document_files "root.bib" "root.tex" diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,811 +1,812 @@ ABY3_Protocols ADS_Functor AI_Planning_Languages_Semantics AODV AOT 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 Approximate_Model_Counting 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 Balog_Szemeredi_Gowers Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binary_Code_Imprimitive Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Birkhoff_Finite_Distributive_Lattices Blue_Eyes Bondy Boolean_Expression_Checkers Boolos_Curious_Inference Boolos_Curious_Inference_Automated Bounded_Deducibility_Security Broadcast_Psi Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CHERI-C_Memory_Model CISC-Kernel Concentration_Inequalities CRDT CRYSTALS-Kyber CRYSTALS-Kyber_Security CSP_RefTK CVP_Hardness CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cardinality_Continuum Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Catoids Cauchy Cayley_Hamilton Certification_Monads Ceva Chandy_Lamport Chebyshev_Polynomials Chord_Segments Circus Clean Clique_and_Monotone_Circuits ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinable_Wands Combinatorial_Enumeration_Algorithms Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon CommCSL Commuting_Hermitian 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 CondNormReasHOL Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers Continued_Fractions Cook_Levin CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots Coupledsim_Contrasim CryptHOL CryptoBasedCompositionalProperties Crypto_Standards CubicalCategories Cubic_Quartic_Equations DCR-ExecutionEquivalence DFS_Framework DOM_Components DPRM_Theorem 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 DigitsInBase Digit_Expansions Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Directed_Sets Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation Disintegration DiskPaxos Distributed_Distinct_Elements Dominance_CHK Doob_Convergence DynamicArchitectures Dynamic_Tables E_Transcendental Earley_Parser Echelon_Form EdmondsKarp_Maxflow Edwards_Elliptic_Curves_Group Efficient-Mergesort Efficient_Weighted_Path_Order Elimination_Of_Repeated_Factors Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Euler_Polyhedron_Formula Eudoxus_Reals Eval_FO Example-Submission Executable_Randomized_Algorithms Expander_Graphs 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 FO_Theory_Rewriting FSM_Tests 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 Finite_Fields Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Fishers_Inequality Fixed_Length_Vector Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier Free-Boolean-Algebra Free-Groups Frequency_Moments 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 Given_Clause_Loops Go GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Gray_Codes Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOL-CSPM HOL-CSP_OpSem HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Hales_Jewett Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms HoareForDivergence Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL HyperHoareLogic Hyperdual Hypergraph_Basics Hypergraph_Colourings IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IMP_Compiler_Reuse Interval_Analysis IO_Language_Conformance IP_Addresses Imperative_Insertion_Sort Implicational_Logic Impossible_Geometry IMP_Noninterference 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 Involutions2Squares Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq IsaNet Isabelle_C Isabelle_hoops Isabelle_Marries_Dirac Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD Karatsuba KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Khovanskii_Theorem Kleene_Algebra Kneser_Cauchy_Davenport Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt KnuthMorrisPratt Koenigsberg_Friendship Kruskal Kummer_Congruence Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LP_Duality 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_Series 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 Lovasz_Local Lowe_Ontological_Argument Lower_Semicontinuous Lp Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Martingales Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Maximum_Segment_Sum Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MHComputation MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines MLSS_Decision_Proc ML_Unification 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 Multirelations_Heterogeneous Multiset_Ordering_NPC Multitape_To_Singletape_TM Myhill-Nerode Name_Carrying_Type_Inference Nano_JSON Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers No_FTL_observers_Gen_Rel Nominal2 Nominal_Myhill_Nerode Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Number_Theoretic_Transform Octonions OmegaCatoidsQuantales 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 PAPP_Impossibility PCF PLM POPLmark-deBruijn PSemigroupsConvolution Package_logic Padic_Field Padic_Ints Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect_Fields Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Pluennecke_Ruzsa_Inequality Poincare_Bendixson Poincare_Disc Polygonal_Number_Theorem Polylog Polynomial_Crit_Geometry Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Prefix_Free_Code_Combinators 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 Probability_Inequality_Completeness Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Logic_Class Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic Q0_Metatheory Q0_Soundness QBF_Solver_Verification QHLProver QR_Decomposition Quantales Quantales_Converse Quantifier_Elimination_Hybrid Quasi_Borel_Spaces Quaternions Query_Optimization 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 Real_Time_Deque Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Region_Quadtrees Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Cardinality Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rensets Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewrite_Properties_Reduction Rewriting_Z Ribbon_Proofs Risk_Free_Lending Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SCC_Bloemen_Sequential SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 S_Finite_Measure_Monad Safe_Distance Safe_OCL Safe_Range_RC Saturation_Framework Saturation_Framework_Extensions Sauer_Shelah_Lemma Schutz_Spacetime Schwartz_Zippel Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL Separation_Logic_Unbounded SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Clause_Learning Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Solidity Sophomores_Dream Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Stalnaker_Logic Standard_Borel_Spaces 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 StrictOmegaCategories Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras Sumcheck_Protocol SumSquares Sunflowers SuperCalc Suppes_Theorem Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Synthetic_Completeness Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Three_Squares Timed_Automata Topological_Semantics Topology TortoiseHare TsirelsonBound Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Transport Treaps Tree-Automata Tree_Decomposition Tree_Enumeration Triangle Trie Turans_Graph_Theorem Twelvefold_Way Two_Generated_Word_Monoids_Intersection Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP +Uncertainty_Principle Undirected_Graph_Theory Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme VYDRA_MDL 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 WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Arithmetic_Geometric_Mean Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Wieferich_Kempner Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeckendorf Zeta_3_Irrational Zeta_Function pGCL Labeled_Transition_Systems Pushdown_Systems diff --git a/thys/Uncertainty_Principle/ROOT b/thys/Uncertainty_Principle/ROOT new file mode 100644 --- /dev/null +++ b/thys/Uncertainty_Principle/ROOT @@ -0,0 +1,12 @@ +chapter AFP + +session "Uncertainty_Principle" = QHLProver + + + options [timeout = 600] + + theories + Uncertainty_Principle + + document_files + "root.bib" + "root.tex" diff --git a/thys/Uncertainty_Principle/Uncertainty_Principle.thy b/thys/Uncertainty_Principle/Uncertainty_Principle.thy new file mode 100644 --- /dev/null +++ b/thys/Uncertainty_Principle/Uncertainty_Principle.thy @@ -0,0 +1,331 @@ +theory Uncertainty_Principle + imports "QHLProver.Complex_Matrix" +begin + +section\Setup\ + +abbreviation bra_ket ("\_|_\") + where "\u|v\ \ inner_prod u v" + +text\Fix an n-dimensional normalized quantum state $\psi$.\ +locale quantum_state = + fixes n:: nat + and \:: "complex Matrix.vec" + assumes dim[simp]: "\ \ carrier_vec n" + and normalized[simp]: "\\|\\ = 1" + +begin + +text\Observables on $\psi$ are hermitian matrices of appropriate dimensions.\ +abbreviation observable:: "complex Matrix.mat \ bool" where + "observable A \ A \ carrier_mat n n \ hermitian A" + +text\ + The mean value of an observable A is defined as $\langle \psi | A | \psi \rangle$. It is useful to + have a scalar matrix of appropriate dimension containing this value. On paper, this is usually implicit. +\ +abbreviation mean_mat :: "complex Matrix.mat \ complex Matrix.mat" ("\_\") + where "\A\ \ \\| A *\<^sub>v \\ \\<^sub>m 1\<^sub>m n" + +text\ + The standard deviation of an observable A = $\sqrt {\langle \psi | A^2 | \psi \rangle - \langle \psi | A | \psi \rangle^2}$. + Since the standard deviation is real (see lemma std-dev-real), we can define it as being of type real using norm. + This simultaneously restricts it to positive values. (powers of two are expanded for simplicity) +\ +abbreviation std_dev :: "complex Matrix.mat \ real" ("\") + where "\ A \ norm (csqrt (\\| (A * A *\<^sub>v \)\ - \\| A *\<^sub>v \\ * \\| A *\<^sub>v \\))" + +end + +abbreviation commutator :: "complex Matrix.mat \ complex Matrix.mat \ complex Matrix.mat" ("\_,_\") + where "commutator A B \ (A * B - B * A)" + +abbreviation anticommutator :: "complex Matrix.mat \ complex Matrix.mat \ complex Matrix.mat" ("\_,_\") + where "anticommutator A B \ (A * B + B * A)" + +section\Auxiliary Lemmas\ + +lemma inner_prod_distrib_add_mat: + fixes u v :: "complex vec" + assumes + "u \ carrier_vec n" + "v \ carrier_vec m" + "A \ carrier_mat n m" + "B \ carrier_mat n m" + shows "\u| (A + B) *\<^sub>v v\ = \u| A *\<^sub>v v\ + \u| B *\<^sub>v v\" + apply (subst add_mult_distrib_mat_vec) + using assms by (auto intro: inner_prod_distrib_right) + +lemma inner_prod_distrib_minus_mat: + fixes u v :: "complex vec" + assumes + "u \ carrier_vec n" + "v \ carrier_vec m" + "A \ carrier_mat n m" + "B \ carrier_mat n m" + shows "\u| (A - B) *\<^sub>v v\ = \u| A *\<^sub>v v\ - \u| B *\<^sub>v v\" + apply (subst minus_mult_distrib_mat_vec) + using assms by (auto intro: inner_prod_minus_distrib_right) + +text\Proving the usual Cauchy-Schwarz inequality using its formulation for complex vector spaces.\ +lemma Cauchy_Schwarz: + assumes "v \ carrier_vec n" "u \ carrier_vec n" + shows "norm (\u|v\)^2 \ Re (\u|u\ * \v|v\)" +proof- + have "norm (\u|v\)^2 \ (\u|u\ * \v|v\)" + using assms + by (metis Cauchy_Schwarz_complex_vec complex_norm_square conjugate_complex_def inner_prod_swap) + moreover have "(\u|u\ * \v|v\) \ \" + by (simp add: complex_is_Real_iff) + ultimately show ?thesis by (simp add: less_eq_complex_def) +qed + +context quantum_state +begin + +text\Show that the the standard deviation yields a real value. This justifies our definition in terms of the norm.\ +lemma std_dev_real: + assumes "observable A" + shows "csqrt (\\| (A * A *\<^sub>v \)\ - \\| A *\<^sub>v \\ * \\| A *\<^sub>v \\) \ \" +proof (subst csqrt_of_real_nonneg) + \\The term under the square root is real ...\ + have "(\\|A * A *\<^sub>v \\ - \\|A *\<^sub>v \\ * \\|A *\<^sub>v \\) \ \" + apply (intro Reals_diff Reals_mult hermitian_inner_prod_real) + using assms by (auto simp: hermitian_def adjoint_mult) + then show "Im (\\|A * A *\<^sub>v \\ - \\|A *\<^sub>v \\ * \\|A *\<^sub>v \\) = 0" + using complex_is_Real_iff by simp +next + have *:"adjoint A = A" using assms hermitian_def by blast + \\... and positive (Cauchy-Schwarz)\ + have "\\|A *\<^sub>v \\ * \\|A *\<^sub>v \\ \ \\|\\ * \\|A * A *\<^sub>v \\" + apply (subst assoc_mult_mat_vec) prefer 4 + apply (subst (2) adjoint_def_alter) prefer 4 + apply (subst (2) adjoint_def_alter) prefer 4 + apply (subst (1 2) *) + apply (rule Cauchy_Schwarz_complex_vec[OF dim]) + using assms by auto + then show "0 \ Re (\\|A * A *\<^sub>v \\ - \\|A *\<^sub>v \\ * \\|A *\<^sub>v \\)" + by (simp add: less_eq_complex_def) + \\Thus the result of the complex square root is real\ +qed simp + +text\This is an alternative way of formulating the standard deviation.\ +lemma std_dev_alt: + assumes "observable A" + shows "\ A = norm (csqrt (\\| (A - \A\) * (A - \A\) *\<^sub>v \\))" +proof- + \\Expand the matrix term\ + have "(A - \A\) * (A - \A\) = (A + - \A\) * (A + - \A\)" + using assms minus_add_uminus_mat by force + also have *: "... = A * A + A * - \A\ + - \A\ * A + - \A\ * - \A\" + apply (mat_assoc n) + using assms by auto + also have "... = A * A - \A\ * A - \A\ * A + \A\ * \A\" + using uminus_mult_right_mat assms by auto + also have "... = A * A - \\| A *\<^sub>v \\ \\<^sub>m A - \\| A *\<^sub>v \\ \\<^sub>m A + \A\ * \A\" + using assms by auto + finally have 1: + "\\| (A - \A\) * (A - \A\) *\<^sub>v \\ = + \\| (A * A - \\| A *\<^sub>v \\ \\<^sub>m A - \\| A *\<^sub>v \\ \\<^sub>m A + \A\ * \A\) *\<^sub>v \\" + by simp + + \\The mean is linear, so it distributes over the matrix term ...\ + have 2: + "\\| (A * A - \\| A *\<^sub>v \\ \\<^sub>m A - \\| A *\<^sub>v \\ \\<^sub>m A + \A\ * \A\) *\<^sub>v \\ = + \\|A * A *\<^sub>v \\ - \\|\\|A *\<^sub>v \\ \\<^sub>m A *\<^sub>v \\ - \\|\\|A *\<^sub>v \\ \\<^sub>m A *\<^sub>v \\ + \\|\A\ * \A\ *\<^sub>v \\" + apply (subst inner_prod_distrib_add_mat) prefer 5 + apply (subst inner_prod_distrib_minus_mat) prefer 5 + apply (subst inner_prod_distrib_minus_mat) + using assms by auto + + \\... and a scaling factor can be pulled outside\ + have 3: "\\|\\|A *\<^sub>v \\ \\<^sub>m A *\<^sub>v \\ = \\|A *\<^sub>v \\ * \\|A *\<^sub>v \\" + by (metis assms dim inner_prod_smult_left mult_mat_vec_carrier smult_mat_mult_mat_vec_assoc) + + \\This also means that this is just the mean squared\ + have "\\|\A\ * \A\ *\<^sub>v \\ = \\|A *\<^sub>v \\ * \\|\A\ *\<^sub>v \\" + apply (subst mult_smult_assoc_mat) prefer 3 + apply (subst smult_mat_mult_mat_vec_assoc) prefer 3 + apply (subst inner_prod_smult_left) + using assms by (auto intro!: mult_mat_vec_carrier) + also have "... = \\|A *\<^sub>v \\ * \\|A *\<^sub>v \\" + apply (subst smult_mat_mult_mat_vec_assoc) prefer 3 + apply (subst inner_prod_smult_left[where n = n]) + using assms by auto + finally have 4: "\\|\A\ * \A\ *\<^sub>v \\ = \\|A *\<^sub>v \\ * \\|A *\<^sub>v \\" by simp + + \\With these four equivalences we can rewrite the standard deviation as specified\ + show ?thesis + by (simp add: 1 2 3 4) +qed + +section\Main Proof\ + +text\Note that when swapping two observables inside an inner product, it is the same as conjugating the result.\ +lemma cnj_observables: + assumes "observable A" "observable B" + shows "cnj \\| (A * B) *\<^sub>v \\ = \\| (B * A) *\<^sub>v \\" +proof - + have "cnj (conjugate \A * B *\<^sub>v \|\\) = \adjoint (B * A) *\<^sub>v \|\\" + using assms by (metis (full_types) adjoint_mult complex_cnj_cnj conjugate_complex_def hermitian_def) + then show ?thesis + using assms by (metis adjoint_def_alter dim inner_prod_swap mult_carrier_mat mult_mat_vec_carrier) +qed + +text\ + With the above lemma we can make two observations about the behaviour of the commutator/ + anticommutator inside an inner product. +\ +lemma commutator_im: + assumes "observable A" "observable B" + shows "\\| \A, B\ *\<^sub>v \\ = 2 * \ * Im(\\| A * B *\<^sub>v \\)" +proof - + have "\\| \A, B\ *\<^sub>v \\ = \\| A * B *\<^sub>v \\ - \\| B * A *\<^sub>v \\" + using assms by (auto intro!: inner_prod_distrib_minus_mat) + also have "... = \\| A * B *\<^sub>v \\ - cnj \\| A * B *\<^sub>v \\" + by (subst cnj_observables[OF assms], simp) + finally show ?thesis + using complex_diff_cnj by simp +qed + +lemma anticommutator_re: + assumes "observable A" "observable B" + shows "\\| \A, B\ *\<^sub>v \\ = 2 * Re(\\| A * B *\<^sub>v \\)" +proof - + have "\\| \A, B\ *\<^sub>v \\ = \\| A * B *\<^sub>v \\ + \\| B * A *\<^sub>v \\" + using assms by (auto intro!: inner_prod_distrib_add_mat) + also have "... = \\| A * B *\<^sub>v \\ + cnj \\| A * B *\<^sub>v \\" + by (subst cnj_observables[OF assms], simp) + finally show ?thesis + using complex_add_cnj by simp +qed + +text\ + This intermediate step already looks similar to the uncertainty principle. The LHS will play the + role of the lower bound in the uncertainty principle. The RHS will turn into the standard + deviation of our observables under a certain substitution. +\ +lemma commutator_ineq: + assumes "observable A" "observable B" + shows "(norm \\| \A, B\ *\<^sub>v \\)^2 \ 4 * Re (\\| A * A *\<^sub>v \\ * \\| B * B *\<^sub>v \\)" +proof - + \\ + The inner product of our quantum state under A and B can be expressed in terms of its real and + imaginary part + \ + let ?x = "Re(\\| A * B *\<^sub>v \\)" + let ?y = "Im(\\| A * B *\<^sub>v \\)" + + \\These parts can be expressed using the commutator/anticommutator as shown above\ + have im: "(norm \\| \A, B\ *\<^sub>v \\)^2 = 4 * ?y^2" + apply (subst commutator_im[OF assms]) + using cmod_power2 by simp + + have re: "(norm \\| \A, B\ *\<^sub>v \\)^2 = 4 * ?x^2" + apply (subst anticommutator_re[OF assms]) + using cmod_power2 by simp + + \\Meaning, the sum of the commutator terms gives us $2 \langle \psi | A B | \psi \rangle$. Squared we get ...\ + from im re have "(norm \\| \A, B\ *\<^sub>v \\)^2 + (norm \\| \A, B\ *\<^sub>v \\)^2 = 4 * (?x^2 + ?y^2)" + by simp + also have "... = 4 * norm(\\| A * B *\<^sub>v \\)^2" + using cmod_power2 by simp + also have "... = 4 * norm(\A *\<^sub>v \| B *\<^sub>v \\)^2" + apply (subst assoc_mult_mat_vec) prefer 4 + apply (subst adjoint_def_alter) + using assms hermitian_def by (auto, force) + \\Now we use the Cauchy-Schwarz inequality\ + also have "... \ 4 * Re (\A *\<^sub>v \| A *\<^sub>v \\ * \B *\<^sub>v \| B *\<^sub>v \\)" + by (smt (verit) assms Cauchy_Schwarz dim mult_mat_vec_carrier) + \\Rewrite this term\ + also have "... = 4 * Re (\\| A * A *\<^sub>v \\ * \\| B * B *\<^sub>v \\)" + apply (subst (1 2) assoc_mult_mat_vec) prefer 7 + apply (subst (3 4) adjoint_def_alter) + using assms by (auto simp: hermitian_def) + \\Dropping a positive term on the LHS does not affect the inequality\ + finally show ?thesis + using norm_ge_zero by (smt (verit, ccfv_threshold) zero_le_power2) +qed + +text\ + This is part of the substitution we need in the final proof. This lemma + shows that the commutator simplifies nicely under that substitution. +\ +lemma commutator_sub_mean[simp]: + assumes "A \ carrier_mat n n" "B \ carrier_mat n n" + shows "\A - \A\, B - \B\\ = \A,B\" +proof - + \\ + Simply expand everything. + The unary minus signs are deliberate, because we want to have addition in the parentheses. + Otherwise mat-assoc cannot remove the parentheses. + \ + have "\A - \A\, B - \B\\ = A * B - \A\ * B - A * \B\ - \A\ * (- \B\) - (B * A + (- (\B\ * A)) + (- (B * \A\)) - \B\ * (- \A\))" + apply (mat_assoc n) + using assms by auto + \\Remove the last subtraction in the parentheses and unnecessary minus signs\ + also have "... = A * B - \A\ * B - A * \B\ - (- (\A\ * \B\)) - (B * A + (- (\B\ * A)) + (- (B * \A\)) - (- (\B\ * \A\)))" + using assms by auto + also have "... = A * B - \A\ * B - A * \B\ + - (- (\A\ * \B\)) - (B * A + (- (\B\ * A)) + (- (B * \A\)) + (- (- (\B\ * \A\))))" + apply (mat_assoc n) + using assms by auto + also have "... = A * B - \A\ * B - A * \B\ + \A\ * \B\ - (B * A + (- (\B\ * A)) + (- (B * \A\)) + \B\ * \A\)" + by simp + \\Remove parentheses\ + also have "... = A * B - \A\ * B - A * \B\ + \A\ * \B\ - B * A + (- (- (\B\ * A))) + (- (- (B * \A\))) - \B\ * \A\" + apply (mat_assoc n) + using assms by auto + also have "... =A * B - \A\ * B - A * \B\ + \A\ * \B\ - B * A + \B\ * A + B * \A\ - \B\ * \A\" + using uminus_uminus_mat by simp + \\Commutative mean\ + also have "...= A * B - \A\ * B - A * \B\ + \A\ * \B\ - B * A + A * \B\ + \A\ * B - \A\ * \B\" + using assms by auto + \\Reorder terms\ + also have "...= A * B - B * A + \A\ * B - \A\ * B + A * \B\ - A * \B\ + \A\ * \B\ - \A\ * \B\" + apply (mat_assoc n) + using assms by auto + \\Everything but the first two terms are eliminated, resulting in the commutator\ + finally show ?thesis using assms minus_r_inv_mat by auto +qed + + +theorem uncertainty_principle: + assumes "observable C" "observable D" + shows "\ C * \ D \ norm \\|\C,D\ *\<^sub>v \\ / 2" +proof - + \\Perform the substitution\ + let ?A = "C - \C\" + let ?B = "D - \D\" + + \\These matrices are valid observables\ + from assms have observables_A_B: "observable ?A" "observable ?B" + using hermitian_inner_prod_real assms Reals_cnj_iff + by (auto simp: hermitian_def adjoint_minus adjoint_one adjoint_scale) + + \\Start with commutator-ineq\ + have "(norm \\| \?A, ?B\ *\<^sub>v \\)^2 \ 4 * Re ((\\| ?A * ?A *\<^sub>v \\) * (\\| ?B * ?B *\<^sub>v \\))" + using commutator_ineq[OF observables_A_B] by auto + \\Simplify the commutator\ + then have "(norm \\| \C, D\ *\<^sub>v \\)^2 \ 4 * Re ((\\| ?A * ?A *\<^sub>v \\) * (\\| ?B * ?B *\<^sub>v \\))" + using assms by simp + \\Apply sqrt to both sides\ + then have "sqrt ((norm (\\| \C, D\ *\<^sub>v \\))^2) \ sqrt (4 * Re ((\\| ?A * ?A *\<^sub>v \\) * (\\| ?B * ?B *\<^sub>v \\)))" + using real_sqrt_le_mono by blast + \\Simplify\ + then have "norm (\\| \C, D\ *\<^sub>v \\) \ 2 * sqrt (Re ((\\| ?A * ?A *\<^sub>v \\) * (\\| ?B * ?B *\<^sub>v \\)))" + by (auto cong: real_sqrt_mult) + \\Because these inner products are positive and real, norm = Re\ + then have "norm (\\| \C, D\ *\<^sub>v \\) \ 2 * sqrt ( \Re ((\\| ?A * ?A *\<^sub>v \\) * (\\| ?B * ?B *\<^sub>v \\))\)" + by (smt (verit, ccfv_SIG) real_sqrt_le_iff) + then have "norm (\\| \C, D\ *\<^sub>v \\) \ 2 * sqrt (norm ((\\| ?A * ?A *\<^sub>v \\) * (\\| ?B * ?B *\<^sub>v \\)))" + by (auto simp: in_Reals_norm Reals_cnj_iff cnj_observables observables_A_B) + \\Rewrite term to recover the standard deviation (As formulated in std-dev-alt)\ + then have "norm (\\| \C, D\ *\<^sub>v \\) \ 2 * norm (csqrt (\\| ?A * ?A *\<^sub>v \\)) * norm (csqrt (\\| ?B * ?B *\<^sub>v \\))" + by (simp add: norm_mult real_sqrt_mult) + then show "\ C * \ D \ norm \\|\C, D\ *\<^sub>v \\ / 2" + using assms by (auto cong: std_dev_alt) +qed + +end + +end \ No newline at end of file diff --git a/thys/Uncertainty_Principle/document/root.bib b/thys/Uncertainty_Principle/document/root.bib new file mode 100644 --- /dev/null +++ b/thys/Uncertainty_Principle/document/root.bib @@ -0,0 +1,18 @@ +@book{nielsen2010quantum, + title={Quantum Computation and Quantum Information}, + author={Nielsen, Michael A and Chuang, Isaac L}, + year={2010}, + publisher={Cambridge University Press}, + page={89} +} + +@article{QHLProver-AFP, + author = {Junyi Liu and Bohua Zhan and Shuling Wang and Shenggang Ying and Tao Liu and Yangjia Li and Mingsheng Ying and Naijun Zhan}, + title = {Quantum Hoare Logic}, + journal = {Archive of Formal Proofs}, + month = {March}, + year = {2019}, + note = {\url{https://isa-afp.org/entries/QHLProver.html}, + Formal proof development}, + ISSN = {2150-914x}, +} \ No newline at end of file diff --git a/thys/Uncertainty_Principle/document/root.tex b/thys/Uncertainty_Principle/document/root.tex new file mode 100644 --- /dev/null +++ b/thys/Uncertainty_Principle/document/root.tex @@ -0,0 +1,35 @@ +\documentclass[11pt,a4paper]{article} +\usepackage[T1]{fontenc} +\usepackage{isabelle,isabellesym} + +% 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{Uncertainty Principle} +\author{Alexander Treml} +\maketitle + +\begin{abstract} + This is a formal proof of the uncertainty principle known from quantum mechanics. + It is based upon work on complex vector spaces contained in the QHLProver session\cite{QHLProver-AFP}. + The formalization follows the proof outlined in the book "Quantum computation and quantum information" by Nielsen and Chuang\cite{nielsen2010quantum}. +\end{abstract} + +\tableofcontents + +\pagebreak + +% include generated text of all theories +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document}