OAI/Analysis/Cotype/GrowthScalarData.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Cotype.GrowthPairingData.normalizedMatrix line 15
2. def OAI.Cotype.GrowthPairingData.normalizedPrimal line 18
3. def OAI.Cotype.GrowthPairingData.normalizedDual line 21
4. theorem OAI.Cotype.GrowthPairingData.normalizedPrimal_coefficient line 24
5. theorem OAI.Cotype.GrowthPairingData.normalizedDual_coefficient line 31
6. theorem OAI.Cotype.GrowthPairingData.normalizedMatrix_row line 38
7. theorem OAI.Cotype.GrowthPairingData.normalizedMatrix_column line 51
8. theorem OAI.Cotype.GrowthPairingData.normalized_value_bound line 66
9. theorem OAI.Cotype.GrowthPairingData.normalized_scalar_admissible line 76