OAI/Combinatorics/Progressions/Estimates/IndexedComparableScalarGeometryData.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.scalarTransferCapLog line 12
2. def OAI.Erdos3.scalarTransferAccuracyLog line 14
3. def OAI.Erdos3.scalarTransferCellLog line 17
4. theorem OAI.Erdos3.scalarTransferAllocatedLogs_bounds line 20
5. theorem OAI.Erdos3.scalarTransferMarginalAccuracy_eq_exp line 34
6. def OAI.Erdos3.scalarInitialReferenceInput line 46
7. theorem OAI.Erdos3.scalarInitialReferenceInput_bounds line 51
8. theorem OAI.Erdos3.physicalPairCoefficientLog_mono_dimension line 71
9. def OAI.Erdos3.scalarCombinedLogThreshold line 85
10. theorem OAI.Erdos3.physicalReplacementThresholdLog_mono_dimension line 90
11. theorem OAI.Erdos3.scalarCombinedLogThreshold_bounds line 97
12. theorem OAI.Erdos3.four_mul_exp_le_exp_add_two line 112
13. theorem OAI.Erdos3.scalarCombinedLogThreshold_size_conditions line 123
14. def OAI.Erdos3.scalarInitialPowerInputPolynomial line 161
15. theorem OAI.Erdos3.scalarInitialReferenceInput_le_powerInputPolynomial line 173
16. theorem OAI.Erdos3.exists_scalarInitialReferenceInput_polynomial_input_power line 182
17. theorem OAI.Erdos3.unconditionedSpatialWidthCutoff_le_exp line 199
18. theorem OAI.Erdos3.canonicalScalarPhysicalSize line 235
19. structure OAI.Erdos3.CanonicalScalarGeometryData line 282
20. theorem OAI.Erdos3.canonicalScalarGeometryData line 324
21. structure OAI.Erdos3.ComparableScalarGeometryData line 391
22. theorem OAI.Erdos3.comparableScalarGeometryData line 433
23. structure OAI.Erdos3.IndexedComparableScalarGeometryData line 512
24. theorem OAI.Erdos3.indexedComparableScalarGeometryData line 555