OAI/NumberTheory/Ostmann/Construction/CounterpartNormalizationBoundTemplates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Construction.CounterpartNormalizationBound.bulkCount line 10
2. lemma OAI.Ostmann.Construction.CounterpartNormalizationBound.bulkCount_add_fixedCount line 12
3. lemma OAI.Ostmann.Construction.CounterpartNormalizationBound.sourceSum_bulkCount_initial line 16
4. lemma OAI.Ostmann.Construction.CounterpartNormalizationBound.sourceSum_bulkCount_remainder line 31
5. lemma OAI.Ostmann.Construction.CounterpartNormalizationBound.sourceSum_bulkCount_pruned line 41
6. theorem OAI.Ostmann.Construction.CounterpartNormalizationBound.sourceSum_bulkCount_remaining line 47
7. lemma OAI.Ostmann.Construction.CounterpartNormalizationBound.current_mem_seed line 53
8. theorem OAI.Ostmann.Construction.CounterpartNormalizationBound.remaining_origin_metadata line 62