OAI/Analysis/Cotype/CotypeAmplification.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Cotype.rademacherSum_piLp_apply line 12
2. theorem OAI.Cotype.fixedCotypeBound_l2Amplification line 19