Session Frequency_Moments

Theories

• HOL-Library.Log_Nat
• HOL-Library.Lattice_Algebras
• HOL-Library.Float
• HOL-Library.List_Lexorder
• Prefix_Free_Code_Combinators.Prefix_Free_Code_Combinators
• HOL-Number_Theory.Fib
• HOL-Number_Theory.Cong
• HOL-Algebra.Congruence
• HOL-Algebra.Order
• HOL-Algebra.Lattice
• HOL-Algebra.Complete_Lattice
• HOL-Algebra.Group
• HOL-Algebra.Coset
• HOL-Algebra.FiniteProduct
• HOL-Algebra.Ring
  • File ‹ringsimp.ML›
• HOL-Algebra.Module
• HOL-Algebra.AbelCoset
• HOL-Algebra.Ideal
• HOL-Algebra.RingHom
• HOL-Algebra.UnivPoly
• HOL-Algebra.Generated_Groups
• HOL-Algebra.Elementary_Groups
• HOL-Algebra.Multiplicative_Group
• HOL-Number_Theory.Totient
• HOL-Number_Theory.Residues
• HOL-Number_Theory.Eratosthenes
• HOL-Library.Power_By_Squaring
• HOL-Number_Theory.Mod_Exp
• HOL-Number_Theory.Euler_Criterion
• HOL-Number_Theory.Gauss
• HOL-Number_Theory.Quadratic_Reciprocity
• HOL-Number_Theory.Pocklington
• HOL-Number_Theory.Prime_Powers
• HOL-Number_Theory.Residue_Primitive_Roots
• HOL-Number_Theory.Number_Theory
• HOL-Library.Interval
• HOL-Library.Interval_Float
• HOL-Decision_Procs.Dense_Linear_Order
  • File ‹langford_data.ML›
  • File ‹ferrante_rackoff_data.ML›
  • File ‹langford.ML›
  • File ‹ferrante_rackoff.ML›
• HOL-Decision_Procs.Approximation_Bounds
• HOL-Library.Code_Target_Int
• HOL-Library.Code_Abstract_Nat
• HOL-Library.Code_Target_Nat
• HOL-Library.Code_Target_Numeral
• Lehmer.Lehmer
• Pratt_Certificate.Pratt_Certificate
  • File ‹pratt.ML›
• Bertrands_Postulate.Bertrand
  • File ‹bertrand.ML›
• Frequency_Moments_Preliminary_Results
• HOL-Combinatorics.List_Permutation
• HOL-Algebra.Divisibility
• HOL-Algebra.QuotRing
• HOL-Algebra.Ring_Divisibility
• HOL-Algebra.Subrings
• HOL-Algebra.Polynomials
• HOL-Algebra.Embedded_Algebras
• HOL-Algebra.Polynomial_Divisibility
• Finite_Fields.Finite_Fields_Preliminary_Results
• Finite_Fields.Finite_Fields_Factorization_Ext
• HOL-Algebra.IntRing
• Finite_Fields.Ring_Characteristic
• Universal_Hash_Families.Universal_Hash_Families_More_Finite_Fields
• Interpolation_Polynomials_HOL_Algebra.Bounded_Degree_Polynomials
• Interpolation_Polynomials_HOL_Algebra.Lagrange_Interpolation
• Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
• Frequency_Moments
• Universal_Hash_Families.Universal_Hash_Families
• Universal_Hash_Families.Universal_Hash_Families_More_Independent_Families
• Median_Method.Median
• K_Smallest
• Universal_Hash_Families.Carter_Wegman_Hash_Family
• HOL-Library.Landau_Symbols
• Landau_Ext
• Probability_Ext
• Product_PMF_Ext
• Frequency_Moment_0
• HOL-Combinatorics.Stirling
• Card_Partitions.Set_Partition
• HOL-Eisbach.Eisbach
  • File ‹parse_tools.ML›
  • File ‹method_closure.ML›
  • File ‹eisbach_rule_insts.ML›
  • File ‹match_method.ML›
• Card_Partitions.Injectivity_Solver
• Card_Partitions.Card_Partitions
• Bell_Numbers_Spivey.Bell_Numbers
• Card_Equiv_Relations.Card_Equiv_Relations
• Equivalence_Relation_Enumeration.Equivalence_Relation_Enumeration
• Frequency_Moment_2
• HOL-Library.Function_Algebras
• Ergodic_Theory.SG_Library_Complement
• Lp.Functional_Spaces
• Lp.Lp
• Frequency_Moment_k