OAI/NumberTheory/DirichletL/Inversion/InitialPhysicalSlots.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.InverseInitialPhysicalSlots.livePrimes line 15
2. theorem OAI.SevenEighths.InverseInitialPhysicalSlots.livePrime_data line 21
3. theorem OAI.SevenEighths.InverseInitialPhysicalSlots.amplitude_eq_live line 29
4. theorem OAI.SevenEighths.InverseInitialPhysicalSlots.slot_normalization line 47
5. theorem OAI.SevenEighths.InverseInitialPhysicalSlots.amplitude_product_eq_tuples line 54
6. theorem OAI.SevenEighths.InverseInitialPhysicalSlots.physical_slots_norm_initial line 65
7. theorem OAI.SevenEighths.InverseInitialPhysicalSlots.live_tuple_injective line 106
8. theorem OAI.SevenEighths.InverseInitialPhysicalSlots.live_tuple_admissible line 123