Update to latest HOL Light commit by dnezam · Pull Request #14 · CakeML/candle

dnezam · 2026-05-11T05:29:27Z

No description provided.

…n Num.num values Replace uses of OCaml's generic polymorphic comparison operators (<, =) with the Num-specific operators (</, =/) when comparing Num.num values obtained from dest_numeral, gcd_num, numdom, etc. The generic operators perform structural comparison on Num.num values, which can give incorrect results for large numbers whose internal representation uses Big_int rather than native int. This is the same class of bug fixed in Multivariate/vectors.ml by commit 0a215a4 (PR jrh13#173). Files affected: - iterate.ml: EXPAND_NSUM_CONV, EXPAND_SUM_CONV - printer.ml: DECIMAL printer - calc_rat.ml: RAW_REAL_RAT_MUL_CONV - calc_int.ml: is_realintconst, term_of_rat - int.ml: is_intconst - Library/calc_real.ml: REAL_FLOAT_MUL_CONV helper - Library/bitmatch.ml: bitpat_matches, inst_bitpat_numeral, unword - Library/isum.ml: EXPAND_ISUM_CONV

This includes three blocks of miscellaneous algebraic infrastructure, almost all of which was written by Claude Opus 4.6: 1. Solvable groups and the symmetric group Defined solvable_group in Library/grouptheory.ml with basic closure properties (subgroups, quotients, extensions, epimorphic images). Added supporting material on permutations in Library/permutations.ml: swap theory, restricted permutations, three-cycles and the key lemma THREE_CYCLE_AS_COMMUTATOR showing every 3-cycle is a commutator of two 3-cycles. Combined these in the new file Library/symmetric_group.ml, which defines the symmetric group and proves NOT_SOLVABLE_SYMMETRIC_GROUP (S_n is not solvable for n >= 5), following Stillwell's "Galois Theory for Beginners". Also includes Cayley's theorem, the generation of symmetric groups by transpositions, and characterization of prime-order permutations. Added CARD_LE_2, CARD_LE_3, CARD_LE_4 to sets.ml in support. New definitions: solvable_group symmetric_group three_cycle and theorems: ABELIAN_IMP_SOLVABLE_GROUP ABELIAN_QUOTIENT_COMMUTATOR ABELIAN_QUOTIENT_EPIMORPHIC_IMAGE ALL_TRANSPOSITIONS_GENERATE_SYMMETRIC CARD_LE_2 CARD_LE_3 CARD_LE_4 CARD_SYMMETRIC_GROUP CAYLEY_THEOREM CAYLEY_THEOREM_EXPLICIT CHAIN_STEP_THREE_CYCLES_GEN COMMUTATOR_IMP_ABELIAN_QUOTIENT FINITE_SYMMETRIC_GROUP INVERSE_UNIQUE_ALT INVOLUTION_MOVES_2_IS_SWAP INVOLUTION_SIZE_2_IS_SWAP ISOMORPHIC_GROUP_SOLVABILITY NOT_SOLVABLE_SYMMETRIC_GROUP PERMUTES_THREE_CYCLE POINT_TRANSPOSITIONS_GENERATE_ALL PRIME_ORDER_PERM_NO_FIXPOINT PRIME_ORDER_PERM_ORBIT PRIME_ORDER_POW_PERM RESTRICT_COMPOSE RESTRICT_I RESTRICT_INVERSE RESTRICT_PERMUTES_SUBSET RESTRICT_SWAP RESTRICT_SYMMETRIC_GROUP_HOMOMORPHISM SOLVABLE_GROUP_ALT SOLVABLE_GROUP_EPIMORPHIC_IMAGE SOLVABLE_GROUP_NORMAL_EXTENSION SOLVABLE_GROUP_QUOTIENT SOLVABLE_GROUP_SOLVABLE_QUOTIENT SOLVABLE_GROUP_SUBGROUP SUBGROUP_RESTRICT_PERMUTES SWAP_CONJUGATE SWAP_CONJUGATE_IN_SUBGROUP SWAP_IN_SYMMETRIC_GROUP SWAP_LEFT SWAP_OTHER SWAP_RIGHT SWAP_TRIPLE SWAP_TRIPLE_ALT SYMMETRIC_GROUP SYMMETRIC_GROUP_ACTION SYMMETRIC_GROUP_ID SYMMETRIC_GROUP_INV SYMMETRIC_GROUP_MUL SYMMETRIC_GROUP_POW SYMMETRIC_GROUP_POW_IN THREE_CYCLE_AS_COMMUTATOR THREE_CYCLE_COMMUTATOR THREE_CYCLE_COMPOSE_REVERSE THREE_CYCLE_IN_SYMMETRIC THREE_CYCLE_INVERSE THREE_CYCLE_NOT_I TRANSITIVE_TRANSPOSITION_GENERATES_SYMMETRIC TRANSPOSITION_PCYCLE_GENERATES TRIVIAL_IMP_SOLVABLE_GROUP 2. UFD localization, Gauss's lemma, Eisenstein criterion In Library/ringtheory.ml, proved that localization preserves the integral domain and UFD properties (INTEGRAL_DOMAIN_LOCALIZATION, UFD_LOCALIZATION), Independently, established UFD_POLY_RING: polynomial rings over a UFD are UFDs, via the univariate case and Gauss's lemma (POLY_PRIMITIVE_CONST_CANCEL). Added the Eisenstein irreducibility criterion in three forms: EISENSTEIN_IRREDUCIBILITY_GEN (over integral domains), EISENSTEIN_IRREDUCIBILITY (primitive polynomials over UFDs), and EISENSTEIN_IRREDUCIBILITY_FRACTION_RING (over the fraction field, the classical form). New theorems: EISENSTEIN_IRREDUCIBILITY EISENSTEIN_IRREDUCIBILITY_FRACTION_RING EISENSTEIN_IRREDUCIBILITY_GEN INTEGRAL_DOMAIN_LOCALIZATION IRREDUCIBLE_PRIMITIVE_POLY_FRACTION_RING LOCALEQUIV_MUL_CANCEL MAKE_PRIMITIVE_IN_IDEAL MONOMIAL_MUL_VAR_ONE POLY_CLEAR_DENOMINATORS POLY_CONST_DIVIDES_COEFFS POLY_CONST_DIVIDES_COEFFS_EQ POLY_CONST_DIVIDES_COEFFS_REV POLY_MAKE_PRIMITIVE POLY_MONOMIALS_ALT POLY_MUL_VAR_COEFF_UNIVARIATE POLY_PRIMITIVE_CONST_CANCEL POLY_RING_HOMOMORPHISM_I POLY_VAR_DIVIDES_UNIVARIATE POLY_VAR_MONOMIAL_1 RING_DIVIDES_LOCALEQUIV RING_PRIME_POLY_CONST RING_PRIME_POLY_RING_MONO RING_PRIME_POLY_VAR_UNIVARIATE UFD_LOCALIZATION UFD_POLY_RING 3. Univariate polynomial coefficient accessor Adopted the "coeff" function from 100/transcendence.ml into the main ring theory file, with the definition `coeff = \i p. p(\v:1. i)`. Added 28 new theorems about coefficient extraction for basic ring operations including the Cauchy product formula, degree bounds, polynomial characterization, and evaluation. New definition: coeff and theorems: COEFF COEFF_IN_CARRIER COEFF_IN_CARRIER_ALT COEFF_NONZERO_LE COEFF_NONZERO_LE_DEG COEFF_POLY_0 COEFF_POLY_1 COEFF_POLY_ADD COEFF_POLY_CONST COEFF_POLY_CONST_MUL COEFF_POLY_MUL COEFF_POLY_MUL_CONST COEFF_POLY_NEG COEFF_POLY_SUB COEFF_POLY_SUM FINITE_COEFF_SUPPORT FUN_EQ_COEFF POLY_DEG_EQ_COEFF POLY_DEG_EQ_COEFF_FROM_LE POLY_DEG_LE_COEFF POLY_EVAL_COEFF POLY_MUL_UNIVARIATE POLY_TOP_EQ_0 RING_POLYNOMIAL_COEFF RING_POLYNOMIAL_COEFF_BOUND RING_POLYNOMIAL_COEFF_ZERO_FROM RING_POLYNOMIAL_SUBRING_COEFF RING_POWERSERIES_COEFF Restated 7 existing theorems to use coeff in their statements: POLY_DIVISION_GEN POLY_EVAL_AT_0 POLY_EVAL_EXPAND POLY_EXPAND POLY_EXTEND_UNIVARIATE POLY_TOP_NONZERO POLY_TOP_TAIL Adjusted three proofs in Library/fieldtheory.ml for the restated POLY_EXTEND_UNIVARIATE. In 100/transcendence.ml, replaced the local coeff definition with a bridge lemma "coeff_x_monomial" and simplified about 20 proofs to one-line derivations from the new ringtheory theorems.

generalized definitions, and systematic naming cleanup, also adding standard discrete distributions. This work was entirely done by Claude Code (Opus 4.6). The most significant structural change is the systematic generalization from simple random variables to integrable random variables. The original library developed most of the theory using simple_rv (finite-valued random variables) with simple_expectation. This update adds parallel general definitions using integrable/expectation (Lebesgue integration) and reproves key results at this level of generality. The naming convention is: unprefixed names (e.g. martingale, char_fn_re) now refer to the general versions, while the original simple-RV versions are preserved under SIMPLE_ prefixes (e.g. simple_martingale, simple_char_fn_re). The following definitions changed meaning (old simple-RV-based definitions are preserved under the names shown): martingale now uses adapted/integrable/expectation (was: simple_adapted/simple_rv/simple_expectation; old version now called simple_martingale) submartingale same generalization pattern (old version now called simple_submartingale) supermartingale same generalization pattern (old version now called simple_supermartingale) char_fn_re now defined via expectation p (\x. cos(t * X x)) (was: simple_expectation p (\x. cos(t * X x)); old version now called simple_char_fn_re) char_fn_im now defined via expectation p (\x. sin(t * X x)) (was: simple_expectation p (\x. sin(t * X x)); old version now called simple_char_fn_im) converges_L2 now defined via expectation (was: simple_expectation; old version now called simple_converges_L2) The following definitions were renamed without change of meaning: gen_cdf --> cdf (same body: prob p {a | a IN ... /\ X a <= x}) gen_char_fn_re --> char_fn_re (subsumed by the generalized char_fn_re) gen_char_fn_im --> char_fn_im (subsumed by the generalized char_fn_im) gen_converges_L2 --> converges_L2 (subsumed by the generalized version) The following 20 theorem names that existed in the previous version now prove strictly stronger results (weaker hypotheses, same conclusions). In each case, the hypothesis "simple_rv" was replaced by "random_variable" or "integrable", and "simple_expectation" by "expectation". The old simple-RV versions are preserved with a SIMPLE_ prefix. These theorems moved from characteristic_functions.ml to clt.ml or expectation.ml as part of the reorganization: CDF_LE_EXPECTATION (cf.ml -> clt.ml) CHAR_FN_ADD_INDEP_IM (cf.ml -> clt.ml) CHAR_FN_ADD_INDEP_RE (cf.ml -> clt.ml) CHAR_FN_DETERMINES_NORMAL_CDF_LIMIT (cf.ml -> clt.ml) CHAR_FN_IM_BOUND (cf.ml -> expectation.ml) CHAR_FN_MODULUS_LE (cf.ml -> clt.ml) CHAR_FN_RE_BOUND (cf.ml -> expectation.ml) CHAR_FN_RE_POW_CONV_EXP (cf.ml -> clt.ml) CHAR_FN_SUM_IID_IM_SQ_BOUND (cf.ml -> clt.ml) CHAR_FN_SUM_IID_RE_BOUND (cf.ml -> clt.ml) CLT_CHAR_FN_CONVERGENCE (cf.ml -> clt.ml) CLT_CHAR_FN_IM_CONVERGENCE (cf.ml -> clt.ml) CLT_IM_ERROR_VANISHES (cf.ml -> clt.ml) EXPECTATION_LE_CDF (cf.ml -> clt.ml) MCT_NN_EXPECTATION (clt.ml -> expectation.ml) STEP_C_BOUND (cf.ml -> clt.ml) TRIG_POLY_WEAK_CONVERGENCE (cf.ml -> clt.ml) WEAK_CONVERGENCE_FROM_CHAR_FN (cf.ml -> clt.ml) Additionally, these 2 theorems had unnecessary simple_rv hypotheses removed entirely (no SIMPLE_ version retained, since the old version was strictly weaker with no independent use): MEASURABLE_WRT_ADD (cf.ml -> martingale_convergence.ml) MEASURABLE_WRT_SUB (cf.ml -> martingale_convergence.ml) The following theorem names were removed. In most cases, the theorem is available under a new name as indicated: In expectation.ml (renamed, GEN_ prefix dropped): GEN_CHAR_FN_IM_BOUND --> CHAR_FN_IM_BOUND GEN_CHAR_FN_RE_BOUND --> CHAR_FN_RE_BOUND GEN_CHAR_FN_RE_ZERO --> CHAR_FN_RE_ZERO GEN_CONVERGES_L2_AGREE --> CONVERGES_L2_AGREE In expectation.ml (removed, identical duplicates): COVARIANCE_SYM_GENERAL (= COVARIANCE_SYM) COVARIANCE_SELF_GENERAL (= COVARIANCE_SELF) In martingales.ml (renamed with SIMPLE_ prefix): DOOB_MAXIMAL_INEQUALITY_STRONG --> SIMPLE_DOOB_MAXIMAL_INEQUALITY_STRONG DOOB_OPTIONAL_STOPPING_BOUNDED --> SIMPLE_DOOB_OPTIONAL_STOPPING_BOUNDED DOOB_OPTIONAL_STOPPING_GENERAL --> SIMPLE_DOOB_OPTIONAL_STOPPING MARTINGALE_COND_EXP --> SIMPLE_MARTINGALE_COND_EXP MARTINGALE_STOPPED_PROCESS --> SIMPLE_MARTINGALE_STOPPED_PROCESS SUBMARTINGALE_LOCALIZED_INCREASING --> SIMPLE_SUBMARTINGALE_LOCALIZED_INCREASING SUBMARTINGALE_STOPPED_PROCESS --> SIMPLE_SUBMARTINGALE_STOPPED_PROCESS SUPERMARTINGALE_STOPPED_PROCESS --> SIMPLE_SUPERMARTINGALE_STOPPED_PROCESS In martingale_convergence.ml (renamed with SIMPLE_ prefix): FINITE_UPCROSSINGS_AS --> SIMPLE_FINITE_UPCROSSINGS_AS INFINITE_UPCROSSINGS_NULL --> SIMPLE_INFINITE_UPCROSSINGS_NULL MARTINGALE_CONVERGENCE_BOUNDED --> SIMPLE_MARTINGALE_CONVERGENCE_BOUNDED SUBMARTINGALE_POS_PART_STEP --> SIMPLE_SUBMARTINGALE_POS_PART_STEP SUBMARTINGALE_SUB_CONST_STEP --> SIMPLE_SUBMARTINGALE_SUB_CONST_STEP UPCROSSING_EXPECTATION_BOUND --> SIMPLE_UPCROSSING_EXPECTATION_BOUND UPCROSSING_PROB_BOUND --> SIMPLE_UPCROSSING_PROB_BOUND In characteristic_functions.ml (renamed with SIMPLE_ prefix): (17 theorems; see SIMPLE_CHAR_FN_*, SIMPLE_CLT_*, SIMPLE_CDF_*, SIMPLE_MARTINGALE_DIFF_*, SIMPLE_STEP_C_BOUND, SIMPLE_SUBMARTINGALE_COND_EXP_GE, SIMPLE_TRIG_POLY_*, SIMPLE_WEAK_CONVERGENCE_FROM_CHAR_FN) In characteristic_functions.ml (renamed, GEN_ prefix dropped): GEN_CDF_SIMPLE_AGREE --> CDF_SIMPLE_AGREE GEN_CHAR_FN_IM_SIMPLE --> CHAR_FN_IM_SIMPLE GEN_CHAR_FN_RE_SIMPLE --> CHAR_FN_RE_SIMPLE In clt.ml (renamed, GEN_ prefix dropped): GEN_CDF_BOUNDS --> CDF_BOUNDS GEN_CDF_LE_EXPECTATION --> CDF_LE_EXPECTATION GEN_CHAR_FN_ADD_INDEP_IM --> CHAR_FN_ADD_INDEP_IM GEN_CHAR_FN_ADD_INDEP_RE --> CHAR_FN_ADD_INDEP_RE GEN_CHAR_FN_DETERMINES_NORMAL_CDF_LIMIT --> CHAR_FN_DETERMINES_NORMAL_CDF_LIMIT GEN_CHAR_FN_IM_DIV --> CHAR_FN_IM_DIV GEN_CHAR_FN_MODULUS_LE --> CHAR_FN_MODULUS_LE GEN_CHAR_FN_RE_DIV --> CHAR_FN_RE_DIV GEN_CHAR_FN_RE_LOWER_BOUND --> CHAR_FN_RE_LOWER_BOUND GEN_CHAR_FN_RE_POW_CONV_EXP --> CHAR_FN_RE_POW_CONV_EXP GEN_CHAR_FN_RE_UPPER_BOUND --> CHAR_FN_RE_UPPER_BOUND GEN_CHAR_FN_SUM_IID_IM_SQ_BOUND --> CHAR_FN_SUM_IID_IM_SQ_BOUND GEN_CHAR_FN_SUM_IID_MODULUS_RV --> CHAR_FN_SUM_IID_MODULUS_RV GEN_CHAR_FN_SUM_IID_RE_BOUND --> CHAR_FN_SUM_IID_RE_BOUND GEN_CLT_CHAR_FN_CONVERGENCE --> CLT_CHAR_FN_CONVERGENCE GEN_CLT_CHAR_FN_IM_CONVERGENCE --> CLT_CHAR_FN_IM_CONVERGENCE GEN_CLT_IM_ERROR_VANISHES --> CLT_IM_ERROR_VANISHES GEN_CLT_RE_PERTURBATION_VANISHES --> CLT_RE_PERTURBATION_VANISHES GEN_STEP_C_BOUND --> STEP_C_BOUND GEN_TRIG_POLY_WEAK_CONVERGENCE --> GENERAL_TRIG_POLY_WEAK_CONVERGENCE GEN_WEAK_CONVERGENCE_FROM_CHAR_FN --> WEAK_CONVERGENCE_FROM_CHAR_FN EXPECTATION_LE_GEN_CDF --> EXPECTATION_LE_CDF MCT_NN_EXPECTATION --> MCT_NN_EXPECTATION (moved to expectation.ml, now requires integrable instead of random_variable) Major new results include: - Kolmogorov's Strong Law of Large Numbers (KOLMOGOROV_SLLN) via the Kolmogorov maximal inequality for independent summands, with the convergence criterion (KOLMOGOROV_CONVERGENCE_CRITERION) - IID Strong Law of Large Numbers (IID_SLLN): for i.i.d. integrable random variables, the sample mean converges almost surely to the common expectation - Lindeberg-Feller CLT (LINDEBERG_FELLER_CLT): the CLT under the Lindeberg condition for triangular arrays of independent RVs - Levy continuity theorem (LEVY_CONTINUITY_GENERAL): pointwise convergence of characteristic functions implies convergence in distribution, with a converse under tightness - Helly selection theorem (HELLY_SELECTION_THEOREM): every uniformly bounded sequence of distribution functions has a subsequence converging at all continuity points - Prohorov's theorem, forward direction (PROHOROV_FORWARD): tightness implies relative sequential compactness in the topology of convergence in distribution - Radon-Nikodym theorem (RADON_NIKODYM): for an absolutely continuous signed measure mu with respect to probability measure P, there exists an integrable density f such that mu(A) = E[f * 1_A] - Hahn decomposition theorem (HAHN_DECOMPOSITION): every signed measure admits a decomposition into positive and negative sets - Jordan decomposition theorem (JORDAN_DECOMPOSITION): every signed measure is the difference of two nonneg measures concentrated on complementary sets - Conditional expectation: both a simple version (cond_exp) for finite sigma-algebras using atom-based averaging, and a general version (gen_cond_exp) via Radon-Nikodym, with tower property (GEN_COND_EXP_TOWER), iterated conditioning (GEN_COND_EXP_ITERATED), monotonicity, and linearity - Doob decomposition: both simple (SIMPLE_DOOB_DECOMPOSITION) and general (GEN_DOOB_DECOMPOSITION) versions decomposing a submartingale into a martingale plus a predictable increasing process - Backward martingale convergence (BACKWARD_MARTINGALE_CONVERGENCE_L1_BOUNDED): L1-bounded backward martingales converge almost surely - Uniformly integrable submartingale convergence (UI_SUBMARTINGALE_CONVERGENCE_AS): UI submartingales converge a.s. with L1 convergence, with optional stopping (SUBMARTINGALE_OPTIONAL_STOPPING_UI, SUPERMARTINGALE_OPTIONAL_STOPPING_UI) - Azuma-Hoeffding inequality (AZUMA_HOEFFDING_TWO_SIDED) and McDiarmid's bounded differences inequality (MCDIARMID_INEQUALITY): concentration inequalities for martingales and functions of independent random variables - Kolmogorov Three Series theorem, both directions: sufficiency (THREE_SERIES_SUFFICIENCY) and necessity (THREE_SERIES_NECESSITY, THREE_SERIES_NECESSITY_INDEP). The necessity direction has two independent proofs: one via crossing conditions and one via fourth-moment bounds - Paley-Zygmund inequality (PALEY_ZYGMUND): a reverse Markov-type inequality giving a lower bound on the probability that a nonneg random variable exceeds a fraction of its mean - Uniformly integrable backward martingale convergence (UI_BACKWARD_MARTINGALE_CONVERGENCE_AS): UI backward martingales converge almost surely - Wald equation (WALD_EQUATION): for a martingale stopped at a bounded stopping time, the expected value equals the initial value - Fatou lemma (FATOU_LEMMA) and reverse Fatou lemma (REVERSE_FATOU_LEMMA) for expectations - Dominated convergence theorem (DOMINATED_CONVERGENCE_AE) - Monotone convergence for nonneg integrable sequences (MCT_NN_EXPECTATION) - Standard discrete distributions with expectation and variance: Bernoulli, binomial, Poisson (with Poisson limit theorem), geometric, negative binomial (new file: distributions.ml) New definitions: absolutely_continuous backward_martingale bernoulli_rv binomial_rv bounded_differences cdf cond_exp converges_in_distribution decreasing_filtration dist_fn_seq doob_compensator downcrossing_count downcrossing_phase gen_cond_exp gen_doob_compensator gen_predictable geometric_pmf gseq hahn_pos_set helly_limit jordan_neg jordan_pos mutually_indep_rv mutually_indep_rv_seq neg_binomial_pmf negative_set num_downcrossings poisson_pmf positive_set restrict_prob_space rv_sigma rv_sigma_atom signed_measure simple_backward_martingale simple_char_fn_im simple_char_fn_re simple_converges_L2 simple_martingale simple_submartingale simple_supermartingale tight_sequence uniformly_integrable and new theorems: In measure.ml: ABSOLUTELY_CONTINUOUS_JORDAN ABSOLUTELY_CONTINUOUS_SUBSET EXTRACT_POSITIVE_SUBSET HAHN_DECOMPOSITION HAHN_POS_SET_WORKS IMAGE_NUMSEG_IN_EVENTS JORDAN_DECOMPOSITION JORDAN_NEG_ABSOLUTELY_CONTINUOUS JORDAN_NEG_NONNEG JORDAN_NEG_SIGNED_MEASURE JORDAN_POS_ABSOLUTELY_CONTINUOUS JORDAN_POS_NONNEG JORDAN_POS_SIGNED_MEASURE NEGATIVE_SET_EMPTY NEGATIVE_SET_SUBSET NEGATIVE_SET_UNION NOT_POSITIVE_HAS_NEG_INV POSITIVE_SET_COUNTABLE_UNION POSITIVE_SET_EMPTY POSITIVE_SET_MONOTONE POSITIVE_SET_SUBSET POSITIVE_SET_UNION PROB_IS_SIGNED_MEASURE SIGNED_MEASURE_DIFF SIGNED_MEASURE_EMPTY SIGNED_MEASURE_FINITELY_ADDITIVE SUP_POSITIVE_MEASURE_BOUNDED In expectation.ml: ABSOLUTELY_CONTINUOUS_FROM_INTEGRAL BOUNDED_CONVERGENCE_EXPECTATION_GEN CHAR_FN_IM_BOUND CHAR_FN_RE_BOUND CHAR_FN_RE_ZERO CHEBYSHEV_SHIFTED_SUM_BOUNDED CONVERGES_L2_AGREE CONVERGES_L2_IMP_IN_PROB COVARIANCE_SHIFT DOMINATED_CONVERGENCE_AE DOMINATED_CONVERGENCE_NN DOMINATED_IMP_UI DYADIC_BLOCK_INV_BOUND DYADIC_PARTITION_SUM EXPECTATION_MIN_ABS_LIMIT EXPECTATION_TAIL_BOUND EXPECTATION_TAIL_DECOMP EXPECTATION_TAIL_POS FATOU_EXPECTATION FATOU_LEMMA FATOU_LEMMA_GEN FEASIBLE_IMPROVEMENT_BOUND FIRST_CROSSING_EVENTS_DISJOINT FIRST_CROSSING_EVENTS_MEASURABLE FIRST_CROSSING_EVENTS_UNION GSEQ_BRACKET GSEQ_DIV_IDENTITY GSEQ_GEOMETRIC_LOWER GSEQ_GROWTH_ITERATED GSEQ_GROWTH_STEP GSEQ_INV_POW2_RATIO GSEQ_LINEAR_LOWER GSEQ_MONOTONE GSEQ_NZ GSEQ_POS GSEQ_STEP_BOUND GSEQ_STEP_RATIO GSEQ_SUC_GT GSEQ_SUM_SPLIT GSEQ_UNBOUNDED GSEQ_UPPER_STEP GSEQ_UPPER_STEP_NAT INTEGRABLE_CMUL_ALT INTEGRABLE_IMP_RANDOM_VARIABLE INTEGRABLE_MAX_SUB_CONST INTEGRABLE_MUL_INDICATOR_FN INTEGRABLE_POINTWISE_LIMIT_UI INTEGRABLE_POW2_IMP INTEGRABLE_TAIL_VANISHES KOLMOGOROV_MAXIMAL_INEQ KOLMOGOROV_MAXIMAL_INEQ_SHIFTED L2_BOUNDED_IMP_UI MAX_ABS_SUB_TRIANGLE MAX_IN_FEASIBLE_SET MCT_NN_EXPECTATION MCT_NN_EXPECTATION_INTEGRABLE MCT_SIMPLE_NONNEG MINPOW_DIV_LE_ONE MIN_EQ_LEFT MIN_POW2_SPLIT NONDECREASING_CONVERGENCE_GSEQ NONNEG_SLLN RADON_NIKODYM RADON_NIKODYM_NONNEG RANDOM_VARIABLE_REAL_LIMINF RANDOM_VARIABLE_REAL_LIMSUP REAL_CESARO_MEAN REAL_DIV_FLOOR_LE REAL_FLOOR_EXISTS REAL_LE_DIV_MONO REAL_LIMINF_CONST_MINUS REAL_LIMINF_MIN_CONST_LE REAL_LIMINF_SUB_CONST REAL_LIMSUP_LBOUND REAL_LIMSUP_MONO REAL_LIMSUP_SUB_CONST REAL_LIMSUP_UBOUND REAL_LT_SUB_SWAP REAL_SUMMABLE_BOUND_PARTIAL REVERSE_FATOU_EXPECTATION REVERSE_FATOU_LEMMA SET_INTEGRAL_ZERO_ON_NULL SIGNED_MEASURE_CMUL SIGNED_MEASURE_DIFFERENCE SIGNED_MEASURE_FROM_INTEGRAL SIMPLE_EXPECTATION_NULL_SET SIMPLE_EXPECTATION_ON_CARRIER SIMPLE_EXPECTATION_ZERO_MUL SLLN_BOUNDED_VARIANCE SLLN_GAP_CONTROL_BOUNDED SLLN_GAP_DYADIC SLLN_SUBSEQ_BOUNDED SLLN_SUBSEQ_DYADIC SLLN_SUBSEQ_GSEQ SLLN_SUMMABLE_VARIANCE SUMMABLE_VARIANCE_DYADIC SUMMABLE_VARIANCE_DYADIC_BLOCK SUMMABLE_VARIANCE_GSEQ SUM_INDICATOR_LE_REAL SUM_INV_SQ_BOUND SUM_INV_SQ_LE_INV SUM_TELESCOPING_INV TAIL_LE_SQ_DIV TAIL_MUL_LE_SQ TAIL_PROB_SUMMABLE TAIL_PROB_SUM_LE_EXPECTATION TRUNCATED_VARIANCE_SUMMABLE TRUNCATED_VARIANCE_SUM_BOUND UI_IMP_L1_BOUNDED UI_POINTWISE_L1 In martingales.ml: DOOB_OPTIONAL_STOPPING EXPECTATION_CARRIER_INDICATOR INDICATOR_SUM_STOPPING_TIME INTEGRABLE_STOPPED_PROCESS MARTINGALE_CHARACTERIZATION MARTINGALE_TOWER MARTINGALE_TOWER_EQ RANDOM_VARIABLE_STOPPED_PROCESS SIMPLE_DOOB_MAXIMAL_INEQUALITY_STRONG SIMPLE_DOOB_OPTIONAL_STOPPING SIMPLE_DOOB_OPTIONAL_STOPPING_BOUNDED SIMPLE_IMP_BACKWARD_MARTINGALE SIMPLE_IMP_MARTINGALE SIMPLE_IMP_SUBMARTINGALE SIMPLE_IMP_SUPERMARTINGALE SIMPLE_MARTINGALE_COND_EXP SIMPLE_MARTINGALE_CONST SIMPLE_MARTINGALE_EXPECTATION_CONST SIMPLE_MARTINGALE_IMP_SUBMARTINGALE SIMPLE_MARTINGALE_IMP_SUPERMARTINGALE SIMPLE_MARTINGALE_STOPPED_PROCESS SIMPLE_MARTINGALE_SUB_SUPER SIMPLE_RV_EQ_ON_CARRIER SIMPLE_SUBMARTINGALE_EXPECTATION_INCREASING SIMPLE_SUBMARTINGALE_EXPECTATION_MONO SIMPLE_SUBMARTINGALE_LOCALIZED_INCREASING SIMPLE_SUBMARTINGALE_OPTIONAL_STOPPING_GE SIMPLE_SUBMARTINGALE_OPTIONAL_STOPPING_GE_GENERAL SIMPLE_SUBMARTINGALE_STOPPED_PROCESS SIMPLE_SUPERMARTINGALE_EXPECTATION_DECREASING SIMPLE_SUPERMARTINGALE_EXPECTATION_MONO SIMPLE_SUPERMARTINGALE_OPTIONAL_STOPPING_LE SIMPLE_SUPERMARTINGALE_OPTIONAL_STOPPING_LE_GENERAL SIMPLE_SUPERMARTINGALE_STOPPED_PROCESS STOPPING_TIME_GE_EVENT STOPPING_TIME_GT_IN_FF STOPPING_TIME_SUC_GE_IN_FF SUBMARTINGALE_TOWER SUM_RANDOM_INDEX SUPERMARTINGALE_TOWER WALD_EQUATION WALD_TERM_EXPECTATION In martingale_convergence.ml: ABSOLUTELY_CONTINUOUS_RESTRICT ADAPTED_IMP_RV ADAPTED_NEG_BACKWARD BACKWARD_DOWNCROSSING_EXPECTATION_BOUND BACKWARD_DOWNCROSSING_EXPECTATION_BOUND_L1 BACKWARD_DOWNCROSSING_PROB_BOUND_L1 BACKWARD_MARTINGALE_ALMOST_SURELY_BOUNDED BACKWARD_MARTINGALE_CONVERGENCE_L1_BOUNDED BACKWARD_MARTINGALE_RV BACKWARD_MAXIMAL_POS_PART BACKWARD_NEG_PART_MAXIMAL BACKWARD_SIMPLE_RUNNING_MAX_NEG_PART_EVENT BACKWARD_SIMPLE_RUNNING_MAX_POS_PART_EVENT BOUNDED_FINITE_DOWNCROSSINGS_IMP_CONVERGENT COND_EXP_AGREES_SIMPLE COND_EXP_ATOM_COND COND_EXP_CONDITIONING COND_EXP_CONSTANT_ON_ATOM COND_EXP_INTEGRABLE COND_EXP_MEASURABLE_WRT COND_EXP_RANGE_FINITE COND_EXP_SIMPLE_RV COND_EXP_TOWER DC_CONTINUATION DC_LE_REV_UC DC_LE_REV_UC_CASE_GE DC_LE_REV_UC_CASE_LT DC_PHASE_SHIFT DC_PHASE_STAYS_1 DC_RESTART DOOB_MARTINGALE DOOB_MAXIMAL_POS_PART DOWNCROSSING_COUNT_EQ_NEG DOWNCROSSING_PHASE_EQ_NEG DOWNCROSSING_PROB_BOUND EXPECTATION_RESTRICT FILTRATION_CONST_EVENTS FINITE_DOWNCROSSINGS_AS FINITE_DOWNCROSSINGS_AS_L1_BACKWARD FINITE_PREFIX_LOWER_BOUND FINITE_UPCROSSINGS_AS_L1 FINITE_UPCROSSINGS_CONVERGENT_OR_MINUS_INF GEN_COND_EXP_ADD GEN_COND_EXP_AE_UNIQUE GEN_COND_EXP_CMUL GEN_COND_EXP_CONDITIONING GEN_COND_EXP_CONST GEN_COND_EXP_EXISTS GEN_COND_EXP_INTEGRABLE GEN_COND_EXP_ITERATED GEN_COND_EXP_MEASURABLE_WRT GEN_COND_EXP_MONOTONE GEN_COND_EXP_NONNEG GEN_COND_EXP_SELF GEN_COND_EXP_TOWER GEN_DOOB_COMPENSATOR_AE_INCREASING GEN_DOOB_COMPENSATOR_GEN_PREDICTABLE GEN_DOOB_COMPENSATOR_INTEGRABLE GEN_DOOB_COMPENSATOR_MARTINGALE GEN_DOOB_COMPENSATOR_MEASURABLE_WRT GEN_DOOB_DECOMPOSITION GEN_DOOB_DECOMPOSITION_SUPER GEN_DOOB_MARTINGALE INFINITE_DOWNCROSSINGS_NULL INFINITE_UPCROSSINGS_NULL_L1 INTEGRABLE_CARRIER_AGREE INTEGRABLE_NUM_DOWNCROSSINGS INTEGRABLE_NUM_UPCROSSINGS INTEGRABLE_RESTRICT_IMP INTERS_UNIONS_IN_EVENTS IN_SUBSET_TRANSFER MARKOV_GE MARTINGALE_NEG MEASURABLE_WRT_ADD MEASURABLE_WRT_CMUL MEASURABLE_WRT_DIFF_LT MEASURABLE_WRT_NEG MEASURABLE_WRT_STRICT_LT MEASURABLE_WRT_SUB MIN_LE_IFF MIN_LE_RIGHT NN_EXPECTATION_RESTRICT NN_EXPECTATION_RESTRICT_BOUNDED NONNEG_MEASURABLE_WRT_ZERO_INTEGRALS_AE_ZERO NONNEG_RATIONALS_DENSE NONNEG_SIMPLE_FN_APPROX_RESTRICT NONNEG_SUBMARTINGALE_MAXIMAL NOT_BET_GAIN_NONNEG_EXPECTATION NUM_DOWNCROSSINGS_GE_EVENT NUM_DOWNCROSSINGS_MONO OPTIONAL_STOPPING_UI POS_PART_SUB_LE_ABS PROB_INCREASING_UNION_BOUND RANDOM_VARIABLE_RESTRICT_FORWARD REAL_LE_ZERO_FROM_BOUND RESTRICT_PROB_SPACE_CARRIER RESTRICT_PROB_SPACE_EVENTS RESTRICT_PROB_SPACE_OPS RESTRICT_PROB_SPACE_PROB REVERSED_IS_SUBMARTINGALE RUNNING_MAX_BOUNDED RUNNING_MAX_GE RUNNING_MAX_MONO_SUC RUNNING_MAX_NEG_PART_EVENT RUNNING_MAX_POS_PART_EVENT RUNNING_MAX_REV RV_LE_EVENT RV_NUM_DOWNCROSSINGS RV_NUM_UPCROSSINGS SIMPLE_BACKWARD_MARTINGALE_CONVERGENCE_BOUNDED SIMPLE_DOOB_MAXIMAL_POS_PART SIMPLE_DOOB_UPCROSSING_INEQUALITY SIMPLE_EXPECTATION_MUL_INDICATOR_ZERO_PROB SIMPLE_EXPECTATION_NULL_EVENT SIMPLE_EXPECTATION_PARTITION SIMPLE_EXPECTATION_RESTRICT SIMPLE_FINITE_UPCROSSINGS_AS SIMPLE_FINITE_UPCROSSINGS_AS_L1 SIMPLE_INFINITE_UPCROSSINGS_NULL SIMPLE_INFINITE_UPCROSSINGS_NULL_L1 SIMPLE_MARTINGALE_CONVERGENCE_BOUNDED SIMPLE_MARTINGALE_CONVERGENCE_L1_BOUNDED SIMPLE_NUM_DOWNCROSSINGS_GE_EVENT SIMPLE_NUM_UPCROSSINGS_GE_EVENT SIMPLE_REVERSED_IS_SUBMARTINGALE SIMPLE_RUNNING_MAX_NEG_PART_EVENT SIMPLE_RUNNING_MAX_POS_PART_EVENT SIMPLE_RV_LE_EVENT SIMPLE_RV_NUM_DOWNCROSSINGS SIMPLE_RV_RESTRICT_FORWARD SIMPLE_SUBMARTINGALE_NEG_PART_MAXIMAL SIMPLE_SUBMARTINGALE_POS_PART SIMPLE_SUBMARTINGALE_POS_PART_STEP SIMPLE_SUBMARTINGALE_SUB_CONST_STEP SIMPLE_UI_SUBMARTINGALE_CONVERGENCE_AS SIMPLE_UPCROSSING_EXPECTATION_BOUND SIMPLE_UPCROSSING_EXPECTATION_BOUND_L1 SIMPLE_UPCROSSING_PROB_BOUND SIMPLE_UPCROSSING_PROB_BOUND_L1 STOPPED_PROCESS_POINTWISE_LIMIT STOPPED_PROCESS_TRUNCATION_AGREE STOPPING_TIME_MIN SUBMARTINGALE_ALMOST_SURELY_BOUNDED SUBMARTINGALE_CONVERGENCE_L1_BOUNDED SUBMARTINGALE_GEN_COND_EXP_GE SUBMARTINGALE_MULTI_STEP SUBMARTINGALE_NEG_PART_MAXIMAL SUBMARTINGALE_OPTIONAL_STOPPING_UI SUBMARTINGALE_POS_PART SUBMARTINGALE_SUB_CONST SUB_SIGMA_ALGEBRA_PRED SUB_SIGMA_ALGEBRA_SELF SUB_SIGMA_ALGEBRA_SUBSET SUPERMARTINGALE_NEG_SUBMARTINGALE SUPERMARTINGALE_OPTIONAL_STOPPING_UI UC_COMPLETES UC_INCREMENT_PHASE_CHANGE UC_PREFIX UI_BACKWARD_MARTINGALE_CONVERGENCE_AS UI_SUBMARTINGALE_CONVERGENCE_AS UPCROSSING_COUNT_LE UPCROSSING_EXPECTATION_BOUND_L1 UPCROSSING_PROB_BOUND_L1 UP_PHASE_01 UP_PHASE_1_NOT_GE_B UP_PHASE_WHEN_LE_A In characteristic_functions.ml: ABS_GE_IN_EVENTS AZUMA_HOEFFDING_TWO_SIDED BOUNDED_DIFFERENCES_DOOB_INCREMENT BOUND_FROM_PRODUCT CDF_BOUNDS_FROM_TIGHTNESS CDF_SIMPLE_AGREE CHAR_FN_IM_SIMPLE CHAR_FN_RE_SIMPLE CLAMP_LIPSCHITZ COND_EXP_BOUNDED_VARIATION COND_EXP_ITERATED COND_EXP_PRESERVES_BD COND_EXP_RV_SIGMA_N COND_EXP_RV_SIGMA_TRIVIAL COND_EXP_SELF COND_EXP_SUM_REPR DIAGONAL_BOUNDED_CONVERGENCE DOOB_COMPENSATOR_INCREASING DOOB_COMPENSATOR_MARTINGALE DOOB_COMPENSATOR_MEASURABLE DOOB_COMPENSATOR_PREDICTABLE DOOB_COMPENSATOR_SIMPLE_RV DOOB_CONCENTRATION DOOB_CONCENTRATION_TWO_SIDED DOOB_DECOMPOSITION_SUPER EXPECTATION_SUM_FINITE FIBER_BOUNDED_DIFF FILTRATION_RV_SIGMA FINITE_RV_SIGMA FINITE_RV_SIGMA_ATOMS GAUSSIAN_TRAPEZOIDAL_BOUND GAUSSIAN_TRAPEZOIDAL_LOWER_BOUND GENERAL_CLT_MUTUAL HELLY_LIMIT_APPROACH HELLY_LIMIT_BOUNDS HELLY_LIMIT_LE_RATIONAL HELLY_LIMIT_MONO HELLY_LIMIT_SET_PROPS HELLY_RATIONAL_CONVERGENCE HELLY_SELECTION_THEOREM INDEP_RV_RV_SIGMA_SIMPLE INDEP_RV_SIGMA_EVENT_CDF INDEP_RV_SIGMA_EVENT_POINT_MASS INTEGRABLE_SUM_FINITE INTEGRAL_INV_1_T KOLMOGOROV_CROSS_TERM_VANISH KOLMOGOROV_MAXIMAL_INEQ_INDEP MARTINGALE_IMP_MARTINGALE MCDIARMID_INEQUALITY MCDIARMID_INEQUALITY_TWO_SIDED MEASURABLE_WRT_FINITE_SIMPLE_RV MEASURABLE_WRT_RV_SIGMA MONOTONE_CONTINUITY_DENSE MONOTONE_SMALL_OSC_SUBINTERVAL MUTUALLY_INDEP_RV_IMP_INDEP_RV MUTUALLY_INDEP_RV_MONO MUTUALLY_INDEP_RV_SUM_INDEP_RV POSITIVE_PROB_RV_SIGMA_ATOM PREDICTABLE_MARTINGALE_ZERO PREDICTABLE_NEG PREDICTABLE_SUB PROHOROV_FORWARD_SIMPLE QUANTITATIVE_CDF_LOWER QUANTITATIVE_CDF_UPPER RV_SIGMA_ATOM_EQ RV_SIGMA_ATOM_INDEP_CDF RV_SIGMA_ATOM_INDEP_POINT_MASS RV_SIGMA_ATOM_INDEP_POINT_MASS_GEN RV_SIGMA_ATOM_IN_EVENTS RV_SIGMA_ATOM_IN_SIGMA RV_SIGMA_IN_EVENTS RV_SIGMA_MONO RV_SIGMA_TRIVIAL RV_SIGMA_UNION_OF_ATOMS SE_MEASURABLE_INDICATOR_ATOM SIGMA_ALGEBRA_RV_SIGMA SIGMA_ATOM_RV_SIGMA_0 SIMPLE_AZUMA_HOEFFDING SIMPLE_CDF_LE_EXPECTATION SIMPLE_CDF_LOWER_TRAPEZOIDAL SIMPLE_CDF_UPPER_TRAPEZOIDAL SIMPLE_CHAR_FN_ADD_INDEP_IM SIMPLE_CHAR_FN_ADD_INDEP_RE SIMPLE_CHAR_FN_DETERMINES_NORMAL_CDF_LIMIT SIMPLE_CHAR_FN_IM_BOUND SIMPLE_CHAR_FN_IM_DIV SIMPLE_CHAR_FN_IM_MEAN_ZERO_BOUND SIMPLE_CHAR_FN_MODULUS_LE SIMPLE_CHAR_FN_RE_APPROX SIMPLE_CHAR_FN_RE_BOUND SIMPLE_CHAR_FN_RE_DIV SIMPLE_CHAR_FN_RE_POW_CONV_EXP SIMPLE_CHAR_FN_SUM_IID_IM_SQ_BOUND SIMPLE_CHAR_FN_SUM_IID_MODULUS SIMPLE_CHAR_FN_SUM_IID_RE_BOUND SIMPLE_CHAR_FN_SUM_IID_TRIANGLE SIMPLE_CHAR_FN_ZERO SIMPLE_CLT_CHAR_FN_CONVERGENCE SIMPLE_CLT_CHAR_FN_IM_CONVERGENCE SIMPLE_CLT_IM_ERROR_VANISHES SIMPLE_DOOB_DECOMPOSITION SIMPLE_DOOB_DECOMPOSITION_UNIQUE SIMPLE_EXPECTATION_LE_CDF SIMPLE_MARTINGALE_DIFF_CONVEX_INDICATOR SIMPLE_MARTINGALE_DIFF_EXP_ADAPTED_BOUND SIMPLE_MARTINGALE_DIFF_EXP_INDICATOR_BOUND SIMPLE_MARTINGALE_DIFF_INDICATOR_ZERO SIMPLE_MARTINGALE_SUB SIMPLE_RV_CDF_AS_SUM SIMPLE_RV_CDF_DECOMPOSE SIMPLE_RV_JOINT_CDF_AS_DOUBLE_SUM SIMPLE_RV_WRT_NEG SIMPLE_RV_WRT_SUB SIMPLE_SMOOTHING_INEQUALITY SIMPLE_STEP_C_BOUND SIMPLE_SUBMARTINGALE_COND_EXP_GE SIMPLE_TRIG_POLY_WEAK_CONVERGENCE SIMPLE_WEAK_CONVERGENCE_FROM_CHAR_FN SINC_ABS_INTEGRAL_BOUND_LOG SINC_BOUND SINC_CONTINUOUS SINC_INTEGRABLE STD_NORMAL_CDF_LIPSCHITZ STRICTLY_INCREASING_COMPOSE SUBMARTINGALE_IMP_SUBMARTINGALE SUB_SIGMA_ALGEBRA_RV_SIGMA SUM_TELESCOPE_ALT TIGHT_HELLY_LIMIT_PROPER TRAPEZOIDAL_CONTINUOUS TRAPEZOIDAL_LOWER_CONTINUOUS TRIG_POLY_EXPECTATION_DIFF TRIG_POLY_EXPECTATION_DIFF_BOUND UNIONS_RV_SIGMA WITNESS_EXISTS_RV In clt.ml: ALMOST_SURELY_NONEMPTY AS_CONVERGENCE_TRUNCATED BIDVD_EVENTUALLY BLOCK_INDEP_SUM_POW BOREL_CANTELLI_ALMOST_SURELY BOUNDED_INDEP_DIVERGENT_VARIANCE_DIVERGES CDF_BOUNDS CDF_LE_EXPECTATION CHAR_FN_ADD_INDEP_IM CHAR_FN_ADD_INDEP_RE CHAR_FN_DETERMINES_NORMAL_CDF_LIMIT CHAR_FN_EQ_OF_SAME_DIST CHAR_FN_IM_COMPONENT_BOUND CHAR_FN_IM_DIV CHAR_FN_MODULUS_LE CHAR_FN_RE_COMPONENT_BOUND CHAR_FN_RE_DIV CHAR_FN_RE_LOWER_BOUND CHAR_FN_RE_POW_CONV_EXP CHAR_FN_RE_UPPER_BOUND CHAR_FN_SUM_IID_IM_SQ_BOUND CHAR_FN_SUM_IID_MODULUS_RV CHAR_FN_SUM_IID_RE_BOUND CHAR_FN_SUM_IM_BOUND CHAR_FN_SUM_RE_PRODUCT_BOUND CLAMP_BOUND CLAMP_CENTERED_BOUND CLAMP_DISTRIBUTION_EQ CLAMP_EQ_WHEN_BOUNDED CLAMP_EXPECTATION_BOUND CLT_CHAR_FN_CONVERGENCE CLT_CHAR_FN_IM_CONVERGENCE CLT_IM_ERROR_VANISHES CLT_RE_PERTURBATION_VANISHES CONVERGENT_SERIES_TERMS_VANISH COS_LIPSCHITZ COVARIANCE_BOUNDED_INDEP EQUIDIST_BOUNDED_LIPSCHITZ EQUIDIST_MAX_ZERO EQUIDIST_NEG_MAX_ZERO EQUIDIST_NONNEG_EXPECTATION EQUIDIST_NONNEG_MIN_EXPECTATION EQUIDIST_NONNEG_MIN_SQ_EXPECTATION EQUIDIST_PROB_LT EQUIDIST_TAIL_PROB_GT EXPECTATION_CAUCHY_SCHWARZ EXPECTATION_IF_GT EXPECTATION_LE_CDF EXPECTATION_PRODUCT_POW_BOUNDED_INDEP EXPECTATION_SPLIT EXPECTATION_SUMMABLE_CHEBYSHEV (in satellite file clt_summable.ml) EXPECTATION_SUB_CONST EXPECTATION_SUM_CENTERED EXP_LE_PRODUCT_1_MINUS EXP_NEG_DIV_LE_1_MINUS FINITE_REAL_SEQUENCE_BOUNDED FORALL_SHIFT_INDEX FOURTH_MOMENT_BOUND_INDEP_CENTERED FOURTH_POWER_SUM_BOUND FROM_0_INTER_NUMSEG GENERAL_TRIG_POLY_WEAK_CONVERGENCE GENERAL_WEAK_CONVERGENCE_CONVERGENT IID_SLLN IID_SLLN_NONNEG INDEP_RV_CLAMP INDEP_RV_MIN_DIFF_CONST INDEP_RV_NEG INDEP_RV_RV_LEFT INDEP_RV_RV_RIGHT INTEGRABLE_BOUNDED_SUM_POW INTEGRABLE_CLAMP INTEGRABLE_CLAMP_CENTERED INTEGRABLE_CLAMP_CENTERED_POW2 INTEGRABLE_CLAMP_POW2 INTEGRABLE_CLT_IID INTEGRABLE_INDICATOR_WEIGHTED_POW2 INTEGRABLE_INDICATOR_WEIGHTED_POW2_LE INTEGRABLE_MAX_ZERO_POW2 IN_PROB_IMP_IN_DIST KOLMOGOROV_CONVERGENCE_CRITERION KOLMOGOROV_SLLN LEVY_CONTINUITY_GENERAL LEVY_CONTINUITY_GENERAL_CID LINDEBERG_FELLER_CLT MUTUALLY_INDEP_CDF_POINT_MASS_MIXED MUTUALLY_INDEP_EXPECTATION_PRODUCT_POW MUTUALLY_INDEP_INDICATOR_PRODUCT_EXPECTATION MUTUALLY_INDEP_POINT_MASS MUTUALLY_INDEP_RV_SEQ_CLAMP MUTUALLY_INDEP_RV_SEQ_IMP_FINITE MUTUALLY_INDEP_RV_SEQ_NSFA MUTUALLY_INDEP_RV_SEQ_PAIRWISE MUTUALLY_INDEP_RV_SEQ_SHIFT MUTUALLY_INDEP_RV_SEQ_SHIFT_VARYING MUTUALLY_INDEP_RV_SEQ_STRICT_INEQ MUTUALLY_INDEP_SIMPLE_EXPECTATION_PRODUCT NONNEG_BOUNDED_PARTIAL_SUMS_SUMMABLE NONNEG_DIVERGENT_UNBOUNDED PALEY_ZYGMUND PALEY_ZYGMUND_LOWER_BOUND PARTIAL_SUM_INTERS_SUBSET_NULL PARTIAL_SUM_LEVEL_PROB_VANISHES PARTITION_EXISTENCE PROB_INDEXED_UNION_EVENTS_LEMMA PROB_LIM_HELPER PRODUCT_1_MINUS_LE_EXP PRODUCT_2 PRODUCT_DIFF_SUM_BOUND PRODUCT_INDICATOR_FN_INTERS PROHOROV_FORWARD RANDOM_VARIABLE_CLAMP RANDOM_VARIABLE_INDICATOR_GT RANDOM_VARIABLE_INDICATOR_LE RANDOM_VARIABLE_PRODUCT_FINITE REAL_EQ_OF_ABS_LT_ALL REAL_EQ_SQUEEZE_DIV REAL_EQ_SUB_RADD REAL_POW2_ABS_LE REAL_SUMMABLE_TAIL_BOUND REALLIM_IMP_BOUNDED_NUM REALLIM_PRODUCT_FINITE RIEMANN_LOWER_MIN RV_CDF_EVENTS SECOND_MOMENT_BOUNDED_FROM_AS_CONVERGENCE SIMPLE_RV_PRODUCT_FINITE SIN_LIPSCHITZ SIN_MINUS_X_SPLIT_BOUND STEP_C_BOUND SUMMABLE_VARIANCE_FROM_CONVERGENCE SUMMABLE_VARIANCE_FROM_CONVERGENCE_V2 SUMMABLE_VARIANCE_MAX_ZERO SUM_REINDEX_SHIFT TAIL_EQUIVALENCE_CONVERGENCE TAYLOR_COS_SPLIT_BOUND THREE_SERIES_CONDITION1 THREE_SERIES_CONDITION2 THREE_SERIES_CONDITION3 THREE_SERIES_NECESSITY THREE_SERIES_NECESSITY_INDEP THREE_SERIES_REDUCTION THREE_SERIES_SUFFICIENCY TRIG_POLY_WEAK_CONVERGENCE UNBOUNDED_EVENTUALLY VARIANCE_MAX_ZERO_BOUND VARIANCE_NEG VARIANCE_SUB_CONST WEAK_CONVERGENCE_FROM_CHAR_FN In distributions.ml [new file]: BERNOULLI_IS_BINOMIAL_1 BERNOULLI_RV_EXPECTATION BERNOULLI_RV_PROB_ZERO BERNOULLI_RV_VARIANCE BINOMIAL_RV_EXPECTATION BINOMIAL_RV_VARIANCE BINOM_DIAG BINOM_KBINOM_IDENTITY BINOM_KBINOM_IDENTITY2 BINOM_LE_POW BINOM_PASCAL_ADD BINOM_SYMM_ADD GEOMETRIC_IS_NEG_BINOMIAL_1 GEOMETRIC_MEAN_SERIES GEOMETRIC_PMF_POS GEOMETRIC_PMF_SUMS GEOMETRIC_SECOND_FACTORIAL_MOMENT GEOMETRIC_SECOND_MOMENT GEOMETRIC_VARIANCE_SERIES INDICATOR_BERNOULLI NB_SERIES NB_SERIES_TELESCOPING NEG_BINOMIAL_MEAN_SERIES NEG_BINOMIAL_PMF_POS NEG_BINOMIAL_PMF_SUMS NEG_BINOMIAL_SECOND_FACTORIAL_MOMENT NEG_BINOMIAL_VARIANCE_SERIES NUMERATOR_LIMIT POISSON_LIMIT POISSON_PMF_POS POISSON_PMF_SUMS POLY_IDENTITY POW_PRED REALLIM_BINOM_OVER_NPOWER REALLIM_BINOM_POWN REALLIM_NSQUARED_TIMES_POWN REALLIM_N_TIMES_POWN REALLIM_POW_TIMES_POWN REALLIM_RATIO_TO_1 REALLIM_SHIFT_SUC REAL_EXP_CONVERGES REAL_POW_OFFSET2 REAL_SUMS_KK1X_POW REAL_SUMS_KX_POW SUM_BINOMIAL_FIRST_MOMENT SUM_BINOMIAL_SECOND_MOMENT SUM_BINOMIAL_SECOND_RAW_MOMENT SUM_GP_DERIVATIVE SUM_GP_SECOND_DERIVATIVE SUM_KK1X_POW SUM_KX_POW

dnezam and others added 4 commits April 20, 2026 22:32

Multivariate/vectors.ml: Use </ instead of < (jrh13#173)

0a215a4

dnezam force-pushed the update branch from 2e252e6 to e74968d Compare May 11, 2026 05:35

Merge remote-tracking branch 'upstream/master' into update

49a5ea9

dnezam force-pushed the update branch from e74968d to 49a5ea9 Compare May 11, 2026 06:12

dnezam merged commit bc9fdcf into master May 11, 2026
1 check passed

dnezam deleted the update branch May 11, 2026 06:42

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Update to latest HOL Light commit#14

Update to latest HOL Light commit#14
dnezam merged 5 commits into
masterfrom
update

dnezam commented May 11, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

dnezam commented May 11, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants