OAI/Analysis/Cotype/FiniteLevelLift.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Cotype.rademacherSum_L2_leline 12 - theorem
OAI.Cotype.exists_finiteLevel_liftline 26
OAI/Analysis/Cotype/FiniteLevelLift.lean2 declarations, 0 contain sorry, 0 declared as axioms
OAI.Cotype.rademacherSum_L2_le line 12OAI.Cotype.exists_finiteLevel_lift line 26