OAI/NumberTheory/DirichletL/Inversion/InitialEnergyCallerSourceMask.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseInitialEnergyCallerSourceMask.coprimeSource line 19
  2. theorem OAI.SevenEighths.InverseInitialEnergyCallerSourceMask.physicalBlock_coprimeSource line 22
  3. theorem OAI.SevenEighths.InverseInitialEnergyCallerSourceMask.retained_child_squarefree line 57
  4. def OAI.SevenEighths.InverseInitialEnergyCallerSourceMask.childLabels line 67
  5. theorem OAI.SevenEighths.InverseInitialEnergyCallerSourceMask.childLabels_ne_zero line 72
  6. theorem OAI.SevenEighths.InverseInitialEnergyCallerSourceMask.childLabels_squarefree line 79
  7. theorem OAI.SevenEighths.InverseInitialEnergyCallerSourceMask.child_label_mem line 86
  8. theorem OAI.SevenEighths.InverseInitialEnergyCallerSourceMask.nonzero_child_ball_neg line 91