import FormalSLT.UniformConvergence

/-!
# Uniform-convergence checker

This file checks the finite-class probability bridges used by the current
uniform-convergence spine.

```bash
lake env lean examples/CheckUniformConvergence.lean
```
-/

#check FormalSLT.UniformConvergence.finiteClassUniformDeviationUnionBound
#print axioms FormalSLT.UniformConvergence.finiteClassUniformDeviationUnionBound

#check FormalSLT.UniformConvergence.finiteClassUniformDeviationUnionBound_cardInv
#print axioms FormalSLT.UniformConvergence.finiteClassUniformDeviationUnionBound_cardInv

#check FormalSLT.UniformConvergence.finiteClassTwoSidedUniformDeviationUnionBound
#print axioms FormalSLT.UniformConvergence.finiteClassTwoSidedUniformDeviationUnionBound

#check FormalSLT.UniformConvergence.finiteClassTwoSidedUniformDeviationUnionBound_cardInv
#print axioms FormalSLT.UniformConvergence.finiteClassTwoSidedUniformDeviationUnionBound_cardInv

#check FormalSLT.UniformConvergence.finiteTimeClassUnionBound_cardInv
#print axioms FormalSLT.UniformConvergence.finiteTimeClassUnionBound_cardInv

#check FormalSLT.UniformConvergence.finiteTimeClassTwoSidedUniformDeviationUnionBound_cardInv
#print axioms FormalSLT.UniformConvergence.finiteTimeClassTwoSidedUniformDeviationUnionBound_cardInv

#check FormalSLT.UniformConvergence.finiteTimeClassUnionBound_timeBudget
#print axioms FormalSLT.UniformConvergence.finiteTimeClassUnionBound_timeBudget

#check FormalSLT.UniformConvergence.finiteTimeClassTwoSidedUniformDeviationUnionBound_timeBudget
#print axioms FormalSLT.UniformConvergence.finiteTimeClassTwoSidedUniformDeviationUnionBound_timeBudget

#check FormalSLT.UniformConvergence.finiteTimeClassTwoSidedUniformDeviationUnionBound_timeBudget_threshold
#print axioms FormalSLT.UniformConvergence.finiteTimeClassTwoSidedUniformDeviationUnionBound_timeBudget_threshold

#check FormalSLT.UniformConvergence.finiteDyadicTimeBudget

#check FormalSLT.UniformConvergence.finiteDyadicTimeBudget_sum_fin_le
#print axioms FormalSLT.UniformConvergence.finiteDyadicTimeBudget_sum_fin_le

#check FormalSLT.UniformConvergence.finiteTimeClassUnionBound_dyadicBudget
#print axioms FormalSLT.UniformConvergence.finiteTimeClassUnionBound_dyadicBudget

#check FormalSLT.UniformConvergence.finiteTimeClassTwoSidedUniformDeviationUnionBound_dyadicBudget
#print axioms FormalSLT.UniformConvergence.finiteTimeClassTwoSidedUniformDeviationUnionBound_dyadicBudget

#check FormalSLT.UniformConvergence.finiteTimeClassTwoSidedUniformDeviationUnionBound_dyadicBudget_threshold
#print axioms FormalSLT.UniformConvergence.finiteTimeClassTwoSidedUniformDeviationUnionBound_dyadicBudget_threshold

#check FormalSLT.UniformConvergence.finiteTimeClassTwoSidedUnionBoundFromOneSidedTails_dyadicBudget
#print axioms FormalSLT.UniformConvergence.finiteTimeClassTwoSidedUnionBoundFromOneSidedTails_dyadicBudget

#check FormalSLT.UniformConvergence.empiricalAverageUpperHoeffdingTail

#check FormalSLT.UniformConvergence.empiricalAverageLowerHoeffdingTail

#check FormalSLT.UniformConvergence.finiteTimeClassEmpiricalAverageDeviationFromHoeffding_dyadicBudget
#print axioms FormalSLT.UniformConvergence.finiteTimeClassEmpiricalAverageDeviationFromHoeffding_dyadicBudget

#check FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_dyadicBudget
#print axioms FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_dyadicBudget

#check FormalSLT.UniformConvergence.empiricalAverageUpperHoeffdingTail_eq_lower
#print axioms FormalSLT.UniformConvergence.empiricalAverageUpperHoeffdingTail_eq_lower

#check FormalSLT.UniformConvergence.empiricalAverageTwoSidedHoeffdingTail

#check FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_twoSidedTailBudget
#print axioms FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_twoSidedTailBudget

#check FormalSLT.UniformConvergence.empiricalAverageUniformRangeTwoSidedHoeffdingTail

#check FormalSLT.UniformConvergence.empiricalAverageTwoSidedHoeffdingTail_le_uniformRangeTwoSidedHoeffdingTail
#print axioms FormalSLT.UniformConvergence.empiricalAverageTwoSidedHoeffdingTail_le_uniformRangeTwoSidedHoeffdingTail

#check FormalSLT.UniformConvergence.empiricalAverageRangeSum_le_card_mul_uniformRange
#print axioms FormalSLT.UniformConvergence.empiricalAverageRangeSum_le_card_mul_uniformRange

#check FormalSLT.UniformConvergence.empiricalAverageRangeSum_pos_of_exists_range_pos
#print axioms FormalSLT.UniformConvergence.empiricalAverageRangeSum_pos_of_exists_range_pos

#check FormalSLT.UniformConvergence.empiricalAverageTwoSidedHoeffdingTail_le_uniformRangeTwoSidedHoeffdingTail_of_rangeBound
#print axioms FormalSLT.UniformConvergence.empiricalAverageTwoSidedHoeffdingTail_le_uniformRangeTwoSidedHoeffdingTail_of_rangeBound

#check FormalSLT.UniformConvergence.empiricalAverageTwoSidedHoeffdingTail_le_uniformRangeTwoSidedHoeffdingTail_of_rangeBound_of_exists_range_pos
#print axioms FormalSLT.UniformConvergence.empiricalAverageTwoSidedHoeffdingTail_le_uniformRangeTwoSidedHoeffdingTail_of_rangeBound_of_exists_range_pos

#check FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_uniformRangeBudget
#print axioms FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_uniformRangeBudget

#check FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_uniformRangeBudget_of_rangeBound
#print axioms FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_uniformRangeBudget_of_rangeBound

#check FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_uniformRangeBudget_of_rangeBound_of_exists_range_pos
#print axioms FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_uniformRangeBudget_of_rangeBound_of_exists_range_pos

#check FormalSLT.UniformConvergence.empiricalAverageUniformRangeTwoSidedHoeffdingSampleSizeTail

#check FormalSLT.UniformConvergence.empiricalAverageUniformRangeTwoSidedHoeffdingTail_eq_sampleSizeTail
#print axioms FormalSLT.UniformConvergence.empiricalAverageUniformRangeTwoSidedHoeffdingTail_eq_sampleSizeTail

#check FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize
#print axioms FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize

#check FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize_threshold
#print axioms FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize_threshold

#check FormalSLT.UniformConvergence.empiricalAverageUniformRangeTwoSidedHoeffdingSampleSizeTail_le_of_logBudget
#print axioms FormalSLT.UniformConvergence.empiricalAverageUniformRangeTwoSidedHoeffdingSampleSizeTail_le_of_logBudget

#check FormalSLT.UniformConvergence.empiricalAverageUniformRangeTwoSidedHoeffdingSampleSizeTail_le_of_explicitRadius
#print axioms FormalSLT.UniformConvergence.empiricalAverageUniformRangeTwoSidedHoeffdingSampleSizeTail_le_of_explicitRadius

#check FormalSLT.UniformConvergence.empiricalAverageUniformRangeTwoSidedHoeffdingSampleSizeTail_le_of_sampleSize_ge
#print axioms FormalSLT.UniformConvergence.empiricalAverageUniformRangeTwoSidedHoeffdingSampleSizeTail_le_of_sampleSize_ge

#check FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize_from_logBudget
#print axioms FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize_from_logBudget

#check FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize_ge
#print axioms FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize_ge

#check FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize_dyadicRealBudget
#print axioms FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_sampleSize_dyadicRealBudget

#check FormalSLT.UniformConvergence.finiteDyadicRealBudget_classBudget_ofReal
#print axioms FormalSLT.UniformConvergence.finiteDyadicRealBudget_classBudget_ofReal

#check FormalSLT.UniformConvergence.empiricalAverageUniformRangeSampleSize_ge_of_sqrtBudget_le
#print axioms FormalSLT.UniformConvergence.empiricalAverageUniformRangeSampleSize_ge_of_sqrtBudget_le

#check FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_epsilonOfSampleSize_dyadicRealBudget
#print axioms FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_epsilonOfSampleSize_dyadicRealBudget

#check FormalSLT.UniformConvergence.finiteDyadicRealBudget_horizon_le_time
#print axioms FormalSLT.UniformConvergence.finiteDyadicRealBudget_horizon_le_time

#check FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_horizonUniformRadius_dyadicRealBudget
#print axioms FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_horizonUniformRadius_dyadicRealBudget

#check FormalSLT.UniformConvergence.finiteDyadicRealBudget_horizon_logBudget_eq_closedForm
#print axioms FormalSLT.UniformConvergence.finiteDyadicRealBudget_horizon_logBudget_eq_closedForm

#check FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_closedFormHorizonRadius_dyadicRealBudget
#print axioms FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_closedFormHorizonRadius_dyadicRealBudget

#check FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_closedFormHorizonSampleSize_dyadicRealBudget
#print axioms FormalSLT.UniformConvergence.finiteTimeClassSharedSampleEmpiricalAverageDeviationFromHoeffding_closedFormHorizonSampleSize_dyadicRealBudget

#check FormalSLT.UniformConvergence.finitePrefixFiniteClassDeviationFromHoeffding_closedForm
#print axioms FormalSLT.UniformConvergence.finitePrefixFiniteClassDeviationFromHoeffding_closedForm

#check FormalSLT.UniformConvergence.finitePrefixFiniteClassDeviationFromHoeffding_closedForm_cardSample
#print axioms FormalSLT.UniformConvergence.finitePrefixFiniteClassDeviationFromHoeffding_closedForm_cardSample

#check FormalSLT.UniformConvergence.finitePrefixFiniteClassDeviationFromHoeffding_closedForm_unitRange
#print axioms FormalSLT.UniformConvergence.finitePrefixFiniteClassDeviationFromHoeffding_closedForm_unitRange

#check FormalSLT.UniformConvergence.finitePrefixFiniteClassDeviationFromHoeffding_unitRange_radius
#print axioms FormalSLT.UniformConvergence.finitePrefixFiniteClassDeviationFromHoeffding_unitRange_radius

#check FormalSLT.UniformConvergence.finitePrefixFiniteClassDeviationFromHoeffding_unitRange_explicitRadius
#print axioms FormalSLT.UniformConvergence.finitePrefixFiniteClassDeviationFromHoeffding_unitRange_explicitRadius

#check FormalSLT.UniformConvergence.finitePrefixFiniteClassDeviationFromHoeffding_unitRange_explicitRadius_nonemptySample
#print axioms FormalSLT.UniformConvergence.finitePrefixFiniteClassDeviationFromHoeffding_unitRange_explicitRadius_nonemptySample

#check FormalSLT.UniformConvergence.finitePrefixFiniteClassDeviationFromHoeffding_zeroOneRange_explicitRadius
#print axioms FormalSLT.UniformConvergence.finitePrefixFiniteClassDeviationFromHoeffding_zeroOneRange_explicitRadius

#check FormalSLT.UniformConvergence.finitePrefixFiniteClassDeviationFromHoeffding_zeroOneRange_timeVaryingRadius
#print axioms FormalSLT.UniformConvergence.finitePrefixFiniteClassDeviationFromHoeffding_zeroOneRange_timeVaryingRadius

#check FormalSLT.UniformConvergence.finitePrefixFiniteClassDeviationFromHoeffding_zeroOneRange_timeVaryingRadius_fromHoeffding
#print axioms FormalSLT.UniformConvergence.finitePrefixFiniteClassDeviationFromHoeffding_zeroOneRange_timeVaryingRadius_fromHoeffding

#check FormalSLT.UniformConvergence.finiteDyadicTimeBudget_tsum_le
#print axioms FormalSLT.UniformConvergence.finiteDyadicTimeBudget_tsum_le

#check FormalSLT.UniformConvergence.countableTimeClassUnionBound_timeBudget
#print axioms FormalSLT.UniformConvergence.countableTimeClassUnionBound_timeBudget

#check FormalSLT.UniformConvergence.countableTimeClassUnionBound_dyadicBudget
#print axioms FormalSLT.UniformConvergence.countableTimeClassUnionBound_dyadicBudget

#check FormalSLT.UniformConvergence.countableTimeClassTwoSidedUniformDeviationUnionBound_dyadicBudget_threshold
#print axioms FormalSLT.UniformConvergence.countableTimeClassTwoSidedUniformDeviationUnionBound_dyadicBudget_threshold

#check FormalSLT.UniformConvergence.anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_timeVaryingRadius_fromHoeffding
#print axioms FormalSLT.UniformConvergence.anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_timeVaryingRadius_fromHoeffding

#check FormalSLT.UniformConvergence.countableTimeClass_iUnion_eq_exists
#print axioms FormalSLT.UniformConvergence.countableTimeClass_iUnion_eq_exists

#check FormalSLT.UniformConvergence.anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_timeVaryingRadius_exists_fromHoeffding
#print axioms FormalSLT.UniformConvergence.anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_timeVaryingRadius_exists_fromHoeffding

#check FormalSLT.UniformConvergence.zeroOneDyadicFiniteClassConfidenceRadius

#check FormalSLT.UniformConvergence.zeroOneDyadicFiniteClassConfidenceRadius_le_of_sampleSize_ge
#print axioms FormalSLT.UniformConvergence.zeroOneDyadicFiniteClassConfidenceRadius_le_of_sampleSize_ge

#check FormalSLT.UniformConvergence.countableTimeClass_not_forall_lt_eq_exists_ge
#print axioms FormalSLT.UniformConvergence.countableTimeClass_not_forall_lt_eq_exists_ge

#check FormalSLT.UniformConvergence.anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_namedRadius_exists_fromHoeffding
#print axioms FormalSLT.UniformConvergence.anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_namedRadius_exists_fromHoeffding

#check FormalSLT.UniformConvergence.FiniteClassConfidenceSequence

#check FormalSLT.UniformConvergence.finiteClassConfidenceSequenceFailureEvent

#check FormalSLT.UniformConvergence.FiniteClassConfidenceSequence.failure_probability_le
#print axioms FormalSLT.UniformConvergence.FiniteClassConfidenceSequence.failure_probability_le

#check FormalSLT.UniformConvergence.anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_confidenceSequence_fromHoeffding
#print axioms FormalSLT.UniformConvergence.anytimeFiniteClassDeviationFromHoeffding_zeroOneRange_confidenceSequence_fromHoeffding