import FormalSLT

/-!
# Unit-interval total-bounded Dudley example

Checks the concrete non-finite index-space example used to exercise the
total-bounded finite-net bridge.
-/

#check FormalSLT.Covering.UnitIntervalDudley.UnitInterval
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalZero
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalOne

#check FormalSLT.Covering.UnitIntervalDudley.unitInterval_totallyBounded_univ
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitInterval_totallyBounded_univ

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalFiniteNet
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalFiniteNet_covers
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalFiniteNet_covers

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicFiniteNet
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicFiniteNet_covers
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicFiniteNet_covers

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalQuarterMeshCenter
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalQuarterMeshProject
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalHalfMeshCenter
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalHalfMeshProject

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridIndex
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridCenter
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridCenter_leftEndpoint
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridCenter_leftEndpoint
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridCenter_rightEndpoint
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridCenter_rightEndpoint
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGrid_card
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGrid_card
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridPairCoverCount
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridPairCoverCount_zero
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridPairCoverCount_zero
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridFloorProject
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridFloorProject_dist_le
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridFloorProject_dist_le
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridNet
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridNet_covers
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridNet_covers
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridNet_coveringNumber
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridNet_coveringNumber
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridNet_coveringNumber_one
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridNet_coveringNumber_one
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridNet_coveringNumber_two
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridNet_coveringNumber_two
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridNet_coveringNumberPair_zero
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridNet_coveringNumberPair_zero
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridRoundProject
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridRoundProject_zero
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridRoundProject_zero
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridRoundProject_one
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridRoundProject_one
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridRoundProject_dist_le
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicGridRoundProject_dist_le
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicRoundedGridNet
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicRoundedGridNet_covers
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicRoundedGridNet_covers
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicRoundedGridNet_coveringNumber
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicRoundedGridNet_coveringNumber
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicRoundedGridNet_coveringNumber_one
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicRoundedGridNet_coveringNumber_one
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicRoundedGridNet_coveringNumber_two
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicRoundedGridNet_coveringNumber_two
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicRoundedGridNet_coveringNumberPair_zero
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicRoundedGridNet_coveringNumberPair_zero
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridIndex
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridCoverCount
#check FormalSLT.Covering.UnitIntervalDudley.monotone_unitIntervalRoundedDyadicGridCoverCount
#print axioms FormalSLT.Covering.UnitIntervalDudley.monotone_unitIntervalRoundedDyadicGridCoverCount
#check FormalSLT.Covering.UnitIntervalDudley.monotone_unitIntervalRoundedDyadicGridEntropy
#print axioms FormalSLT.Covering.UnitIntervalDudley.monotone_unitIntervalRoundedDyadicGridEntropy
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridEntropy_prefixSup
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridEntropy_prefixSup
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet_dist
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet_dist
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet_radius_pos
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet_radius_pos
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet_radius_geometric
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet_radius_geometric
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet_pair_card_gt_one
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet_pair_card_gt_one
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet_coveringNumber_product
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet_coveringNumber_product
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet_coverCount_le
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet_coverCount_le
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet_radius_pos_range
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet_radius_pos_range
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet_radius_geometric_range
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet_radius_geometric_range
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet_pair_card_gt_one_range
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet_pair_card_gt_one_range
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet_coverCount_le_range
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNet_coverCount_le_range

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalZeroProcess
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalZeroProcess_increment_mgf
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalZeroProcess_increment_mgf

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalZeroProcess_globalBudget
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalZeroProcess_globalBudget

#check FormalSLT.Covering.UnitIntervalDudley.unitInterval_rademacherLinear_mgf_bound
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitInterval_rademacherLinear_mgf_bound

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearProcess
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearProcess_increment_mgf
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearProcess_increment_mgf

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_expectation
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_expectation

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_upper
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_upper

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_attained
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_attained

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_isLeastUpperBound
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_isLeastUpperBound

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_isLUB_range
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_isLUB_range

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_sSup_range
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_sSup_range

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_dudley_m0_bound
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_dudley_m0_bound

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_dudley_m1_bound_of_entropy
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_dudley_m1_bound_of_entropy

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicPair01_card_gt_one
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicPair01_card_gt_one
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicPair01

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_dudley_m1_bound
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_dudley_m1_bound

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicEntropyM1Condition
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicEntropyCapM1
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicEntropyM1Condition_constCap
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalDyadicEntropyM1Condition_constCap

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_dudley_m1_bound_constEntropy
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_dudley_m1_bound_constEntropy

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_dudley_m1_bound_constEntropy_eval
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_dudley_m1_bound_constEntropy_eval

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalQuarterMeshNet
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalQuarterMeshNet_covers
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalQuarterMeshNet_covers

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalQuarterMeshNet_coveringNumber
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalQuarterMeshNet_coveringNumber

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalHalfMeshNet
#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalHalfMeshNet_covers
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalHalfMeshNet_covers

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalHalfMeshNet_coveringNumber
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalHalfMeshNet_coveringNumber

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalHalfQuarterPair_card_gt_one
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalHalfQuarterPair_card_gt_one

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalHalfQuarter_coveringNumber_product
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalHalfQuarter_coveringNumber_product

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalHalfQuarter_coveringNumber_product_eq_dyadicGridPairCoverCount_zero
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalHalfQuarter_coveringNumber_product_eq_dyadicGridPairCoverCount_zero

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinear_halfQuarter_increment_log15_bound
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinear_halfQuarter_increment_log15_bound

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinear_projectedQuarterMesh_dudley_log15_bound
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinear_projectedQuarterMesh_dudley_log15_bound

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_projectedQuarterMesh_dudley_log15_bound
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_projectedQuarterMesh_dudley_log15_bound

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_projectedQuarterMesh_dudley_log15_bound_eval
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_projectedQuarterMesh_dudley_log15_bound_eval

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinear_roundedDyadicGrid_dudley_log15_bound
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinear_roundedDyadicGrid_dudley_log15_bound

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_log15_bound
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_log15_bound

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_log15_bound_eval
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_log15_bound_eval

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m2_bound
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m2_bound

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m2_bound
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m2_bound

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m_bound
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m_bound

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m_bound_prefixFree
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m_bound_prefixFree

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_le_projectedRoundedDyadicGridSup
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_le_projectedRoundedDyadicGridSup

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinear_projectedRoundedDyadicGridSup_eq
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinear_projectedRoundedDyadicGridSup_eq

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSupRoundedDyadicGridAdapter
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSupRoundedDyadicGridAdapter

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m_bound
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m_bound

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m_bound_prefixFree
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m_bound_prefixFree

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m3_bound
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinear_roundedDyadicGrid_dudley_m3_bound

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m3_bound
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRademacherLinearSup_roundedDyadicGrid_dudley_m3_bound

#check FormalSLT.Covering.FiniteSubGaussianChaining.FiniteSubGaussianProcess.FiniteDyadicNetSequence
#check FormalSLT.Covering.FiniteSubGaussianChaining.FiniteSubGaussianProcess.FiniteDyadicNetSequence.projectedNet_dudley_bound
#print axioms FormalSLT.Covering.FiniteSubGaussianChaining.FiniteSubGaussianProcess.FiniteDyadicNetSequence.projectedNet_dudley_bound

#check FormalSLT.Covering.FiniteSubGaussianChaining.FiniteSubGaussianProcess.FiniteDyadicNetSequence.supFunctional_dudley_bound
#print axioms FormalSLT.Covering.FiniteSubGaussianChaining.FiniteSubGaussianProcess.FiniteDyadicNetSequence.supFunctional_dudley_bound

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNetSequence
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridNetSequence

#check FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridDudleyInstance
#print axioms FormalSLT.Covering.UnitIntervalDudley.unitIntervalRoundedDyadicGridDudleyInstance

#check FormalSLT.Covering.FiniteSubGaussianChaining.FiniteSubGaussianProcess.finiteDyadicEntropyIntegralBudget_one_const
#print axioms FormalSLT.Covering.FiniteSubGaussianChaining.FiniteSubGaussianProcess.finiteDyadicEntropyIntegralBudget_one_const

#check FormalSLT.Covering.FiniteSubGaussianChaining.FiniteSubGaussianProcess.finitePrefixSupEnvelope_const
#print axioms FormalSLT.Covering.FiniteSubGaussianChaining.FiniteSubGaussianProcess.finitePrefixSupEnvelope_const

#check FormalSLT.Covering.FiniteSubGaussianChaining.FiniteSubGaussianProcess.finitePrefixSupEnvelope_eq_self_of_monotone
#print axioms FormalSLT.Covering.FiniteSubGaussianChaining.FiniteSubGaussianProcess.finitePrefixSupEnvelope_eq_self_of_monotone