OAI/Analysis/Cotype/GrowthCoefficient.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Cotype.abs_character_finite line 10
2. theorem OAI.Cotype.fourier_matrixTwist line 14
3. theorem OAI.Cotype.paritySign_one_or_neg_one line 27
4. theorem OAI.Cotype.GrowthPairingData.normalized_coefficient_identity line 38
5. theorem OAI.Cotype.GrowthPairingData.exists_fixed_lift_coefficient line 54
6. theorem OAI.Cotype.GrowthPairingData.exists_rank_coefficient_constant line 75