# FormalSLT theorem index (concept-keyed)

Search by mathematical concept, not by declaration name. Generated from
`docs/proof-frontier-manifest.json` plus the Lean sources by
`scripts/generate_theorem_index.py`. For a searchable version with a live
filter box, open `docs/INDEX.html`.

531 declarations, 530 resolved to a `file:line`.

## By concept

- **(untagged)** (38): `binaryClassTrace`, `countableTimeClass_iUnion_eq_exists`, `countableTimeClass_not_forall_lt_eq_exists_ge`, `covariance_cauchy_schwarz`, `effectiveClass`, `empiricalAverageRangeSum_le_card_mul_uniformRange`, `empiricalAverageRangeSum_pos_of_exists_range_pos`, `empiricalAverageUniformRangeSampleSize_ge_of_sqrtBudget_le`, `finiteDyadicRealBudget_classBudget_ofReal`, `finiteDyadicRealBudget_horizon_le_time`, `finiteDyadicTimeBudget`, `finiteDyadicTimeBudget_sum_fin_le`, `finiteDyadicTimeBudget_tsum_le`, `finiteExponentialFamily_fisherInformation_eq_variance`, `finiteExponentialFamily_logPartition_secondDeriv_eq_fisherInformation`, `finiteExponentialFamily_mean_eq_logPartition_deriv`, `finiteExponentialFamily_score_eq_centered`, `finiteExponentialFamily_variance_eq_logPartition_secondDeriv`, `finiteExponentialPMF`, `finiteExponentialPMFDeriv`, `finiteExponentialPMF_hasDerivAt`, `finiteExponentialPMF_pos`, `finiteExponentialPMF_sum_one`, `finiteLogPartition`, `finiteLogPartition_hasDerivAt`, `finiteLogPartition_hasDerivAt_of_positiveBase`, `finiteLogPartition_hasSecondDerivAt`, `finiteLogPartition_hasSecondDerivAt_of_positiveBase`, `finiteMean_deriv_eq_variance`, `finiteMean_hasDerivAt`, `finitePartition`, `finitePartition_pos`, `fisherInformation`, `piMeasure`, `scoreFunction`, `score_mean_zero_of_finite_regular`, `weightedCovariance`, `weightedExpectation`
- **Azuma** (1): `genGap_tail_bound_azuma_explicit`
- **Bennett** (5): `bennett_mgf`, `bennett_mgf_subgamma`, `bennett_tail`, `bennett_taylor_bound`, `exp_le_quadratic_of_le`
- **Bernoulli** (22): `bernoulliFisherInformation`, `bernoulliHalfCramerRaoWitness`, `bernoulliHalfFisherInformation`, `bernoulliLogLikelihood_global_argmax_from_count`, `bernoulliMean_eq`, `bernoulliNaturalBase`, `bernoulliNaturalStatistic`, `bernoulliNatural_fisher_eq_variance_zero`, `bernoulliNatural_fisher_zero`, `bernoulliNatural_logPartition_deriv_zero`, `bernoulliNatural_logPartition_secondDeriv_zero`, `bernoulliNatural_logPartition_zero`, `bernoulliNatural_mean_zero`, `bernoulliNatural_partition`, `bernoulliNatural_pmf_zero`, `bernoulliNatural_variance_zero`, `bernoulliNatural_witness`, `bernoulliPMF`, `bernoulliScoreAtSampleMean_eq_zero`, `bernoulliThreeZerosOneOne_uniformDeviation_le_quarter`, `bernoulliVariance_eq`, `bernoulli_bernstein_tail`
- **Bernstein** (19): `BernsteinCondition`, `averaged_bernstein_tail`, `bernoulli_bernstein_tail`, `bernstein_tail`, `centeredSecondMoment_le_of_bernstein_localized`, `finiteExcessRisk_le_of_localizedDeviation_bernstein_fixedPoint`, `finiteExcessRisk_le_of_localizedFastRateUpperDeviationEvent_bernstein_fixedPoint`, `finiteExcessRisk_le_of_localizedUpperDeviationEvent_bernstein_fixedPoint`, `finitePACBayesBernsteinMargin_badEventMass_le_delta`, `finitePACBayesBernsteinPenalty_badEventMass_le_delta`, `finitePACBayesBernstein_fixedLambda_badEventMass_le_delta`, `localizedExcessRiskEmpiricalRademacherComplexity_le_of_bernstein_fixedPointCertificate`, `localizedExcessRiskEmpiricalRademacherComplexity_le_secondMoment`, `localizedFastRateHighConfidence_bernstein_fixedPoint_boundedExcess`, `localizedFastRateHighConfidence_bernstein_fixedPoint_of_centeredShiftedExpMoment`, `localizedFastRateHighConfidence_bernstein_fixedPoint_of_shiftedExpMoment`, `localizedFiniteClassBernsteinHighConfidence_empirical_nonpos`, `posteriorGeneralizationGap_le_bernstein_of_priorBernsteinExpMoment_le`, `priorBernsteinExpMoment`
- **Chernoff** (1): `chernoff_tail`
- **ERM** (78): `EpsilonizedSupremumBoundaryChoice`, `FiniteDyadicDudleyInstance.SupremumAdapter`, `FixedPointUpperCertificate`, `IsERM`, `LocalizedDeviationCertificate`, `abs_expectedFiniteGeneralizationGap_le_uniformStability_finiteProduct`, `abs_expectedFiniteGeneralizationGap_le_uniformStability_of_coordinateSwap`, `atTop_time_uniform_confidence_sequence_subGamma_mixture`, `bettingWealth_supermartingale`, `countableWeightedSupermartingale_tsum`, `dyadicEpochMixture_supermartingale`, `eProcess_product_of_supermartingale`, `empiricalRisk`, `excessRisk`, `expectedFiniteGeneralizationGap_le_uniformStability_finiteProduct`, `expectedFiniteGeneralizationGap_le_uniformStability_of_coordinateSwap`, `expected_genGap_le_two_expected_empiricalRademacherComplexity`, `finDiscreteRademacherSup_le_projectedSup`, `finiteDyadicRealBudget_horizon_logBudget_eq_closedForm`, `finiteEmpiricalRisk`, `finiteExcessRisk_le_of_localizedDeviation_bernstein_fixedPoint`, `finiteExcessRisk_le_of_localizedDeviation_empirical_nonpos`, `finiteExcessRisk_le_of_localizedFastRateUpperDeviationEvent_bernstein_fixedPoint`, `finiteExcessRisk_le_of_localizedSampleDependentUpperDeviationEvent_empirical_nonpos`, `finiteExcessRisk_le_of_localizedUpperDeviationEvent_bernstein_fixedPoint`, `finiteExcessRisk_le_of_localizedUpperDeviationEvent_empirical_nonpos`, `finiteExpectation_supFunctional_le_projected_add_skeleton_terminalError`, `finiteExpectation_supFunctional_le_projected_add_terminalError`, `finitePartition_hasDerivAt`, `finitePriorAveraged_mgf_empiricalRiskDeviation_le`, `finiteProduct_mgf_empiricalRiskDeviation_eq_pow`, `finiteProduct_mgf_empiricalRiskDeviation_le_of_single`, `finiteSup_skeleton_le_projectedSup_add_terminalError`, `finite_dudley_entropy_sum_totalBounded_dyadic_coveringNumbers`, `finite_epsilonizedSup_modulus_dudley_totalBounded_dyadic_entropy_truncatedIntervalIntegral_comparison`, `finite_projectedNet_dudley_entropy_sum_totalBounded_dyadic_coveringNumbers`, `finite_projected_chaining_expectation_bound`, `finite_projected_dudley_entropy_sum_totalBounded_dyadic_coveringNumbers`, `finite_separableSupFunctional_dudley_entropy_sum_coveringNumbers_geometric_entropy_truncatedIntervalIntegral_comparison`, `finite_separableSupFunctional_dudley_totalBounded_dyadic_entropy_truncatedIntervalIntegral_comparison`, `finite_supFunctional_dudley_entropy_sum_coveringNumbers_geometric_entropy_truncatedIntervalIntegral_comparison`, `finite_supFunctional_dudley_totalBounded_dyadic_entropy_truncatedIntervalIntegral_comparison`, `genGap`, `genGap_highProb_finiteClass`, `genGap_highProb_rademacher`, `genGap_highProb_vcClass`, `genGap_tail_bound_azuma_explicit`, `genGap_tail_bound_sharp_explicit`, `localizedDeviationCertificate_of_mem_upperDeviationEvent`, `localizedExcessRiskEmpiricalRademacherComplexity_le_of_bernstein_fixedPointCertificate`, `localizedExcessRiskEmpiricalRademacherComplexity_le_secondMoment`, `localizedExcessRiskEmpiricalRademacherComplexity_nonneg`, `lowerRayBracketing_uniformDeviation_bound`, `mixture_is_supermartingale`, `optimized_lambda_two_sided_confidence_sequence`, `pacBayesPriorMixture_supermartingale`, `pac_bayes_generalization`, `pacbayes_mcallester_deterministic`, `pacbayes_mcallester_sqrt`, `pacbayes_mcallester_subGaussian`, `posteriorGeneralizationGap_le_bernstein_of_priorBernsteinExpMoment_le`, `posteriorRisk_bound_of_priorDeviationMGF_le`, `posteriorRisk_bound_of_priorDeviationMGF_le_complexity_sqrt`, `priorBernsteinExpMoment`, `rademacherERMBridge_for_gcClass`, `stability_genGap_hasBoundedDifferences`, `subGamma_stitched_boundary_supermartingale`, `terminalApprox_of_pathwise_modulus`, `terminalApprox_of_pathwise_modulus_radiusBound`, `twoPointRademacherSup_le_projectedSup`, `unitIntervalQuarterMeshNet_coveringNumber`, `unitIntervalQuarterMeshNet_covers`, `unitIntervalRademacherLinearSup_projectedQuarterMesh_dudley_log15_bound`, `unitIntervalRademacherLinearSup_projectedQuarterMesh_dudley_log15_bound_eval`, `unitIntervalRademacherLinear_halfQuarter_increment_log15_bound`, `unitIntervalRademacherLinear_projectedQuarterMesh_dudley_log15_bound`, `vc_erm_excessRisk_tail`, `vc_erm_sample_complexity`
- **Glivenko-Cantelli** (30): `IsGCClass`, `bernoulliThreeZerosOneOne_uniformDeviation_le_quarter`, `classicalGlivenkoCantelli_iid`, `classicalGlivenkoCantelli_of_pointwise_lowerRay`, `countableTimeClassTwoSidedUniformDeviationUnionBound_dyadicBudget_threshold`, `empiricalCDF`, `empiricalCDFUniformDeviation`, `empiricalCDF_eq_lowerRayEmpiricalAverage`, `finiteClassTwoSidedUniformDeviationUnionBound`, `finiteClassTwoSidedUniformDeviationUnionBound_cardInv`, `finiteClassUniformDeviationUnionBound`, `finiteClassUniformDeviationUnionBound_cardInv`, `finiteLowerRayBracketingGrid`, `finiteTimeClassTwoSidedUniformDeviationUnionBound_cardInv`, `finiteTimeClassTwoSidedUniformDeviationUnionBound_dyadicBudget`, `finiteTimeClassTwoSidedUniformDeviationUnionBound_dyadicBudget_threshold`, `finiteTimeClassTwoSidedUniformDeviationUnionBound_timeBudget`, `finiteTimeClassTwoSidedUniformDeviationUnionBound_timeBudget_threshold`, `integral_lowerRayIndicator_comp_eq_cdf`, `lowerRayBracketing_uniformDeviation_bound`, `lowerRayGC_iff_classicalGlivenkoCantelli`, `lowerRayIndicator`, `lowerRayPointwiseStrongLaw`, `rademacherERMBridge_for_gcClass`, `strictLowerRayIndicator`, `strictLowerRayPointwiseStrongLaw`, `uniformDeviation_highProb_finiteClass`, `uniformDeviation_highProb_vcClass`, `vcHoeffdingBridge_for_gcClass`, `vcPacBayesHybridBridge_for_gcClass`
- **Hoeffding** (44): `anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_confidenceSequence_fromHoeffding`, `anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_namedRadius_exists_fromHoeffding`, `anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_timeVaryingRadius_exists_fromHoeffding`, `anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_timeVaryingRadius_fromHoeffding`, `empiricalAverageLowerHoeffdingTail`, `empiricalAverageTwoSidedHoeffdingTail`, `empiricalAverageTwoSidedHoeffdingTail_le_uniformRangeTwoSidedHoeffdingTail`, `empiricalAverageTwoSidedHoeffdingTail_le_uniformRangeTwoSidedHoeffdingTail_of_rangeBound`, `empiricalAverageTwoSidedHoeffdingTail_le_uniformRangeTwoSidedHoeffdingTail_of_rangeBound_of_exists_range_pos`, `empiricalAverageUniformRangeTwoSidedHoeffdingSampleSizeTail`, `empiricalAverageUniformRangeTwoSidedHoeffdingSampleSizeTail_le_of_explicitRadius`, `empiricalAverageUniformRangeTwoSidedHoeffdingSampleSizeTail_le_of_logBudget`, `empiricalAverageUniformRangeTwoSidedHoeffdingSampleSizeTail_le_of_sampleSize_ge`, `empiricalAverageUniformRangeTwoSidedHoeffdingTail`, `empiricalAverageUniformRangeTwoSidedHoeffdingTail_eq_sampleSizeTail`, `empiricalAverageUpperHoeffdingTail`, `empiricalAverageUpperHoeffdingTail_eq_lower`, `finitePrefixFiniteClassDeviationFromHoeffding_closedForm`, `finitePrefixFiniteClassDeviationFromHoeffding_closedForm_cardSample`, `finitePrefixFiniteClassDeviationFromHoeffding_closedForm_unitRange`, `finitePrefixFiniteClassDeviationFromHoeffding_unitRange_explicitRadius`, `finitePrefixFiniteClassDeviationFromHoeffding_unitRange_explicitRadius_nonemptySample`, `finitePrefixFiniteClassDeviationFromHoeffding_unitRange_radius`, `finitePrefixFiniteClassDeviationFromHoeffding_zeroOneRange_explicitRadius`, `finitePrefixFiniteClassDeviationFromHoeffding_zeroOneRange_timeVaryingRadius`, `finitePrefixFiniteClassDeviationFromHoeffding_zeroOneRange_timeVaryingRadius_fromHoeffding`, `finiteTimeClassEmpiricalAverageDeviationFromHoeffding_dyadicBudget`, `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_closedFormHorizonRadius_dyadicRealBudget`, `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_closedFormHorizonSampleSize_dyadicRealBudget`, `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_dyadicBudget`, `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_epsilonOfSampleSize_dyadicRealBudget`, `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_horizonUniformRadius_dyadicRealBudget`, `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize`, `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize_dyadicRealBudget`, `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize_from_logBudget`, `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize_ge`, `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize_threshold`, `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_twoSidedTailBudget`, `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_uniformRangeBudget`, `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_uniformRangeBudget_of_rangeBound`, `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_uniformRangeBudget_of_rangeBound_of_exists_range_pos`, `hoeffding_mean_tail_twoSided`, `sampleMean_hoeffding_tail`, `vcHoeffdingBridge_for_gcClass`
- **KL divergence** (4): `continuousPriorPosterior_certificate_derived`, `continuous_catoni_changeOfMeasure_bound`, `klDiv_nonneg`, `pacbayes_changeOfMeasure`
- **MGF** (25): `bennett_mgf`, `bennett_mgf_subgamma`, `chernoff_tail`, `condSubGammaMGF_of_bounded_centered_condVariance`, `continuous_catoni_changeOfMeasure_bound`, `finDiscrete_rademacher_mgf_bound`, `finitePriorAveraged_mgf_empiricalRiskDeviation_le`, `finiteProduct_mgf_empiricalRiskDeviation_eq_pow`, `finiteProduct_mgf_empiricalRiskDeviation_le_of_single`, `finite_expectedSup_le_of_mgf_log`, `finite_expectedSup_le_of_subGaussian_mgf_sqrt`, `localizedOneCoordinateDeviationMGF_le_of_excessLoss_mem_Icc_neg_one_one`, `localizedPointwiseUpperDeviationExpMoment_finiteProduct_le_of_single`, `oneCoordinate_boundedLoss_mgf`, `pacbayes_mcallester_deterministic`, `pacbayes_mcallester_sqrt`, `posteriorRisk_bound_of_priorDeviationMGF_le`, `posteriorRisk_bound_of_priorDeviationMGF_le_complexity_sqrt`, `priorAveraged_boundedLoss_mgf`, `priorAveraged_boundedLoss_mgf_badEventMass_le_delta`, `sampleAverage_boundedLoss_mgf`, `subGaussianMGF_tail_twoSided`, `twoPoint_rademacher_mgf_bound`, `unitIntervalRademacherLinearProcess_increment_mgf`, `unitInterval_rademacherLinear_mgf_bound`
- **Markov** (3): `cond_markov_of_nonneg`, `localizedPointwiseUpperDeviationBadEventMass_le_expMoment_div`, `priorAveraged_boundedLoss_mgf_badEventMass_le_delta`
- **McDiarmid** (9): `hasBoundedDifferences_tail_sharp`, `mcdiarmid_inequality_iid_const_width`, `mcdiarmid_of_hasBoundedDifferences_sharp`, `mcdiarmid_of_hasBoundedDifferences_sharp_hetero`, `mcdiarmid_of_hasBoundedDifferences_sharp_hetero_lower`, `mcdiarmid_of_hasBoundedDifferences_sharp_lower`, `mcdiarmid_of_hasBoundedDifferences_sharp_of_hetero`, `stability_genGap_hasBoundedDifferences`, `trainingLoss_hasBoundedDifferences`
- **PAC-Bayes** (120): `BernsteinCondition`, `FiniteCoordinateSwapIdentity`, `FixedPointUpperCertificate`, `LocalizedDeviationCertificate`, `abs_expectedFiniteGeneralizationGap_le_uniformStability_finiteProduct`, `abs_expectedFiniteGeneralizationGap_le_uniformStability_of_coordinateSwap`, `abs_expectedFiniteStabilityGap_le_uniformStability_finiteProduct`, `abs_expectedFiniteStabilityGap_le_uniformStability_of_coordinateSwap`, `abs_expectedStabilityGap_le_uniformStability_piMeasure_of_boundedLoss`, `averaged_bernstein_tail`, `bennett_mgf`, `bennett_mgf_subgamma`, `bernstein_tail`, `boundedLoss_coordinateSelectedLoss_integrable`, `boundedLoss_selectedLoss_integrable`, `boundedLoss_updateSelectedLoss_integrable`, `bousquet_elisseeff_expectedGap_variant`, `bousquet_elisseeff_expectedGap_variant_of_boundedLoss`, `bousquet_elisseeff_uniform_stability_corollary`, `bousquet_elisseeff_uniform_stability_corollary_of_boundedLoss`, `catoni_fixedLambda_budget_eq_sqrt`, `centeredSecondMoment_le_of_bernstein_localized`, `continuousPriorPosterior_certificate_derived`, `continuous_catoni_changeOfMeasure_bound`, `continuous_donsker_varadhan`, `exp_le_quadratic_of_le`, `expectedFiniteGeneralizationGap_le_uniformStability_finiteProduct`, `expectedFiniteGeneralizationGap_le_uniformStability_of_coordinateSwap`, `expectedFiniteStabilityGap_le_uniformStability_finiteProduct`, `expectedFiniteStabilityGap_le_uniformStability_of_coordinateSwap`, `expectedStabilityGap_le_uniformStability_piMeasure_of_boundedLoss`, `finiteCatoni_badEventMass_le_delta`, `finiteClass_loss_measurable`, `finiteEmpiricalRisk`, `finiteExcessRisk_le_of_localizedDeviation_bernstein_fixedPoint`, `finiteExcessRisk_le_of_localizedDeviation_empirical_nonpos`, `finiteExcessRisk_le_of_localizedFastRateUpperDeviationEvent_bernstein_fixedPoint`, `finiteExcessRisk_le_of_localizedSampleDependentUpperDeviationEvent_empirical_nonpos`, `finiteExcessRisk_le_of_localizedUpperDeviationEvent_bernstein_fixedPoint`, `finiteExcessRisk_le_of_localizedUpperDeviationEvent_empirical_nonpos`, `finiteMcAllesterBoundedComplexity_badEventMass_le_delta`, `finiteMcAllesterGridOptimized_badEventMass_le_delta`, `finiteMcAllesterGridPeeling_badEventMass_le_delta`, `finitePACBayesBernsteinMargin_badEventMass_le_delta`, `finitePACBayesBernsteinPenalty_badEventMass_le_delta`, `finitePACBayesBernstein_fixedLambda_badEventMass_le_delta`, `finitePriorAveraged_mgf_empiricalRiskDeviation_le`, `finiteProductSampleWeight`, `finiteProductSampleWeight_coordinateSwapIdentity`, `finiteProduct_mgf_empiricalRiskDeviation_eq_pow`, `finiteProduct_mgf_empiricalRiskDeviation_le_of_single`, `klDiv_nonneg`, `localizedDeviationCertificate_of_mem_upperDeviationEvent`, `localizedEmpiricalRademacherComplexity_mono`, `localizedEmpiricalRademacherComplexity_nonneg_of_zero`, `localizedExcessRiskEmpiricalRademacherComplexity_le_of_bernstein_fixedPointCertificate`, `localizedExcessRiskEmpiricalRademacherComplexity_le_secondMoment`, `localizedExcessRiskEmpiricalRademacherComplexity_nonneg`, `localizedFastRateHighConfidence_bernstein_fixedPoint_boundedExcess`, `localizedFastRateHighConfidence_bernstein_fixedPoint_of_centeredShiftedExpMoment`, `localizedFastRateHighConfidence_bernstein_fixedPoint_of_shiftedExpMoment`, `localizedFastRatePointwiseShiftedExpMoment_finiteProduct_le_boundedExcess`, `localizedFastRatePointwiseShiftedExpMoment_le_centered_div`, `localizedFastRateUpperDeviationBadEventMass`, `localizedFastRateUpperDeviationBadEventMass_finiteProduct_le_delta_boundedExcess`, `localizedFastRateUpperDeviationBadEventMass_le_fixed_epsilon`, `localizedFastRateUpperDeviationBadEventMass_le_sum_centeredShiftedExpMoment_div`, `localizedFastRateUpperDeviationBadEventMass_le_sum_shiftedExpMoment`, `localizedFastRateUpperDeviationEvent`, `localizedFiniteClassBernsteinHighConfidence_empirical_nonpos`, `localizedFiniteClassHighConfidence_empirical_nonpos_boundedExcess`, `localizedOneCoordinateDeviationMGF_le_of_excessLoss_mem_Icc_neg_one_one`, `localizedPointwiseSampleDependentUpperDeviationBadEventMass`, `localizedPointwiseSampleDependentUpperDeviationBadEventMass_le_shiftedExpMoment`, `localizedPointwiseSampleDependentUpperDeviationShiftedExpMoment`, `localizedPointwiseSampleDependentUpperDeviationShiftedExpMoment_add_const`, `localizedPointwiseSampleDependentUpperDeviationShiftedExpMoment_le_fixedExpMoment_div`, `localizedPointwiseUpperDeviationBadEventMass`, `localizedPointwiseUpperDeviationBadEventMass_le_expMoment_div`, `localizedPointwiseUpperDeviationExpMoment`, `localizedPointwiseUpperDeviationExpMoment_finiteProduct_le_of_single`, `localizedSampleDependentHighConfidence_empirical_nonpos`, `localizedSampleDependentHighConfidence_empirical_nonpos_of_shiftedExpMoment`, `localizedSampleDependentUpperDeviationBadEventMass`, `localizedSampleDependentUpperDeviationBadEventMass_le_fixed`, `localizedSampleDependentUpperDeviationBadEventMass_le_sum_pointwise`, `localizedSampleDependentUpperDeviationBadEventMass_le_sum_shiftedExpMoment`, `localizedSampleDependentUpperDeviationBadEventMass_le_sum_tails`, `localizedSampleDependentUpperDeviationEvent`, `localizedSecondMomentEmpiricalRademacherComplexity_le_of_fixedPointCertificate`, `localizedUpperDeviation`, `localizedUpperDeviationBadEventMass`, `localizedUpperDeviationBadEventMass_finiteProduct_le_delta_boundedExcess`, `localizedUpperDeviationBadEventMass_finiteProduct_le_sum_boundedExcess`, `localizedUpperDeviationBadEventMass_le_delta`, `localizedUpperDeviationBadEventMass_le_sum_expMoment_div`, `localizedUpperDeviationBadEventMass_le_sum_pointwise`, `localizedUpperDeviationBadEventMass_le_sum_tails`, `localizedUpperDeviationEvent`, `mcdiarmid_inequality_iid_const_width`, `oneCoordinate_boundedLoss_mgf`, `pacBayesPriorMixture_supermartingale`, `pac_bayes_generalization`, `pacbayes_changeOfMeasure`, `pacbayes_mcallester_deterministic`, `pacbayes_mcallester_sqrt`, `pacbayes_mcallester_subGaussian`, `posteriorGeneralizationGap_le_bernstein_of_priorBernsteinExpMoment_le`, `posteriorMarginVarianceProxy`, `posteriorRisk_bound_of_priorDeviationMGF_le`, `posteriorRisk_bound_of_priorDeviationMGF_le_complexity_sqrt`, `priorAveraged_boundedLoss_mgf`, `priorAveraged_boundedLoss_mgf_badEventMass_le_delta`, `priorBernsteinExpMoment`, `sampleAverage_boundedLoss_mgf`, `stability_genGap_hasBoundedDifferences`, `timeUniformPACBayes_bound`, `timeUniformPACBayes_crossing_bound`, `trainingLoss_hasBoundedDifferences`, `vcPacBayesHybridBridge_for_gcClass`
- **Rademacher** (84): `contraction_1lip`, `contraction_empirical`, `effectiveClass_zeroOneLoss_card_eq_binaryClassTrace`, `effectiveClass_zeroOneLoss_card_le_sauerShelah`, `empiricalRademacherComplexity`, `empiricalRademacherComplexity_contraction_lipschitz`, `empiricalRademacherComplexity_le_massart_effective`, `expected_genGap_le_two_expected_empiricalRademacherComplexity`, `finDiscreteDudleyInstance`, `finDiscreteRademacherProcess`, `finDiscreteRademacherSup`, `finDiscreteRademacherSupAdapter`, `finDiscreteRademacherSup_dudley_m_bound`, `finDiscreteRademacherSup_le_projectedSup`, `finDiscreteRademacherSup_true`, `finDiscreteRademacherValue`, `finDiscreteRademacher_projected_dudley_m_bound`, `finDiscrete_rademacher_mgf_bound`, `genGap_highProb_finiteClass`, `genGap_highProb_rademacher`, `genGap_highProb_vcClass`, `genGap_tail_bound_azuma_explicit`, `genGap_tail_bound_sharp_explicit`, `hasBoundedDifferences_tail_sharp`, `localizedEmpiricalRademacherComplexity_mono`, `localizedEmpiricalRademacherComplexity_nonneg_of_zero`, `localizedExcessRiskEmpiricalRademacherComplexity_le_of_bernstein_fixedPointCertificate`, `localizedExcessRiskEmpiricalRademacherComplexity_le_secondMoment`, `localizedExcessRiskEmpiricalRademacherComplexity_nonneg`, `localizedSecondMomentEmpiricalRademacherComplexity_le_of_fixedPointCertificate`, `massart_finite_class`, `mcdiarmid_of_hasBoundedDifferences_sharp`, `mcdiarmid_of_hasBoundedDifferences_sharp_hetero`, `mcdiarmid_of_hasBoundedDifferences_sharp_hetero_lower`, `mcdiarmid_of_hasBoundedDifferences_sharp_lower`, `mcdiarmid_of_hasBoundedDifferences_sharp_of_hetero`, `one_step_contraction`, `rademacherERMBridge_for_gcClass`, `rademacher_covering_bound`, `rademacher_covering_massart`, `rademacher_two_step_chaining`, `sauerShelah_polynomial_bound`, `twoPointDudleyInstance`, `twoPointRademacherProcess`, `twoPointRademacherSupAdapter`, `twoPointRademacherSup_dudley_m_bound`, `twoPointRademacherSup_le_projectedSup`, `twoPointRademacher_projected_dudley_m_bound`, `twoPoint_rademacher_mgf_bound`, `uniformDeviation_highProb_finiteClass`, `uniformDeviation_highProb_vcClass`, `unitIntervalRademacherLinearProcess_increment_mgf`, `unitIntervalRademacherLinearSupRoundedDyadicGridAdapter`, `unitIntervalRademacherLinearSup_attained`, `unitIntervalRademacherLinearSup_dudley_m0_bound`, `unitIntervalRademacherLinearSup_dudley_m1_bound_constEntropy_eval`, `unitIntervalRademacherLinearSup_dudley_m1_bound_of_entropy`, `unitIntervalRademacherLinearSup_expectation`, `unitIntervalRademacherLinearSup_isLUB_range`, `unitIntervalRademacherLinearSup_isLeastUpperBound`, `unitIntervalRademacherLinearSup_le_projectedRoundedDyadicGridSup`, `unitIntervalRademacherLinearSup_projectedQuarterMesh_dudley_log15_bound`, `unitIntervalRademacherLinearSup_projectedQuarterMesh_dudley_log15_bound_eval`, `unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_log15_bound`, `unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_log15_bound_eval`, `unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m2_bound`, `unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m3_bound`, `unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m_bound`, `unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m_bound_prefixFree`, `unitIntervalRademacherLinearSup_sSup_range`, `unitIntervalRademacherLinearSup_upper`, `unitIntervalRademacherLinear_halfQuarter_increment_log15_bound`, `unitIntervalRademacherLinear_projectedQuarterMesh_dudley_log15_bound`, `unitIntervalRademacherLinear_projectedRoundedDyadicGridSup_eq`, `unitIntervalRademacherLinear_roundedDyadicGrid_dudley_log15_bound`, `unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m2_bound`, `unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m3_bound`, `unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m_bound`, `unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m_bound_prefixFree`, `unitIntervalRoundedDyadicGridNet_dist`, `unitInterval_rademacherLinear_mgf_bound`, `vcRademacher_pointwise`, `vc_erm_excessRisk_tail`, `vc_erm_sample_complexity`
- **VC dimension** (24): `effectiveClass_zeroOneLoss_card_eq_binaryClassTrace`, `effectiveClass_zeroOneLoss_card_le_sauerShelah`, `empiricalRademacherComplexity_le_massart_effective`, `expected_genGap_le_two_expected_empiricalRademacherComplexity`, `genGap_highProb_finiteClass`, `genGap_highProb_rademacher`, `genGap_highProb_vcClass`, `genGap_tail_bound_azuma_explicit`, `genGap_tail_bound_sharp_explicit`, `hasBoundedDifferences_tail_sharp`, `massart_finite_class`, `mcdiarmid_of_hasBoundedDifferences_sharp`, `mcdiarmid_of_hasBoundedDifferences_sharp_hetero`, `mcdiarmid_of_hasBoundedDifferences_sharp_hetero_lower`, `mcdiarmid_of_hasBoundedDifferences_sharp_lower`, `mcdiarmid_of_hasBoundedDifferences_sharp_of_hetero`, `sauerShelah_polynomial_bound`, `uniformDeviation_highProb_finiteClass`, `uniformDeviation_highProb_vcClass`, `vcHoeffdingBridge_for_gcClass`, `vcPacBayesHybridBridge_for_gcClass`, `vcRademacher_pointwise`, `vc_erm_excessRisk_tail`, `vc_erm_sample_complexity`
- **confidence sequence** (48): `FiniteClassConfidenceSequence`, `FiniteClassConfidenceSequence.failure_probability_le`, `anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_confidenceSequence_fromHoeffding`, `anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_namedRadius_exists_fromHoeffding`, `anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_timeVaryingRadius_exists_fromHoeffding`, `anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_timeVaryingRadius_fromHoeffding`, `atTop_time_uniform_confidence_sequence_subGamma_mixture`, `bettingWealth_supermartingale`, `betting_confidence_sequence_of_condMean`, `betting_time_uniform_confidence_sequence`, `condExp_mixture_swap`, `countableWeightedSupermartingale_tsum`, `dyadicEpochMixture_supermartingale`, `dyadic_epoch_confidence_sequence_subGamma`, `dyadic_epoch_two_sided_confidence_sequence`, `eProcess_optionalContinuation`, `eProcess_product_of_supermartingale`, `eProcess_typeI_control`, `empiricalAverageUniformRangeTwoSidedHoeffdingSampleSizeTail_le_of_explicitRadius`, `finiteClassConfidenceSequenceFailureEvent`, `finiteMcAllesterGridPeeling_badEventMass_le_delta`, `finitePrefixFiniteClassDeviationFromHoeffding_unitRange_explicitRadius`, `finitePrefixFiniteClassDeviationFromHoeffding_unitRange_radius`, `fixedGrid_logLog_bridge_forces_exact_boundary`, `literalDyadicEpochWeight_not_summable`, `localizedFastRateHighConfidence_bernstein_fixedPoint_boundedExcess`, `localizedFastRateHighConfidence_bernstein_fixedPoint_of_centeredShiftedExpMoment`, `localizedFastRateHighConfidence_bernstein_fixedPoint_of_shiftedExpMoment`, `localizedFiniteClassBernsteinHighConfidence_empirical_nonpos`, `localizedFiniteClassHighConfidence_empirical_nonpos_boundedExcess`, `localizedSampleDependentHighConfidence_empirical_nonpos`, `localizedSampleDependentHighConfidence_empirical_nonpos_of_shiftedExpMoment`, `mixture_is_supermartingale`, `optimized_lambda_confidence_sequence_subGamma`, `optimized_lambda_two_sided_closed_form_pointwise`, `optimized_lambda_two_sided_confidence_sequence`, `pSeriesDyadicEpochWeight_summable`, `pSeriesDyadicEpochWeight_zero_unitPenalty`, `pacBayesPriorMixture_supermartingale`, `stitched_atTop_crossing_bound`, `subGammaLogLogWidth_add_stitchingPenalty`, `subGammaLogLogWidth_eq_boundary_optTilt`, `subGammaLogLogWidth_loglog_rate`, `subGamma_stitched_boundary_supermartingale`, `timeUniformPACBayes_bound`, `timeUniformPACBayes_crossing_bound`, `zeroOneDyadicFiniteClassConfidenceRadius`, `zeroOneDyadicFiniteClassConfidenceRadius_le_of_sampleSize_ge`
- **covering / chaining** (188): `EpsilonizedSupremumBoundaryChoice`, `FiniteCoverSupremumBoundaryChoice`, `FiniteDyadicDudleyInstance`, `FiniteDyadicDudleyInstance.SupremumAdapter`, `FiniteDyadicDudleyInstance.projected_dudley_bound`, `FiniteDyadicDudleyInstance.suppliedSup_dudley_bound`, `FiniteNet`, `FiniteNet.ProjectedIndex`, `TwoPoint`, `UnitInterval`, `bennett_mgf`, `bennett_mgf_subgamma`, `bennett_tail`, `bennett_taylor_bound`, `dyadicChainingFiniteNetOfTotallyBoundedUniv_pair_radius_le`, `dyadicChainingFiniteNetSequenceOfTotallyBounded`, `exp_le_quadratic_of_le`, `finDiscreteDist`, `finDiscreteDist_nonneg`, `finDiscreteDist_symm`, `finDiscreteDist_triangle`, `finDiscreteDudleyInstance`, `finDiscreteDyadicCoverCount`, `finDiscreteDyadicNet`, `finDiscreteDyadicNetSequence`, `finDiscreteDyadicNet_coverCount_le`, `finDiscreteDyadicNet_coveringNumber`, `finDiscreteDyadicNet_dist`, `finDiscreteRademacherProcess`, `finDiscreteRademacherSup`, `finDiscreteRademacherSupAdapter`, `finDiscreteRademacherSup_dudley_m_bound`, `finDiscreteRademacherSup_le_projectedSup`, `finDiscreteRademacherSup_true`, `finDiscreteRademacherValue`, `finDiscreteRademacher_projected_dudley_m_bound`, `finDiscrete_rademacher_mgf_bound`, `finiteDyadicDudleyInstanceOfTotallyBounded`, `finiteDyadicEntropyAtRadiusUpperSum`, `finiteDyadicEntropyAtRadiusUpperSum_le_two_mul_truncatedIntervalIntegral`, `finiteDyadicEntropyIntegralBudget_le_entropyAtRadiusUpperSum`, `finiteDyadicEntropyIntegralBudget_one_const`, `finiteExpectation_supFunctional_le_projected_add_skeleton_terminalError`, `finiteExpectation_supFunctional_le_projected_add_terminalError`, `finiteMetricCoverOfTotallyBoundedUniv`, `finiteNetOfTotallyBoundedUniv`, `finitePrefixSupEnvelope_const`, `finitePrefixSupEnvelope_eq_self_of_monotone`, `finiteSup_le_skeletonSup_add_of_pointwise_approx`, `finiteSup_skeleton_le_projectedSup_add_terminalError`, `finite_chaining_expectation_bound`, `finite_chaining_expectation_bound_of_net_sequence_coveringNumbers_sqrt`, `finite_chaining_expectation_bound_of_net_sequence_pairs_sqrt`, `finite_chaining_expectation_bound_of_radius_sqrt`, `finite_dudley_entropy_sum_coveringNumbers`, `finite_dudley_entropy_sum_coveringNumbers_geometric_annulus_budget`, `finite_dudley_entropy_sum_coveringNumbers_geometric_entropy_budget`, `finite_dudley_entropy_sum_coveringNumbers_geometric_integral_budget`, `finite_dudley_entropy_sum_coveringNumbers_geometric_integral_budget_prefix_envelope`, `finite_dudley_entropy_sum_coveringNumbers_geometric_radius`, `finite_dudley_entropy_sum_coveringNumbers_geometric_uniform_entropy`, `finite_dudley_entropy_sum_projection_pairs`, `finite_dudley_entropy_sum_projection_pairs_geometric_annulus_budget`, `finite_dudley_entropy_sum_projection_pairs_geometric_entropy_budget`, `finite_dudley_entropy_sum_projection_pairs_geometric_integral_budget`, `finite_dudley_entropy_sum_projection_pairs_geometric_radius`, `finite_dudley_entropy_sum_projection_pairs_geometric_uniform_entropy`, `finite_dudley_entropy_sum_totalBounded_dyadic_coveringNumbers`, `finite_epsilonizedSup_dudley_totalBounded_of_finiteCoverSupremumBoundaryChoice`, `finite_epsilonizedSup_modulus_dudley_totalBounded_dyadic_entropy_truncatedIntervalIntegral_comparison`, `finite_expectedSup_le_of_mgf_log`, `finite_expectedSup_le_of_subGaussian_mgf_sqrt`, `finite_projectedNet_chaining_expectation_bound_of_net_sequence_coveringNumbers_sqrt`, `finite_projectedNet_dudley_entropy_sum_coveringNumbers_geometric_entropy_integral_comparison`, `finite_projectedNet_dudley_entropy_sum_coveringNumbers_geometric_entropy_truncatedIntervalIntegral_comparison`, `finite_projectedNet_dudley_entropy_sum_coveringNumbers_geometric_integral_budget_prefix_envelope`, `finite_projectedNet_dudley_entropy_sum_totalBounded_dyadic_coveringNumbers`, `finite_projectedNet_dudley_entropy_sum_totalBounded_dyadic_entropy_integral_comparison`, `finite_projectedNet_dudley_entropy_sum_totalBounded_dyadic_entropy_truncatedIntervalIntegral_comparison`, `finite_projected_chaining_expectation_bound`, `finite_projected_chaining_expectation_bound_of_net_sequence_coveringNumbers_sqrt`, `finite_projected_dudley_entropy_sum_coveringNumbers_geometric_integral_budget_prefix_envelope`, `finite_projected_dudley_entropy_sum_totalBounded_dyadic_coveringNumbers`, `finite_separableSupFunctional_dudley_entropy_sum_coveringNumbers_geometric_entropy_truncatedIntervalIntegral_comparison`, `finite_separableSupFunctional_dudley_totalBounded_dyadic_entropy_truncatedIntervalIntegral_comparison`, `finite_supFunctional_dudley_entropy_sum_coveringNumbers_geometric_entropy_truncatedIntervalIntegral_comparison`, `finite_supFunctional_dudley_totalBounded_dyadic_entropy_truncatedIntervalIntegral_comparison`, `finite_witnessedSup_modulus_dudley_totalBounded_dyadic_entropy_truncatedIntervalIntegral_comparison`, `monotone_unitIntervalRoundedDyadicGridCoverCount`, `monotone_unitIntervalRoundedDyadicGridEntropy`, `pSeriesDyadicEpochWeight_summable`, `rademacher_covering_bound`, `rademacher_covering_massart`, `rademacher_two_step_chaining`, `shiftedDyadicIntervalIntegralSum_eq_truncatedIntervalIntegral`, `skeletonApprox_of_finiteCover_pathwiseModulus`, `supFunctional_le_skeletonSup_add_of_witnessed_pointwise_approx`, `terminalApprox_of_pathwise_modulus`, `terminalApprox_of_pathwise_modulus_radiusBound`, `twoPointDist_nonneg`, `twoPointDist_symm`, `twoPointDist_triangle`, `twoPointDudleyInstance`, `twoPointDyadicNet`, `twoPointDyadicNetSequence`, `twoPointDyadicNet_coverCount_le`, `twoPointDyadicNet_pair_card_gt_one`, `twoPointDyadicNet_radius_geometric`, `twoPointRademacherProcess`, `twoPointRademacherSupAdapter`, `twoPointRademacherSup_dudley_m_bound`, `twoPointRademacherSup_le_projectedSup`, `twoPointRademacher_projected_dudley_m_bound`, `twoPoint_rademacher_mgf_bound`, `unitIntervalDyadicFiniteNet_covers`, `unitIntervalDyadicGridCenter_leftEndpoint`, `unitIntervalDyadicGridCenter_rightEndpoint`, `unitIntervalDyadicGridFloorProject`, `unitIntervalDyadicGridFloorProject_dist_le`, `unitIntervalDyadicGridNet_coveringNumber`, `unitIntervalDyadicGridNet_coveringNumberPair_zero`, `unitIntervalDyadicGridNet_coveringNumber_one`, `unitIntervalDyadicGridNet_coveringNumber_two`, `unitIntervalDyadicGridNet_covers`, `unitIntervalDyadicGridPairCoverCount_zero`, `unitIntervalDyadicGridRoundProject`, `unitIntervalDyadicGridRoundProject_dist_le`, `unitIntervalDyadicGridRoundProject_one`, `unitIntervalDyadicGridRoundProject_zero`, `unitIntervalDyadicGrid_card`, `unitIntervalDyadicRoundedGridNet_coveringNumber`, `unitIntervalDyadicRoundedGridNet_coveringNumberPair_zero`, `unitIntervalDyadicRoundedGridNet_coveringNumber_one`, `unitIntervalDyadicRoundedGridNet_coveringNumber_two`, `unitIntervalDyadicRoundedGridNet_covers`, `unitIntervalFiniteNet_covers`, `unitIntervalHalfMeshNet_coveringNumber`, `unitIntervalHalfMeshNet_covers`, `unitIntervalHalfQuarterPair_card_gt_one`, `unitIntervalHalfQuarter_coveringNumber_product`, `unitIntervalHalfQuarter_coveringNumber_product_eq_dyadicGridPairCoverCount_zero`, `unitIntervalQuarterMeshNet_coveringNumber`, `unitIntervalQuarterMeshNet_covers`, `unitIntervalRademacherLinearProcess_increment_mgf`, `unitIntervalRademacherLinearSupRoundedDyadicGridAdapter`, `unitIntervalRademacherLinearSup_attained`, `unitIntervalRademacherLinearSup_dudley_m0_bound`, `unitIntervalRademacherLinearSup_dudley_m1_bound_constEntropy_eval`, `unitIntervalRademacherLinearSup_dudley_m1_bound_of_entropy`, `unitIntervalRademacherLinearSup_expectation`, `unitIntervalRademacherLinearSup_isLUB_range`, `unitIntervalRademacherLinearSup_isLeastUpperBound`, `unitIntervalRademacherLinearSup_le_projectedRoundedDyadicGridSup`, `unitIntervalRademacherLinearSup_projectedQuarterMesh_dudley_log15_bound`, `unitIntervalRademacherLinearSup_projectedQuarterMesh_dudley_log15_bound_eval`, `unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_log15_bound`, `unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_log15_bound_eval`, `unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m2_bound`, `unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m3_bound`, `unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m_bound`, `unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m_bound_prefixFree`, `unitIntervalRademacherLinearSup_sSup_range`, `unitIntervalRademacherLinearSup_upper`, `unitIntervalRademacherLinear_halfQuarter_increment_log15_bound`, `unitIntervalRademacherLinear_projectedQuarterMesh_dudley_log15_bound`, `unitIntervalRademacherLinear_projectedRoundedDyadicGridSup_eq`, `unitIntervalRademacherLinear_roundedDyadicGrid_dudley_log15_bound`, `unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m2_bound`, `unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m3_bound`, `unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m_bound`, `unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m_bound_prefixFree`, `unitIntervalRoundedDyadicGridCoverCount`, `unitIntervalRoundedDyadicGridDudleyInstance`, `unitIntervalRoundedDyadicGridEntropy_prefixSup`, `unitIntervalRoundedDyadicGridIndex`, `unitIntervalRoundedDyadicGridNet`, `unitIntervalRoundedDyadicGridNet_coverCount_le`, `unitIntervalRoundedDyadicGridNet_coverCount_le_range`, `unitIntervalRoundedDyadicGridNet_coveringNumber_product`, `unitIntervalRoundedDyadicGridNet_dist`, `unitIntervalRoundedDyadicGridNet_pair_card_gt_one`, `unitIntervalRoundedDyadicGridNet_pair_card_gt_one_range`, `unitIntervalRoundedDyadicGridNet_radius_geometric`, `unitIntervalRoundedDyadicGridNet_radius_geometric_range`, `unitIntervalRoundedDyadicGridNet_radius_pos`, `unitIntervalRoundedDyadicGridNet_radius_pos_range`, `unitInterval_rademacherLinear_mgf_bound`, `unitInterval_totallyBounded_univ`
- **risk** (25): `BernsteinCondition`, `IsERM`, `LocalizedDeviationCertificate`, `empiricalRisk`, `excessRisk`, `finiteCatoni_badEventMass_le_delta`, `finiteEmpiricalRisk`, `finiteExcessRisk_le_of_localizedDeviation_bernstein_fixedPoint`, `finiteExcessRisk_le_of_localizedDeviation_empirical_nonpos`, `finiteExcessRisk_le_of_localizedFastRateUpperDeviationEvent_bernstein_fixedPoint`, `finiteExcessRisk_le_of_localizedSampleDependentUpperDeviationEvent_empirical_nonpos`, `finiteExcessRisk_le_of_localizedUpperDeviationEvent_bernstein_fixedPoint`, `finiteExcessRisk_le_of_localizedUpperDeviationEvent_empirical_nonpos`, `finitePriorAveraged_mgf_empiricalRiskDeviation_le`, `finiteProduct_mgf_empiricalRiskDeviation_eq_pow`, `finiteProduct_mgf_empiricalRiskDeviation_le_of_single`, `localizedExcessRiskEmpiricalRademacherComplexity_le_of_bernstein_fixedPointCertificate`, `localizedExcessRiskEmpiricalRademacherComplexity_le_secondMoment`, `localizedExcessRiskEmpiricalRademacherComplexity_nonneg`, `localizedUpperDeviation`, `pac_bayes_generalization`, `posteriorRisk_bound_of_priorDeviationMGF_le`, `posteriorRisk_bound_of_priorDeviationMGF_le_complexity_sqrt`, `risk`, `vc_erm_excessRisk_tail`
- **sample statistics** (19): `bernoulliHalfCramerRaoWitness`, `bernoulliLogLikelihood_global_argmax_from_count`, `bernoulliScoreAtSampleMean_eq_zero`, `bootstrapMean_eq_sampleMean`, `covariance_score_eq_deriv_mean`, `cramerRao_unbiased`, `gaussianKnownVarianceLogLikelihood_mle`, `hoeffding_mean_tail_twoSided`, `horvitzThompson_design_unbiased`, `sampleMean`, `sampleMean_hoeffding_tail`, `sampleMean_unbiased_finite`, `sampleVariance`, `sampleVarianceBessel`, `sampleVarianceBessel_unbiased_finite`, `sampleVariance_eq_secondMoment_sub_meanSq`, `sampleVariance_nonneg`, `weightedExpectation_linear`, `weightedVariance`
- **stability** (116): `BernsteinCondition`, `FiniteCoordinateSwapIdentity`, `FixedPointUpperCertificate`, `LocalizedDeviationCertificate`, `abs_expectedFiniteGeneralizationGap_le_uniformStability_finiteProduct`, `abs_expectedFiniteGeneralizationGap_le_uniformStability_of_coordinateSwap`, `abs_expectedFiniteStabilityGap_le_uniformStability_finiteProduct`, `abs_expectedFiniteStabilityGap_le_uniformStability_of_coordinateSwap`, `abs_expectedStabilityGap_le_uniformStability_piMeasure_of_boundedLoss`, `averaged_bernstein_tail`, `bennett_mgf`, `bennett_mgf_subgamma`, `bernstein_tail`, `boundedLoss_coordinateSelectedLoss_integrable`, `boundedLoss_selectedLoss_integrable`, `boundedLoss_updateSelectedLoss_integrable`, `bousquet_elisseeff_expectedGap_variant`, `bousquet_elisseeff_expectedGap_variant_of_boundedLoss`, `bousquet_elisseeff_uniform_stability_corollary`, `bousquet_elisseeff_uniform_stability_corollary_of_boundedLoss`, `catoni_fixedLambda_budget_eq_sqrt`, `centeredSecondMoment_le_of_bernstein_localized`, `continuousPriorPosterior_certificate_derived`, `continuous_catoni_changeOfMeasure_bound`, `continuous_donsker_varadhan`, `exp_le_quadratic_of_le`, `expectedFiniteGeneralizationGap_le_uniformStability_finiteProduct`, `expectedFiniteGeneralizationGap_le_uniformStability_of_coordinateSwap`, `expectedFiniteStabilityGap_le_uniformStability_finiteProduct`, `expectedFiniteStabilityGap_le_uniformStability_of_coordinateSwap`, `expectedStabilityGap_le_uniformStability_piMeasure_of_boundedLoss`, `finiteCatoni_badEventMass_le_delta`, `finiteClass_loss_measurable`, `finiteEmpiricalRisk`, `finiteExcessRisk_le_of_localizedDeviation_bernstein_fixedPoint`, `finiteExcessRisk_le_of_localizedDeviation_empirical_nonpos`, `finiteExcessRisk_le_of_localizedFastRateUpperDeviationEvent_bernstein_fixedPoint`, `finiteExcessRisk_le_of_localizedSampleDependentUpperDeviationEvent_empirical_nonpos`, `finiteExcessRisk_le_of_localizedUpperDeviationEvent_bernstein_fixedPoint`, `finiteExcessRisk_le_of_localizedUpperDeviationEvent_empirical_nonpos`, `finiteMcAllesterBoundedComplexity_badEventMass_le_delta`, `finiteMcAllesterGridOptimized_badEventMass_le_delta`, `finiteMcAllesterGridPeeling_badEventMass_le_delta`, `finitePACBayesBernsteinMargin_badEventMass_le_delta`, `finitePACBayesBernsteinPenalty_badEventMass_le_delta`, `finitePACBayesBernstein_fixedLambda_badEventMass_le_delta`, `finitePriorAveraged_mgf_empiricalRiskDeviation_le`, `finiteProductSampleWeight`, `finiteProductSampleWeight_coordinateSwapIdentity`, `finiteProduct_mgf_empiricalRiskDeviation_eq_pow`, `finiteProduct_mgf_empiricalRiskDeviation_le_of_single`, `klDiv_nonneg`, `localizedDeviationCertificate_of_mem_upperDeviationEvent`, `localizedEmpiricalRademacherComplexity_mono`, `localizedEmpiricalRademacherComplexity_nonneg_of_zero`, `localizedExcessRiskEmpiricalRademacherComplexity_le_of_bernstein_fixedPointCertificate`, `localizedExcessRiskEmpiricalRademacherComplexity_le_secondMoment`, `localizedExcessRiskEmpiricalRademacherComplexity_nonneg`, `localizedFastRateHighConfidence_bernstein_fixedPoint_boundedExcess`, `localizedFastRateHighConfidence_bernstein_fixedPoint_of_centeredShiftedExpMoment`, `localizedFastRateHighConfidence_bernstein_fixedPoint_of_shiftedExpMoment`, `localizedFastRatePointwiseShiftedExpMoment_finiteProduct_le_boundedExcess`, `localizedFastRatePointwiseShiftedExpMoment_le_centered_div`, `localizedFastRateUpperDeviationBadEventMass`, `localizedFastRateUpperDeviationBadEventMass_finiteProduct_le_delta_boundedExcess`, `localizedFastRateUpperDeviationBadEventMass_le_fixed_epsilon`, `localizedFastRateUpperDeviationBadEventMass_le_sum_centeredShiftedExpMoment_div`, `localizedFastRateUpperDeviationBadEventMass_le_sum_shiftedExpMoment`, `localizedFastRateUpperDeviationEvent`, `localizedFiniteClassBernsteinHighConfidence_empirical_nonpos`, `localizedFiniteClassHighConfidence_empirical_nonpos_boundedExcess`, `localizedOneCoordinateDeviationMGF_le_of_excessLoss_mem_Icc_neg_one_one`, `localizedPointwiseSampleDependentUpperDeviationBadEventMass`, `localizedPointwiseSampleDependentUpperDeviationBadEventMass_le_shiftedExpMoment`, `localizedPointwiseSampleDependentUpperDeviationShiftedExpMoment`, `localizedPointwiseSampleDependentUpperDeviationShiftedExpMoment_add_const`, `localizedPointwiseSampleDependentUpperDeviationShiftedExpMoment_le_fixedExpMoment_div`, `localizedPointwiseUpperDeviationBadEventMass`, `localizedPointwiseUpperDeviationBadEventMass_le_expMoment_div`, `localizedPointwiseUpperDeviationExpMoment`, `localizedPointwiseUpperDeviationExpMoment_finiteProduct_le_of_single`, `localizedSampleDependentHighConfidence_empirical_nonpos`, `localizedSampleDependentHighConfidence_empirical_nonpos_of_shiftedExpMoment`, `localizedSampleDependentUpperDeviationBadEventMass`, `localizedSampleDependentUpperDeviationBadEventMass_le_fixed`, `localizedSampleDependentUpperDeviationBadEventMass_le_sum_pointwise`, `localizedSampleDependentUpperDeviationBadEventMass_le_sum_shiftedExpMoment`, `localizedSampleDependentUpperDeviationBadEventMass_le_sum_tails`, `localizedSampleDependentUpperDeviationEvent`, `localizedSecondMomentEmpiricalRademacherComplexity_le_of_fixedPointCertificate`, `localizedUpperDeviation`, `localizedUpperDeviationBadEventMass`, `localizedUpperDeviationBadEventMass_finiteProduct_le_delta_boundedExcess`, `localizedUpperDeviationBadEventMass_finiteProduct_le_sum_boundedExcess`, `localizedUpperDeviationBadEventMass_le_delta`, `localizedUpperDeviationBadEventMass_le_sum_expMoment_div`, `localizedUpperDeviationBadEventMass_le_sum_pointwise`, `localizedUpperDeviationBadEventMass_le_sum_tails`, `localizedUpperDeviationEvent`, `mcdiarmid_inequality_iid_const_width`, `oneCoordinate_boundedLoss_mgf`, `pac_bayes_generalization`, `pacbayes_changeOfMeasure`, `pacbayes_mcallester_deterministic`, `pacbayes_mcallester_sqrt`, `pacbayes_mcallester_subGaussian`, `posteriorGeneralizationGap_le_bernstein_of_priorBernsteinExpMoment_le`, `posteriorMarginVarianceProxy`, `posteriorRisk_bound_of_priorDeviationMGF_le`, `posteriorRisk_bound_of_priorDeviationMGF_le_complexity_sqrt`, `priorAveraged_boundedLoss_mgf`, `priorAveraged_boundedLoss_mgf_badEventMass_le_delta`, `priorBernsteinExpMoment`, `sampleAverage_boundedLoss_mgf`, `stability_genGap_hasBoundedDifferences`, `trainingLoss_hasBoundedDifferences`
- **sub-Gamma** (19): `atTop_time_uniform_confidence_sequence_subGamma_mixture`, `bennett_mgf_subgamma`, `bennett_tail`, `bennett_taylor_bound`, `condExp_mul_bounded_left`, `condExp_sq_eq_condVar_of_centered`, `condJensen_real`, `condSubGammaMGF_of_bounded_centered_condVariance`, `cond_markov_of_nonneg`, `dyadicEpochMixture_supermartingale`, `dyadic_epoch_confidence_sequence_subGamma`, `integrable_exp_mul_of_bounded`, `mixture_is_supermartingale`, `optimized_lambda_confidence_sequence_subGamma`, `stitched_atTop_crossing_bound`, `subGammaLogLogWidth_add_stitchingPenalty`, `subGammaLogLogWidth_eq_boundary_optTilt`, `subGammaLogLogWidth_loglog_rate`, `subGamma_stitched_boundary_supermartingale`
- **sub-Gaussian** (10): `chernoff_tail`, `finDiscreteRademacherProcess`, `finDiscrete_rademacher_mgf_bound`, `finite_expectedSup_le_of_subGaussian_mgf_sqrt`, `pacbayes_mcallester_subGaussian`, `subGaussianMGF_tail_twoSided`, `twoPointRademacherProcess`, `twoPoint_rademacher_mgf_bound`, `unitIntervalRademacherLinearProcess_increment_mgf`, `unitInterval_rademacherLinear_mgf_bound`
- **tail bound** (36): `averaged_bernstein_tail`, `bennett_tail`, `bernoulli_bernstein_tail`, `bernstein_tail`, `chernoff_tail`, `empiricalAverageLowerHoeffdingTail`, `empiricalAverageTwoSidedHoeffdingTail`, `empiricalAverageTwoSidedHoeffdingTail_le_uniformRangeTwoSidedHoeffdingTail`, `empiricalAverageTwoSidedHoeffdingTail_le_uniformRangeTwoSidedHoeffdingTail_of_rangeBound`, `empiricalAverageTwoSidedHoeffdingTail_le_uniformRangeTwoSidedHoeffdingTail_of_rangeBound_of_exists_range_pos`, `empiricalAverageUniformRangeTwoSidedHoeffdingSampleSizeTail`, `empiricalAverageUniformRangeTwoSidedHoeffdingSampleSizeTail_le_of_explicitRadius`, `empiricalAverageUniformRangeTwoSidedHoeffdingSampleSizeTail_le_of_logBudget`, `empiricalAverageUniformRangeTwoSidedHoeffdingSampleSizeTail_le_of_sampleSize_ge`, `empiricalAverageUniformRangeTwoSidedHoeffdingTail`, `empiricalAverageUniformRangeTwoSidedHoeffdingTail_eq_sampleSizeTail`, `empiricalAverageUpperHoeffdingTail`, `empiricalAverageUpperHoeffdingTail_eq_lower`, `finiteClassUniformDeviationUnionBound`, `genGap_highProb_vcClass`, `genGap_tail_bound_azuma_explicit`, `genGap_tail_bound_sharp_explicit`, `hasBoundedDifferences_tail_sharp`, `hoeffding_mean_tail_twoSided`, `localizedFiniteClassBernsteinHighConfidence_empirical_nonpos`, `localizedSampleDependentUpperDeviationBadEventMass_le_sum_tails`, `localizedUpperDeviationBadEventMass_le_delta`, `localizedUpperDeviationBadEventMass_le_sum_tails`, `mcdiarmid_inequality_iid_const_width`, `mcdiarmid_of_hasBoundedDifferences_sharp`, `mcdiarmid_of_hasBoundedDifferences_sharp_hetero`, `mcdiarmid_of_hasBoundedDifferences_sharp_hetero_lower`, `mcdiarmid_of_hasBoundedDifferences_sharp_lower`, `sampleMean_hoeffding_tail`, `subGaussianMGF_tail_twoSided`, `vc_erm_excessRisk_tail`
- **union bound** (23): `countableTimeClassTwoSidedUniformDeviationUnionBound_dyadicBudget_threshold`, `countableTimeClassUnionBound_dyadicBudget`, `countableTimeClassUnionBound_timeBudget`, `finiteClassTwoSidedUniformDeviationUnionBound`, `finiteClassTwoSidedUniformDeviationUnionBound_cardInv`, `finiteClassUniformDeviationUnionBound`, `finiteClassUniformDeviationUnionBound_cardInv`, `finiteMeasureUnionBound`, `finiteMeasureUnionBound_budget`, `finiteMeasureUnionBound_cardInv`, `finiteMeasureUnionBound_const`, `finiteMeasureUnionBound_equalBudget`, `finiteTimeClassTwoSidedUniformDeviationUnionBound_cardInv`, `finiteTimeClassTwoSidedUniformDeviationUnionBound_dyadicBudget`, `finiteTimeClassTwoSidedUniformDeviationUnionBound_dyadicBudget_threshold`, `finiteTimeClassTwoSidedUniformDeviationUnionBound_timeBudget`, `finiteTimeClassTwoSidedUniformDeviationUnionBound_timeBudget_threshold`, `finiteTimeClassTwoSidedUnionBoundFromOneSidedTails_dyadicBudget`, `finiteTimeClassUnionBound_cardInv`, `finiteTimeClassUnionBound_dyadicBudget`, `finiteTimeClassUnionBound_timeBudget`, `localizedFastRateUpperDeviationBadEventMass_le_sum_centeredShiftedExpMoment_div`, `localizedUpperDeviationBadEventMass_le_sum_pointwise`

## All declarations

| Concept(s) | Declaration | Kind | Location | Role |
|---|---|---|---|---|
| sub-Gamma, confidence sequence, ERM | `atTop_time_uniform_confidence_sequence_subGamma_mixture` | theorem | `FormalSLT/AnytimeValid/MixtureCS.lean:293` | Time-uniform mixture confidence sequence from the sub-Gamma exponential supermartingale |
| confidence sequence, ERM | `bettingWealth_supermartingale` | theorem | `FormalSLT/AnytimeValid/BettingCS.lean:144` | Betting wealth from predictable bets under the conditional-mean null is a nonnegative supermartingale |
| confidence sequence | `betting_confidence_sequence_of_condMean` | theorem | `FormalSLT/AnytimeValid/BettingCS.lean:242` | End-to-end betting confidence sequence for a bounded mean from predictable bets and the conditional-mean null |
| confidence sequence | `betting_time_uniform_confidence_sequence` | theorem | `FormalSLT/AnytimeValid/BettingCS.lean:203` | Countable-time Ville confidence sequence for the betting wealth e-process |
| confidence sequence | `condExp_mixture_swap` | theorem | `FormalSLT/AnytimeValid/MixtureCS.lean:84` | Conditional-expectation swap for the mixture exponential process |
| confidence sequence, ERM | `countableWeightedSupermartingale_tsum` | theorem | `FormalSLT/AnytimeValid/DyadicEpochCS.lean:124` | Weighted countable sums of real supermartingales are supermartingales under the domination hypothesis, the countable analogue of supermartingale_finset_sum |
| sub-Gamma, confidence sequence, ERM | `dyadicEpochMixture_supermartingale` | theorem | `FormalSLT/AnytimeValid/DyadicEpochCS.lean:283` | The p-series dyadic-epoch mixture of stitched sub-Gamma exponential processes is a nonnegative supermartingale |
| sub-Gamma, confidence sequence | `dyadic_epoch_confidence_sequence_subGamma` | theorem | `FormalSLT/AnytimeValid/DyadicEpochCS.lean:425` | One-sided all-n dyadic-epoch sub-Gamma confidence sequence with the explicit grid budget |
| confidence sequence | `dyadic_epoch_two_sided_confidence_sequence` | theorem | `FormalSLT/AnytimeValid/DyadicEpochCS.lean:489` | Two-sided all-n dyadic-epoch confidence sequence via the X/-X transfer and the explicit stitching penalty |
| confidence sequence | `eProcess_optionalContinuation` | theorem | `FormalSLT/AnytimeValid/EProcess.lean:183` | Optional continuation: the stopped value of an e-process keeps integral at most one |
| confidence sequence, ERM | `eProcess_product_of_supermartingale` | theorem | `FormalSLT/AnytimeValid/EProcess.lean:162` | Product of nonnegative supermartingale factors with unit start is an e-process |
| confidence sequence | `eProcess_typeI_control` | theorem | `FormalSLT/AnytimeValid/EProcess.lean:131` | Safe-testing Type-I control: an e-process rejection event has mass at most the level α over the Ville maximal inequality |
| confidence sequence | `fixedGrid_logLog_bridge_forces_exact_boundary` | theorem | `FormalSLT/AnytimeValid/OptimizedLambdaCS.lean:679` | Obstruction: a fixed finite-grid all-time closed-form bridge forces the grid to attain the exact per-time optimal boundary |
| confidence sequence | `literalDyadicEpochWeight_not_summable` | theorem | `FormalSLT/AnytimeValid/DyadicEpochCS.lean:60` | Obstruction: the literal harmonic dyadic-epoch weights are not summable, ruling out the naive all-n epoch mixture |
| sub-Gamma, confidence sequence, ERM | `mixture_is_supermartingale` | theorem | `FormalSLT/AnytimeValid/MixtureCS.lean:230` | Mixture of sub-Gamma exponential processes is a nonnegative supermartingale |
| sub-Gamma, confidence sequence | `optimized_lambda_confidence_sequence_subGamma` | theorem | `FormalSLT/AnytimeValid/OptimizedLambdaCS.lean:373` | Optimized-λ sub-Gamma confidence sequence with the stitched boundary |
| confidence sequence | `optimized_lambda_two_sided_closed_form_pointwise` | theorem | `FormalSLT/AnytimeValid/OptimizedLambdaCS.lean:859` | Closed-form pointwise interval-width form of the two-sided optimized-λ confidence sequence |
| confidence sequence, ERM | `optimized_lambda_two_sided_confidence_sequence` | theorem | `FormalSLT/AnytimeValid/OptimizedLambdaCS.lean:752` | Two-sided optimized-λ iterated-log confidence sequence via the deterministic stitching bridge and the X/-X transfer |
| confidence sequence, covering / chaining | `pSeriesDyadicEpochWeight_summable` | theorem | `FormalSLT/AnytimeValid/DyadicEpochCS.lean:79` | The redirected p-series dyadic-epoch weights are summable, recovering a finite epoch-capital budget |
| confidence sequence | `pSeriesDyadicEpochWeight_zero_unitPenalty` | theorem | `FormalSLT/AnytimeValid/DyadicEpochCS.lean:107` | The concrete unit-capital stitching penalty for the first p-series epoch is log 2 |
| confidence sequence, PAC-Bayes, ERM | `pacBayesPriorMixture_supermartingale` | theorem | `FormalSLT/PACBayes/TimeUniformPACBayes.lean:99` | Prior mixture of per-hypothesis fixed-tilt exponential processes is a nonnegative supermartingale |
| sub-Gamma, confidence sequence | `stitched_atTop_crossing_bound` | theorem | `FormalSLT/AnytimeValid/OptimizedLambdaCS.lean:247` | Ville crossing bound for the stitched sub-Gamma boundary |
| sub-Gamma, confidence sequence | `subGammaLogLogWidth_add_stitchingPenalty` | theorem | `FormalSLT/AnytimeValid/DyadicEpochCS.lean:261` | The all-n dyadic-epoch boundary is the log-log width plus the explicit per-epoch stitching penalty |
| sub-Gamma, confidence sequence | `subGammaLogLogWidth_eq_boundary_optTilt` | theorem | `FormalSLT/AnytimeValid/OptimizedLambdaCS.lean:590` | The closed-form log-log width equals the sub-Gamma boundary at the per-time optimal tilt |
| sub-Gamma, confidence sequence | `subGammaLogLogWidth_loglog_rate` | theorem | `FormalSLT/AnytimeValid/OptimizedLambdaCS.lean:430` | Stitched boundary half-width grows at the iterated-logarithm rate |
| sub-Gamma, confidence sequence, ERM | `subGamma_stitched_boundary_supermartingale` | theorem | `FormalSLT/AnytimeValid/OptimizedLambdaCS.lean:198` | Stitched-over-λ sub-Gamma exponential process is a nonnegative supermartingale |
| confidence sequence, PAC-Bayes | `timeUniformPACBayes_bound` | theorem | `FormalSLT/PACBayes/TimeUniformPACBayes.lean:309` | Process-level time-uniform PAC-Bayes bound: with probability at least 1 - δ, the posterior running mean of the abstract martingale-difference process stays under the cgf/KL/log(1/δ) boundary for every n ≥ 1 |
| confidence sequence, PAC-Bayes | `timeUniformPACBayes_crossing_bound` | theorem | `FormalSLT/PACBayes/TimeUniformPACBayes.lean:144` | Ville crossing bound for the prior-mixture process over all times |
| sample statistics, Bernoulli | `bernoulliLogLikelihood_global_argmax_from_count` | theorem | `FormalSLT/Statistics/ClassicalEstimation.lean:390` | Sample mean is the global Bernoulli log-likelihood maximizer |
| sample statistics, Bernoulli | `bernoulliScoreAtSampleMean_eq_zero` | theorem | `FormalSLT/Statistics/ClassicalEstimation.lean:364` | Bernoulli log-likelihood score vanishes at the sample-mean MLE |
| sample statistics | `bootstrapMean_eq_sampleMean` | theorem | `FormalSLT/Statistics/ClassicalEstimation.lean:596` | Bootstrap-resample mean equals the sample mean |
| sample statistics | `gaussianKnownVarianceLogLikelihood_mle` | theorem | `FormalSLT/Statistics/ClassicalEstimation.lean:501` | Sample mean is the known-variance Gaussian MLE |
| sample statistics | `horvitzThompson_design_unbiased` | theorem | `FormalSLT/Statistics/ClassicalEstimation.lean:554` | Horvitz-Thompson estimator is design-unbiased for the finite-population total |
| sample statistics | `sampleMean_unbiased_finite` | theorem | `FormalSLT/Statistics/ClassicalEstimation.lean:228` | Sample mean is unbiased for the finite population mean |
| sample statistics | `sampleVarianceBessel` | theorem | `FormalSLT/Statistics/ClassicalEstimation.lean:260` | Bessel-corrected sample variance (1/(n-1)) ∑ (x i - x̄)² |
| sample statistics | `sampleVarianceBessel_unbiased_finite` | theorem | `FormalSLT/Statistics/ClassicalEstimation.lean:299` | Bessel-corrected sample variance is unbiased for the finite-population variance |
|  | `weightedExpectation` | theorem | `FormalSLT/Statistics/ClassicalEstimation.lean:35` | Finite weighted expectation ∑ w x · X x, the population-mean primitive |
| sample statistics | `weightedExpectation_linear` | theorem | `FormalSLT/Statistics/ClassicalEstimation.lean:86` | Linearity of the weighted expectation in the estimator |
| Bennett, sub-Gamma, covering / chaining | `bennett_taylor_bound` | theorem | `FormalSLT/Concentration/SubGamma/BennettBound.lean:196` | Pointwise Bennett Taylor bound for bounded increments in the regime b * λ < 3 |
| sub-Gamma | `condExp_mul_bounded_left` | theorem | `FormalSLT/Concentration/SubGamma/CondExpProduct.lean:33` | Pulls a bounded measurable factor through conditional expectation under the stated integrability hypotheses |
| sub-Gamma | `condExp_sq_eq_condVar_of_centered` | theorem | `FormalSLT/Concentration/SubGamma/CondVarianceFromSquare.lean:40` | Under conditional centering, the conditional second moment is the conditional variance proxy |
| sub-Gamma | `condJensen_real` | theorem | `FormalSLT/Concentration/SubGamma/CondJensen.lean:40` | Conditional Jensen inequality for real-valued conditional expectations |
| sub-Gamma, MGF | `condSubGammaMGF_of_bounded_centered_condVariance` | theorem | `FormalSLT/Concentration/SubGamma/Extractor.lean:52` | Boundedness, conditional centering, and a conditional second-moment proxy imply a conditional sub-Gamma MGF bound |
| Markov, sub-Gamma | `cond_markov_of_nonneg` | theorem | `FormalSLT/Concentration/SubGamma/CondMarkov.lean:48` | Conditional Markov-style inequality for nonnegative real functions |
| sub-Gamma | `integrable_exp_mul_of_bounded` | theorem | `FormalSLT/Concentration/SubGamma/BoundedExpIntegrable.lean:27` | Bounded real increments have integrable exponential tilts under a finite measure |
| Rademacher | `contraction_1lip` | theorem | `FormalSLT/Rademacher/Contraction.lean:357` | Finite-sample scalar contraction for 1-Lipschitz transforms |
| Rademacher | `contraction_empirical` | theorem | `FormalSLT/Rademacher/Contraction.lean:454` | Empirical Rademacher wrapper for 1-Lipschitz transforms |
| Rademacher | `empiricalRademacherComplexity_contraction_lipschitz` | theorem | `FormalSLT/Rademacher/Contraction.lean:477` | Rad_S(φ ∘ F) <= L * Rad_S(F) for finite scalar classes |
| Rademacher | `one_step_contraction` | theorem | `FormalSLT/Rademacher/Contraction.lean:136` | One coordinate replacement step for the finite contraction proof |
| covering / chaining | `FiniteNet` | definition | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:66` | Finite net with an explicit nearest projection |
| ERM, risk | `IsERM` | definition | `FormalSLT/ERM.lean:52` | Predicate selecting empirical risk minimizers over a finite class |
|  | `binaryClassTrace` | definition | `FormalSLT/VC/PACBridge.lean:58` | Binary label patterns realized on a sample |
|  | `effectiveClass` | definition | `FormalSLT/VC/Rademacher.lean:45` | Distinct loss vectors realized on a sample |
| Rademacher | `empiricalRademacherComplexity` | definition | `FormalSLT/Rademacher/FiniteSample.lean:173` | Finite-sample empirical Rademacher complexity |
| ERM, risk | `empiricalRisk` | definition | `FormalSLT/Risk.lean:49` | Sample average loss |
| ERM, risk | `excessRisk` | definition | `FormalSLT/ERM.lean` | Risk above the best-in-class comparator |
| ERM | `genGap` | definition | `FormalSLT/GhostSample.lean:185` | One-sided uniform generalization gap |
|  | `piMeasure` | definition | `FormalSLT/GhostSample.lean:69` | IID product measure on Fin n -> Z |
| risk | `risk` | definition | `FormalSLT/Risk.lean:42` | Expected loss under a measure |
| covering / chaining, ERM | `EpsilonizedSupremumBoundaryChoice` | theorem | `FormalSLT/Covering/TotalBoundedDudley.lean:2079` | Finite skeleton and terminal-scale certificate for an epsilonized Dudley boundary step |
| covering / chaining | `FiniteCoverSupremumBoundaryChoice` | theorem | `FormalSLT/Covering/TotalBoundedDudley.lean:2345` | Finite-cover/pathwise-modulus certificate for the epsilonized Dudley boundary step |
| covering / chaining | `FiniteDyadicDudleyInstance` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:4573` | Packaged reusable finite dyadic Dudley instance: net sequence, coarse budget, variance positivity, and coarse projected-supremum bound |
| covering / chaining, ERM | `FiniteDyadicDudleyInstance.SupremumAdapter` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:4592` | Optional supplied-supremum adapter to a terminal projected finite-net supremum plus explicit terminal error |
| covering / chaining | `FiniteDyadicDudleyInstance.projected_dudley_bound` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:4607` | Projected finite-net Dudley bound from a packaged finite dyadic Dudley instance |
| covering / chaining | `FiniteDyadicDudleyInstance.suppliedSup_dudley_bound` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:4626` | Supplied-supremum finite Dudley bound from a packaged instance and adapter |
| covering / chaining | `FiniteNet.ProjectedIndex` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:103` | Finite image of a net projection, used to avoid a finite ambient index assumption |
| covering / chaining | `dyadicChainingFiniteNetOfTotallyBoundedUniv_pair_radius_le` | theorem | `FormalSLT/Covering/TotalBoundedDudley.lean:276` | Dyadic total-bounded net schedule satisfies the adjacent-radius budget used by finite chaining |
| covering / chaining | `dyadicChainingFiniteNetSequenceOfTotallyBounded` | theorem | `FormalSLT/Covering/TotalBoundedDudley.lean:614` | Packages the total-bounded dyadic net schedule as a FiniteDyadicNetSequence under global projection-pair hypotheses |
| covering / chaining | `finiteDyadicDudleyInstanceOfTotallyBounded` | theorem | `FormalSLT/Covering/TotalBoundedDudley.lean:667` | Packages the total-bounded dyadic net schedule as a FiniteDyadicDudleyInstance when global coarse-budget and projection-pair hypotheses are available |
| covering / chaining | `finiteDyadicEntropyAtRadiusUpperSum` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:3173` | Finite dyadic entropy-at-radius upper sum sampled at lower annulus endpoints |
| covering / chaining | `finiteDyadicEntropyAtRadiusUpperSum_le_two_mul_truncatedIntervalIntegral` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:3346` | Finite entropy-at-radius upper sum dominated by a single truncated interval integral |
| covering / chaining | `finiteDyadicEntropyIntegralBudget_le_entropyAtRadiusUpperSum` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:3414` | Finite dyadic budget comparison to an entropy-at-radius upper sum |
| covering / chaining | `finiteDyadicEntropyIntegralBudget_one_const` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:3159` | One-step dyadic entropy budget for a constant entropy envelope |
| covering / chaining, ERM | `finiteExpectation_supFunctional_le_projected_add_skeleton_terminalError` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:465` | Expected supplied supremum controlled through explicit finite-skeleton and terminal-projection errors |
| covering / chaining, ERM | `finiteExpectation_supFunctional_le_projected_add_terminalError` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:368` | Finite expectation adapter from a supplied supremum functional to a projected finite-supremum surrogate |
| covering / chaining | `finiteMetricCoverOfTotallyBoundedUniv` | theorem | `FormalSLT/Covering/TotalBoundedDudley.lean:136` | Totally bounded metric spaces admit finite covers at every positive real radius |
| covering / chaining | `finiteNetOfTotallyBoundedUniv` | theorem | `FormalSLT/Covering/TotalBoundedDudley.lean:152` | Extracts the repo's bundled finite-net record from total boundedness |
| covering / chaining | `finitePrefixSupEnvelope_const` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:3373` | Constant scale budgets remain constant under the finite prefix-sup envelope |
| covering / chaining | `finitePrefixSupEnvelope_eq_self_of_monotone` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:3386` | Monotone scale budgets equal their finite prefix-sup envelope |
| covering / chaining | `finiteSup_le_skeletonSup_add_of_pointwise_approx` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:538` | Finite ambient supremum controlled by a finite skeleton under pointwise approximation |
| covering / chaining, ERM | `finiteSup_skeleton_le_projectedSup_add_terminalError` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:398` | Finite skeleton supremum controlled by terminal projected finite-net supremum plus explicit error |
| covering / chaining | `finite_chaining_expectation_bound` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:1006` | Finite multiscale chaining decomposition in expectation |
| covering / chaining | `finite_chaining_expectation_bound_of_net_sequence_coveringNumbers_sqrt` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:2184` | Covering-number version for finite net sequences |
| covering / chaining | `finite_chaining_expectation_bound_of_net_sequence_pairs_sqrt` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:2068` | Projection-pair entropy version for finite net sequences |
| covering / chaining | `finite_chaining_expectation_bound_of_radius_sqrt` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:1539` | Radius-bounded finite chaining with square-root entropy budgets |
| covering / chaining | `finite_dudley_entropy_sum_coveringNumbers` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:2742` | Finite Dudley-style entropy sum with covering-number products |
| covering / chaining | `finite_dudley_entropy_sum_coveringNumbers_geometric_annulus_budget` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:3648` | Finite dyadic annulus-budget bridge for covering numbers |
| covering / chaining | `finite_dudley_entropy_sum_coveringNumbers_geometric_entropy_budget` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:3003` | Per-scale entropy-budget wrapper for covering numbers |
| covering / chaining | `finite_dudley_entropy_sum_coveringNumbers_geometric_integral_budget` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:3761` | Finite dyadic entropy-integral budget for covering numbers |
| covering / chaining | `finite_dudley_entropy_sum_coveringNumbers_geometric_integral_budget_prefix_envelope` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:3811` | Finite covering-count wrapper with a monotone prefix-sup entropy envelope |
| covering / chaining | `finite_dudley_entropy_sum_coveringNumbers_geometric_radius` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:2879` | Dyadic/geometric radius schedule for covering numbers |
| covering / chaining | `finite_dudley_entropy_sum_coveringNumbers_geometric_uniform_entropy` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:3517` | Uniform entropy cap collapses the dyadic covering-number sum to a 2 * radiusScale budget |
| covering / chaining | `finite_dudley_entropy_sum_projection_pairs` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:2663` | Finite Dudley-style entropy sum over projection-pair families |
| covering / chaining | `finite_dudley_entropy_sum_projection_pairs_geometric_annulus_budget` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:3584` | Finite dyadic annulus-budget bridge for projection pairs |
| covering / chaining | `finite_dudley_entropy_sum_projection_pairs_geometric_entropy_budget` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:2939` | Per-scale entropy-budget wrapper for projection pairs |
| covering / chaining | `finite_dudley_entropy_sum_projection_pairs_geometric_integral_budget` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:3715` | Finite dyadic entropy-integral budget for projection pairs |
| covering / chaining | `finite_dudley_entropy_sum_projection_pairs_geometric_radius` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:2818` | Dyadic/geometric radius schedule for projection pairs |
| covering / chaining | `finite_dudley_entropy_sum_projection_pairs_geometric_uniform_entropy` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:3450` | Uniform entropy cap collapses the dyadic sum to a 2 * radiusScale budget for projection pairs |
| covering / chaining, ERM | `finite_dudley_entropy_sum_totalBounded_dyadic_coveringNumbers` | theorem | `FormalSLT/Covering/TotalBoundedDudley.lean:3742` | Finite-terminal total-bounded dyadic wrapper composed with the finite Dudley entropy-budget theorem |
| covering / chaining | `finite_epsilonizedSup_dudley_totalBounded_of_finiteCoverSupremumBoundaryChoice` | theorem | `FormalSLT/Covering/TotalBoundedDudley.lean:2499` | Epsilonized total-bounded Dudley wrapper from finite-cover and pathwise-modulus certificates |
| covering / chaining, ERM | `finite_epsilonizedSup_modulus_dudley_totalBounded_dyadic_entropy_truncatedIntervalIntegral_comparison` | theorem | `FormalSLT/Covering/TotalBoundedDudley.lean:2190` | For every positive error budget, a finite skeleton/terminal-scale certificate yields a Dudley bound with + eta |
| MGF, covering / chaining | `finite_expectedSup_le_of_mgf_log` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:752` | MGF control gives finite expected-sup entropy budget |
| sub-Gaussian, MGF, covering / chaining | `finite_expectedSup_le_of_subGaussian_mgf_sqrt` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:847` | Optimized finite sub-Gaussian max bound |
| covering / chaining | `finite_projectedNet_chaining_expectation_bound_of_net_sequence_coveringNumbers_sqrt` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:2452` | Projected finite-net-image chaining bound without [Fintype T] |
| covering / chaining | `finite_projectedNet_dudley_entropy_sum_coveringNumbers_geometric_entropy_integral_comparison` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:4655` | Projected finite-net Dudley wrapper compared to a supplied finite entropy-at-radius integral budget |
| covering / chaining | `finite_projectedNet_dudley_entropy_sum_coveringNumbers_geometric_entropy_truncatedIntervalIntegral_comparison` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:4801` | Projected finite-net Dudley wrapper with a truncated interval-integral entropy budget |
| covering / chaining | `finite_projectedNet_dudley_entropy_sum_coveringNumbers_geometric_integral_budget_prefix_envelope` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:4064` | Projected finite-net-image Dudley wrapper without [Fintype T] |
| covering / chaining, ERM | `finite_projectedNet_dudley_entropy_sum_totalBounded_dyadic_coveringNumbers` | theorem | `FormalSLT/Covering/TotalBoundedDudley.lean:715` | Total-bounded dyadic wrapper over the terminal projected finite-net image, without [Fintype T] |
| covering / chaining | `finite_projectedNet_dudley_entropy_sum_totalBounded_dyadic_entropy_integral_comparison` | theorem | `FormalSLT/Covering/TotalBoundedDudley.lean:889` | Total-bounded projected finite-net wrapper compared to a supplied finite entropy-at-radius integral budget |
| covering / chaining | `finite_projectedNet_dudley_entropy_sum_totalBounded_dyadic_entropy_truncatedIntervalIntegral_comparison` | theorem | `FormalSLT/Covering/TotalBoundedDudley.lean:1100` | Total-bounded projected finite-net wrapper with one truncated interval-integral entropy budget |
| covering / chaining, ERM | `finite_projected_chaining_expectation_bound` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:1070` | Finite projected-supremum chaining without an identity terminal projection |
| covering / chaining | `finite_projected_chaining_expectation_bound_of_net_sequence_coveringNumbers_sqrt` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:2277` | Projected finite-net chaining bound with covering-number entropy budgets |
| covering / chaining | `finite_projected_dudley_entropy_sum_coveringNumbers_geometric_integral_budget_prefix_envelope` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:3875` | Projected finite Dudley wrapper with a monotone prefix-sup entropy envelope |
| covering / chaining, ERM | `finite_projected_dudley_entropy_sum_totalBounded_dyadic_coveringNumbers` | theorem | `FormalSLT/Covering/TotalBoundedDudley.lean:3476` | Total-bounded dyadic wrapper for the terminal projected supremum, without an identity terminal net |
| covering / chaining, ERM | `finite_separableSupFunctional_dudley_entropy_sum_coveringNumbers_geometric_entropy_truncatedIntervalIntegral_comparison` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:5132` | Boundary-layer finite Dudley wrapper with explicit finite-skeleton and terminal-projection hypotheses |
| covering / chaining, ERM | `finite_separableSupFunctional_dudley_totalBounded_dyadic_entropy_truncatedIntervalIntegral_comparison` | theorem | `FormalSLT/Covering/TotalBoundedDudley.lean:1593` | Total-bounded boundary wrapper with explicit finite-skeleton/dense-net and terminal-projection assumptions |
| covering / chaining, ERM | `finite_supFunctional_dudley_entropy_sum_coveringNumbers_geometric_entropy_truncatedIntervalIntegral_comparison` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:5046` | Boundary-layer finite Dudley wrapper for a supplied supremum functional plus terminal error |
| covering / chaining, ERM | `finite_supFunctional_dudley_totalBounded_dyadic_entropy_truncatedIntervalIntegral_comparison` | theorem | `FormalSLT/Covering/TotalBoundedDudley.lean:1476` | Total-bounded boundary wrapper for a supplied supremum functional under explicit terminal approximation |
| covering / chaining | `finite_witnessedSup_modulus_dudley_totalBounded_dyadic_entropy_truncatedIntervalIntegral_comparison` | theorem | `FormalSLT/Covering/TotalBoundedDudley.lean:1915` | Total-bounded Dudley boundary wrapper using approximate witnesses, finite skeleton selectors, and pathwise modulus |
| Rademacher, covering / chaining | `rademacher_covering_bound` | theorem | `FormalSLT/Covering/Rademacher.lean:52` | Rad(F) <= ε + Rad(N_ε) |
| Rademacher, covering / chaining | `rademacher_covering_massart` | theorem | `FormalSLT/Covering/Rademacher.lean:130` | Covering plus Massart |
| Rademacher, covering / chaining | `rademacher_two_step_chaining` | theorem | `FormalSLT/Covering/DudleyChaining.lean:43` | Two-scale finite chaining bound |
| covering / chaining | `shiftedDyadicIntervalIntegralSum_eq_truncatedIntervalIntegral` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:3297` | Shifted finite dyadic annulus integrals compose into one truncated interval integral |
| covering / chaining | `skeletonApprox_of_finiteCover_pathwiseModulus` | theorem | `FormalSLT/Covering/TotalBoundedDudley.lean:2316` | Finite-cover radius plus pathwise modulus gives the finite-skeleton approximation hypothesis |
| covering / chaining | `supFunctional_le_skeletonSup_add_of_witnessed_pointwise_approx` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:569` | Supplied supremum functional controlled by an approximate witness and finite skeleton selector |
| covering / chaining, ERM | `terminalApprox_of_pathwise_modulus` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:500` | Terminal net radius plus pathwise modulus discharges the terminal-projection approximation hypothesis |
| covering / chaining, ERM | `terminalApprox_of_pathwise_modulus_radiusBound` | theorem | `FormalSLT/Covering/FiniteSubGaussianChaining.lean:517` | Radius-bound variant of terminal pathwise-modulus approximation |
| Bernoulli | `bernoulliMean_eq` | theorem | `FormalSLT/Statistics/Bernoulli.lean:74` | Bernoulli mean equals p |
| Bernoulli | `bernoulliPMF` | theorem | `FormalSLT/Statistics/Bernoulli.lean:41` | Bernoulli(p) probability mass function on Bool |
| Bernoulli | `bernoulliVariance_eq` | theorem | `FormalSLT/Statistics/Bernoulli.lean:79` | Bernoulli variance equals p(1 - p) |
| Bernstein, tail bound, Bernoulli | `bernoulli_bernstein_tail` | theorem | `FormalSLT/Statistics/Bernoulli.lean:121` | Two-sided Bernstein tail specialized to Bernoulli(p) |
| sample statistics | `sampleMean` | theorem | `FormalSLT/Statistics/SampleStatistics.lean:41` | Sample mean (1/n) ∑ x i of a finite sample |
| Hoeffding, tail bound, sample statistics | `sampleMean_hoeffding_tail` | theorem | `FormalSLT/Statistics/SampleStatistics.lean:91` | Two-sided Hoeffding tail for the named sample mean |
| sample statistics | `sampleVariance` | theorem | `FormalSLT/Statistics/SampleStatistics.lean:45` | Population-form sample variance (1/n) ∑ (x i - x̄)² |
| sample statistics | `sampleVariance_eq_secondMoment_sub_meanSq` | theorem | `FormalSLT/Statistics/SampleStatistics.lean:65` | Variance decomposition Var = E[X²] - x̄² |
| sample statistics | `sampleVariance_nonneg` | theorem | `FormalSLT/Statistics/SampleStatistics.lean:51` | Sample variance is nonnegative |
| covering / chaining | `finDiscreteDist` | definition | `FormalSLT/Covering/FiniteDiscreteDudley.lean:28` | Discrete metric on Fin n |
| covering / chaining | `finDiscreteDist_nonneg` | definition | `FormalSLT/Covering/FiniteDiscreteDudley.lean:31` | The finite discrete metric is nonnegative |
| covering / chaining | `finDiscreteDist_symm` | definition | `FormalSLT/Covering/FiniteDiscreteDudley.lean:35` | The finite discrete metric is symmetric |
| covering / chaining | `finDiscreteDist_triangle` | definition | `FormalSLT/Covering/FiniteDiscreteDudley.lean:45` | The finite discrete metric satisfies the triangle inequality |
| Rademacher, covering / chaining | `finDiscreteDudleyInstance` | definition | `FormalSLT/Covering/FiniteDiscreteDudley.lean:286` | Packaged finite dyadic Dudley instance for the Fin n embedded Rademacher process |
| covering / chaining | `finDiscreteDyadicCoverCount` | definition | `FormalSLT/Covering/FiniteDiscreteDudley.lean:171` | Explicit adjacent-scale cover-count envelope n * n |
| covering / chaining | `finDiscreteDyadicNet` | definition | `FormalSLT/Covering/FiniteDiscreteDudley.lean:159` | Full finite net on Fin n at every dyadic scale |
| covering / chaining | `finDiscreteDyadicNetSequence` | definition | `FormalSLT/Covering/FiniteDiscreteDudley.lean:240` | General FiniteDyadicNetSequence instance for Fin n with [Fact (2 ≤ n)] |
| covering / chaining | `finDiscreteDyadicNet_coverCount_le` | definition | `FormalSLT/Covering/FiniteDiscreteDudley.lean:232` | Adjacent finite-discrete covering-number products are bounded by the n * n envelope |
| covering / chaining | `finDiscreteDyadicNet_coveringNumber` | definition | `FormalSLT/Covering/FiniteDiscreteDudley.lean:228` | The full finite discrete net has covering number n |
| covering / chaining | `finDiscreteDyadicNet_dist` | definition | `FormalSLT/Covering/FiniteDiscreteDudley.lean:174` | Finite discrete nets use the process metric |
| sub-Gaussian, Rademacher, covering / chaining | `finDiscreteRademacherProcess` | definition | `FormalSLT/Covering/FiniteDiscreteDudley.lean:146` | The embedded Rademacher process packaged as a finite sub-Gaussian process over Fin n |
| Rademacher, covering / chaining | `finDiscreteRademacherSup` | definition | `FormalSLT/Covering/FiniteDiscreteDudley.lean:311` | Supremum functional for the embedded Rademacher process over Fin n |
| Rademacher, covering / chaining | `finDiscreteRademacherSupAdapter` | definition | `FormalSLT/Covering/FiniteDiscreteDudley.lean:347` | Supplied-supremum adapter for the finite-discrete packaged Dudley instance |
| Rademacher, covering / chaining | `finDiscreteRademacherSup_dudley_m_bound` | definition | `FormalSLT/Covering/FiniteDiscreteDudley.lean:357` | Supplied-supremum finite Dudley bound for the embedded Rademacher process routed through the packaged finite dyadic Dudley API |
| Rademacher, covering / chaining, ERM | `finDiscreteRademacherSup_le_projectedSup` | definition | `FormalSLT/Covering/FiniteDiscreteDudley.lean:329` | Terminal projected-net adapter for the finite-discrete supplied supremum |
| Rademacher, covering / chaining | `finDiscreteRademacherSup_true` | definition | `FormalSLT/Covering/FiniteDiscreteDudley.lean:314` | The supplied supremum is nontrivial: it equals 1 on the positive Rademacher outcome |
| Rademacher, covering / chaining | `finDiscreteRademacherValue` | definition | `FormalSLT/Covering/FiniteDiscreteDudley.lean:75` | One-coordinate Rademacher process embedded in the finite discrete family |
| Rademacher, covering / chaining | `finDiscreteRademacher_projected_dudley_m_bound` | definition | `FormalSLT/Covering/FiniteDiscreteDudley.lean:295` | Arbitrary finite-horizon projected Dudley bound for the embedded Rademacher process routed through the packaged finite dyadic Dudley API |
| sub-Gaussian, MGF, Rademacher, covering / chaining | `finDiscrete_rademacher_mgf_bound` | definition | `FormalSLT/Covering/FiniteDiscreteDudley.lean:85` | Embedded Rademacher process increments satisfy the sub-Gaussian MGF bound |
| Bernoulli | `bernoulliNaturalBase` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:353` | Bernoulli natural-family base weights on Bool |
| Bernoulli | `bernoulliNaturalStatistic` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:356` | Bernoulli natural sufficient statistic 1{true} |
| Bernoulli | `bernoulliNatural_fisher_eq_variance_zero` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:457` | Bernoulli natural Fisher information equals variance at theta = 0 |
| Bernoulli | `bernoulliNatural_fisher_zero` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:443` | Bernoulli natural Fisher information at theta = 0 is 1/4 |
| Bernoulli | `bernoulliNatural_logPartition_deriv_zero` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:391` | Bernoulli natural A'(0) = 1/2 |
| Bernoulli | `bernoulliNatural_logPartition_secondDeriv_zero` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:427` | Bernoulli natural A''(0) = 1/4 |
| Bernoulli | `bernoulliNatural_logPartition_zero` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:368` | Bernoulli natural log-partition at theta = 0 is log 2 |
| Bernoulli | `bernoulliNatural_mean_zero` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:376` | Bernoulli natural mean at theta = 0 is 1/2 |
| Bernoulli | `bernoulliNatural_partition` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:359` | Bernoulli natural partition sum is 1 + exp(theta) |
| Bernoulli | `bernoulliNatural_pmf_zero` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:404` | Both Bernoulli natural atoms have mass 1/2 at theta = 0 |
| Bernoulli | `bernoulliNatural_variance_zero` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:416` | Bernoulli natural variance at theta = 0 is 1/4 |
| Bernoulli | `bernoulliNatural_witness` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:473` | Concrete Bernoulli witness with mean 1/2, variance 1/4, and Fisher information 1/4 |
|  | `finiteExponentialFamily_fisherInformation_eq_variance` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:321` | Natural-parameter Fisher information equals finite variance |
|  | `finiteExponentialFamily_logPartition_secondDeriv_eq_fisherInformation` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:336` | Direct bridge I(theta) = A''(theta) |
|  | `finiteExponentialFamily_mean_eq_logPartition_deriv` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:126` | Finite exponential-family mean equals the log-partition derivative numerator divided by Z(theta) |
|  | `finiteExponentialFamily_score_eq_centered` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:307` | Natural-parameter score equals the centered sufficient statistic |
|  | `finiteExponentialFamily_variance_eq_logPartition_secondDeriv` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:295` | Finite exponential-family variance equals log-partition second derivative |
|  | `finiteExponentialPMF` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:57` | Natural-parameter finite exponential-family probability mass |
|  | `finiteExponentialPMFDeriv` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:62` | Natural-parameter derivative of the finite exponential-family mass |
|  | `finiteExponentialPMF_hasDerivAt` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:176` | Derivative of the normalized finite exponential-family mass |
|  | `finiteExponentialPMF_pos` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:102` | Positive base weights give positive normalized masses |
|  | `finiteExponentialPMF_sum_one` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:76` | Normalized exponential-family masses sum to one |
|  | `finiteLogPartition` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:53` | Log-partition function A(theta) = log Z(theta) |
|  | `finiteLogPartition_hasDerivAt` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:153` | Log-partition derivative identity A'(theta) = E_theta[T] |
|  | `finiteLogPartition_hasDerivAt_of_positiveBase` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:164` | Positive-base wrapper for A'(theta) = E_theta[T] |
|  | `finiteLogPartition_hasSecondDerivAt` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:273` | Log-partition curvature identity A''(theta) = Var_theta(T) |
|  | `finiteLogPartition_hasSecondDerivAt_of_positiveBase` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:284` | Positive-base wrapper for A''(theta) = Var_theta(T) |
|  | `finiteMean_deriv_eq_variance` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:209` | Centered second-moment derivative equals finite weighted variance |
|  | `finiteMean_hasDerivAt` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:192` | Differentiating the finite mean gives a centered second moment |
|  | `finitePartition` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:49` | Finite exponential-family partition sum Z(theta) |
| ERM | `finitePartition_hasDerivAt` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:111` | Termwise derivative of the finite partition sum |
|  | `finitePartition_pos` | definition | `FormalSLT/Statistics/ExponentialFamily.lean:68` | Positive base weights give positive finite partition sum |
| union bound | `finiteMeasureUnionBound` | theorem | `FormalSLT/Probability/FiniteUnionBound.lean:130` | Finite-index measure union bound |
| union bound | `finiteMeasureUnionBound_budget` | theorem | `FormalSLT/Probability/FiniteUnionBound.lean:143` | Supplied finite per-event budgets whose sum is bounded by a total budget |
| union bound | `finiteMeasureUnionBound_cardInv` | theorem | `FormalSLT/Probability/FiniteUnionBound.lean:198` | Nonempty finite class with per-event budget α / card has union mass ≤ α |
| union bound | `finiteMeasureUnionBound_const` | theorem | `FormalSLT/Probability/FiniteUnionBound.lean:163` | Common per-event budget gives card * β total mass |
| union bound | `finiteMeasureUnionBound_equalBudget` | theorem | `FormalSLT/Probability/FiniteUnionBound.lean:183` | Explicit per-event budget whose finite sum is bounded by a total budget |
| Bernoulli | `bernoulliFisherInformation` | theorem | `FormalSLT/Statistics/CramerRao.lean:73` | Bernoulli Fisher information 1 / (p(1-p)) |
| sample statistics, Bernoulli | `bernoulliHalfCramerRaoWitness` | theorem | `FormalSLT/Statistics/CramerRao.lean:135` | Concrete witness: identity estimator attains variance 1/4 = 1 / I(1/2) |
| Bernoulli | `bernoulliHalfFisherInformation` | theorem | `FormalSLT/Statistics/CramerRao.lean:103` | Concrete witness: I(1/2) = 4 |
|  | `covariance_cauchy_schwarz` | theorem | `FormalSLT/Statistics/FisherInformation.lean:179` | Weighted Cauchy-Schwarz: Cov² ≤ Var · Var |
| sample statistics | `covariance_score_eq_deriv_mean` | theorem | `FormalSLT/Statistics/FisherInformation.lean:122` | Estimator-score covariance equals the derivative of the estimator mean |
| sample statistics | `cramerRao_unbiased` | theorem | `FormalSLT/Statistics/CramerRao.lean:38` | Cramér-Rao lower bound 1 / I(θ) ≤ Var(T) for an unbiased estimator |
|  | `fisherInformation` | theorem | `FormalSLT/Statistics/FisherInformation.lean:78` | Fisher information as the weighted variance of the score |
|  | `scoreFunction` | theorem | `FormalSLT/Statistics/FisherInformation.lean:73` | Score ∂_θ log p(x; θ) as pmfDeriv / pmf |
|  | `score_mean_zero_of_finite_regular` | theorem | `FormalSLT/Statistics/FisherInformation.lean:105` | Score has zero mean under regularity (∑ p' = 0) |
|  | `weightedCovariance` | theorem | `FormalSLT/Statistics/FisherInformation.lean:50` | Finite weighted covariance of two functions |
| sample statistics | `weightedVariance` | theorem | `FormalSLT/Statistics/FisherInformation.lean:46` | Finite weighted variance of an estimator under a weight vector |
| Glivenko-Cantelli | `IsGCClass` | theorem | `FormalSLT/GlivenkoCantelli.lean:659` | Glivenko-Cantelli class predicate: a.s. uniform-deviation convergence to zero |
| Glivenko-Cantelli, Bernoulli | `bernoulliThreeZerosOneOne_uniformDeviation_le_quarter` | theorem | `FormalSLT/GlivenkoCantelli.lean:1020` | Concrete non-vacuity witness: explicit four-sample uniform empirical-CDF deviation ≤ 1/4 |
| Glivenko-Cantelli | `classicalGlivenkoCantelli_iid` | theorem | `FormalSLT/GlivenkoCantelli.lean:852` | Classical Glivenko-Cantelli for i.i.d. real samples: empirical CDF converges uniformly a.s. to the population CDF |
| Glivenko-Cantelli | `classicalGlivenkoCantelli_of_pointwise_lowerRay` | theorem | `FormalSLT/GlivenkoCantelli.lean:696` | Uniform a.s. GC from pointwise convergence on closed and strict lower rays |
| Glivenko-Cantelli | `empiricalCDF` | theorem | `FormalSLT/GlivenkoCantelli.lean:418` | Empirical CDF as the lower-ray indicator-class empirical average |
| Glivenko-Cantelli | `empiricalCDFUniformDeviation` | theorem | `FormalSLT/GlivenkoCantelli.lean:603` | Uniform empirical-CDF deviation sup_x abs(F_n(x) - F(x)) |
| Glivenko-Cantelli | `empiricalCDF_eq_lowerRayEmpiricalAverage` | theorem | `FormalSLT/GlivenkoCantelli.lean:428` | Empirical CDF equals the lower-ray indicator empirical average |
| Glivenko-Cantelli | `finiteLowerRayBracketingGrid` | theorem | `FormalSLT/GlivenkoCantelli.lean:236` | Finite grid of bracket points that controls every threshold at a chosen mesh |
| Glivenko-Cantelli | `integral_lowerRayIndicator_comp_eq_cdf` | theorem | `FormalSLT/GlivenkoCantelli.lean:99` | Population lower-ray mass equals the CDF of the pushed-forward law |
| ERM, Glivenko-Cantelli | `lowerRayBracketing_uniformDeviation_bound` | theorem | `FormalSLT/GlivenkoCantelli.lean:541` | Deterministic finite-grid bracketing bound on the uniform empirical-CDF deviation |
| Glivenko-Cantelli | `lowerRayGC_iff_classicalGlivenkoCantelli` | theorem | `FormalSLT/GlivenkoCantelli.lean:681` | The classical empirical-CDF GC statement is exactly the lower-ray indicator-class GC statement |
| Glivenko-Cantelli | `lowerRayIndicator` | theorem | `FormalSLT/GlivenkoCantelli.lean:37` | Closed lower-ray indicator 1{x ≤ z} as the empirical-CDF integrand |
| Glivenko-Cantelli | `lowerRayPointwiseStrongLaw` | theorem | `FormalSLT/GlivenkoCantelli.lean:796` | Pointwise empirical-CDF strong law at a fixed threshold from the mathlib strong law |
| Rademacher, ERM, Glivenko-Cantelli | `rademacherERMBridge_for_gcClass` | theorem | `FormalSLT/GlivenkoCantelli.lean:953` | Wraps the GC class into the Rademacher ERM generalization surface |
| Glivenko-Cantelli | `strictLowerRayIndicator` | theorem | `FormalSLT/GlivenkoCantelli.lean:41` | Open lower-ray indicator 1{x < z}, the atom-safe upper bracket |
| Glivenko-Cantelli | `strictLowerRayPointwiseStrongLaw` | theorem | `FormalSLT/GlivenkoCantelli.lean:824` | Open-upper-bracket pointwise strong law, the atom-safe companion |
| Hoeffding, VC dimension, Glivenko-Cantelli | `vcHoeffdingBridge_for_gcClass` | theorem | `FormalSLT/GlivenkoCantelli.lean:923` | Wraps the GC class into the finite-class VC/Hoeffding empirical-process surface |
| PAC-Bayes, VC dimension, Glivenko-Cantelli | `vcPacBayesHybridBridge_for_gcClass` | theorem | `FormalSLT/GlivenkoCantelli.lean:976` | Wraps the GC class into the VC/PAC-Bayes hybrid surface |
| Bennett, sub-Gamma, tail bound, covering / chaining | `bennett_tail` | theorem | `FormalSLT/Concentration/NamedTails.lean:312` | Two-sided Bennett / sub-Gamma tail at a chosen λ for a finite distribution |
| Bernstein, tail bound | `bernstein_tail` | theorem | `FormalSLT/Concentration/NamedTails.lean:256` | Two-sided Bernstein tail P(abs X ≥ ε) ≤ 2 exp(-ε²/(2(v + bε/3))) for a finite distribution |
| Chernoff, sub-Gaussian, tail bound, MGF | `chernoff_tail` | theorem | `FormalSLT/Concentration/NamedTails.lean:61` | Generic two-sided sub-Gaussian tail P(abs X ≥ t) ≤ 2 exp(-t²/(2c)) from an MGF bound |
| Hoeffding, tail bound, sample statistics | `hoeffding_mean_tail_twoSided` | theorem | `FormalSLT/Concentration/NamedTails.lean:112` | Two-sided Hoeffding tail for the sample mean P(abs (X̄ - E X̄) ≥ t) ≤ 2 exp(-2 n t²/(b-a)²) |
| sub-Gaussian, tail bound, MGF | `subGaussianMGF_tail_twoSided` | theorem | `FormalSLT/Concentration/NamedTails.lean:93` | Centered two-sided sub-Gaussian tail P(abs (X - E X) ≥ t) ≤ 2 exp(-t²/(2c)) |
| Rademacher, VC dimension | `effectiveClass_zeroOneLoss_card_eq_binaryClassTrace` | theorem | `FormalSLT/VC/BinaryVCBridge.lean:137` | Effective 0-1 loss patterns equal binary traces |
| Rademacher, VC dimension | `effectiveClass_zeroOneLoss_card_le_sauerShelah` | theorem | `FormalSLT/VC/BinaryVCBridge.lean:154` | Binary VC Sauer-Shelah corollary |
| Rademacher, VC dimension | `empiricalRademacherComplexity_le_massart_effective` | theorem | `FormalSLT/VC/Rademacher.lean:85` | Effective-class Massart bound |
| Rademacher, VC dimension, ERM | `expected_genGap_le_two_expected_empiricalRademacherComplexity` | theorem | `FormalSLT/Rademacher/Symmetrization.lean:196` | E[genGap] <= 2 * E[Rad] |
| Rademacher, VC dimension, ERM | `genGap_highProb_finiteClass` | theorem | `FormalSLT/Rademacher/FiniteClassHighProb.lean:93` | Massart plus sharp high-probability Rademacher |
| Rademacher, VC dimension, ERM | `genGap_highProb_rademacher` | theorem | `FormalSLT/Rademacher/HighProbability.lean:95` | P(genGap >= 2 * E[Rad] + ε) <= exp(-ε² n / (2B²)) |
| tail bound, Rademacher, VC dimension, ERM | `genGap_highProb_vcClass` | theorem | `FormalSLT/VC/SampleComplexity.lean:236` | VC-style one-sided genGap tail with sharp exponent |
| Azuma, tail bound, Rademacher, VC dimension, ERM | `genGap_tail_bound_azuma_explicit` | theorem | `FormalSLT/Azuma/GenGapTail.lean:520` | P(genGap - E[genGap] >= ε) <= exp(-ε² n / (8B²)) |
| tail bound, Rademacher, VC dimension, ERM | `genGap_tail_bound_sharp_explicit` | theorem | `FormalSLT/Azuma/GenGapTail.lean:595` | P(genGap - E[genGap] >= ε) <= exp(-ε² n / (2B²)) |
| McDiarmid, tail bound, Rademacher, VC dimension | `hasBoundedDifferences_tail_sharp` | theorem | `FormalSLT/Azuma/GenGapTail.lean:416` | P(f - E[f] >= ε) <= exp(-2ε² / sum_k c_k²) |
| Rademacher, VC dimension | `massart_finite_class` | theorem | `FormalSLT/Rademacher/Massart.lean:347` | Rad(H,S) <= B * sqrt(2 * log card(H) / n) |
| McDiarmid, tail bound, Rademacher, VC dimension | `mcdiarmid_of_hasBoundedDifferences_sharp` | theorem | `FormalSLT/Concentration/SharpMcDiarmid.lean:115` | Public wrapper for the sharp product bounded-differences tail |
| McDiarmid, tail bound, Rademacher, VC dimension | `mcdiarmid_of_hasBoundedDifferences_sharp_hetero` | theorem | `FormalSLT/Concentration/HeterogeneousMcDiarmid.lean:37` | Heterogeneous-law product upper tail with the sharp McDiarmid exponent |
| McDiarmid, tail bound, Rademacher, VC dimension | `mcdiarmid_of_hasBoundedDifferences_sharp_hetero_lower` | theorem | `FormalSLT/Concentration/HeterogeneousMcDiarmid.lean:53` | Heterogeneous-law product lower tail with the sharp McDiarmid exponent |
| McDiarmid, tail bound, Rademacher, VC dimension | `mcdiarmid_of_hasBoundedDifferences_sharp_lower` | theorem | `FormalSLT/Concentration/SharpMcDiarmid.lean:134` | Lower-tail wrapper obtained from the upper tail applied to -f |
| McDiarmid, Rademacher, VC dimension | `mcdiarmid_of_hasBoundedDifferences_sharp_of_hetero` | theorem | `FormalSLT/Concentration/HeterogeneousMcDiarmid.lean:142` | Homogeneous recovery from the heterogeneous product theorem by taking a constant law family |
| Rademacher, VC dimension | `sauerShelah_polynomial_bound` | theorem | `FormalSLT/VC/SauerShelah.lean:44` | sum_{k<=d} C(n,k) <= (en/d)^d |
| Rademacher, VC dimension, Glivenko-Cantelli | `uniformDeviation_highProb_finiteClass` | theorem | `FormalSLT/Rademacher/UniformDeviation.lean:99` | Two-sided finite-class uniform deviation with sharp one-sided tails |
| Rademacher, VC dimension, Glivenko-Cantelli | `uniformDeviation_highProb_vcClass` | theorem | `FormalSLT/VC/SampleComplexity.lean:282` | VC-style two-sided uniform deviation with sharp one-sided tails |
| Rademacher, VC dimension | `vcRademacher_pointwise` | theorem | `FormalSLT/VC/SampleComplexity.lean:137` | Rad <= B * sqrt(2d * log(en/d) / n) |
| tail bound, Rademacher, VC dimension, ERM, risk | `vc_erm_excessRisk_tail` | theorem | `FormalSLT/VC/SampleComplexity.lean:350` | VC-style ERM excess-risk tail with sharp concentration term |
| Rademacher, VC dimension, ERM | `vc_erm_sample_complexity` | theorem | `FormalSLT/VC/SampleComplexity.lean:424` | Closed-form VC ERM sample-complexity theorem with explicit 72 * B^2 constant |
| Bernstein, PAC-Bayes, stability, risk | `BernsteinCondition` | theorem | `FormalSLT/Rademacher/Localized.lean:86` | Finite Bernstein condition: excess-loss second moment controlled by excess risk |
| PAC-Bayes, stability | `FiniteCoordinateSwapIdentity` | theorem | `FormalSLT/AlgorithmicStability.lean:1074` | Finite coordinate-swap symmetry predicate for explicit sample weights |
| PAC-Bayes, ERM, stability | `FixedPointUpperCertificate` | theorem | `FormalSLT/Rademacher/Localized.lean:377` | Deterministic envelope certificate: above rStar, the localized envelope is below the identity |
| PAC-Bayes, ERM, stability, risk | `LocalizedDeviationCertificate` | theorem | `FormalSLT/Rademacher/Localized.lean:430` | Deterministic localized concentration-event interface for population excess risk versus empirical excess risk |
| PAC-Bayes, ERM, stability | `abs_expectedFiniteGeneralizationGap_le_uniformStability_finiteProduct` | theorem | `FormalSLT/AlgorithmicStability.lean:1680` | Literal finite iid product-weight absolute expected generalization-gap wrapper |
| PAC-Bayes, ERM, stability | `abs_expectedFiniteGeneralizationGap_le_uniformStability_of_coordinateSwap` | theorem | `FormalSLT/AlgorithmicStability.lean:1657` | Literal finite absolute expected generalization-gap wrapper under a finite swap identity |
| PAC-Bayes, stability | `abs_expectedFiniteStabilityGap_le_uniformStability_finiteProduct` | theorem | `FormalSLT/AlgorithmicStability.lean:1555` | Uniform stability gives finite iid two-sided expected stability gap ≤ β |
| PAC-Bayes, stability | `abs_expectedFiniteStabilityGap_le_uniformStability_of_coordinateSwap` | theorem | `FormalSLT/AlgorithmicStability.lean:1514` | Uniform stability gives finite two-sided expected stability gap ≤ β under a finite swap identity |
| PAC-Bayes, stability | `abs_expectedStabilityGap_le_uniformStability_piMeasure_of_boundedLoss` | theorem | `FormalSLT/AlgorithmicStability.lean:957` | Product-measure two-sided expected gap ≤ β with bounded-loss integrability discharged |
| Bernstein, tail bound, PAC-Bayes, stability | `averaged_bernstein_tail` | theorem | `FormalSLT/Probability/BernsteinMGF.lean:358` | Iid product-weight Bernstein tail with the n * eps^2 exponent |
| Bennett, MGF, PAC-Bayes, covering / chaining, stability | `bennett_mgf` | theorem | `FormalSLT/Probability/BernsteinMGF.lean:160` | Finite centered bounded-variance Bennett MGF |
| Bennett, sub-Gamma, MGF, PAC-Bayes, covering / chaining, stability | `bennett_mgf_subgamma` | theorem | `FormalSLT/Probability/BernsteinMGF.lean:251` | Sub-Gamma denominator form of the finite Bennett MGF |
| Bernstein, tail bound, PAC-Bayes, stability | `bernstein_tail` | theorem | `FormalSLT/Probability/BernsteinMGF.lean:323` | One-sample finite Bernstein upper-tail bound |
| PAC-Bayes, stability | `boundedLoss_coordinateSelectedLoss_integrable` | theorem | `FormalSLT/AlgorithmicStability.lean:901` | Bounded empirical coordinate loss is integrable under μⁿ |
| PAC-Bayes, stability | `boundedLoss_selectedLoss_integrable` | theorem | `FormalSLT/AlgorithmicStability.lean:845` | Bounded finite-class selected loss is integrable under μⁿ × μ |
| PAC-Bayes, stability | `boundedLoss_updateSelectedLoss_integrable` | theorem | `FormalSLT/AlgorithmicStability.lean:870` | Bounded coordinate-updated selected loss is integrable under μⁿ × μ |
| PAC-Bayes, stability | `bousquet_elisseeff_expectedGap_variant` | theorem | `FormalSLT/Stability/BousquetElisseeff.lean:348` | Stability high-probability bound with explicit expected-gap and measurability hypotheses |
| PAC-Bayes, stability | `bousquet_elisseeff_expectedGap_variant_of_boundedLoss` | theorem | `FormalSLT/Stability/BousquetElisseeff.lean:517` | Bounded-loss finite-class wrapper for the sharp stability high-probability theorem |
| PAC-Bayes, stability | `bousquet_elisseeff_uniform_stability_corollary` | theorem | `FormalSLT/Stability/BousquetElisseeff.lean:575` | β = c0 / n stability corollary for the sharp variant |
| PAC-Bayes, stability | `bousquet_elisseeff_uniform_stability_corollary_of_boundedLoss` | theorem | `FormalSLT/Stability/BousquetElisseeff.lean:609` | Bounded-loss finite-class β = c0 / n high-probability stability corollary |
| PAC-Bayes, stability | `catoni_fixedLambda_budget_eq_sqrt` | theorem | `FormalSLT/PACBayesBoundedLoss.lean:484` | Fixed-λ Catoni penalty optimized to a square-root budget |
| Bernstein, PAC-Bayes, stability | `centeredSecondMoment_le_of_bernstein_localized` | theorem | `FormalSLT/Rademacher/Localized.lean:2126` | Variance proxy for the centered excess-loss deviation is bounded by c * r on the localized class |
| PAC-Bayes, KL divergence, stability | `continuousPriorPosterior_certificate_derived` | theorem | `FormalSLT/PACBayes/ContinuousPriorPosterior.lean:68` | Continuous prior/posterior certificate with the PAC gate derived by change of measure |
| MGF, PAC-Bayes, KL divergence, stability | `continuous_catoni_changeOfMeasure_bound` | theorem | `FormalSLT/PACBayes/ContinuousChangeOfMeasure.lean:73` | Continuous fixed-lambda Catoni change-of-measure bound from a prior log-MGF certificate |
| PAC-Bayes, stability | `continuous_donsker_varadhan` | theorem | `FormalSLT/PACBayes/ContinuousChangeOfMeasure.lean:27` | Measure-theoretic Donsker-Varadhan bound from Radon-Nikodym tilting |
| Bennett, PAC-Bayes, covering / chaining, stability | `exp_le_quadratic_of_le` | theorem | `FormalSLT/Probability/BernsteinMGF.lean:136` | Pointwise Bennett inequality for a centered bounded variable |
| PAC-Bayes, ERM, stability | `expectedFiniteGeneralizationGap_le_uniformStability_finiteProduct` | theorem | `FormalSLT/AlgorithmicStability.lean:1603` | Literal finite iid product-weight E[R(A(S)) - Rhat_S(A(S))] ≤ β wrapper |
| PAC-Bayes, ERM, stability | `expectedFiniteGeneralizationGap_le_uniformStability_of_coordinateSwap` | theorem | `FormalSLT/AlgorithmicStability.lean:1575` | Literal finite E[R(A(S)) - Rhat_S(A(S))] ≤ β wrapper under a finite swap identity |
| PAC-Bayes, stability | `expectedFiniteStabilityGap_le_uniformStability_finiteProduct` | theorem | `FormalSLT/AlgorithmicStability.lean:1467` | Uniform stability gives finite iid product-weight expected gap ≤ β |
| PAC-Bayes, stability | `expectedFiniteStabilityGap_le_uniformStability_of_coordinateSwap` | theorem | `FormalSLT/AlgorithmicStability.lean:1346` | Uniform stability gives finite expected gap ≤ β under a finite swap identity |
| PAC-Bayes, stability | `expectedStabilityGap_le_uniformStability_piMeasure_of_boundedLoss` | theorem | `FormalSLT/AlgorithmicStability.lean:930` | Product-measure expected gap ≤ β with bounded-loss integrability discharged |
| PAC-Bayes, stability, risk | `finiteCatoni_badEventMass_le_delta` | theorem | `FormalSLT/PACBayesBoundedLoss.lean:408` | Finite [0,1] Catoni-style PAC-Bayes posterior-risk bad-event bound |
| PAC-Bayes, stability | `finiteClass_loss_measurable` | theorem | `FormalSLT/AlgorithmicStability.lean:813` | Finite per-hypothesis loss measurability gives joint loss measurability |
| PAC-Bayes, ERM, stability, risk | `finiteEmpiricalRisk` | theorem | `FormalSLT/PACBayesFiniteProductMGF.lean:45` | Finite empirical risk for a real-valued loss |
| Bernstein, PAC-Bayes, ERM, stability, risk | `finiteExcessRisk_le_of_localizedDeviation_bernstein_fixedPoint` | theorem | `FormalSLT/Rademacher/Localized.lean:1595` | Localized deviation plus Bernstein/fixed-point control gives a finite fast-rate shell |
| PAC-Bayes, ERM, stability, risk | `finiteExcessRisk_le_of_localizedDeviation_empirical_nonpos` | theorem | `FormalSLT/Rademacher/Localized.lean:1428` | Localized deviation plus nonpositive empirical excess risk controls population excess risk by the deviation slack |
| Bernstein, PAC-Bayes, ERM, stability, risk | `finiteExcessRisk_le_of_localizedFastRateUpperDeviationEvent_bernstein_fixedPoint` | theorem | `FormalSLT/Rademacher/Localized.lean:1685` | Fast-rate shell stated through the named sample-dependent upper-deviation event |
| PAC-Bayes, ERM, stability, risk | `finiteExcessRisk_le_of_localizedSampleDependentUpperDeviationEvent_empirical_nonpos` | theorem | `FormalSLT/Rademacher/Localized.lean:1508` | Sample-dependent localized upper-deviation event payoff for empirical competitors |
| Bernstein, PAC-Bayes, ERM, stability, risk | `finiteExcessRisk_le_of_localizedUpperDeviationEvent_bernstein_fixedPoint` | theorem | `FormalSLT/Rademacher/Localized.lean:1641` | Event-facing finite fast-rate shell, reducing the remaining localized task to proving the upper-deviation event |
| PAC-Bayes, ERM, stability, risk | `finiteExcessRisk_le_of_localizedUpperDeviationEvent_empirical_nonpos` | theorem | `FormalSLT/Rademacher/Localized.lean:1444` | Fixed-threshold localized upper-deviation event payoff for empirical competitors |
| PAC-Bayes, stability | `finiteMcAllesterBoundedComplexity_badEventMass_le_delta` | theorem | `FormalSLT/PACBayesBoundedLoss.lean:573` | Finite [0,1] fixed-budget McAllester-style bad-event bound |
| PAC-Bayes, stability | `finiteMcAllesterGridOptimized_badEventMass_le_delta` | theorem | `FormalSLT/PACBayesBoundedLoss.lean:856` | Posterior-dependent finite-grid McAllester wrapper under an explicit bucket certificate |
| confidence sequence, PAC-Bayes, stability | `finiteMcAllesterGridPeeling_badEventMass_le_delta` | theorem | `FormalSLT/PACBayesBoundedLoss.lean:766` | Finite-grid McAllester peeling bound with allocated confidence mass |
| Bernstein, PAC-Bayes, stability | `finitePACBayesBernsteinMargin_badEventMass_le_delta` | theorem | `FormalSLT/PACBayesBernstein.lean:521` | Finite supplied margin-proxy wrapper with sqrt(2 * Vρ * Cρ) + scale * Cρ penalty form |
| Bernstein, PAC-Bayes, stability | `finitePACBayesBernsteinPenalty_badEventMass_le_delta` | theorem | `FormalSLT/PACBayesBernstein.lean:452` | Posterior-dependent finite Bernstein bad-event wrapper under complexity and penalty certificates |
| Bernstein, PAC-Bayes, stability | `finitePACBayesBernstein_fixedLambda_badEventMass_le_delta` | theorem | `FormalSLT/PACBayesBernstein.lean:355` | Finite fixed-lambda PAC-Bayes Bernstein bad-event bound |
| MGF, PAC-Bayes, ERM, stability, risk | `finitePriorAveraged_mgf_empiricalRiskDeviation_le` | theorem | `FormalSLT/PACBayesFiniteProductMGF.lean:174` | Prior-averaged finite iid empirical-risk-deviation MGF bound |
| PAC-Bayes, stability | `finiteProductSampleWeight` | theorem | `FormalSLT/AlgorithmicStability.lean:1087` | Iid finite product sample weights ∏ k, p (S k) |
| PAC-Bayes, stability | `finiteProductSampleWeight_coordinateSwapIdentity` | theorem | `FormalSLT/AlgorithmicStability.lean:1180` | Finite iid product weights satisfy the coordinate-swap identity |
| MGF, PAC-Bayes, ERM, stability, risk | `finiteProduct_mgf_empiricalRiskDeviation_eq_pow` | theorem | `FormalSLT/PACBayesFiniteProductMGF.lean:94` | Exact iid product factorization of E exp(lam * (R_i - Rhat_i)) |
| MGF, PAC-Bayes, ERM, stability, risk | `finiteProduct_mgf_empiricalRiskDeviation_le_of_single` | theorem | `FormalSLT/PACBayesFiniteProductMGF.lean:134` | Single-coordinate MGF budget lifts to the finite sample-average MGF |
| PAC-Bayes, KL divergence, stability | `klDiv_nonneg` | theorem | `FormalSLT/PACBayesKL.lean:130` | Finite KL divergence is nonnegative under full support |
| PAC-Bayes, ERM, stability | `localizedDeviationCertificate_of_mem_upperDeviationEvent` | theorem | `FormalSLT/Rademacher/Localized.lean:1415` | Event membership constructs the deterministic localized deviation certificate |
| PAC-Bayes, Rademacher, stability | `localizedEmpiricalRademacherComplexity_mono` | theorem | `FormalSLT/Rademacher/Localized.lean:253` | Finite localized empirical Rademacher complexity is monotone under predicate inclusion |
| PAC-Bayes, Rademacher, stability | `localizedEmpiricalRademacherComplexity_nonneg_of_zero` | theorem | `FormalSLT/Rademacher/Localized.lean:193` | Localized empirical Rademacher complexity is nonnegative when the class contains an identically zero excess-loss comparator |
| Bernstein, PAC-Bayes, Rademacher, ERM, stability, risk | `localizedExcessRiskEmpiricalRademacherComplexity_le_of_bernstein_fixedPointCertificate` | theorem | `FormalSLT/Rademacher/Localized.lean:400` | Bernstein bridge plus fixed-point certificate controls excess-risk localized empirical complexity by c * r |
| Bernstein, PAC-Bayes, Rademacher, ERM, stability, risk | `localizedExcessRiskEmpiricalRademacherComplexity_le_secondMoment` | theorem | `FormalSLT/Rademacher/Localized.lean:337` | Bernstein embeds excess-risk localized complexity into second-moment localized complexity |
| PAC-Bayes, Rademacher, ERM, stability, risk | `localizedExcessRiskEmpiricalRademacherComplexity_nonneg` | theorem | `FormalSLT/Rademacher/Localized.lean:310` | Excess-risk localized empirical Rademacher complexity is nonnegative because the comparator belongs to every nonnegative radius |
| Bernstein, confidence sequence, PAC-Bayes, stability | `localizedFastRateHighConfidence_bernstein_fixedPoint_boundedExcess` | theorem | `FormalSLT/Rademacher/Localized.lean:2072` | Conservative finite fast-rate high-confidence wrapper pairing the bounded-excess bad-event mass with the Bernstein/fixed-point payoff |
| Bernstein, confidence sequence, PAC-Bayes, stability | `localizedFastRateHighConfidence_bernstein_fixedPoint_of_centeredShiftedExpMoment` | theorem | `FormalSLT/Rademacher/Localized.lean:2016` | Assumption-facing high-confidence wrapper from supplied centered shifted-moment budgets. Interface only — the budgets it consumes are conservative-only per hypothesis |
| Bernstein, confidence sequence, PAC-Bayes, stability | `localizedFastRateHighConfidence_bernstein_fixedPoint_of_shiftedExpMoment` | theorem | `FormalSLT/Rademacher/Localized.lean:1958` | Assumption-facing high-confidence finite fast-rate wrapper from shifted exponential-moment budgets |
| PAC-Bayes, stability | `localizedFastRatePointwiseShiftedExpMoment_finiteProduct_le_boundedExcess` | theorem | `FormalSLT/Rademacher/Localized.lean:1872` | Bounded-excess finite-product shifted-moment budget for one hypothesis in the named fast-rate random-threshold event |
| PAC-Bayes, stability | `localizedFastRatePointwiseShiftedExpMoment_le_centered_div` | theorem | `FormalSLT/Rademacher/Localized.lean:1769` | Algebraic interface: factors the fixed slack out of the shifted moment. Conservative-only (per-hypothesis centered moment ≤ fixed moment); names the whole-supremum obligation, does not discharge it |
| PAC-Bayes, stability | `localizedFastRateUpperDeviationBadEventMass` | theorem | `FormalSLT/Rademacher/Localized.lean:540` | Finite weighted mass outside the named fast-rate random-threshold localized event |
| PAC-Bayes, stability | `localizedFastRateUpperDeviationBadEventMass_finiteProduct_le_delta_boundedExcess` | theorem | `FormalSLT/Rademacher/Localized.lean:1333` | Conservative finite product-mass bound for the named fast-rate event by reduction to the fixed-threshold bounded-excess theorem |
| PAC-Bayes, stability | `localizedFastRateUpperDeviationBadEventMass_le_fixed_epsilon` | theorem | `FormalSLT/Rademacher/Localized.lean:1296` | Named fast-rate bad-event mass is controlled by the fixed-ε bad-event mass using nonnegativity of the empirical localized complexity |
| union bound, PAC-Bayes, stability | `localizedFastRateUpperDeviationBadEventMass_le_sum_centeredShiftedExpMoment_div` | theorem | `FormalSLT/Rademacher/Localized.lean:1829` | Algebraic interface: bad-event mass via summed centered moments and a fixed-slack denominator. Conservative-only union bound; not a non-conservative concentration result |
| PAC-Bayes, stability | `localizedFastRateUpperDeviationBadEventMass_le_sum_shiftedExpMoment` | theorem | `FormalSLT/Rademacher/Localized.lean:1719` | Named fast-rate bad-event mass controlled by shifted exponential-moment budgets |
| PAC-Bayes, stability | `localizedFastRateUpperDeviationEvent` | theorem | `FormalSLT/Rademacher/Localized.lean:482` | Named random-threshold event used by the finite fast-rate shell |
| Bernstein, tail bound, confidence sequence, PAC-Bayes, stability | `localizedFiniteClassBernsteinHighConfidence_empirical_nonpos` | theorem | `FormalSLT/Rademacher/Localized.lean:2162` | Finite localized Bernstein high-confidence theorem with bad-event mass bounded by the averaged Bernstein tail and fixed-threshold payoff |
| confidence sequence, PAC-Bayes, stability | `localizedFiniteClassHighConfidence_empirical_nonpos_boundedExcess` | theorem | `FormalSLT/Rademacher/Localized.lean:1472` | Fixed-threshold finite high-confidence localized statement combining bounded-excess bad-event mass with the empirical-competitor payoff |
| MGF, PAC-Bayes, stability | `localizedOneCoordinateDeviationMGF_le_of_excessLoss_mem_Icc_neg_one_one` | theorem | `FormalSLT/Rademacher/Localized.lean:690` | Bounded excess losses in [-1,1] supply the localized one-coordinate MGF budget |
| PAC-Bayes, stability | `localizedPointwiseSampleDependentUpperDeviationBadEventMass` | theorem | `FormalSLT/Rademacher/Localized.lean:506` | Finite weighted mass of one pointwise upper-deviation bad event with a sample-dependent threshold |
| PAC-Bayes, stability | `localizedPointwiseSampleDependentUpperDeviationBadEventMass_le_shiftedExpMoment` | theorem | `FormalSLT/Rademacher/Localized.lean:891` | Pointwise sample-dependent bad-event mass controlled by its shifted exponential moment |
| PAC-Bayes, stability | `localizedPointwiseSampleDependentUpperDeviationShiftedExpMoment` | theorem | `FormalSLT/Rademacher/Localized.lean:565` | Shifted exponential moment for one localized upper-deviation gap with a sample-dependent threshold |
| PAC-Bayes, stability | `localizedPointwiseSampleDependentUpperDeviationShiftedExpMoment_add_const` | theorem | `FormalSLT/Rademacher/Localized.lean:1003` | Fixed slack added to a sample-dependent threshold factors out of the shifted exponential moment |
| PAC-Bayes, stability | `localizedPointwiseSampleDependentUpperDeviationShiftedExpMoment_le_fixedExpMoment_div` | theorem | `FormalSLT/Rademacher/Localized.lean:957` | Sample-dependent shifted moment controlled by a fixed-threshold exponential moment under a pointwise lower bound on the random threshold |
| PAC-Bayes, stability | `localizedPointwiseUpperDeviationBadEventMass` | theorem | `FormalSLT/Rademacher/Localized.lean:496` | Finite weighted mass of one pointwise upper-deviation bad event |
| Markov, PAC-Bayes, stability | `localizedPointwiseUpperDeviationBadEventMass_le_expMoment_div` | theorem | `FormalSLT/Rademacher/Localized.lean:595` | Pointwise Markov adapter from an exponential-moment budget to an upper-deviation bad-event mass |
| PAC-Bayes, stability | `localizedPointwiseUpperDeviationExpMoment` | theorem | `FormalSLT/Rademacher/Localized.lean:554` | Finite weighted exponential moment for one localized upper-deviation gap |
| MGF, PAC-Bayes, stability | `localizedPointwiseUpperDeviationExpMoment_finiteProduct_le_of_single` | theorem | `FormalSLT/Rademacher/Localized.lean:665` | Finite iid product MGF bridge for one localized upper-deviation gap from a one-coordinate MGF budget |
| confidence sequence, PAC-Bayes, stability | `localizedSampleDependentHighConfidence_empirical_nonpos` | theorem | `FormalSLT/Rademacher/Localized.lean:1534` | Supplied-mass high-confidence adapter for sample-dependent localized upper-deviation events |
| confidence sequence, PAC-Bayes, stability | `localizedSampleDependentHighConfidence_empirical_nonpos_of_shiftedExpMoment` | theorem | `FormalSLT/Rademacher/Localized.lean:1563` | Sample-dependent high-confidence adapter from shifted exponential-moment budgets |
| PAC-Bayes, stability | `localizedSampleDependentUpperDeviationBadEventMass` | theorem | `FormalSLT/Rademacher/Localized.lean:528` | Finite weighted mass outside a sample-dependent localized upper-deviation event |
| PAC-Bayes, stability | `localizedSampleDependentUpperDeviationBadEventMass_le_fixed` | theorem | `FormalSLT/Rademacher/Localized.lean:1269` | Sample-dependent bad-event mass is controlled by a fixed-threshold bad-event mass when the random threshold is pointwise larger |
| PAC-Bayes, stability | `localizedSampleDependentUpperDeviationBadEventMass_le_sum_pointwise` | theorem | `FormalSLT/Rademacher/Localized.lean:1033` | Sample-dependent localized upper-deviation bad-event mass is controlled by pointwise sample-dependent bad-event masses |
| PAC-Bayes, stability | `localizedSampleDependentUpperDeviationBadEventMass_le_sum_shiftedExpMoment` | theorem | `FormalSLT/Rademacher/Localized.lean:1137` | Sample-dependent localized bad-event mass controlled by summed shifted exponential-moment budgets |
| tail bound, PAC-Bayes, stability | `localizedSampleDependentUpperDeviationBadEventMass_le_sum_tails` | theorem | `FormalSLT/Rademacher/Localized.lean:1118` | Sample-dependent localized bad-event mass controlled by supplied pointwise tail budgets |
| PAC-Bayes, stability | `localizedSampleDependentUpperDeviationEvent` | theorem | `FormalSLT/Rademacher/Localized.lean:470` | Sample-dependent localized upper-deviation event for random-threshold arguments |
| PAC-Bayes, Rademacher, stability | `localizedSecondMomentEmpiricalRademacherComplexity_le_of_fixedPointCertificate` | theorem | `FormalSLT/Rademacher/Localized.lean:382` | Envelope bound plus fixed-point certificate controls second-moment localized empirical complexity by its radius |
| PAC-Bayes, stability, risk | `localizedUpperDeviation` | theorem | `FormalSLT/Rademacher/Localized.lean:441` | Finite localized supremum of population-minus-empirical excess-risk gaps |
| PAC-Bayes, stability | `localizedUpperDeviationBadEventMass` | theorem | `FormalSLT/Rademacher/Localized.lean:516` | Finite weighted mass outside the localized upper-deviation event |
| PAC-Bayes, stability | `localizedUpperDeviationBadEventMass_finiteProduct_le_delta_boundedExcess` | theorem | `FormalSLT/Rademacher/Localized.lean:1230` | Delta-form iid product-weight localized concentration bound under pointwise [-1,1] excess-loss assumptions |
| PAC-Bayes, stability | `localizedUpperDeviationBadEventMass_finiteProduct_le_sum_boundedExcess` | theorem | `FormalSLT/Rademacher/Localized.lean:1200` | Iid product-weight localized bad-event mass bound under pointwise [-1,1] excess-loss assumptions |
| tail bound, PAC-Bayes, stability | `localizedUpperDeviationBadEventMass_le_delta` | theorem | `FormalSLT/Rademacher/Localized.lean:1251` | Delta-form finite localized concentration adapter from supplied pointwise tail budgets |
| PAC-Bayes, stability | `localizedUpperDeviationBadEventMass_le_sum_expMoment_div` | theorem | `FormalSLT/Rademacher/Localized.lean:865` | Localized bad-event mass controlled by summed pointwise exponential-moment budgets |
| union bound, PAC-Bayes, stability | `localizedUpperDeviationBadEventMass_le_sum_pointwise` | theorem | `FormalSLT/Rademacher/Localized.lean:768` | Finite weighted union bound: localized upper-deviation bad-event mass is controlled by pointwise localized bad-event masses |
| tail bound, PAC-Bayes, stability | `localizedUpperDeviationBadEventMass_le_sum_tails` | theorem | `FormalSLT/Rademacher/Localized.lean:848` | Localized bad-event mass controlled by supplied pointwise tail budgets |
| PAC-Bayes, stability | `localizedUpperDeviationEvent` | theorem | `FormalSLT/Rademacher/Localized.lean:458` | Sample event where the localized upper-deviation statistic is bounded |
| McDiarmid, tail bound, PAC-Bayes, stability | `mcdiarmid_inequality_iid_const_width` | theorem | `FormalSLT/Stability/BousquetElisseeff.lean:104` | Iid bounded-differences upper tail with the sharp McDiarmid constant |
| MGF, PAC-Bayes, stability | `oneCoordinate_boundedLoss_mgf` | theorem | `FormalSLT/PACBayesBoundedLoss.lean:135` | [0,1] bounded-loss one-coordinate MGF instantiation |
| PAC-Bayes, ERM, stability, risk | `pac_bayes_generalization` | theorem | `FormalSLT/PACBayesBoundedLoss.lean:930` | Closed PAC-Bayes good-event theorem: with product-sample mass at least 1 - delta, every posterior satisfies the Catoni-form risk bound |
| PAC-Bayes, KL divergence, stability | `pacbayes_changeOfMeasure` | theorem | `FormalSLT/PACBayesMcAllester.lean:86` | Rescaled finite Donsker-Varadhan change-of-measure inequality |
| MGF, PAC-Bayes, ERM, stability | `pacbayes_mcallester_deterministic` | theorem | `FormalSLT/PACBayesMcAllester.lean:120` | Deterministic PAC-Bayes posterior bound from a prior log-MGF certificate |
| MGF, PAC-Bayes, ERM, stability | `pacbayes_mcallester_sqrt` | theorem | `FormalSLT/PACBayesMcAllester.lean:242` | Deterministic sqrt-form bound under a uniform-in-λ MGF certificate |
| sub-Gaussian, PAC-Bayes, ERM, stability | `pacbayes_mcallester_subGaussian` | theorem | `FormalSLT/PACBayesMcAllester.lean:144` | Fixed-λ sub-Gaussian deterministic PAC-Bayes bound |
| Bernstein, PAC-Bayes, ERM, stability | `posteriorGeneralizationGap_le_bernstein_of_priorBernsteinExpMoment_le` | theorem | `FormalSLT/PACBayesBernstein.lean:227` | Deterministic fixed-sample PAC-Bayes Bernstein adapter from a prior-moment certificate |
| PAC-Bayes, stability | `posteriorMarginVarianceProxy` | theorem | `FormalSLT/PACBayesBernstein.lean:64` | Posterior average of a supplied per-hypothesis margin-variance proxy |
| MGF, PAC-Bayes, ERM, stability, risk | `posteriorRisk_bound_of_priorDeviationMGF_le` | theorem | `FormalSLT/PACBayesBoundedLoss.lean:313` | Deterministic posterior-risk adapter from a prior MGF certificate |
| MGF, PAC-Bayes, ERM, stability, risk | `posteriorRisk_bound_of_priorDeviationMGF_le_complexity_sqrt` | theorem | `FormalSLT/PACBayesBoundedLoss.lean:514` | Deterministic fixed-budget McAllester-style posterior-risk adapter |
| MGF, PAC-Bayes, stability | `priorAveraged_boundedLoss_mgf` | theorem | `FormalSLT/PACBayesBoundedLoss.lean:229` | Prior-averaged bounded-loss MGF bound |
| Markov, MGF, PAC-Bayes, stability | `priorAveraged_boundedLoss_mgf_badEventMass_le_delta` | theorem | `FormalSLT/PACBayesBoundedLoss.lean:261` | Finite Markov bad-event bound for the prior MGF |
| Bernstein, PAC-Bayes, ERM, stability | `priorBernsteinExpMoment` | theorem | `FormalSLT/PACBayesBernstein.lean:79` | Normalized Bernstein prior exponential moment with variance and scale terms |
| MGF, PAC-Bayes, stability | `sampleAverage_boundedLoss_mgf` | theorem | `FormalSLT/PACBayesBoundedLoss.lean:206` | Finite sample-average bounded-loss MGF bound |
| McDiarmid, PAC-Bayes, ERM, stability | `stability_genGap_hasBoundedDifferences` | theorem | `FormalSLT/AlgorithmicStability.lean:550` | Uniform stability gives bounded differences for the gen gap scaffold |
| McDiarmid, PAC-Bayes, stability | `trainingLoss_hasBoundedDifferences` | theorem | `FormalSLT/AlgorithmicStability.lean:463` | Uniform stability gives bounded differences for training loss |
| covering / chaining | `TwoPoint` | definition | `FormalSLT/Covering/TwoPointDudley.lean:27` | The two-point discrete metric index type |
| covering / chaining | `twoPointDist_nonneg` | definition | `FormalSLT/Covering/TwoPointDudley.lean:33` | The two-point discrete metric is nonnegative |
| covering / chaining | `twoPointDist_symm` | definition | `FormalSLT/Covering/TwoPointDudley.lean:36` | The two-point discrete metric is symmetric |
| covering / chaining | `twoPointDist_triangle` | definition | `FormalSLT/Covering/TwoPointDudley.lean:40` | The two-point discrete metric satisfies the triangle inequality |
| Rademacher, covering / chaining | `twoPointDudleyInstance` | definition | `FormalSLT/Covering/TwoPointDudley.lean:220` | Packaged finite dyadic Dudley instance for the two-point Rademacher process |
| covering / chaining | `twoPointDyadicNet` | definition | `FormalSLT/Covering/TwoPointDudley.lean:102` | Full two-point finite net with dyadic positive radius |
| covering / chaining | `twoPointDyadicNetSequence` | definition | `FormalSLT/Covering/TwoPointDudley.lean:174` | A second concrete FiniteDyadicNetSequence instantiation, independent of [0,1] |
| covering / chaining | `twoPointDyadicNet_coverCount_le` | definition | `FormalSLT/Covering/TwoPointDudley.lean:166` | Adjacent two-point covering-number products are bounded by the constant cover-count envelope |
| covering / chaining | `twoPointDyadicNet_pair_card_gt_one` | definition | `FormalSLT/Covering/TwoPointDudley.lean:150` | Adjacent two-point projection-pair families are nontrivial |
| covering / chaining | `twoPointDyadicNet_radius_geometric` | definition | `FormalSLT/Covering/TwoPointDudley.lean:124` | Adjacent two-point dyadic radii satisfy the geometric chaining budget |
| sub-Gaussian, Rademacher, covering / chaining | `twoPointRademacherProcess` | definition | `FormalSLT/Covering/TwoPointDudley.lean:89` | The two-point Rademacher process packaged as a finite sub-Gaussian process |
| Rademacher, covering / chaining | `twoPointRademacherSupAdapter` | definition | `FormalSLT/Covering/TwoPointDudley.lean:265` | Supplied-supremum adapter for the two-point packaged Dudley instance |
| Rademacher, covering / chaining | `twoPointRademacherSup_dudley_m_bound` | definition | `FormalSLT/Covering/TwoPointDudley.lean:275` | Supplied-supremum finite Dudley bound routed through the packaged finite dyadic Dudley API |
| Rademacher, covering / chaining, ERM | `twoPointRademacherSup_le_projectedSup` | definition | `FormalSLT/Covering/TwoPointDudley.lean:248` | Terminal projected-net adapter for the two-point supplied supremum |
| Rademacher, covering / chaining | `twoPointRademacher_projected_dudley_m_bound` | definition | `FormalSLT/Covering/TwoPointDudley.lean:229` | Arbitrary finite-horizon projected Dudley bound routed through the packaged finite dyadic Dudley API |
| sub-Gaussian, MGF, Rademacher, covering / chaining | `twoPoint_rademacher_mgf_bound` | definition | `FormalSLT/Covering/TwoPointDudley.lean:52` | One-coordinate Rademacher process increments satisfy the sub-Gaussian MGF bound |
| confidence sequence | `FiniteClassConfidenceSequence` | theorem | `FormalSLT/UniformConvergence.lean:3641` | Bundled assumptions for the [0,1] finite-class dyadic confidence sequence |
| confidence sequence | `FiniteClassConfidenceSequence.failure_probability_le` | theorem | `FormalSLT/UniformConvergence.lean:3718` | Bundled API theorem bounding the named confidence-sequence failure event |
| Hoeffding, confidence sequence | `anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_confidenceSequence_fromHoeffding` | theorem | `FormalSLT/UniformConvergence.lean:3663` | Confidence-sequence failure-probability theorem for all natural times and finite hypotheses |
| Hoeffding, confidence sequence | `anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_namedRadius_exists_fromHoeffding` | theorem | `FormalSLT/UniformConvergence.lean:3582` | Existential-event anytime theorem using the named dyadic confidence radius |
| Hoeffding, confidence sequence | `anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_timeVaryingRadius_exists_fromHoeffding` | theorem | `FormalSLT/UniformConvergence.lean:3518` | Existential-event version of the countable-time finite-class Hoeffding theorem |
| Hoeffding, confidence sequence | `anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_timeVaryingRadius_fromHoeffding` | theorem | `FormalSLT/UniformConvergence.lean:3318` | Countable-time finite-class Hoeffding theorem for [0,1] losses with dyadic per-time radii |
| union bound, Glivenko-Cantelli | `countableTimeClassTwoSidedUniformDeviationUnionBound_dyadicBudget_threshold` | theorem | `FormalSLT/UniformConvergence.lean:307` | Countable-time dyadic absolute-deviation shell with time-varying thresholds |
| union bound | `countableTimeClassUnionBound_dyadicBudget` | theorem | `FormalSLT/UniformConvergence.lean:286` | Countable-time finite-class union shell using the standard dyadic schedule |
| union bound | `countableTimeClassUnionBound_timeBudget` | theorem | `FormalSLT/UniformConvergence.lean:260` | Countable-time finite-class union shell with a supplied summable time-budget sequence |
|  | `countableTimeClass_iUnion_eq_exists` | theorem | `FormalSLT/UniformConvergence.lean:322` | Rewrites a countable time-class indexed union as an existential event |
|  | `countableTimeClass_not_forall_lt_eq_exists_ge` | theorem | `FormalSLT/UniformConvergence.lean:346` | Rewrites failure of an all-times/all-hypotheses strict bound as an existential crossing event |
| Hoeffding, tail bound | `empiricalAverageLowerHoeffdingTail` | theorem | `FormalSLT/UniformConvergence.lean:792` | Named ENNReal lower-tail budget produced by the fixed-hypothesis Hoeffding wrapper |
|  | `empiricalAverageRangeSum_le_card_mul_uniformRange` | theorem | `FormalSLT/UniformConvergence.lean:1057` | Finite-sum range envelope from a pointwise uniform range-width bound |
|  | `empiricalAverageRangeSum_pos_of_exists_range_pos` | theorem | `FormalSLT/UniformConvergence.lean:1082` | Positive finite-sum denominator certificate from one sampled coordinate with positive range |
| Hoeffding, tail bound | `empiricalAverageTwoSidedHoeffdingTail` | theorem | `FormalSLT/UniformConvergence.lean:817` | Combined two-sided empirical-average Hoeffding budget |
| Hoeffding, tail bound | `empiricalAverageTwoSidedHoeffdingTail_le_uniformRangeTwoSidedHoeffdingTail` | theorem | `FormalSLT/UniformConvergence.lean:1014` | Algebraic bridge from the concrete finite sum of squared half-ranges to the uniform range proxy |
| Hoeffding, tail bound | `empiricalAverageTwoSidedHoeffdingTail_le_uniformRangeTwoSidedHoeffdingTail_of_rangeBound` | theorem | `FormalSLT/UniformConvergence.lean:1107` | Two-sided Hoeffding tail bridge from a pointwise range-width bound and closed-form proxy |
| Hoeffding, tail bound | `empiricalAverageTwoSidedHoeffdingTail_le_uniformRangeTwoSidedHoeffdingTail_of_rangeBound_of_exists_range_pos` | theorem | `FormalSLT/UniformConvergence.lean:1131` | Two-sided Hoeffding tail bridge using pointwise range width and an explicit nondegenerate sample coordinate |
|  | `empiricalAverageUniformRangeSampleSize_ge_of_sqrtBudget_le` | theorem | `FormalSLT/UniformConvergence.lean:2124` | Algebraic bridge from a square-root radius condition to the displayed sample-size lower bound |
| Hoeffding, tail bound | `empiricalAverageUniformRangeTwoSidedHoeffdingSampleSizeTail` | theorem | `FormalSLT/UniformConvergence.lean:839` | Displayed two-sided Hoeffding budget 2 * exp(-2 * sampleSize * ε^2 / R^2) |
| Hoeffding, tail bound, confidence sequence | `empiricalAverageUniformRangeTwoSidedHoeffdingSampleSizeTail_le_of_explicitRadius` | theorem | `FormalSLT/UniformConvergence.lean:903` | Unit-range displayed Hoeffding tail is bounded at the inverted square-root confidence radius |
| Hoeffding, tail bound | `empiricalAverageUniformRangeTwoSidedHoeffdingSampleSizeTail_le_of_logBudget` | theorem | `FormalSLT/UniformConvergence.lean:870` | Real log-budget condition implies the displayed Hoeffding tail fits a target budget |
| Hoeffding, tail bound | `empiricalAverageUniformRangeTwoSidedHoeffdingSampleSizeTail_le_of_sampleSize_ge` | theorem | `FormalSLT/UniformConvergence.lean:972` | Explicit sample-size lower bound implies the displayed Hoeffding tail fits a target budget |
| Hoeffding, tail bound | `empiricalAverageUniformRangeTwoSidedHoeffdingTail` | theorem | `FormalSLT/UniformConvergence.lean:827` | Uniform-range two-sided empirical-average Hoeffding budget with one denominator proxy |
| Hoeffding, tail bound | `empiricalAverageUniformRangeTwoSidedHoeffdingTail_eq_sampleSizeTail` | theorem | `FormalSLT/UniformConvergence.lean:848` | Algebraic identification between the range-proxy budget and the sample-size display |
| Hoeffding, tail bound | `empiricalAverageUpperHoeffdingTail` | theorem | `FormalSLT/UniformConvergence.lean:780` | Named ENNReal upper-tail budget produced by the fixed-hypothesis Hoeffding wrapper |
| Hoeffding, tail bound | `empiricalAverageUpperHoeffdingTail_eq_lower` | theorem | `FormalSLT/UniformConvergence.lean:804` | Normalizes the upper-tail Hoeffding range expression to the lower-tail expression |
| confidence sequence | `finiteClassConfidenceSequenceFailureEvent` | theorem | `FormalSLT/UniformConvergence.lean:3624` | Named failure event for the [0,1] finite-class dyadic confidence sequence |
| union bound, Glivenko-Cantelli | `finiteClassTwoSidedUniformDeviationUnionBound` | theorem | `FormalSLT/UniformConvergence.lean:86` | Pointwise absolute-deviation tails imply a simultaneous finite-class bound |
| union bound, Glivenko-Cantelli | `finiteClassTwoSidedUniformDeviationUnionBound_cardInv` | theorem | `FormalSLT/UniformConvergence.lean:99` | Equal-budget absolute-deviation bridge for finite hypothesis classes |
| union bound, tail bound, Glivenko-Cantelli | `finiteClassUniformDeviationUnionBound` | theorem | `FormalSLT/UniformConvergence.lean:48` | Pointwise finite-class bad-event tails imply a simultaneous card * tail bound |
| union bound, Glivenko-Cantelli | `finiteClassUniformDeviationUnionBound_cardInv` | theorem | `FormalSLT/UniformConvergence.lean:68` | Equal split of a target failure budget gives simultaneous mass ≤ δ |
|  | `finiteDyadicRealBudget_classBudget_ofReal` | theorem | `FormalSLT/UniformConvergence.lean:1945` | Concrete real dyadic class budget maps exactly to the ENNReal dyadic time/class split |
|  | `finiteDyadicRealBudget_horizon_le_time` | theorem | `FormalSLT/UniformConvergence.lean:2239` | Finite-horizon dyadic real-budget monotonicity: the horizon budget is no larger than any prefix time budget |
| ERM | `finiteDyadicRealBudget_horizon_logBudget_eq_closedForm` | theorem | `FormalSLT/UniformConvergence.lean:2404` | Closed-form rewrite of the finite-horizon dyadic log-budget term |
|  | `finiteDyadicTimeBudget` | theorem | `FormalSLT/UniformConvergence.lean:224` | Standard dyadic time-budget schedule δ * 2^(-1-t) |
|  | `finiteDyadicTimeBudget_sum_fin_le` | theorem | `FormalSLT/UniformConvergence.lean:228` | Every finite prefix of the dyadic time-budget schedule sums to at most δ |
|  | `finiteDyadicTimeBudget_tsum_le` | theorem | `FormalSLT/UniformConvergence.lean:244` | The full natural-time dyadic schedule has total budget at most δ |
| Hoeffding | `finitePrefixFiniteClassDeviationFromHoeffding_closedForm` | theorem | `FormalSLT/UniformConvergence.lean:2645` | Route-facing finite-prefix finite-class Hoeffding deviation theorem with the closed-form sample-size condition |
| Hoeffding | `finitePrefixFiniteClassDeviationFromHoeffding_closedForm_cardSample` | theorem | `FormalSLT/UniformConvergence.lean:2702` | Route-facing finite-prefix finite-class Hoeffding theorem with denominator written directly as (s.card : ℝ) |
| Hoeffding | `finitePrefixFiniteClassDeviationFromHoeffding_closedForm_unitRange` | theorem | `FormalSLT/UniformConvergence.lean:2766` | Route-facing unit-range finite-prefix finite-class Hoeffding theorem with compact log(card/time/budget) / (2 * ε^2) sample-size condition |
| Hoeffding, confidence sequence | `finitePrefixFiniteClassDeviationFromHoeffding_unitRange_explicitRadius` | theorem | `FormalSLT/UniformConvergence.lean:2906` | Route-facing unit-range finite-prefix finite-class Hoeffding theorem with the confidence radius written directly in the deviation event |
| Hoeffding | `finitePrefixFiniteClassDeviationFromHoeffding_unitRange_explicitRadius_nonemptySample` | theorem | `FormalSLT/UniformConvergence.lean:2974` | Route-facing explicit-radius theorem with radius positivity discharged by nonempty sample and strict finite-prefix budget assumptions |
| Hoeffding, confidence sequence | `finitePrefixFiniteClassDeviationFromHoeffding_unitRange_radius` | theorem | `FormalSLT/UniformConvergence.lean:2835` | Route-facing unit-range finite-prefix finite-class Hoeffding theorem in confidence-radius form |
| Hoeffding | `finitePrefixFiniteClassDeviationFromHoeffding_zeroOneRange_explicitRadius` | theorem | `FormalSLT/UniformConvergence.lean:3057` | Route-facing explicit-radius theorem for losses bounded in [0,1], removing caller-supplied lower and upper range functions and discharging the negative-integral identity internally |
| Hoeffding | `finitePrefixFiniteClassDeviationFromHoeffding_zeroOneRange_timeVaryingRadius` | theorem | `FormalSLT/UniformConvergence.lean:3127` | Finite-prefix time-varying dyadic-radius event from supplied pointwise tails and checked dyadic budget conversion |
| Hoeffding | `finitePrefixFiniteClassDeviationFromHoeffding_zeroOneRange_timeVaryingRadius_fromHoeffding` | theorem | `FormalSLT/UniformConvergence.lean:3202` | Finite-prefix time-varying dyadic-radius theorem for [0,1] losses with the pointwise tails discharged from Hoeffding |
| Hoeffding | `finiteTimeClassEmpiricalAverageDeviationFromHoeffding_dyadicBudget` | theorem | `FormalSLT/UniformConvergence.lean:1161` | Finite-prefix dyadic finite-class deviation bound from bounded independent empirical-average losses |
| Hoeffding | `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_closedFormHorizonRadius_dyadicRealBudget` | theorem | `FormalSLT/UniformConvergence.lean:2439` | Shared-sample finite-prefix wrapper using a closed-form horizon/class/budget radius |
| Hoeffding | `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_closedFormHorizonSampleSize_dyadicRealBudget` | theorem | `FormalSLT/UniformConvergence.lean:2513` | Shared-sample finite-prefix wrapper using a closed-form horizon/class/budget sample-size condition |
| Hoeffding | `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_dyadicBudget` | theorem | `FormalSLT/UniformConvergence.lean:1252` | Shared-sample finite-prefix wrapper for bounded independent empirical-average losses |
| Hoeffding | `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_epsilonOfSampleSize_dyadicRealBudget` | theorem | `FormalSLT/UniformConvergence.lean:2162` | Shared-sample finite-prefix wrapper using a radius-style condition and the concrete dyadic real budget |
| Hoeffding | `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_horizonUniformRadius_dyadicRealBudget` | theorem | `FormalSLT/UniformConvergence.lean:2278` | Shared-sample finite-prefix wrapper using one horizon-level radius condition |
| Hoeffding | `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize` | theorem | `FormalSLT/UniformConvergence.lean:1566` | Shared-sample finite-prefix wrapper using the displayed sample-size Hoeffding budget |
| Hoeffding | `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize_dyadicRealBudget` | theorem | `FormalSLT/UniformConvergence.lean:2002` | Shared-sample finite-prefix wrapper using explicit sample-size lower bounds and the concrete dyadic real budget δ * 2^(-1-t) / card(H) |
| Hoeffding | `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize_from_logBudget` | theorem | `FormalSLT/UniformConvergence.lean:1800` | Shared-sample finite-prefix wrapper using real log budgets below the dyadic ENNReal budget split |
| Hoeffding | `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize_ge` | theorem | `FormalSLT/UniformConvergence.lean:1872` | Shared-sample finite-prefix wrapper using explicit sample-size lower bounds and real budgets |
| Hoeffding | `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize_threshold` | theorem | `FormalSLT/UniformConvergence.lean:1638` | Shared-sample finite-prefix wrapper using a displayed sample-size Hoeffding budget and time-varying thresholds |
| Hoeffding | `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_twoSidedTailBudget` | theorem | `FormalSLT/UniformConvergence.lean:1308` | Shared-sample finite-prefix wrapper using one combined two-sided Hoeffding budget |
| Hoeffding | `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_uniformRangeBudget` | theorem | `FormalSLT/UniformConvergence.lean:1373` | Shared-sample finite-prefix wrapper using one uniform range proxy and dyadic time budgets |
| Hoeffding | `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_uniformRangeBudget_of_rangeBound` | theorem | `FormalSLT/UniformConvergence.lean:1435` | Shared-sample finite-prefix wrapper with pointwise uniform range width and one closed-form proxy |
| Hoeffding | `finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_uniformRangeBudget_of_rangeBound_of_exists_range_pos` | theorem | `FormalSLT/UniformConvergence.lean:1501` | Shared-sample finite-prefix wrapper with pointwise uniform range width and nondegenerate sample-coordinate certificates |
| union bound, Glivenko-Cantelli | `finiteTimeClassTwoSidedUniformDeviationUnionBound_cardInv` | theorem | `FormalSLT/UniformConvergence.lean:132` | Finite-horizon absolute-deviation shell over all (time, hypothesis) pairs |
| union bound, Glivenko-Cantelli | `finiteTimeClassTwoSidedUniformDeviationUnionBound_dyadicBudget` | theorem | `FormalSLT/UniformConvergence.lean:377` | Finite-prefix absolute-deviation shell using the standard dyadic schedule |
| union bound, Glivenko-Cantelli | `finiteTimeClassTwoSidedUniformDeviationUnionBound_dyadicBudget_threshold` | theorem | `FormalSLT/UniformConvergence.lean:395` | Finite-prefix dyadic absolute-deviation shell with time-varying thresholds |
| union bound, Glivenko-Cantelli | `finiteTimeClassTwoSidedUniformDeviationUnionBound_timeBudget` | theorem | `FormalSLT/UniformConvergence.lean:176` | Finite-horizon absolute-deviation shell with a supplied time-budget sequence |
| union bound, Glivenko-Cantelli | `finiteTimeClassTwoSidedUniformDeviationUnionBound_timeBudget_threshold` | theorem | `FormalSLT/UniformConvergence.lean:200` | Finite-horizon absolute-deviation shell with a threshold depending on (time, hypothesis) |
| union bound | `finiteTimeClassTwoSidedUnionBoundFromOneSidedTails_dyadicBudget` | theorem | `FormalSLT/UniformConvergence.lean:446` | Finite-prefix dyadic shell from one-sided upper and lower pointwise tails |
| union bound | `finiteTimeClassUnionBound_cardInv` | theorem | `FormalSLT/UniformConvergence.lean:114` | Equal-budget union bound over a finite time horizon and finite hypothesis class |
| union bound | `finiteTimeClassUnionBound_dyadicBudget` | theorem | `FormalSLT/UniformConvergence.lean:360` | Finite-prefix time-class union shell using the standard dyadic schedule |
| union bound | `finiteTimeClassUnionBound_timeBudget` | theorem | `FormalSLT/UniformConvergence.lean:151` | Finite time budgets whose sum is ≤ δ, with each time split across hypotheses |
| confidence sequence | `zeroOneDyadicFiniteClassConfidenceRadius` | theorem | `FormalSLT/UniformConvergence.lean:333` | Named dyadic confidence radius for [0,1] finite-class empirical-average deviations |
| confidence sequence | `zeroOneDyadicFiniteClassConfidenceRadius_le_of_sampleSize_ge` | theorem | `FormalSLT/UniformConvergence.lean:3748` | Sample-size lower bound implies the named dyadic confidence radius is at most a target ε |
| covering / chaining | `UnitInterval` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:31` | The closed interval [0,1] as a metric index type |
| covering / chaining | `monotone_unitIntervalRoundedDyadicGridCoverCount` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1189` | Rounded dyadic adjacent-level cover counts are monotone in the scale |
| covering / chaining | `monotone_unitIntervalRoundedDyadicGridEntropy` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1206` | Rounded dyadic entropy-at-scale sequence is monotone |
| covering / chaining | `unitIntervalDyadicFiniteNet_covers` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:76` | Dyadic total-bounded finite net covers the unit interval at the dyadic chaining radius |
| covering / chaining | `unitIntervalDyadicGridCenter_leftEndpoint` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:119` | The reusable dyadic grid center map contains the left endpoint |
| covering / chaining | `unitIntervalDyadicGridCenter_rightEndpoint` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:127` | The reusable dyadic grid center map contains the right endpoint |
| covering / chaining | `unitIntervalDyadicGridFloorProject` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:157` | Floor projection from [0,1] to the level-k dyadic grid |
| covering / chaining | `unitIntervalDyadicGridFloorProject_dist_le` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:177` | Floor-projected dyadic grid covers [0,1] at spacing radius 1 / 2^k |
| covering / chaining | `unitIntervalDyadicGridNet_coveringNumber` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:267` | Generic dyadic finite net has 2^k + 1 centers |
| covering / chaining | `unitIntervalDyadicGridNet_coveringNumberPair_zero` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:286` | Level-1 and level-2 generic dyadic finite-net covering-number product is the first dyadic pair count |
| covering / chaining | `unitIntervalDyadicGridNet_coveringNumber_one` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:273` | Level-1 generic dyadic finite net has 3 centers |
| covering / chaining | `unitIntervalDyadicGridNet_coveringNumber_two` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:279` | Level-2 generic dyadic finite net has 5 centers |
| covering / chaining | `unitIntervalDyadicGridNet_covers` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:261` | Generic dyadic finite net covers [0,1] at spacing radius 1 / 2^k |
| covering / chaining | `unitIntervalDyadicGridPairCoverCount_zero` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:151` | The first adjacent dyadic grid pair count is 15 |
| covering / chaining | `unitIntervalDyadicGridRoundProject` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:296` | Rounded nearest-grid projection from [0,1] to the level-k dyadic grid |
| covering / chaining | `unitIntervalDyadicGridRoundProject_dist_le` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:323` | Rounded dyadic grid covers [0,1] at half-spacing radius 1 / 2^(k+1) |
| covering / chaining | `unitIntervalDyadicGridRoundProject_one` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:397` | Rounded dyadic projection fixes the right endpoint |
| covering / chaining | `unitIntervalDyadicGridRoundProject_zero` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:388` | Rounded dyadic projection fixes the left endpoint |
| covering / chaining | `unitIntervalDyadicGrid_card` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:139` | Level-k dyadic grid has cardinality 2^k + 1 |
| covering / chaining | `unitIntervalDyadicRoundedGridNet_coveringNumber` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:441` | Rounded generic dyadic finite net has 2^k + 1 centers |
| covering / chaining | `unitIntervalDyadicRoundedGridNet_coveringNumberPair_zero` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:460` | Level-1 and level-2 rounded dyadic finite-net covering-number product is the first dyadic pair count |
| covering / chaining | `unitIntervalDyadicRoundedGridNet_coveringNumber_one` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:447` | Level-1 rounded dyadic finite net has 3 centers |
| covering / chaining | `unitIntervalDyadicRoundedGridNet_coveringNumber_two` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:453` | Level-2 rounded dyadic finite net has 5 centers |
| covering / chaining | `unitIntervalDyadicRoundedGridNet_covers` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:435` | Rounded generic dyadic finite net covers [0,1] at half-spacing radius 1 / 2^(k+1) |
| covering / chaining | `unitIntervalFiniteNet_covers` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:61` | Total-bounded finite net covers the unit interval at a supplied radius |
| covering / chaining | `unitIntervalHalfMeshNet_coveringNumber` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:600` | Explicit half mesh has covering number 3 |
| covering / chaining | `unitIntervalHalfMeshNet_covers` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:595` | Explicit three-point mesh covers [0,1] at radius 1/4 |
| covering / chaining | `unitIntervalHalfQuarterPair_card_gt_one` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:605` | Adjacent half/quarter projection-pair family is nontrivial |
| covering / chaining | `unitIntervalHalfQuarter_coveringNumber_product` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:626` | Half/quarter covering-number product is 15 |
| covering / chaining | `unitIntervalHalfQuarter_coveringNumber_product_eq_dyadicGridPairCoverCount_zero` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:634` | The half/quarter product is identified with the first adjacent dyadic grid pair count |
| covering / chaining, ERM | `unitIntervalQuarterMeshNet_coveringNumber` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:541` | Explicit quarter mesh has covering number 5 |
| covering / chaining, ERM | `unitIntervalQuarterMeshNet_covers` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:536` | Explicit five-point mesh covers [0,1] at radius 1/8 |
| sub-Gaussian, MGF, Rademacher, covering / chaining | `unitIntervalRademacherLinearProcess_increment_mgf` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:817` | The packaged finite sub-Gaussian process has the required increment MGF |
| Rademacher, covering / chaining | `unitIntervalRademacherLinearSupRoundedDyadicGridAdapter` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1883` | Supplied-supremum adapter for the packaged rounded unit-interval Dudley instance |
| Rademacher, covering / chaining | `unitIntervalRademacherLinearSup_attained` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:939` | The supplied supremum is attained at an endpoint |
| Rademacher, covering / chaining | `unitIntervalRademacherLinearSup_dudley_m0_bound` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:2178` | Coarse finite-horizon m = 0 Dudley bound for the supplied supremum |
| Rademacher, covering / chaining | `unitIntervalRademacherLinearSup_dudley_m1_bound_constEntropy_eval` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:2497` | Constant-envelope first-scale bound evaluated to a scalar expression |
| Rademacher, covering / chaining | `unitIntervalRademacherLinearSup_dudley_m1_bound_of_entropy` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:2349` | First-scale supplied-supremum Dudley bound under an explicit entropy envelope |
| Rademacher, covering / chaining | `unitIntervalRademacherLinearSup_expectation` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:912` | The supplied supremum has expectation 1/2 |
| Rademacher, covering / chaining | `unitIntervalRademacherLinearSup_isLUB_range` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:967` | The supplied supremum is the least upper bound of the actual process range |
| Rademacher, covering / chaining | `unitIntervalRademacherLinearSup_isLeastUpperBound` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:953` | The supplied supremum is the least upper bound over the non-finite unit-interval family |
| Rademacher, covering / chaining | `unitIntervalRademacherLinearSup_le_projectedRoundedDyadicGridSup` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1789` | Endpoint adapter from the supplied supremum to any rounded dyadic projected finite supremum |
| Rademacher, covering / chaining, ERM | `unitIntervalRademacherLinearSup_projectedQuarterMesh_dudley_log15_bound` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1761` | The nonzero supplied supremum routes through the projected quarter-mesh Dudley bound |
| Rademacher, covering / chaining, ERM | `unitIntervalRademacherLinearSup_projectedQuarterMesh_dudley_log15_bound_eval` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:2155` | The projected quarter-mesh supplied-supremum bound evaluated to 1 + sqrt 2 * sqrt(log 15) |
| Rademacher, covering / chaining | `unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_log15_bound` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1963` | The nonzero supplied supremum routes through the rounded generic dyadic-grid Dudley bound |
| Rademacher, covering / chaining | `unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_log15_bound_eval` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:2141` | The rounded-grid supplied-supremum bound evaluated to 1 + sqrt 2 * sqrt(log 15) |
| Rademacher, covering / chaining | `unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m2_bound` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:2054` | The nonzero supplied supremum routes through the m = 2 rounded dyadic-grid Dudley bound |
| Rademacher, covering / chaining | `unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m3_bound` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:2128` | Named m = 3 supplied-supremum rounded dyadic-grid Dudley corollary |
| Rademacher, covering / chaining | `unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m_bound` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:2088` | Arbitrary finite-horizon rounded dyadic-grid Dudley bound for the supplied supremum routed through the packaged API |
| Rademacher, covering / chaining | `unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m_bound_prefixFree` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:2113` | Arbitrary finite-horizon supplied-supremum rounded-grid Dudley bound with the prefix-sup envelope removed |
| Rademacher, covering / chaining | `unitIntervalRademacherLinearSup_sSup_range` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:983` | The supplied supremum equals the order supremum of the actual process range |
| Rademacher, covering / chaining | `unitIntervalRademacherLinearSup_upper` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:926` | The supplied supremum upper-bounds the full non-finite unit-interval family |
| Rademacher, covering / chaining, ERM | `unitIntervalRademacherLinear_halfQuarter_increment_log15_bound` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:833` | Half/quarter projection-pair increment pays the concrete log 15 entropy term |
| Rademacher, covering / chaining, ERM | `unitIntervalRademacherLinear_projectedQuarterMesh_dudley_log15_bound` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1139` | Projected quarter-mesh supremum satisfies the finite-net Dudley bound with a sqrt(log 15) prefix envelope |
| Rademacher, covering / chaining | `unitIntervalRademacherLinear_projectedRoundedDyadicGridSup_eq` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1864` | Projected finite supremum over any rounded dyadic grid equals the supplied supremum |
| Rademacher, covering / chaining | `unitIntervalRademacherLinear_roundedDyadicGrid_dudley_log15_bound` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1567` | Rounded generic dyadic-grid projected supremum satisfies the finite-net Dudley bound with a sqrt(log 15) prefix envelope |
| Rademacher, covering / chaining | `unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m2_bound` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1603` | Three-level rounded dyadic-grid projected supremum satisfies the finite-net Dudley bound with reusable adjacent cover counts |
| Rademacher, covering / chaining | `unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m3_bound` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1683` | Named m = 3 projected rounded dyadic-grid Dudley corollary |
| Rademacher, covering / chaining | `unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m_bound` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1641` | Arbitrary finite-horizon rounded dyadic-grid projected supremum Dudley bound routed through the packaged API |
| Rademacher, covering / chaining | `unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m_bound_prefixFree` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1665` | Arbitrary finite-horizon projected rounded-grid Dudley bound with the prefix-sup envelope removed |
| covering / chaining | `unitIntervalRoundedDyadicGridCoverCount` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1184` | Adjacent-level covering-product envelope for the shifted rounded dyadic sequence |
| covering / chaining | `unitIntervalRoundedDyadicGridDudleyInstance` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1555` | Packaged finite dyadic Dudley instance for the rounded unit-interval grid sequence |
| covering / chaining | `unitIntervalRoundedDyadicGridEntropy_prefixSup` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1222` | Prefix-sup envelope collapses for the rounded dyadic entropy sequence |
| covering / chaining | `unitIntervalRoundedDyadicGridIndex` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1174` | Shifted rounded dyadic grid index sequence, starting at level 1 |
| covering / chaining | `unitIntervalRoundedDyadicGridNet` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1179` | Shifted rounded dyadic finite-net sequence for finite-scale Dudley chaining |
| covering / chaining | `unitIntervalRoundedDyadicGridNet_coverCount_le` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1349` | Adjacent rounded dyadic covering-number product is bounded by the cover-count envelope |
| covering / chaining | `unitIntervalRoundedDyadicGridNet_coverCount_le_range` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1379` | Range wrapper for the adjacent rounded-grid covering-product envelope over any finite horizon |
| covering / chaining | `unitIntervalRoundedDyadicGridNet_coveringNumber_product` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1278` | Adjacent rounded dyadic covering-number product equals the reusable cover-count envelope |
| Rademacher, covering / chaining | `unitIntervalRoundedDyadicGridNet_dist` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1231` | Shifted rounded dyadic finite nets use the Rademacher process metric |
| covering / chaining | `unitIntervalRoundedDyadicGridNet_pair_card_gt_one` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1303` | Adjacent rounded dyadic projection-pair family is nontrivial at every scale |
| covering / chaining | `unitIntervalRoundedDyadicGridNet_pair_card_gt_one_range` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1370` | Range wrapper for nontrivial adjacent projection-pair families over any finite horizon |
| covering / chaining | `unitIntervalRoundedDyadicGridNet_radius_geometric` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1246` | Adjacent rounded dyadic radii satisfy the geometric chaining radius budget |
| covering / chaining | `unitIntervalRoundedDyadicGridNet_radius_geometric_range` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1362` | Range wrapper for the geometric radius budget over any finite horizon |
| covering / chaining | `unitIntervalRoundedDyadicGridNet_radius_pos` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1237` | Adjacent rounded dyadic radii have positive sum at every scale |
| covering / chaining | `unitIntervalRoundedDyadicGridNet_radius_pos_range` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:1355` | Range wrapper for positive adjacent rounded dyadic radii over any finite horizon |
| sub-Gaussian, MGF, Rademacher, covering / chaining | `unitInterval_rademacherLinear_mgf_bound` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:755` | Rademacher linear process increment satisfies the sub-Gaussian MGF bound |
| covering / chaining | `unitInterval_totallyBounded_univ` | definition | `FormalSLT/Covering/UnitIntervalDudley.lean:47` | The unit interval is totally bounded |