OAI/NumberTheory/DirichletL/Inversion/InitialEnergyCallerRanges.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.InverseInitialEnergyCallerRanges.sourceIdeal_admissible line 23
2. theorem OAI.SevenEighths.InverseInitialEnergyCallerRanges.retained_label_admissible line 35
3. theorem OAI.SevenEighths.InverseInitialEnergyCallerRanges.childLabels_subset_range line 44
4. theorem OAI.SevenEighths.InverseInitialEnergyCallerRanges.canonical_child_domains line 63