OAI/NumberTheory/Ostmann/Arithmetic/HistorySelectedFlagMassBoundsBasic.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistorySelectedFlagMassBounds.occurrenceCap line 13
2. def OAI.Ostmann.Arithmetic.HistorySelectedFlagMassBounds.massCap line 15
3. def OAI.Ostmann.Arithmetic.HistorySelectedFlagMassBounds.atomCap line 17
4. structure OAI.Ostmann.Arithmetic.HistorySelectedFlagMassBounds.Bounds line 20
5. lemma OAI.Ostmann.Arithmetic.HistorySelectedFlagMassBounds.one_le_occurrenceCap line 25
6. lemma OAI.Ostmann.Arithmetic.HistorySelectedFlagMassBounds.le_cap_mul line 27
7. lemma OAI.Ostmann.Arithmetic.HistorySelectedFlagMassBounds.one_le_massCap line 31
8. lemma OAI.Ostmann.Arithmetic.HistorySelectedFlagMassBounds.source_atom_le_cap line 34
9. theorem OAI.Ostmann.Arithmetic.HistorySelectedFlagMassBounds.prior_bounds line 38
10. theorem OAI.Ostmann.Arithmetic.HistorySelectedFlagMassBounds.sourceWeight_bounds line 46
11. theorem OAI.Ostmann.Arithmetic.HistorySelectedFlagMassBounds.literal_block_bounds line 60