OAI/Analysis/Cotype/CoefficientPowerGap.lean
1 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Cotype.projectionLinearCoefficient_bound_of_power_gapline 10
OAI/Analysis/Cotype/CoefficientPowerGap.lean1 declarations, 0 contain sorry, 0 declared as axioms
OAI.Cotype.projectionLinearCoefficient_bound_of_power_gap line 10