OAI/Analysis/Cotype/ParameterChoice.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Cotype.degreeCutoff_pow_twoline 10 - theorem
OAI.Cotype.twice_lt_two_powline 16 - theorem
OAI.Cotype.eventually_cube_le_exponentialline 21 - theorem
OAI.Cotype.source_lift_scaleline 29 - theorem
OAI.Cotype.exists_admissible_cotype_parametersline 43