OAI/Combinatorics/SharpRamsey/Parameters/SourceScaleComparisons.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.SourceScales.scaleK line 12
2. def OAI.SharpLogRamsey.SourceScales.scaleKstar line 13
3. lemma OAI.SharpLogRamsey.SourceScales.Kstar_eq line 15
4. lemma OAI.SharpLogRamsey.SourceScales.R_bound line 22
5. lemma OAI.SharpLogRamsey.SourceScales.L_pos line 27
6. lemma OAI.SharpLogRamsey.SourceScales.P_pos line 33
7. theorem OAI.SharpLogRamsey.SourceScales.eventually_sparse_loss line 38
8. theorem OAI.SharpLogRamsey.SourceScales.eventually_log_le_L line 76