Skip to content

Commit 3170739

Browse files
jrh13jrh13
committed
Substantially extended the probability theory library with new results,
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
1 parent d19bdec commit 3170739

9 files changed

Lines changed: 47511 additions & 7490 deletions

File tree

‎CHANGES‎

Lines changed: 125 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,131 @@
88
* page: https://github.com/jrh13/hol-light/commits/master *
99
* *****************************************************************
1010

11+
Mon 27th Apr 2026 Probability/*
12+
13+
Substantially extended the probability theory library with new results,
14+
generalized definitions, and systematic naming cleanup, also adding
15+
standard discrete distributions. This work was entirely done by Claude
16+
Opus 4.6.
17+
18+
The most significant structural change is the systematic generalization
19+
from simple random variables to integrable random variables. The original
20+
library developed much of the theory using simple_rv (finite-valued
21+
random variables) with simple_expectation. This update adds parallel
22+
general definitions using integrable/expectation (Lebesgue integration)
23+
and reproves key results at this level of generality. The naming
24+
convention is: unprefixed names (e.g. martingale, char_fn_re) now refer
25+
to the general versions, while the original simple-RV versions are
26+
preserved under SIMPLE_ prefixes (e.g. simple_martingale,
27+
simple_char_fn_re).
28+
29+
IMPORTANT: Several definitions and theorem names that existed in the
30+
previous version now refer to different (strictly more general) objects.
31+
32+
The following definitions changed meaning (old simple-RV-based
33+
definitions are preserved under the names shown):
34+
35+
martingale now uses adapted/integrable/expectation
36+
(was: simple_adapted/simple_rv/simple_expectation;
37+
old version now called simple_martingale)
38+
39+
submartingale same generalization pattern
40+
(old version now called simple_submartingale)
41+
42+
supermartingale same generalization pattern
43+
(old version now called simple_supermartingale)
44+
45+
char_fn_re now defined via expectation p (\x. cos(t * X x))
46+
(was: simple_expectation p (\x. cos(t * X x));
47+
old version now called simple_char_fn_re)
48+
49+
char_fn_im now defined via expectation p (\x. sin(t * X x))
50+
(was: simple_expectation p (\x. sin(t * X x));
51+
old version now called simple_char_fn_im)
52+
53+
converges_L2 now defined via expectation
54+
(was: simple_expectation;
55+
old version now called simple_converges_L2)
56+
57+
The following 20 theorem names that existed in the previous version now
58+
prove strictly stronger results (weaker hypotheses, same conclusions).
59+
In each case, the hypothesis "simple_rv" was replaced by
60+
"random_variable" or "integrable", and "simple_expectation" by
61+
"expectation". The old simple-RV versions are preserved with a SIMPLE_
62+
prefix:
63+
64+
CDF_LE_EXPECTATION CLT_CHAR_FN_CONVERGENCE
65+
CHAR_FN_ADD_INDEP_IM CLT_CHAR_FN_IM_CONVERGENCE
66+
CHAR_FN_ADD_INDEP_RE CLT_IM_ERROR_VANISHES
67+
CHAR_FN_DETERMINES_NORMAL_CDF_LIMIT EXPECTATION_LE_CDF
68+
CHAR_FN_IM_BOUND MCT_NN_EXPECTATION
69+
CHAR_FN_MODULUS_LE STEP_C_BOUND
70+
CHAR_FN_RE_BOUND TRIG_POLY_WEAK_CONVERGENCE
71+
CHAR_FN_RE_POW_CONV_EXP WEAK_CONVERGENCE_FROM_CHAR_FN
72+
CHAR_FN_SUM_IID_IM_SQ_BOUND MEASURABLE_WRT_ADD
73+
CHAR_FN_SUM_IID_RE_BOUND MEASURABLE_WRT_SUB
74+
75+
Major new results include:
76+
77+
KOLMOGOROV_SLLN: Kolmogorov's Strong Law of Large Numbers via the
78+
maximal inequality for independent summands
79+
80+
IID_SLLN: for i.i.d. integrable random variables, the sample mean
81+
converges almost surely to the common expectation
82+
83+
LINDEBERG_FELLER_CLT: the CLT under the Lindeberg condition for
84+
triangular arrays of independent random variables
85+
86+
LEVY_CONTINUITY_GENERAL: pointwise convergence of characteristic
87+
functions implies convergence in distribution
88+
89+
HELLY_SELECTION_THEOREM: every uniformly bounded sequence of
90+
distribution functions has a convergent subsequence
91+
92+
PROHOROV_FORWARD: tightness implies relative sequential compactness
93+
in the topology of convergence in distribution
94+
95+
RADON_NIKODYM: for an absolutely continuous signed measure, there
96+
exists an integrable density
97+
98+
HAHN_DECOMPOSITION / JORDAN_DECOMPOSITION: every signed measure
99+
admits a Hahn decomposition and a Jordan decomposition into
100+
nonneg measures concentrated on complementary sets
101+
102+
GEN_COND_EXP_EXISTS / GEN_COND_EXP_TOWER / GEN_COND_EXP_ITERATED:
103+
general conditional expectation via Radon-Nikodym with tower
104+
property, iterated conditioning, monotonicity, and linearity
105+
106+
GEN_DOOB_DECOMPOSITION: general Doob decomposition of a
107+
submartingale into a martingale plus a predictable increasing
108+
process
109+
110+
BACKWARD_MARTINGALE_CONVERGENCE_L1_BOUNDED: L1-bounded backward
111+
martingales converge almost surely
112+
113+
UI_SUBMARTINGALE_CONVERGENCE_AS / OPTIONAL_STOPPING_UI: uniformly
114+
integrable submartingale convergence and optional stopping
115+
116+
AZUMA_HOEFFDING_TWO_SIDED / MCDIARMID_INEQUALITY: concentration
117+
inequalities for martingales and bounded-differences functions
118+
119+
THREE_SERIES_SUFFICIENCY / THREE_SERIES_NECESSITY /
120+
THREE_SERIES_NECESSITY_INDEP: Kolmogorov three-series theorem (both
121+
directions; two independent proofs of necessity)
122+
123+
PALEY_ZYGMUND: reverse Markov-type inequality for lower bounds on
124+
the probability that a nonneg RV exceeds a fraction of its mean
125+
126+
UI_BACKWARD_MARTINGALE_CONVERGENCE_AS: UI backward martingales
127+
converge almost surely
128+
129+
WALD_EQUATION: for a martingale stopped at a bounded stopping time
130+
131+
FATOU_LEMMA / REVERSE_FATOU_LEMMA / DOMINATED_CONVERGENCE_AE:
132+
convergence theorems for expectations
133+
134+
POISSON_LIMIT: the Poisson limit theorem (binomial -> Poisson)
135+
11136
Thu 23rd Apr 2026 Library/ringtheory.ml, Library/fieldtheory.ml, 100/transcendence.ml
12137

13138
Adopted the "coeff" function from 100/transcendence.ml in the main ring theory

0 commit comments

Comments
 (0)