import FormalSLT.PACBayes.ContinuousInfiniteEmpiricalBernsteinStitch

open FormalSLT.PACBayes.ContinuousInfiniteEmpiricalBernsteinStitch

#check continuousInfiniteEmpiricalBernsteinComplexity_pos
#print axioms continuousInfiniteEmpiricalBernsteinComplexity_pos

#check continuousInfiniteEmpiricalBernsteinReverseSqrtFailure_measurable
#print axioms continuousInfiniteEmpiricalBernsteinReverseSqrtFailure_measurable

#check continuousInfiniteEmpiricalBernsteinReverseSqrtFailure_mass_le_delta
#print axioms continuousInfiniteEmpiricalBernsteinReverseSqrtFailure_mass_le_delta

#check continuousInfiniteEmpiricalBernstein_posteriorRisk_lt_of_not_mem
#print axioms continuousInfiniteEmpiricalBernstein_posteriorRisk_lt_of_not_mem

#check continuousInfiniteEmpiricalBernstein_posteriorRisk_lt_n_of_not_mem
#print axioms continuousInfiniteEmpiricalBernstein_posteriorRisk_lt_n_of_not_mem

#check exists_continuousInfiniteEmpiricalBernstein_event
#print axioms exists_continuousInfiniteEmpiricalBernstein_event