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.
659 declarations, 659 resolved to a file:line.
- (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 (6):
bennett_mgf,bennett_mgf_le_one_add,bennett_mgf_subgamma,bennett_tail,bennett_taylor_bound,exp_le_quadratic_of_le - Bernoulli (44):
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,fairBoolThreshold_endToEnd_certificate,fairBoolThreshold_twoGaussianSelected_certificate,indicatorBernsteinVarianceProxy_le_risk_div,indicatorBernstein_normalization_eq_budget,indicatorDeviation_centered,indicatorDeviation_secondMoment_eq,indicatorFinitePACBayesBernsteinBadSamples,indicatorFinitePACBayesBernsteinWeightedCatalogBadSamples,indicatorFixedTiltBadSamples_subset_weightedCatalog,indicatorPopulationRisk_mem_Icc,indicator_expectedPriorBernsteinExpMoment_le_one,indicator_finitePACBayesBernstein_fixedLambda_badEventMass_le_delta,indicator_finitePACBayesBernstein_weightedCatalog_badEventMass_le_delta,indicator_mem_weightedCatalog_iff,indicator_not_mem_weightedCatalog_iff,indicator_oneCoordinateDeviationMGF_le,indicator_posteriorGeneralizationGap_le_of_not_mem,indicator_posteriorGeneralizationGap_le_weightedCatalog_of_not_mem,indicator_posteriorRisk_le_weightedLowRiskCatalog_of_not_mem,indicator_posteriorRisk_le_weightedLowRiskCatalog_selected_of_not_mem,indicator_product_mgf_le,indicator_product_normalizedMGF_le_one - Bernstein (32):
BernsteinCondition,averaged_bernstein_tail,bernoulli_bernstein_tail,bernstein_tail,centeredSecondMoment_le_of_bernstein_localized,finiteEmpiricalVariance_expectedPriorBernsteinExpMoment_le_one,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,indicatorBernsteinVarianceProxy_le_risk_div,indicatorBernstein_normalization_eq_budget,indicatorFinitePACBayesBernsteinBadSamples,indicatorFinitePACBayesBernsteinWeightedCatalogBadSamples,indicatorFixedTiltBadSamples_subset_weightedCatalog,indicator_expectedPriorBernsteinExpMoment_le_one,indicator_finitePACBayesBernstein_fixedLambda_badEventMass_le_delta,indicator_finitePACBayesBernstein_twoThirds_badEventMass_le_delta,indicator_finitePACBayesBernstein_weightedCatalog_badEventMass_le_delta,indicator_posteriorGeneralizationGap_le_of_not_mem,indicator_product_mgf_le,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,posteriorIndicatorBernsteinVarianceProxy_le_risk_div,priorBernsteinExpMoment - Chernoff (1):
chernoff_tail - ERM (83):
EpsilonizedSupremumBoundaryChoice,FiniteDyadicDudleyInstance.SupremumAdapter,FixedPointUpperCertificate,IsERM,LocalizedDeviationCertificate,abs_expectedFiniteGeneralizationGap_le_uniformStability_finiteProduct,abs_expectedFiniteGeneralizationGap_le_uniformStability_of_coordinateSwap,atTop_time_uniform_confidence_sequence_subGamma_mixture,average_perm_finiteCanonicalPairMean_eq_sampleVarianceBessel,average_perm_pairCatalog_eq_sampleVarianceBessel,bettingWealth_supermartingale,countableWeightedSupermartingale_tsum,dyadicEpochMixture_supermartingale,eProcess_product_of_supermartingale,empiricalRisk,expectedFiniteGeneralizationGap_le_uniformStability_finiteProduct,expectedFiniteGeneralizationGap_le_uniformStability_of_coordinateSwap,expected_genGap_le_two_expected_empiricalRademacherComplexity,finDiscreteRademacherSup_le_projectedSup,finiteDyadicRealBudget_horizon_logBudget_eq_closedForm,finiteEmpiricalRisk,finiteEmpiricalVariance_le_card_div_pred_mul_empiricalRisk,finiteEmpiricalVariance_normalizedLowerTailMGF_le_one,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,indicator_posteriorGeneralizationGap_le_of_not_mem,indicator_posteriorGeneralizationGap_le_weightedCatalog_of_not_mem,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 (11):
continuousPriorPosterior_certificate_derived,continuous_catoni_changeOfMeasure_bound,finiteEmpiricalVariance_normalizedLowerTailMGF_le_one,indicator_posteriorRisk_le_twoThirds_of_not_mem,klDiv_nonneg,markovPACBayes_prequentialRisk_certificate,markovPosteriorAverageConditionalRisk_lt_of_not_mem,pacbayes_changeOfMeasure,posteriorPopulationVariance_le_empiricalVariance_of_not_mem,sphericalGaussianMeasure_klDiv_toReal_eq,timeUniformIIDGaussianPACBayes_bound - MGF (34):
bennett_mgf,bennett_mgf_le_one_add,bennett_mgf_subgamma,chernoff_tail,condSubGammaMGF_of_bounded_centered_condVariance,continuous_catoni_changeOfMeasure_bound,finDiscrete_rademacher_mgf_bound,finiteEmpiricalVariance_lowerTailMGF_randomMatching,finiteEmpiricalVariance_lowerTailMGF_tolstikhinSeldin,finiteEmpiricalVariance_normalizedLowerTailMGF_le_one,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,indicatorBernstein_normalization_eq_budget,indicator_expectedPriorBernsteinExpMoment_le_one,indicator_oneCoordinateDeviationMGF_le,indicator_product_mgf_le,indicator_product_normalizedMGF_le_one,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 (26):
abs_markovRiskShortfall_le_one,averageConditionalRisk_lt_empiricalPrequentialRisk_add_boundary_of_not_mem,cond_markov_of_nonneg,integrable_markovRiskShortfall,localizedPointwiseUpperDeviationBadEventMass_le_expMoment_div,markovPACBayesAnyPosteriorUpperFailure_subset_processFailure,markovPACBayesExceptionalEvent_mass_le_delta,markovPACBayesExceptionalEvent_measurable,markovPACBayesRawFailure_subset_exceptionalEvent,markovPACBayes_allPosteriors_bound,markovPACBayes_prequentialRisk_certificate,markovPosteriorAverageConditionalRisk_lt_of_not_mem,markovPrequentialRiskExceptionalEvent_mass_le_delta,markovRiskInnovation_condExp_eq_zero,markovRiskInnovation_condSecondMoment_le_one,markovRiskInnovation_condSecondMoment_le_one_fourth,markovRiskShortfall_condExp_eq_zero,markovRiskShortfall_condSecondMoment_le_one_fourth,markovRiskShortfall_incrementAdapted,measurable_markovRiskShortfall,pathSquaredLoss_condExp,posteriorAverage_runningMean_markovRiskShortfall,priorAveraged_boundedLoss_mgf_badEventMass_le_delta,runningMean_markovRiskInnovation,runningMean_markovRiskShortfall,subGammaCgf_oneFourth_one_div - 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 (166):
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_le_one_add,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,fairBoolGaussianPACBayesFailure_mass_ge_twoPowNegHundred,fairBoolThreshold_endToEnd_certificate,fairBoolThreshold_twoGaussianGrid_certificate,fairBoolThreshold_twoGaussianSelected_certificate,finiteCatoni_badEventMass_le_delta,finiteClass_loss_measurable,finiteEmpiricalRisk,finiteEmpiricalVariancePACBayes_badEventMass_le_delta,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,finiteProductSampleWeight_isPMF,finiteProduct_mgf_empiricalRiskDeviation_eq_pow,finiteProduct_mgf_empiricalRiskDeviation_le_of_single,indicatorBernsteinVarianceProxy_le_risk_div,indicatorBernstein_normalization_eq_budget,indicatorDeviation_centered,indicatorDeviation_secondMoment_eq,indicatorFinitePACBayesBernsteinBadSamples,indicatorFinitePACBayesBernsteinWeightedCatalogBadSamples,indicatorFixedTiltBadSamples_subset_weightedCatalog,indicatorPopulationRisk_mem_Icc,indicator_expectedPriorBernsteinExpMoment_le_one,indicator_finitePACBayesBernstein_fixedLambda_badEventMass_le_delta,indicator_finitePACBayesBernstein_twoThirds_badEventMass_le_delta,indicator_finitePACBayesBernstein_weightedCatalog_badEventMass_le_delta,indicator_mem_weightedCatalog_iff,indicator_not_mem_weightedCatalog_iff,indicator_oneCoordinateDeviationMGF_le,indicator_posteriorGeneralizationGap_le_of_not_mem,indicator_posteriorGeneralizationGap_le_weightedCatalog_of_not_mem,indicator_posteriorRisk_le_lowRisk_of_not_mem,indicator_posteriorRisk_le_min_one_twoThirds_of_not_mem,indicator_posteriorRisk_le_twoThirds_of_not_mem,indicator_posteriorRisk_le_weightedLowRiskCatalog_of_not_mem,indicator_posteriorRisk_le_weightedLowRiskCatalog_selected_of_not_mem,indicator_product_mgf_le,indicator_product_normalizedMGF_le_one,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,markovPACBayesAnyPosteriorUpperFailure_subset_processFailure,markovPACBayesExceptionalEvent_mass_le_delta,markovPACBayesExceptionalEvent_measurable,markovPACBayesRawFailure_subset_exceptionalEvent,markovPACBayes_allPosteriors_bound,markovPACBayes_prequentialRisk_certificate,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,posteriorIndicatorBernsteinVarianceProxy_le_risk_div,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,sphericalGaussianMeasure_klDiv_toReal_eq,stability_genGap_hasBoundedDifferences,timeUniformContinuousPACBayes_bound,timeUniformIIDGaussianPACBayes_bound,timeUniformIIDGaussianPACBayes_grid_bound,timeUniformIIDGaussianPACBayes_selected_bound,timeUniformIIDPACBayes_allPosteriors_bound,timeUniformIIDPACBayes_grid_allPosteriors_bound,timeUniformPACBayes_bound,timeUniformPACBayes_crossing_bound,timeUniformSphericalGaussianPACBayes_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 (75):
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,average_perm_finiteCanonicalPairMean_eq_sampleVarianceBessel,average_perm_pairCatalog_eq_sampleVarianceBessel,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,finiteEmpiricalVariance,finiteEmpiricalVariancePACBayes_badEventMass_le_delta,finiteEmpiricalVariance_eq_pairwise,finiteEmpiricalVariance_expectedPriorBernsteinExpMoment_le_one,finiteEmpiricalVariance_le_card_div_pred_mul_empiricalRisk,finiteEmpiricalVariance_le_half,finiteEmpiricalVariance_lowerTailMGF_randomMatching,finiteEmpiricalVariance_lowerTailMGF_tolstikhinSeldin,finiteEmpiricalVariance_nonneg,finiteEmpiricalVariance_normalizedLowerTailMGF_le_one,finiteEmpiricalVariance_unbiased_finiteProduct,finiteMcAllesterGridPeeling_badEventMass_le_delta,finitePairBlock_factorization,finitePairVarianceKernelExpectation_eq_populationVariance,finitePairwiseEmpiricalVariance,finitePopulationRisk_mem_Icc_of_bounded,finitePopulationVariance,finitePopulationVariance_eq_secondMoment_sub_riskSq,finitePopulationVariance_le_quarter,finitePopulationVariance_nonneg,finitePrefixFiniteClassDeviationFromHoeffding_unitRange_explicitRadius,finitePrefixFiniteClassDeviationFromHoeffding_unitRange_radius,finiteProductSampleWeight_pairExpectation,finiteProductSampleWeight_pairSquaredDifferenceExpectation_eq,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,markovPACBayesExceptionalEvent_measurable,mixture_is_supermartingale,optimized_lambda_confidence_sequence_subGamma,optimized_lambda_two_sided_closed_form_pointwise,optimized_lambda_two_sided_confidence_sequence,orderedOffDiagonalSquaredDifference,orderedOffDiagonalSquaredDifference_eq_two_mul_card_mul_centeredSum,orderedOffDiagonalSquaredDifference_le,pSeriesDyadicEpochWeight_summable,pSeriesDyadicEpochWeight_zero_unitPenalty,posteriorPopulationVariance_le_empiricalVariance_of_not_mem,stitched_atTop_crossing_bound,subGammaLogLogWidth_add_stitchingPenalty,subGammaLogLogWidth_eq_boundary_optTilt,subGammaLogLogWidth_loglog_rate,subGamma_stitched_boundary_supermartingale,timeUniformIIDGaussianPACBayes_grid_bound,timeUniformPACBayes_crossing_bound,zeroOneDyadicFiniteClassConfidenceRadius,zeroOneDyadicFiniteClassConfidenceRadius_le_of_sampleSize_ge - covering / chaining (229):
EpsilonizedSupremumBoundaryChoice,FiniteCoverSupremumBoundaryChoice,FiniteDyadicDudleyInstance,FiniteDyadicDudleyInstance.SupremumAdapter,FiniteDyadicDudleyInstance.projected_dudley_bound,FiniteDyadicDudleyInstance.suppliedSup_dudley_bound,FiniteNet,FiniteNet.ProjectedIndex,TwoPoint,UnitInterval,bennett_mgf,bennett_mgf_le_one_add,bennett_mgf_subgamma,bennett_tail,bennett_taylor_bound,continuous_dudley_entropy_integral_iSup_totalBounded_minimalDyadicCoverCountEnvelope,continuous_dudley_entropy_integral_iSup_totalBounded_minimalMetricCoveringNumber_shifted,continuous_dudley_entropy_integral_iSup_totalBounded_selectedCoverCountEnvelope_not_minimalCoveringNumber,continuous_dudley_oneStep_entropy_integral_iSup_unitInterval_pairCountEnvelope,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,finiteDyadicEntropyAtRadiusUpperSum_shifted_div_four_le_eight_mul_full_integral,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_projectedNet_dudley_entropy_sum_totalBounded_minimalDyadic_entropy_integral_comparison_nonempty,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,minimalDyadicChainingCoverCountEntropy_dominates_shiftedMinimalEntropy_sample,minimalDyadicChainingCoverCount_entropy_le_sqrt_two_mul_next_minimalMetricCoveringEntropy,minimalDyadicChainingCoverCount_eq_minimalMetricCoveringNumber_mul,minimalDyadicChainingCoverCount_le_next_minimalMetricCoveringNumber_sq,minimalDyadicChainingFiniteNetOfTotallyBoundedUniv_coveringNumber_eq,minimalDyadicCoverCountEntropyAtRadius_guarded,minimalFiniteNetOfTotallyBoundedUniv_coveringNumber_eq,minimalMetricCoverOfTotallyBoundedUniv,minimalMetricCoverOfTotallyBoundedUniv_card_eq,minimalMetricCoverOfTotallyBoundedUniv_card_minimal,minimalMetricCoveringNumber,minimalMetricCoveringNumber_antitone,minimalMetricCoveringNumber_le_dyadicSelectedCoveringNumber,minimalMetricCoveringNumber_le_of_metricCoverCardinalityLe,minimalMetricCoveringNumber_le_totalBoundedDyadicCoverCountEnvelope,minimalMetricCoveringNumber_pos,minimalMetricCoveringNumber_spec,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,totalBoundedCoveringEntropyAtRadius_guarded,totalBoundedCoveringEntropy_dominates_dyadicEnvelope_sample,totalBoundedCoveringNumberAtRadius,totalBoundedCoveringNumberAtRadiusENat_ne_top,totalBoundedCoveringNumberAtRadius_dyadic,totalBoundedMinimalDyadicCoverCount_dyadicProfileBound_of_boundaryChoice,totalBoundedSelectedCoverCount_dyadicProfileBound_of_boundaryChoice,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,unitIntervalChainingPairCountEnvelope,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,unitIntervalPairCountEntropy_eq_pair_count_sample,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_minimalDyadicCoverCountEnvelope_sample_positive,unitInterval_minimalMetricCoverOfTotallyBoundedUniv_sample_card_positive,unitInterval_minimalMetricCoveringNumber_sample_positive,unitInterval_pairCountEntropy_integral_positive,unitInterval_pairCountEntropy_nonconstant,unitInterval_rademacherLinear_mgf_bound,unitInterval_shiftedMinimalMetricCoveringEntropy_sample_nonneg,unitInterval_totalBoundedCoveringNumber_sample_positive,unitInterval_totalBoundedSelectedCoverCountEnvelope_sample_positive,unitInterval_totallyBounded_univ - risk (59):
BernsteinCondition,IsERM,LocalizedDeviationCertificate,abs_markovRiskShortfall_le_one,averageConditionalRisk_lt_empiricalPrequentialRisk_add_boundary_of_not_mem,empiricalRisk,fairBoolThreshold_endToEnd_certificate,finiteCatoni_badEventMass_le_delta,finiteEmpiricalRisk,finiteEmpiricalVariance_le_card_div_pred_mul_empiricalRisk,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,finitePopulationRisk_mem_Icc_of_bounded,finitePopulationVariance_eq_secondMoment_sub_riskSq,finitePriorAveraged_mgf_empiricalRiskDeviation_le,finiteProduct_mgf_empiricalRiskDeviation_eq_pow,finiteProduct_mgf_empiricalRiskDeviation_le_of_single,indicatorBernsteinVarianceProxy_le_risk_div,indicatorPopulationRisk_mem_Icc,indicator_posteriorRisk_le_lowRisk_of_not_mem,indicator_posteriorRisk_le_min_one_twoThirds_of_not_mem,indicator_posteriorRisk_le_twoThirds_of_not_mem,indicator_posteriorRisk_le_weightedLowRiskCatalog_of_not_mem,indicator_posteriorRisk_le_weightedLowRiskCatalog_selected_of_not_mem,integrable_markovRiskShortfall,localizedExcessRiskEmpiricalRademacherComplexity_le_of_bernstein_fixedPointCertificate,localizedExcessRiskEmpiricalRademacherComplexity_le_secondMoment,localizedExcessRiskEmpiricalRademacherComplexity_nonneg,localizedUpperDeviation,markovPACBayesAnyPosteriorUpperFailure_subset_processFailure,markovPACBayesExceptionalEvent_mass_le_delta,markovPACBayesExceptionalEvent_measurable,markovPACBayesRawFailure_subset_exceptionalEvent,markovPACBayes_allPosteriors_bound,markovPACBayes_prequentialRisk_certificate,markovPosteriorAverageConditionalRisk_lt_of_not_mem,markovPrequentialRiskExceptionalEvent_mass_le_delta,markovRiskInnovation_condExp_eq_zero,markovRiskInnovation_condSecondMoment_le_one,markovRiskInnovation_condSecondMoment_le_one_fourth,markovRiskShortfall_condExp_eq_zero,markovRiskShortfall_condSecondMoment_le_one_fourth,markovRiskShortfall_incrementAdapted,measurable_markovRiskShortfall,pac_bayes_generalization,pathSquaredLoss_condExp,posteriorAverage_runningMean_markovRiskShortfall,posteriorIndicatorBernsteinVarianceProxy_le_risk_div,posteriorRisk_bound_of_priorDeviationMGF_le,posteriorRisk_bound_of_priorDeviationMGF_le_complexity_sqrt,risk,runningMean_markovRiskInnovation,runningMean_markovRiskShortfall,subGammaCgf_oneFourth_one_div,vc_erm_excessRisk_tail - sample statistics (46):
average_perm_finiteCanonicalPairMean_eq_sampleVarianceBessel,average_perm_pairCatalog_eq_sampleVarianceBessel,bernoulliHalfCramerRaoWitness,bernoulliLogLikelihood_global_argmax_from_count,bernoulliScoreAtSampleMean_eq_zero,bootstrapMean_eq_sampleMean,covariance_score_eq_deriv_mean,cramerRao_unbiased,finiteEmpiricalVariance,finiteEmpiricalVariancePACBayes_badEventMass_le_delta,finiteEmpiricalVariance_eq_pairwise,finiteEmpiricalVariance_expectedPriorBernsteinExpMoment_le_one,finiteEmpiricalVariance_le_card_div_pred_mul_empiricalRisk,finiteEmpiricalVariance_le_half,finiteEmpiricalVariance_lowerTailMGF_randomMatching,finiteEmpiricalVariance_lowerTailMGF_tolstikhinSeldin,finiteEmpiricalVariance_nonneg,finiteEmpiricalVariance_normalizedLowerTailMGF_le_one,finiteEmpiricalVariance_unbiased_finiteProduct,finitePairBlock_factorization,finitePairVarianceKernelExpectation_eq_populationVariance,finitePairwiseEmpiricalVariance,finitePopulationRisk_mem_Icc_of_bounded,finitePopulationVariance,finitePopulationVariance_eq_secondMoment_sub_riskSq,finitePopulationVariance_le_quarter,finitePopulationVariance_nonneg,finiteProductSampleWeight_pairExpectation,finiteProductSampleWeight_pairSquaredDifferenceExpectation_eq,gaussianKnownVarianceLogLikelihood_mle,hoeffding_mean_tail_twoSided,horvitzThompson_design_unbiased,orderedOffDiagonalSquaredDifference,orderedOffDiagonalSquaredDifference_eq_two_mul_card_mul_centeredSum,orderedOffDiagonalSquaredDifference_le,posteriorPopulationVariance_le_empiricalVariance_of_not_mem,sampleMean,sampleMean_hoeffding_tail,sampleMean_unbiased_finite,sampleVariance,sampleVarianceBessel,sampleVarianceBessel_unbiased_finite,sampleVariance_eq_secondMoment_sub_meanSq,sampleVariance_nonneg,weightedExpectation_linear,weightedVariance - stability (143):
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_le_one_add,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,finiteProductSampleWeight_isPMF,finiteProduct_mgf_empiricalRiskDeviation_eq_pow,finiteProduct_mgf_empiricalRiskDeviation_le_of_single,indicatorBernsteinVarianceProxy_le_risk_div,indicatorBernstein_normalization_eq_budget,indicatorDeviation_centered,indicatorDeviation_secondMoment_eq,indicatorFinitePACBayesBernsteinBadSamples,indicatorFinitePACBayesBernsteinWeightedCatalogBadSamples,indicatorFixedTiltBadSamples_subset_weightedCatalog,indicatorPopulationRisk_mem_Icc,indicator_expectedPriorBernsteinExpMoment_le_one,indicator_finitePACBayesBernstein_fixedLambda_badEventMass_le_delta,indicator_finitePACBayesBernstein_twoThirds_badEventMass_le_delta,indicator_finitePACBayesBernstein_weightedCatalog_badEventMass_le_delta,indicator_mem_weightedCatalog_iff,indicator_not_mem_weightedCatalog_iff,indicator_oneCoordinateDeviationMGF_le,indicator_posteriorGeneralizationGap_le_of_not_mem,indicator_posteriorGeneralizationGap_le_weightedCatalog_of_not_mem,indicator_posteriorRisk_le_lowRisk_of_not_mem,indicator_posteriorRisk_le_min_one_twoThirds_of_not_mem,indicator_posteriorRisk_le_twoThirds_of_not_mem,indicator_posteriorRisk_le_weightedLowRiskCatalog_of_not_mem,indicator_posteriorRisk_le_weightedLowRiskCatalog_selected_of_not_mem,indicator_product_mgf_le,indicator_product_normalizedMGF_le_one,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,posteriorIndicatorBernsteinVarianceProxy_le_risk_div,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 (23):
atTop_time_uniform_confidence_sequence_subGamma_mixture,averageConditionalRisk_lt_empiricalPrequentialRisk_add_boundary_of_not_mem,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,indicator_oneCoordinateDeviationMGF_le,integrable_exp_mul_of_bounded,markovPosteriorAverageConditionalRisk_lt_of_not_mem,mixture_is_supermartingale,optimized_lambda_confidence_sequence_subGamma,stitched_atTop_crossing_bound,subGammaCgf_oneFourth_one_div,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 (37):
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,finiteEmpiricalVariance_lowerTailMGF_randomMatching,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 (24):
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,indicator_finitePACBayesBernstein_weightedCatalog_badEventMass_le_delta,localizedFastRateUpperDeviationBadEventMass_le_sum_centeredShiftedExpMoment_div,localizedUpperDeviationBadEventMass_le_sum_pointwise
| 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:151 |
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:249 |
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:210 |
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 |
| 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 |
| 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 | 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:2018 |
Finite skeleton and terminal-scale certificate for an epsilonized Dudley boundary step |
| covering / chaining | FiniteCoverSupremumBoundaryChoice |
theorem | FormalSLT/Covering/TotalBoundedDudley.lean:2284 |
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 | continuous_dudley_entropy_integral_iSup_totalBounded_minimalDyadicCoverCountEnvelope |
theorem | FormalSLT/Covering/TotalBoundedDudleyMinimalCapstone.lean:649 |
Generic totally bounded continuous Dudley capstone with the cardinal-minimal dyadic adjacent-product envelope |
| covering / chaining | continuous_dudley_entropy_integral_iSup_totalBounded_minimalMetricCoveringNumber_shifted |
theorem | FormalSLT/Covering/TotalBoundedDudleyMinimalShift.lean:512 |
Generic totally bounded continuous Dudley capstone with pure genuine minimal-cover entropy in the conclusion, paid by shifted boundary certificates and constants |
| covering / chaining | continuous_dudley_entropy_integral_iSup_totalBounded_selectedCoverCountEnvelope_not_minimalCoveringNumber |
theorem | FormalSLT/Covering/TotalBoundedDudleySelectedCapstone.lean:158 |
Generic totally bounded continuous Dudley capstone with the selected-cover-count envelope integrand, not genuine minimal covering number |
| covering / chaining | dyadicChainingFiniteNetOfTotallyBoundedUniv_pair_radius_le |
theorem | FormalSLT/Covering/TotalBoundedDudley.lean:275 |
Dyadic total-bounded net schedule satisfies the adjacent-radius budget used by finite chaining |
| covering / chaining | dyadicChainingFiniteNetSequenceOfTotallyBounded |
theorem | FormalSLT/Covering/TotalBoundedDudley.lean:613 |
Packages the total-bounded dyadic net schedule as a FiniteDyadicNetSequence under global projection-pair hypotheses |
| covering / chaining | finiteDyadicDudleyInstanceOfTotallyBounded |
theorem | FormalSLT/Covering/TotalBoundedDudley.lean:666 |
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 | finiteDyadicEntropyAtRadiusUpperSum_shifted_div_four_le_eight_mul_full_integral |
theorem | FormalSLT/Covering/TotalBoundedDudleyMinimalShift.lean:325 |
Finite shifted dyadic upper sums are bounded by the pure entropy integral with explicit shift constants |
| 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:3676 |
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:2438 |
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:2129 |
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:714 |
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:878 |
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:1079 |
Total-bounded projected finite-net wrapper with one truncated interval-integral entropy budget |
| covering / chaining | finite_projectedNet_dudley_entropy_sum_totalBounded_minimalDyadic_entropy_integral_comparison_nonempty |
theorem | FormalSLT/Covering/TotalBoundedDudleyMinimalCapstone.lean:403 |
Projected finite-chain Dudley wrapper threaded through the cardinal-minimal dyadic net schedule |
| 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:3415 |
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:1547 |
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:1435 |
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:1854 |
Total-bounded Dudley boundary wrapper using approximate witnesses, finite skeleton selectors, and pathwise modulus |
| covering / chaining | minimalDyadicChainingCoverCountEntropy_dominates_shiftedMinimalEntropy_sample |
theorem | FormalSLT/Covering/TotalBoundedDudleyMinimalShift.lean:257 |
The shifted one-radius minimal-cover entropy dominates the finite prefix-envelope sample |
| covering / chaining | minimalDyadicChainingCoverCount_entropy_le_sqrt_two_mul_next_minimalMetricCoveringEntropy |
theorem | FormalSLT/Covering/TotalBoundedDudleyMinimalShift.lean:147 |
Adjacent-product entropy is bounded by sqrt 2 times one shifted minimal-cover entropy |
| covering / chaining | minimalDyadicChainingCoverCount_eq_minimalMetricCoveringNumber_mul |
theorem | FormalSLT/Covering/TotalBoundedDudleyMinimalCapstone.lean:49 |
Adjacent cardinal-minimal dyadic cover count equals the product of genuine minimal covering numbers at the sampled radii |
| covering / chaining | minimalDyadicChainingCoverCount_le_next_minimalMetricCoveringNumber_sq |
theorem | FormalSLT/Covering/TotalBoundedDudleyMinimalShift.lean:65 |
Adjacent cardinal-minimal dyadic cover products are bounded by the next smaller-radius minimal covering number squared |
| covering / chaining | minimalDyadicChainingFiniteNetOfTotallyBoundedUniv_coveringNumber_eq |
theorem | FormalSLT/Covering/TotalBoundedMinimalCovering.lean:237 |
The dyadic minimal-net schedule has genuine minimal covering count at each sampled radius |
| covering / chaining | minimalDyadicCoverCountEntropyAtRadius_guarded |
theorem | FormalSLT/Covering/TotalBoundedDudleyMinimalCapstone.lean:328 |
Cardinal-minimal dyadic adjacent-product entropy staircase satisfies the guarded closed-annulus condition |
| covering / chaining | minimalFiniteNetOfTotallyBoundedUniv_coveringNumber_eq |
theorem | FormalSLT/Covering/TotalBoundedMinimalCovering.lean:196 |
The bundled finite net built from the minimal cover has covering count equal to the genuine minimal covering number |
| covering / chaining | minimalMetricCoverOfTotallyBoundedUniv |
theorem | FormalSLT/Covering/TotalBoundedMinimalCovering.lean:106 |
Chooses a cardinal-minimal finite metric cover from the genuine minimal covering-number witness |
| covering / chaining | minimalMetricCoverOfTotallyBoundedUniv_card_eq |
theorem | FormalSLT/Covering/TotalBoundedMinimalCovering.lean:136 |
The chosen finite metric cover has cardinality exactly equal to the genuine minimal covering number |
| covering / chaining | minimalMetricCoverOfTotallyBoundedUniv_card_minimal |
theorem | FormalSLT/Covering/TotalBoundedMinimalCovering.lean:151 |
Every finite metric cover has at least as many centers as the chosen minimal cover |
| covering / chaining | minimalMetricCoveringNumber |
theorem | FormalSLT/Covering/TotalBoundedMinimalCovering.lean:52 |
Genuine minimal finite metric covering number for a nonempty totally bounded metric index space |
| covering / chaining | minimalMetricCoveringNumber_antitone |
theorem | FormalSLT/Covering/TotalBoundedDudleyMinimalShift.lean:37 |
Genuine minimal covering numbers are antitone in the positive radius |
| covering / chaining | minimalMetricCoveringNumber_le_dyadicSelectedCoveringNumber |
theorem | FormalSLT/Covering/TotalBoundedMinimalCovering.lean:282 |
The genuine minimal covering number is bounded by each selected dyadic finite-net count |
| covering / chaining | minimalMetricCoveringNumber_le_of_metricCoverCardinalityLe |
theorem | FormalSLT/Covering/TotalBoundedMinimalCovering.lean:71 |
Any finite metric cover with at most n centers bounds the genuine minimal covering number by n |
| covering / chaining | minimalMetricCoveringNumber_le_totalBoundedDyadicCoverCountEnvelope |
theorem | FormalSLT/Covering/TotalBoundedMinimalCovering.lean:306 |
The selected dyadic envelope dominates the genuine minimal covering number at sampled dyadic net radii |
| covering / chaining | minimalMetricCoveringNumber_pos |
theorem | FormalSLT/Covering/TotalBoundedMinimalCovering.lean:84 |
Nonempty totally bounded spaces have positive genuine minimal covering number at positive radius |
| covering / chaining | minimalMetricCoveringNumber_spec |
theorem | FormalSLT/Covering/TotalBoundedMinimalCovering.lean:59 |
The genuine minimal covering number is realized by a finite metric cover |
| 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:2255 |
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 |
| covering / chaining | totalBoundedCoveringEntropyAtRadius_guarded |
theorem | FormalSLT/Covering/TotalBoundedDudleyCovering.lean:298 |
The induced entropy staircase satisfies the guarded closed-annulus condition |
| covering / chaining | totalBoundedCoveringEntropy_dominates_dyadicEnvelope_sample |
theorem | FormalSLT/Covering/TotalBoundedDudleyCovering.lean:332 |
Dyadic samples dominate the finite entropy prefix envelope used by total-bounded finite wrappers |
| covering / chaining | totalBoundedCoveringNumberAtRadius |
theorem | FormalSLT/Covering/TotalBoundedDudleyCovering.lean:50 |
Half-open real-radius selected-cover-count staircase for the total-bounded dyadic net schedule |
| covering / chaining | totalBoundedCoveringNumberAtRadiusENat_ne_top |
theorem | FormalSLT/Covering/TotalBoundedDudleyCovering.lean:256 |
The selected-cover-count staircase has a finite ℕ∞ surface |
| covering / chaining | totalBoundedCoveringNumberAtRadius_dyadic |
theorem | FormalSLT/Covering/TotalBoundedDudleyCovering.lean:234 |
The staircase samples the monotone prefix envelope of selected adjacent dyadic cover-count products at dyadic radii |
| covering / chaining | totalBoundedMinimalDyadicCoverCount_dyadicProfileBound_of_boundaryChoice |
theorem | FormalSLT/Covering/TotalBoundedDudleyMinimalCapstone.lean:528 |
Minimal-schedule boundary certificates give the guarded dyadic upper-sum input |
| covering / chaining | totalBoundedSelectedCoverCount_dyadicProfileBound_of_boundaryChoice |
theorem | FormalSLT/Covering/TotalBoundedDudleySelectedCapstone.lean:37 |
Boundary certificates give the guarded dyadic upper-sum input for the selected-cover-count entropy profile |
| covering / chaining | unitInterval_minimalDyadicCoverCountEnvelope_sample_positive |
theorem | FormalSLT/Covering/TotalBoundedDudleyMinimalCapstone.lean:694 |
Unit-interval non-vacuity witness for the cardinal-minimal dyadic cover-count envelope |
| covering / chaining | unitInterval_minimalMetricCoverOfTotallyBoundedUniv_sample_card_positive |
theorem | FormalSLT/Covering/TotalBoundedMinimalCovering.lean:351 |
Concrete non-vacuity witness for the chosen minimal finite cover on the unit interval |
| covering / chaining | unitInterval_minimalMetricCoveringNumber_sample_positive |
theorem | FormalSLT/Covering/TotalBoundedMinimalCovering.lean:338 |
Concrete non-vacuity witness for the genuine minimal covering number on the unit interval |
| covering / chaining | unitInterval_shiftedMinimalMetricCoveringEntropy_sample_nonneg |
theorem | FormalSLT/Covering/TotalBoundedDudleyMinimalShift.lean:672 |
Unit-interval non-vacuity witness for the shifted minimal-cover entropy profile |
| covering / chaining | unitInterval_totalBoundedCoveringNumber_sample_positive |
theorem | FormalSLT/Covering/TotalBoundedDudleyCovering.lean:371 |
Concrete non-vacuity witness for the generic selected-cover-count surface on the unit interval |
| covering / chaining | unitInterval_totalBoundedSelectedCoverCountEnvelope_sample_positive |
theorem | FormalSLT/Covering/TotalBoundedDudleySelectedCapstone.lean:203 |
Unit-interval non-vacuity witness for the selected-cover-count envelope surface |
| 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 |
| Markov, risk | abs_markovRiskShortfall_le_one |
theorem | FormalSLT/StochasticDynamics/MarkovPACBayes.lean:123 |
Supplies the uniform absolute bound for [0,1] squared losses |
| Markov, sub-Gamma, risk | averageConditionalRisk_lt_empiricalPrequentialRisk_add_boundary_of_not_mem |
theorem | FormalSLT/StochasticDynamics/MarkovRisk.lean:554 |
Bounds average conditional risk by observed prequential loss plus the declared sub-Gamma boundary outside that event |
| Markov, risk | integrable_markovRiskShortfall |
theorem | FormalSLT/StochasticDynamics/MarkovPACBayes.lean:115 |
Establishes integrability under the actual finite Markov path law |
| Markov, PAC-Bayes, risk | markovPACBayesAnyPosteriorUpperFailure_subset_processFailure |
theorem | FormalSLT/StochasticDynamics/MarkovPACBayes.lean:182 |
Embeds the risk-facing posterior failure event into the generic time-uniform PAC-Bayes process failure event |
| Markov, PAC-Bayes, risk | markovPACBayesExceptionalEvent_mass_le_delta |
theorem | FormalSLT/StochasticDynamics/MarkovPACBayes.lean:257 |
Gives one measurable exceptional event of ordinary probability at most delta |
| Markov, confidence sequence, PAC-Bayes, risk | markovPACBayesExceptionalEvent_measurable |
theorem | FormalSLT/StochasticDynamics/MarkovPACBayes.lean:240 |
Proves measurability of the hull used for the public confidence event |
| Markov, PAC-Bayes, risk | markovPACBayesRawFailure_subset_exceptionalEvent |
theorem | FormalSLT/StochasticDynamics/MarkovPACBayes.lean:247 |
Shows that the measurable hull contains every raw posterior-existential violation |
| Markov, PAC-Bayes, risk | markovPACBayes_allPosteriors_bound |
theorem | FormalSLT/StochasticDynamics/MarkovPACBayes.lean:198 |
Controls the raw all-time, all-posterior Markov failure set in outer probability at fixed tilt |
| Markov, PAC-Bayes, KL divergence, risk | markovPACBayes_prequentialRisk_certificate |
theorem | FormalSLT/StochasticDynamics/MarkovPACBayes.lean:305 |
Publication-facing finite-catalog theorem with a measurable common event, all-time and all-posterior validity, and explicit KL penalty |
| Markov, sub-Gamma, KL divergence, risk | markovPosteriorAverageConditionalRisk_lt_of_not_mem |
theorem | FormalSLT/StochasticDynamics/MarkovPACBayes.lean:271 |
Outside the common event, controls every posterior and every positive time by empirical prequential risk plus KL and the sub-Gamma boundary |
| Markov, risk | markovPrequentialRiskExceptionalEvent_mass_le_delta |
theorem | FormalSLT/StochasticDynamics/MarkovRisk.lean:523 |
Gives one measurable all-time finite-grid exceptional event with probability at most delta |
| Markov, risk | markovRiskInnovation_condExp_eq_zero |
theorem | FormalSLT/StochasticDynamics/MarkovRisk.lean:303 |
Centers observed loss minus transition-row conditional risk under the generated filtration |
| Markov, risk | markovRiskInnovation_condSecondMoment_le_one |
theorem | FormalSLT/StochasticDynamics/MarkovRisk.lean:393 |
Conservative unit conditional-second-moment bound retained as a simple compatibility lemma |
| Markov, risk | markovRiskInnovation_condSecondMoment_le_one_fourth |
theorem | FormalSLT/StochasticDynamics/MarkovRisk.lean:345 |
Sharp universal 1/4 conditional-second-moment bound for the centered [0,1] one-step loss |
| Markov, risk | markovRiskShortfall_condExp_eq_zero |
theorem | FormalSLT/StochasticDynamics/MarkovPACBayes.lean:134 |
Derives conditional centering of the risk shortfall from the Markov path-law identity |
| Markov, risk | markovRiskShortfall_condSecondMoment_le_one_fourth |
theorem | FormalSLT/StochasticDynamics/MarkovPACBayes.lean:153 |
Transfers the sharp universal 1/4 conditional-second-moment proxy to the risk shortfall |
| Markov, risk | markovRiskShortfall_incrementAdapted |
theorem | FormalSLT/StochasticDynamics/MarkovPACBayes.lean:102 |
Preserves increment adaptedness under the risk-shortfall sign change |
| Markov, risk | measurable_markovRiskShortfall |
theorem | FormalSLT/StochasticDynamics/MarkovPACBayes.lean:109 |
Establishes measurability of every catalog member's risk-shortfall increment |
| Markov, risk | pathSquaredLoss_condExp |
theorem | FormalSLT/StochasticDynamics/MarkovRisk.lean:173 |
Derives the next-step squared-loss conditional expectation from the finite transition PMF and its Ionescu--Tulcea path law |
| Markov, risk | posteriorAverage_runningMean_markovRiskShortfall |
theorem | FormalSLT/StochasticDynamics/MarkovPACBayes.lean:83 |
Identifies the posterior-averaged shortfall with posterior conditional risk minus posterior empirical prequential risk |
| Markov, risk | runningMean_markovRiskInnovation |
theorem | FormalSLT/StochasticDynamics/MarkovRisk.lean:418 |
Identifies the innovation mean with observed prequential risk minus average conditional risk |
| Markov, risk | runningMean_markovRiskShortfall |
theorem | FormalSLT/StochasticDynamics/MarkovPACBayes.lean:71 |
Reorients the Markov innovation as conditional risk minus observed loss, the sign required for an upper-risk certificate |
| Markov, sub-Gamma, risk | subGammaCgf_oneFourth_one_div |
theorem | FormalSLT/StochasticDynamics/MarkovPACBayes.lean:294 |
Rewrites the 1/4-variance sub-Gamma contribution as lambda / (8 * (1 - lambda / 3)) |
| 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:287 |
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:241 |
General FiniteDyadicNetSequence instance for Fin n with [Fact (2 ≤ n)] |
| covering / chaining | finDiscreteDyadicNet_coverCount_le |
definition | FormalSLT/Covering/FiniteDiscreteDudley.lean:233 |
Adjacent finite-discrete covering-number products are bounded by the n * n envelope |
| covering / chaining | finDiscreteDyadicNet_coveringNumber |
definition | FormalSLT/Covering/FiniteDiscreteDudley.lean:229 |
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:314 |
Supremum functional for the embedded Rademacher process over Fin n |
| Rademacher, covering / chaining | finDiscreteRademacherSupAdapter |
definition | FormalSLT/Covering/FiniteDiscreteDudley.lean:350 |
Supplied-supremum adapter for the finite-discrete packaged Dudley instance |
| Rademacher, covering / chaining | finDiscreteRademacherSup_dudley_m_bound |
definition | FormalSLT/Covering/FiniteDiscreteDudley.lean:361 |
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:332 |
Terminal projected-net adapter for the finite-discrete supplied supremum |
| Rademacher, covering / chaining | finDiscreteRademacherSup_true |
definition | FormalSLT/Covering/FiniteDiscreteDudley.lean:317 |
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:296 |
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 |
| confidence sequence, ERM, sample statistics | average_perm_finiteCanonicalPairMean_eq_sampleVarianceBessel |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVarianceMatching.lean:435 |
Identifies the permutation average of the canonical random-matching statistic with Bessel sample variance |
| confidence sequence, ERM, sample statistics | average_perm_pairCatalog_eq_sampleVarianceBessel |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVarianceMatching.lean:250 |
Averaging any fixed nonempty catalog of distinct coordinate pairs over all permutations recovers Bessel sample variance |
| confidence sequence, sample statistics | finiteEmpiricalVariance |
definition | FormalSLT/PACBayes/FiniteEmpiricalVariance.lean:66 |
Per-hypothesis Bessel-corrected empirical loss variance |
| confidence sequence, PAC-Bayes, sample statistics | finiteEmpiricalVariancePACBayes_badEventMass_le_delta |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVariancePACBayes.lean:161 |
Bounds one fixed-sample, fixed-tilt exceptional set by delta; the event is shared by every finite posterior |
| confidence sequence, sample statistics | finiteEmpiricalVariance_eq_pairwise |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVariance.lean:243 |
Exact second-order pair-statistic representation of Bessel empirical variance |
| Bernstein, confidence sequence, sample statistics | finiteEmpiricalVariance_expectedPriorBernsteinExpMoment_le_one |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVariancePACBayes.lean:41 |
Averages the normalized per-hypothesis empirical-variance moment under a finite prior |
| confidence sequence, ERM, sample statistics, risk | finiteEmpiricalVariance_le_card_div_pred_mul_empiricalRisk |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVariance.lean:292 |
Source-facing self-bound V_n <= n/(n-1) * Rhat_n for [0,1] losses |
| confidence sequence, sample statistics | finiteEmpiricalVariance_le_half |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVariance.lean:334 |
Universal 1/2 bound for Bessel empirical variance of a finite [0,1] sample |
| tail bound, MGF, confidence sequence, sample statistics | finiteEmpiricalVariance_lowerTailMGF_randomMatching |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVarianceMGF.lean:535 |
Random-matching and finite-Jensen lower-tail MGF bound, with the exact disjoint-pair count in its coefficient |
| MGF, confidence sequence, sample statistics | finiteEmpiricalVariance_lowerTailMGF_tolstikhinSeldin |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVarianceMGF.lean:671 |
All-n >= 2 source-normalized finite-IID empirical-variance MGF inequality |
| confidence sequence, sample statistics | finiteEmpiricalVariance_nonneg |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVariance.lean:166 |
Bessel-corrected empirical loss variance is nonnegative for sample size at least two |
| MGF, confidence sequence, KL divergence, ERM, sample statistics | finiteEmpiricalVariance_normalizedLowerTailMGF_le_one |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVarianceMGF.lean:745 |
Moves the deterministic variance penalty inside the exponential to obtain the normalized moment used by change of measure |
| confidence sequence, sample statistics | finiteEmpiricalVariance_unbiased_finiteProduct |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVariance.lean:629 |
End-to-end finite-IID unbiasedness of the per-hypothesis Bessel empirical loss variance |
| confidence sequence, sample statistics | finitePairBlock_factorization |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVarianceMatching.lean:313 |
Factors the finite-product expectation of a product over disjoint pair blocks into independent two-coordinate expectations |
| confidence sequence, sample statistics | finitePairVarianceKernelExpectation_eq_populationVariance |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVariance.lean:534 |
The independent-pair half squared-difference kernel has expectation equal to population variance |
| confidence sequence, sample statistics | finitePairwiseEmpiricalVariance |
definition | FormalSLT/PACBayes/FiniteEmpiricalVariance.lean:76 |
Normalized second-order pair-statistic form of empirical variance |
| confidence sequence, sample statistics, risk | finitePopulationRisk_mem_Icc_of_bounded |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVariance.lean:130 |
Places the population risk of a finite [0,1] loss in [0,1] |
| confidence sequence, sample statistics | finitePopulationVariance |
definition | FormalSLT/PACBayes/FiniteEmpiricalVariance.lean:57 |
Per-hypothesis population loss variance under a finite weight function |
| confidence sequence, sample statistics, risk | finitePopulationVariance_eq_secondMoment_sub_riskSq |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVariance.lean:90 |
Identifies population loss variance with the second moment minus squared risk |
| confidence sequence, sample statistics | finitePopulationVariance_le_quarter |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVariance.lean:146 |
Gives the universal 1/4 population-variance bound for finite [0,1] losses |
| confidence sequence, sample statistics | finitePopulationVariance_nonneg |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVariance.lean:82 |
Population loss variance is nonnegative under a finite PMF |
| confidence sequence, sample statistics | finiteProductSampleWeight_pairExpectation |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVariance.lean:480 |
Two distinct coordinates of the finite IID product sample have the product marginal |
| confidence sequence, sample statistics | finiteProductSampleWeight_pairSquaredDifferenceExpectation_eq |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVariance.lean:594 |
Expected squared loss difference across two distinct IID coordinates is twice the population variance |
| confidence sequence, sample statistics | orderedOffDiagonalSquaredDifference |
definition | FormalSLT/PACBayes/FiniteEmpiricalVariance.lean:71 |
Ordered sum of squared differences across distinct sample indices |
| confidence sequence, sample statistics | orderedOffDiagonalSquaredDifference_eq_two_mul_card_mul_centeredSum |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVariance.lean:175 |
Equates the ordered off-diagonal square-difference sum with twice the sample size times the centered sum of squares |
| confidence sequence, sample statistics | orderedOffDiagonalSquaredDifference_le |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVariance.lean:257 |
Bounds the ordered pair numerator for samples in [0,1] |
| confidence sequence, KL divergence, sample statistics | posteriorPopulationVariance_le_empiricalVariance_of_not_mem |
theorem | FormalSLT/PACBayes/FiniteEmpiricalVariancePACBayes.lean:188 |
Outside the shared event, bounds the posterior average of per-hypothesis population variances by the corresponding empirical average and KL-confidence penalty |
| Bernoulli | bernoulliNaturalBase |
definition | FormalSLT/Statistics/ExponentialFamily.lean:362 |
Bernoulli natural-family base weights on Bool |
| Bernoulli | bernoulliNaturalStatistic |
definition | FormalSLT/Statistics/ExponentialFamily.lean:365 |
Bernoulli natural sufficient statistic 1{true} |
| Bernoulli | bernoulliNatural_fisher_eq_variance_zero |
definition | FormalSLT/Statistics/ExponentialFamily.lean:466 |
Bernoulli natural Fisher information equals variance at theta = 0 |
| Bernoulli | bernoulliNatural_fisher_zero |
definition | FormalSLT/Statistics/ExponentialFamily.lean:452 |
Bernoulli natural Fisher information at theta = 0 is 1/4 |
| Bernoulli | bernoulliNatural_logPartition_deriv_zero |
definition | FormalSLT/Statistics/ExponentialFamily.lean:400 |
Bernoulli natural A'(0) = 1/2 |
| Bernoulli | bernoulliNatural_logPartition_secondDeriv_zero |
definition | FormalSLT/Statistics/ExponentialFamily.lean:436 |
Bernoulli natural A''(0) = 1/4 |
| Bernoulli | bernoulliNatural_logPartition_zero |
definition | FormalSLT/Statistics/ExponentialFamily.lean:377 |
Bernoulli natural log-partition at theta = 0 is log 2 |
| Bernoulli | bernoulliNatural_mean_zero |
definition | FormalSLT/Statistics/ExponentialFamily.lean:385 |
Bernoulli natural mean at theta = 0 is 1/2 |
| Bernoulli | bernoulliNatural_partition |
definition | FormalSLT/Statistics/ExponentialFamily.lean:368 |
Bernoulli natural partition sum is 1 + exp(theta) |
| Bernoulli | bernoulliNatural_pmf_zero |
definition | FormalSLT/Statistics/ExponentialFamily.lean:413 |
Both Bernoulli natural atoms have mass 1/2 at theta = 0 |
| Bernoulli | bernoulliNatural_variance_zero |
definition | FormalSLT/Statistics/ExponentialFamily.lean:425 |
Bernoulli natural variance at theta = 0 is 1/4 |
| Bernoulli | bernoulliNatural_witness |
definition | FormalSLT/Statistics/ExponentialFamily.lean:482 |
Concrete Bernoulli witness with mean 1/2, variance 1/4, and Fisher information 1/4 |
finiteExponentialFamily_fisherInformation_eq_variance |
definition | FormalSLT/Statistics/ExponentialFamily.lean:330 |
Natural-parameter Fisher information equals finite variance | |
finiteExponentialFamily_logPartition_secondDeriv_eq_fisherInformation |
definition | FormalSLT/Statistics/ExponentialFamily.lean:345 |
Direct bridge I(theta) = A''(theta) | |
finiteExponentialFamily_mean_eq_logPartition_deriv |
definition | FormalSLT/Statistics/ExponentialFamily.lean:133 |
Finite exponential-family mean equals the log-partition derivative numerator divided by Z(theta) | |
finiteExponentialFamily_score_eq_centered |
definition | FormalSLT/Statistics/ExponentialFamily.lean:316 |
Natural-parameter score equals the centered sufficient statistic | |
finiteExponentialFamily_variance_eq_logPartition_secondDeriv |
definition | FormalSLT/Statistics/ExponentialFamily.lean:304 |
Finite exponential-family variance equals log-partition second derivative | |
finiteExponentialPMF |
definition | FormalSLT/Statistics/ExponentialFamily.lean:63 |
Natural-parameter finite exponential-family probability mass | |
finiteExponentialPMFDeriv |
definition | FormalSLT/Statistics/ExponentialFamily.lean:68 |
Natural-parameter derivative of the finite exponential-family mass | |
finiteExponentialPMF_hasDerivAt |
definition | FormalSLT/Statistics/ExponentialFamily.lean:183 |
Derivative of the normalized finite exponential-family mass | |
finiteExponentialPMF_pos |
definition | FormalSLT/Statistics/ExponentialFamily.lean:108 |
Positive base weights give positive normalized masses | |
finiteExponentialPMF_sum_one |
definition | FormalSLT/Statistics/ExponentialFamily.lean:82 |
Normalized exponential-family masses sum to one | |
finiteLogPartition |
definition | FormalSLT/Statistics/ExponentialFamily.lean:59 |
Log-partition function A(theta) = log Z(theta) | |
finiteLogPartition_hasDerivAt |
definition | FormalSLT/Statistics/ExponentialFamily.lean:160 |
Log-partition derivative identity A'(theta) = E_theta[T] | |
finiteLogPartition_hasDerivAt_of_positiveBase |
definition | FormalSLT/Statistics/ExponentialFamily.lean:171 |
Positive-base wrapper for A'(theta) = E_theta[T] | |
finiteLogPartition_hasSecondDerivAt |
definition | FormalSLT/Statistics/ExponentialFamily.lean:282 |
Log-partition curvature identity A''(theta) = Var_theta(T) | |
finiteLogPartition_hasSecondDerivAt_of_positiveBase |
definition | FormalSLT/Statistics/ExponentialFamily.lean:293 |
Positive-base wrapper for A''(theta) = Var_theta(T) | |
finiteMean_deriv_eq_variance |
definition | FormalSLT/Statistics/ExponentialFamily.lean:218 |
Centered second-moment derivative equals finite weighted variance | |
finiteMean_hasDerivAt |
definition | FormalSLT/Statistics/ExponentialFamily.lean:201 |
Differentiating the finite mean gives a centered second moment | |
finitePartition |
definition | FormalSLT/Statistics/ExponentialFamily.lean:55 |
Finite exponential-family partition sum Z(theta) | |
| ERM | finitePartition_hasDerivAt |
definition | FormalSLT/Statistics/ExponentialFamily.lean:117 |
Termwise derivative of the finite partition sum |
finitePartition_pos |
definition | FormalSLT/Statistics/ExponentialFamily.lean:74 |
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:182 |
Weighted Cauchy-Schwarz: Cov² ≤ Var · Var | |
| sample statistics | covariance_score_eq_deriv_mean |
theorem | FormalSLT/Statistics/FisherInformation.lean:125 |
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:108 |
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:662 |
Glivenko-Cantelli class predicate: a.s. uniform-deviation convergence to zero |
| Glivenko-Cantelli, Bernoulli | bernoulliThreeZerosOneOne_uniformDeviation_le_quarter |
theorem | FormalSLT/GlivenkoCantelli.lean:1023 |
Concrete non-vacuity witness: explicit four-sample uniform empirical-CDF deviation ≤ 1/4 |
| Glivenko-Cantelli | classicalGlivenkoCantelli_iid |
theorem | FormalSLT/GlivenkoCantelli.lean:855 |
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:699 |
Uniform a.s. GC from pointwise convergence on closed and strict lower rays |
| Glivenko-Cantelli | empiricalCDF |
theorem | FormalSLT/GlivenkoCantelli.lean:420 |
Empirical CDF as the lower-ray indicator-class empirical average |
| Glivenko-Cantelli | empiricalCDFUniformDeviation |
theorem | FormalSLT/GlivenkoCantelli.lean:605 |
Uniform empirical-CDF deviation sup_x abs(F_n(x) - F(x)) |
| Glivenko-Cantelli | empiricalCDF_eq_lowerRayEmpiricalAverage |
theorem | FormalSLT/GlivenkoCantelli.lean:430 |
Empirical CDF equals the lower-ray indicator empirical average |
| Glivenko-Cantelli | finiteLowerRayBracketingGrid |
theorem | FormalSLT/GlivenkoCantelli.lean:238 |
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:543 |
Deterministic finite-grid bracketing bound on the uniform empirical-CDF deviation |
| Glivenko-Cantelli | lowerRayGC_iff_classicalGlivenkoCantelli |
theorem | FormalSLT/GlivenkoCantelli.lean:684 |
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:799 |
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:956 |
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:827 |
Open-upper-bracket pointwise strong law, the atom-safe companion |
| Hoeffding, VC dimension, Glivenko-Cantelli | vcHoeffdingBridge_for_gcClass |
theorem | FormalSLT/GlivenkoCantelli.lean:926 |
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:979 |
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:313 |
Two-sided Bennett / sub-Gamma tail at a chosen λ for a finite distribution |
| Bernstein, tail bound | bernstein_tail |
theorem | FormalSLT/Concentration/NamedTails.lean:257 |
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:197 |
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:352 |
VC-style ERM excess-risk tail with sharp concentration term |
| Rademacher, VC dimension, ERM | vc_erm_sample_complexity |
theorem | FormalSLT/VC/SampleComplexity.lean:426 |
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:1072 |
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:1678 |
Literal finite iid product-weight absolute expected generalization-gap wrapper |
| PAC-Bayes, ERM, stability | abs_expectedFiniteGeneralizationGap_le_uniformStability_of_coordinateSwap |
theorem | FormalSLT/AlgorithmicStability.lean:1655 |
Literal finite absolute expected generalization-gap wrapper under a finite swap identity |
| PAC-Bayes, stability | abs_expectedFiniteStabilityGap_le_uniformStability_finiteProduct |
theorem | FormalSLT/AlgorithmicStability.lean:1553 |
Uniform stability gives finite iid two-sided expected stability gap ≤ β |
| PAC-Bayes, stability | abs_expectedFiniteStabilityGap_le_uniformStability_of_coordinateSwap |
theorem | FormalSLT/AlgorithmicStability.lean:1512 |
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:955 |
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:381 |
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:205 |
Finite centered bounded-variance Bennett MGF |
| Bennett, MGF, PAC-Bayes, covering / chaining, stability | bennett_mgf_le_one_add |
theorem | FormalSLT/Probability/BernsteinMGF.lean:161 |
Finite Bennett MGF with the affine variance factor retained |
| Bennett, sub-Gamma, MGF, PAC-Bayes, covering / chaining, stability | bennett_mgf_subgamma |
theorem | FormalSLT/Probability/BernsteinMGF.lean:274 |
Sub-Gamma denominator form of the finite Bennett MGF |
| Bernstein, tail bound, PAC-Bayes, stability | bernstein_tail |
theorem | FormalSLT/Probability/BernsteinMGF.lean:346 |
One-sample finite Bernstein upper-tail bound |
| PAC-Bayes, stability | boundedLoss_coordinateSelectedLoss_integrable |
theorem | FormalSLT/AlgorithmicStability.lean:899 |
Bounded empirical coordinate loss is integrable under μⁿ |
| PAC-Bayes, stability | boundedLoss_selectedLoss_integrable |
theorem | FormalSLT/AlgorithmicStability.lean:843 |
Bounded finite-class selected loss is integrable under μⁿ × μ |
| PAC-Bayes, stability | boundedLoss_updateSelectedLoss_integrable |
theorem | FormalSLT/AlgorithmicStability.lean:868 |
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:519 |
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:577 |
β = c0 / n stability corollary for the sharp variant |
| PAC-Bayes, stability | bousquet_elisseeff_uniform_stability_corollary_of_boundedLoss |
theorem | FormalSLT/Stability/BousquetElisseeff.lean:611 |
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:138 |
Pointwise Bennett inequality for a centered bounded variable |
| PAC-Bayes, ERM, stability | expectedFiniteGeneralizationGap_le_uniformStability_finiteProduct |
theorem | FormalSLT/AlgorithmicStability.lean:1601 |
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:1573 |
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:1465 |
Uniform stability gives finite iid product-weight expected gap ≤ β |
| PAC-Bayes, stability | expectedFiniteStabilityGap_le_uniformStability_of_coordinateSwap |
theorem | FormalSLT/AlgorithmicStability.lean:1344 |
Uniform stability gives finite expected gap ≤ β under a finite swap identity |
| PAC-Bayes, stability | expectedStabilityGap_le_uniformStability_piMeasure_of_boundedLoss |
theorem | FormalSLT/AlgorithmicStability.lean:928 |
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:811 |
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:1085 |
Iid finite product sample weights ∏ k, p (S k) |
| PAC-Bayes, stability | finiteProductSampleWeight_coordinateSwapIdentity |
theorem | FormalSLT/AlgorithmicStability.lean:1178 |
Finite iid product weights satisfy the coordinate-swap identity |
| PAC-Bayes, stability | finiteProductSampleWeight_isPMF |
theorem | FormalSLT/PACBayes/FiniteProductBernstein.lean:60 |
Finite i.i.d. product weights package as a PMF on the sample space |
| 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 |
| Bernstein, PAC-Bayes, stability, Bernoulli, risk | indicatorBernsteinVarianceProxy_le_risk_div |
theorem | FormalSLT/PACBayes/IndicatorBernsteinLowRisk.lean:49 |
Pointwise Bernoulli self-bound R_i(1 - R_i)/n <= R_i/n for positive sample size |
| Bernstein, MGF, PAC-Bayes, stability, Bernoulli | indicatorBernstein_normalization_eq_budget |
theorem | FormalSLT/PACBayes/IndicatorBernsteinMoment.lean:56 |
Exact identification of the product-MGF budget with scale 1/(3n) and variance proxy R * (1 - R) / n |
| PAC-Bayes, stability, Bernoulli | indicatorDeviation_centered |
theorem | FormalSLT/PACBayes/IndicatorVariance.lean:77 |
The population-centered indicator loss has exactly zero finite-PMF mean |
| PAC-Bayes, stability, Bernoulli | indicatorDeviation_secondMoment_eq |
theorem | FormalSLT/PACBayes/IndicatorVariance.lean:86 |
Exact finite-PMF variance identity R * (1 - R) for arbitrary Boolean indicator predicates |
| Bernstein, PAC-Bayes, stability, Bernoulli | indicatorFinitePACBayesBernsteinBadSamples |
theorem | FormalSLT/PACBayes/IndicatorBernsteinConfidence.lean:50 |
Samples on which some finite posterior violates the explicit fixed-tilt indicator Bernstein inequality |
| Bernstein, PAC-Bayes, stability, Bernoulli | indicatorFinitePACBayesBernsteinWeightedCatalogBadSamples |
theorem | FormalSLT/PACBayes/IndicatorBernsteinTiltCatalog.lean:54 |
Single exceptional set formed by the finite union of fixed indicator-Bernstein tilt events with budgets delta * weight j |
| Bernstein, PAC-Bayes, stability, Bernoulli | indicatorFixedTiltBadSamples_subset_weightedCatalog |
theorem | FormalSLT/PACBayes/IndicatorBernsteinTiltCatalog.lean:101 |
Every entrywise indicator-Bernstein exceptional set is contained in the catalog union |
| PAC-Bayes, stability, risk, Bernoulli | indicatorPopulationRisk_mem_Icc |
theorem | FormalSLT/PACBayes/IndicatorVariance.lean:70 |
Population risk of an arbitrary Boolean indicator under a finite PMF lies in [0,1] |
| Bernstein, PAC-Bayes, stability, Bernoulli, MGF | indicator_expectedPriorBernsteinExpMoment_le_one |
theorem | FormalSLT/PACBayes/IndicatorBernsteinMoment.lean:82 |
Prior-averaged normalized indicator Bernstein moment under the finite i.i.d. product law |
| Bernstein, PAC-Bayes, stability, Bernoulli | indicator_finitePACBayesBernstein_fixedLambda_badEventMass_le_delta |
theorem | FormalSLT/PACBayes/IndicatorBernsteinConfidence.lean:95 |
End-to-end finite i.i.d. indicator PAC-Bayes Bernstein bad-event mass bound, simultaneous over all finite posteriors |
| Bernstein, PAC-Bayes, stability | indicator_finitePACBayesBernstein_twoThirds_badEventMass_le_delta |
theorem | FormalSLT/PACBayes/IndicatorBernsteinLowRisk.lean:287 |
Product-law mass bound for the shared fixed-tilt exceptional set at lambda = 2n/3 |
| Bernstein, union bound, PAC-Bayes, stability, Bernoulli | indicator_finitePACBayesBernstein_weightedCatalog_badEventMass_le_delta |
theorem | FormalSLT/PACBayes/IndicatorBernsteinTiltCatalog.lean:162 |
Finite weighted union bound giving catalog exceptional mass at most delta when positive weights sum to at most one |
| PAC-Bayes, stability, Bernoulli | indicator_mem_weightedCatalog_iff |
theorem | FormalSLT/PACBayes/IndicatorBernsteinTiltCatalog.lean:66 |
Membership in the weighted catalog event is equivalent to membership in at least one entrywise bad set |
| PAC-Bayes, stability, Bernoulli | indicator_not_mem_weightedCatalog_iff |
theorem | FormalSLT/PACBayes/IndicatorBernsteinTiltCatalog.lean:80 |
A sample is outside the catalog event exactly when it is outside every entrywise bad set |
| sub-Gamma, MGF, PAC-Bayes, stability, Bernoulli | indicator_oneCoordinateDeviationMGF_le |
theorem | FormalSLT/PACBayes/FiniteProductBernstein.lean:75 |
One-coordinate indicator sub-Gamma MGF using exact hypothesis-specific variance |
| Bernstein, PAC-Bayes, ERM, stability, Bernoulli | indicator_posteriorGeneralizationGap_le_of_not_mem |
theorem | FormalSLT/PACBayes/IndicatorBernsteinConfidence.lean:64 |
Every finite posterior satisfies the explicit indicator Bernstein inequality outside the specialized bad set |
| PAC-Bayes, ERM, stability, Bernoulli | indicator_posteriorGeneralizationGap_le_weightedCatalog_of_not_mem |
theorem | FormalSLT/PACBayes/IndicatorBernsteinTiltCatalog.lean:118 |
On one good event, every posterior satisfies every fixed tilt in the weighted finite catalog |
| PAC-Bayes, stability, risk | indicator_posteriorRisk_le_lowRisk_of_not_mem |
theorem | FormalSLT/PACBayes/IndicatorBernsteinLowRisk.lean:187 |
General fixed-tilt observable risk inequality for 0 < lambda < 6n/5, with exact rearranged coefficients |
| PAC-Bayes, stability, risk | indicator_posteriorRisk_le_min_one_twoThirds_of_not_mem |
theorem | FormalSLT/PACBayes/IndicatorBernsteinLowRisk.lean:263 |
Public certificate form truncating the observable low-risk bound by the universal upper bound one |
| PAC-Bayes, KL divergence, stability, risk | indicator_posteriorRisk_le_twoThirds_of_not_mem |
theorem | FormalSLT/PACBayes/IndicatorBernsteinLowRisk.lean:239 |
At lambda = 2n/3, every posterior outside the parent bad set satisfies R_rho <= (7/4) Rhat_rho + (21/(8n))(KL + log(1/delta)) |
| PAC-Bayes, stability, risk, Bernoulli | indicator_posteriorRisk_le_weightedLowRiskCatalog_of_not_mem |
theorem | FormalSLT/PACBayes/IndicatorBernsteinTiltCatalog.lean:224 |
Observable low-risk bound for every entry of the weighted finite catalog |
| PAC-Bayes, stability, risk, Bernoulli | indicator_posteriorRisk_le_weightedLowRiskCatalog_selected_of_not_mem |
theorem | FormalSLT/PACBayes/IndicatorBernsteinTiltCatalog.lean:255 |
Valid post-sample and posterior-dependent selection from the fixed finite weighted tilt catalog |
| Bernstein, MGF, PAC-Bayes, stability, Bernoulli | indicator_product_mgf_le |
theorem | FormalSLT/PACBayes/FiniteProductBernstein.lean:110 |
Tensorized finite-product MGF with exact R * (1 - R) Bernstein budget |
| MGF, PAC-Bayes, stability, Bernoulli | indicator_product_normalizedMGF_le_one |
theorem | FormalSLT/PACBayes/FiniteProductBernstein.lean:149 |
Hypothesis-specific normalized product MGF at fixed 0 < lambda < 3n |
| 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 |
| Bernstein, PAC-Bayes, stability, risk | posteriorIndicatorBernsteinVarianceProxy_le_risk_div |
theorem | FormalSLT/PACBayes/IndicatorBernsteinLowRisk.lean:61 |
Posterior-average self-bound V_rho <= R_rho/n |
| 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:548 |
Uniform stability gives bounded differences for the gen gap scaffold |
| McDiarmid, PAC-Bayes, stability | trainingLoss_hasBoundedDifferences |
theorem | FormalSLT/AlgorithmicStability.lean:461 |
Uniform stability gives bounded differences for training loss |
| PAC-Bayes | fairBoolGaussianPACBayesFailure_mass_ge_twoPowNegHundred |
theorem | FormalSLT/PACBayes/IIDContinuousGaussian.lean:846 |
Explicit positive-mass witness: the first-100-true cylinder has probability 2⁻¹⁰⁰ and lies inside the worked Gaussian PAC-Bayes failure event |
| PAC-Bayes, Bernoulli, risk | fairBoolThreshold_endToEnd_certificate |
theorem | FormalSLT/PACBayes/IIDContinuousGaussian.lean:889 |
Stochastic fair-Bernoulli product-stream instance with a checked nonconstant Gaussian-threshold loss, exact population risk 1/2, evaluated penalty 54/275, and a positive-probability failure cylinder, without a tightness claim |
| PAC-Bayes | fairBoolThreshold_twoGaussianGrid_certificate |
theorem | FormalSLT/PACBayes/IIDContinuousGaussianGrid.lean:272 |
Stochastic two-entry certificate for N(0,1) at tilt 1/2 and N(1,1) at tilt 1/4, with total failure budget exp(-1) |
| PAC-Bayes, Bernoulli | fairBoolThreshold_twoGaussianSelected_certificate |
theorem | FormalSLT/PACBayes/IIDContinuousGaussianGrid.lean:303 |
The worked two-entry fair-Bernoulli catalog remains valid for every sample-dependent Boolean selector |
| PAC-Bayes, ERM | pacBayesPriorMixture_supermartingale |
theorem | FormalSLT/PACBayes/TimeUniformPACBayes.lean:98 |
Prior mixture of per-hypothesis fixed-tilt exponential processes is a nonnegative supermartingale |
| PAC-Bayes, KL divergence | sphericalGaussianMeasure_klDiv_toReal_eq |
theorem | FormalSLT/PACBayes/GaussianMeasureKL.lean:741 |
Measure-theoretic KL between finite-dimensional spherical Gaussian laws equals its explicit closed form |
| PAC-Bayes | timeUniformContinuousPACBayes_bound |
theorem | FormalSLT/PACBayes/TimeUniformContinuousPACBayes.lean:275 |
Process-level time-uniform PAC-Bayes theorem on an arbitrary measurable hypothesis space for a fixed prior and posterior |
| PAC-Bayes, KL divergence | timeUniformIIDGaussianPACBayes_bound |
theorem | FormalSLT/PACBayes/IIDContinuousGaussian.lean:162 |
End-to-end i.i.d. bounded-loss theorem over a continuous finite-dimensional hypothesis space with explicit spherical-Gaussian KL |
| confidence sequence, PAC-Bayes | timeUniformIIDGaussianPACBayes_grid_bound |
theorem | FormalSLT/PACBayes/IIDContinuousGaussianGrid.lean:118 |
Simultaneous time-uniform i.i.d. bound for a finite catalog of fixed spherical-Gaussian posterior/tilt pairs, with entrywise confidence budgets summed explicitly |
| PAC-Bayes | timeUniformIIDGaussianPACBayes_selected_bound |
theorem | FormalSLT/PACBayes/IIDContinuousGaussianGrid.lean:184 |
Data-dependent selector corollary for an arbitrary choice from the fixed finite Gaussian posterior/tilt catalog |
| PAC-Bayes | timeUniformIIDPACBayes_allPosteriors_bound |
theorem | FormalSLT/PACBayes/TimeUniformIID.lean:368 |
End-to-end finite-class i.i.d. bounded-loss theorem, simultaneous over all posterior PMFs at every positive sample time |
| PAC-Bayes | timeUniformIIDPACBayes_grid_allPosteriors_bound |
theorem | FormalSLT/PACBayes/TimeUniformIIDGrid.lean:88 |
Finite-class i.i.d. theorem with a fixed finite grid of data-dependent tilt choices, simultaneous over all posterior PMFs |
| PAC-Bayes | timeUniformPACBayes_bound |
theorem | FormalSLT/PACBayes/TimeUniformPACBayes.lean:342 |
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:148 |
Ville crossing bound for the prior-mixture process over all times |
| PAC-Bayes | timeUniformSphericalGaussianPACBayes_bound |
theorem | FormalSLT/PACBayes/TimeUniformGaussianPACBayes.lean:72 |
Process-level time-uniform PAC-Bayes theorem specialized to a fixed finite-dimensional spherical-Gaussian prior/posterior pair |
| 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:266 |
Supplied-supremum adapter for the two-point packaged Dudley instance |
| Rademacher, covering / chaining | twoPointRademacherSup_dudley_m_bound |
definition | FormalSLT/Covering/TwoPointDudley.lean:277 |
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:249 |
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:3663 |
Bundled assumptions for the [0,1] finite-class dyadic confidence sequence |
| confidence sequence | FiniteClassConfidenceSequence.failure_probability_le |
theorem | FormalSLT/UniformConvergence.lean:3740 |
Bundled API theorem bounding the named confidence-sequence failure event |
| Hoeffding, confidence sequence | anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_confidenceSequence_fromHoeffding |
theorem | FormalSLT/UniformConvergence.lean:3685 |
Confidence-sequence failure-probability theorem for all natural times and finite hypotheses |
| Hoeffding, confidence sequence | anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_namedRadius_exists_fromHoeffding |
theorem | FormalSLT/UniformConvergence.lean:3604 |
Existential-event anytime theorem using the named dyadic confidence radius |
| Hoeffding, confidence sequence | anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_timeVaryingRadius_exists_fromHoeffding |
theorem | FormalSLT/UniformConvergence.lean:3540 |
Existential-event version of the countable-time finite-class Hoeffding theorem |
| Hoeffding, confidence sequence | anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_timeVaryingRadius_fromHoeffding |
theorem | FormalSLT/UniformConvergence.lean:3340 |
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:1067 |
Finite-sum range envelope from a pointwise uniform range-width bound | |
empiricalAverageRangeSum_pos_of_exists_range_pos |
theorem | FormalSLT/UniformConvergence.lean:1092 |
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:1024 |
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:1117 |
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:1141 |
Two-sided Hoeffding tail bridge using pointwise range width and an explicit nondegenerate sample coordinate |
empiricalAverageUniformRangeSampleSize_ge_of_sqrtBudget_le |
theorem | FormalSLT/UniformConvergence.lean:2134 |
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:3646 |
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:1955 |
Concrete real dyadic class budget maps exactly to the ENNReal dyadic time/class split | |
finiteDyadicRealBudget_horizon_le_time |
theorem | FormalSLT/UniformConvergence.lean:2261 |
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:2426 |
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:2667 |
Route-facing finite-prefix finite-class Hoeffding deviation theorem with the closed-form sample-size condition |
| Hoeffding | finitePrefixFiniteClassDeviationFromHoeffding_closedForm_cardSample |
theorem | FormalSLT/UniformConvergence.lean:2724 |
Route-facing finite-prefix finite-class Hoeffding theorem with denominator written directly as (s.card : ℝ) |
| Hoeffding | finitePrefixFiniteClassDeviationFromHoeffding_closedForm_unitRange |
theorem | FormalSLT/UniformConvergence.lean:2788 |
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:2928 |
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:2996 |
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:2857 |
Route-facing unit-range finite-prefix finite-class Hoeffding theorem in confidence-radius form |
| Hoeffding | finitePrefixFiniteClassDeviationFromHoeffding_zeroOneRange_explicitRadius |
theorem | FormalSLT/UniformConvergence.lean:3079 |
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:3149 |
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:3224 |
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:1171 |
Finite-prefix dyadic finite-class deviation bound from bounded independent empirical-average losses |
| Hoeffding | finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_closedFormHorizonRadius_dyadicRealBudget |
theorem | FormalSLT/UniformConvergence.lean:2461 |
Shared-sample finite-prefix wrapper using a closed-form horizon/class/budget radius |
| Hoeffding | finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_closedFormHorizonSampleSize_dyadicRealBudget |
theorem | FormalSLT/UniformConvergence.lean:2535 |
Shared-sample finite-prefix wrapper using a closed-form horizon/class/budget sample-size condition |
| Hoeffding | finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_dyadicBudget |
theorem | FormalSLT/UniformConvergence.lean:1262 |
Shared-sample finite-prefix wrapper for bounded independent empirical-average losses |
| Hoeffding | finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_epsilonOfSampleSize_dyadicRealBudget |
theorem | FormalSLT/UniformConvergence.lean:2184 |
Shared-sample finite-prefix wrapper using a radius-style condition and the concrete dyadic real budget |
| Hoeffding | finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_horizonUniformRadius_dyadicRealBudget |
theorem | FormalSLT/UniformConvergence.lean:2300 |
Shared-sample finite-prefix wrapper using one horizon-level radius condition |
| Hoeffding | finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize |
theorem | FormalSLT/UniformConvergence.lean:1576 |
Shared-sample finite-prefix wrapper using the displayed sample-size Hoeffding budget |
| Hoeffding | finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize_dyadicRealBudget |
theorem | FormalSLT/UniformConvergence.lean:2012 |
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:1810 |
Shared-sample finite-prefix wrapper using real log budgets below the dyadic ENNReal budget split |
| Hoeffding | finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize_ge |
theorem | FormalSLT/UniformConvergence.lean:1882 |
Shared-sample finite-prefix wrapper using explicit sample-size lower bounds and real budgets |
| Hoeffding | finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize_threshold |
theorem | FormalSLT/UniformConvergence.lean:1648 |
Shared-sample finite-prefix wrapper using a displayed sample-size Hoeffding budget and time-varying thresholds |
| Hoeffding | finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_twoSidedTailBudget |
theorem | FormalSLT/UniformConvergence.lean:1318 |
Shared-sample finite-prefix wrapper using one combined two-sided Hoeffding budget |
| Hoeffding | finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_uniformRangeBudget |
theorem | FormalSLT/UniformConvergence.lean:1383 |
Shared-sample finite-prefix wrapper using one uniform range proxy and dyadic time budgets |
| Hoeffding | finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_uniformRangeBudget_of_rangeBound |
theorem | FormalSLT/UniformConvergence.lean:1445 |
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:1511 |
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:3770 |
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 | continuous_dudley_oneStep_entropy_integral_iSup_unitInterval_pairCountEnvelope |
definition | FormalSLT/Covering/ContinuousDudleyUnitIntervalCovering.lean:462 |
Guarded continuous Dudley capstone for [0,1] with the pair-count chaining envelope integrand |
| covering / chaining | monotone_unitIntervalRoundedDyadicGridCoverCount |
definition | FormalSLT/Covering/UnitIntervalDudley.lean:1204 |
Rounded dyadic adjacent-level cover counts are monotone in the scale |
| covering / chaining | monotone_unitIntervalRoundedDyadicGridEntropy |
definition | FormalSLT/Covering/UnitIntervalDudley.lean:1221 |
Rounded dyadic entropy-at-scale sequence is monotone |
| covering / chaining | unitIntervalChainingPairCountEnvelope |
definition | FormalSLT/Covering/ContinuousDudleyUnitIntervalCovering.lean:40 |
Real-radius half-open pair-count chaining envelope for [0,1]; not a metric covering number |
| 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 | unitIntervalPairCountEntropy_eq_pair_count_sample |
definition | FormalSLT/Covering/ContinuousDudleyUnitIntervalCovering.lean:295 |
The staircase entropy samples the rounded-grid adjacent pair-count product at every dyadic radius |
| 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:1900 |
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:2198 |
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:2517 |
Constant-envelope first-scale bound evaluated to a scalar expression |
| Rademacher, covering / chaining | unitIntervalRademacherLinearSup_dudley_m1_bound_of_entropy |
definition | FormalSLT/Covering/UnitIntervalDudley.lean:2369 |
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:1806 |
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:1778 |
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:2175 |
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:1982 |
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:2161 |
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:2073 |
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:2148 |
Named m = 3 supplied-supremum rounded dyadic-grid Dudley corollary |
| Rademacher, covering / chaining | unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m_bound |
definition | FormalSLT/Covering/UnitIntervalDudley.lean:2107 |
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:2133 |
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:1154 |
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:1881 |
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:1583 |
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:1619 |
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:1700 |
Named m = 3 projected rounded dyadic-grid Dudley corollary |
| Rademacher, covering / chaining | unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m_bound |
definition | FormalSLT/Covering/UnitIntervalDudley.lean:1657 |
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:1682 |
Arbitrary finite-horizon projected rounded-grid Dudley bound with the prefix-sup envelope removed |
| covering / chaining | unitIntervalRoundedDyadicGridCoverCount |
definition | FormalSLT/Covering/UnitIntervalDudley.lean:1199 |
Adjacent-level covering-product envelope for the shifted rounded dyadic sequence |
| covering / chaining | unitIntervalRoundedDyadicGridDudleyInstance |
definition | FormalSLT/Covering/UnitIntervalDudley.lean:1571 |
Packaged finite dyadic Dudley instance for the rounded unit-interval grid sequence |
| covering / chaining | unitIntervalRoundedDyadicGridEntropy_prefixSup |
definition | FormalSLT/Covering/UnitIntervalDudley.lean:1237 |
Prefix-sup envelope collapses for the rounded dyadic entropy sequence |
| covering / chaining | unitIntervalRoundedDyadicGridIndex |
definition | FormalSLT/Covering/UnitIntervalDudley.lean:1189 |
Shifted rounded dyadic grid index sequence, starting at level 1 |
| covering / chaining | unitIntervalRoundedDyadicGridNet |
definition | FormalSLT/Covering/UnitIntervalDudley.lean:1194 |
Shifted rounded dyadic finite-net sequence for finite-scale Dudley chaining |
| covering / chaining | unitIntervalRoundedDyadicGridNet_coverCount_le |
definition | FormalSLT/Covering/UnitIntervalDudley.lean:1365 |
Adjacent rounded dyadic covering-number product is bounded by the cover-count envelope |
| covering / chaining | unitIntervalRoundedDyadicGridNet_coverCount_le_range |
definition | FormalSLT/Covering/UnitIntervalDudley.lean:1395 |
Range wrapper for the adjacent rounded-grid covering-product envelope over any finite horizon |
| covering / chaining | unitIntervalRoundedDyadicGridNet_coveringNumber_product |
definition | FormalSLT/Covering/UnitIntervalDudley.lean:1293 |
Adjacent rounded dyadic covering-number product equals the reusable cover-count envelope |
| Rademacher, covering / chaining | unitIntervalRoundedDyadicGridNet_dist |
definition | FormalSLT/Covering/UnitIntervalDudley.lean:1246 |
Shifted rounded dyadic finite nets use the Rademacher process metric |
| covering / chaining | unitIntervalRoundedDyadicGridNet_pair_card_gt_one |
definition | FormalSLT/Covering/UnitIntervalDudley.lean:1318 |
Adjacent rounded dyadic projection-pair family is nontrivial at every scale |
| covering / chaining | unitIntervalRoundedDyadicGridNet_pair_card_gt_one_range |
definition | FormalSLT/Covering/UnitIntervalDudley.lean:1386 |
Range wrapper for nontrivial adjacent projection-pair families over any finite horizon |
| covering / chaining | unitIntervalRoundedDyadicGridNet_radius_geometric |
definition | FormalSLT/Covering/UnitIntervalDudley.lean:1261 |
Adjacent rounded dyadic radii satisfy the geometric chaining radius budget |
| covering / chaining | unitIntervalRoundedDyadicGridNet_radius_geometric_range |
definition | FormalSLT/Covering/UnitIntervalDudley.lean:1378 |
Range wrapper for the geometric radius budget over any finite horizon |
| covering / chaining | unitIntervalRoundedDyadicGridNet_radius_pos |
definition | FormalSLT/Covering/UnitIntervalDudley.lean:1252 |
Adjacent rounded dyadic radii have positive sum at every scale |
| covering / chaining | unitIntervalRoundedDyadicGridNet_radius_pos_range |
definition | FormalSLT/Covering/UnitIntervalDudley.lean:1371 |
Range wrapper for positive adjacent rounded dyadic radii over any finite horizon |
| covering / chaining | unitInterval_pairCountEntropy_integral_positive |
definition | FormalSLT/Covering/ContinuousDudleyUnitIntervalCovering.lean:339 |
The pair-count entropy integrand has positive interval mass |
| covering / chaining | unitInterval_pairCountEntropy_nonconstant |
definition | FormalSLT/Covering/ContinuousDudleyUnitIntervalCovering.lean:304 |
The pair-count entropy integrand is nonconstant |
| 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 |