OAI/NumberTheory/DirichletL/Inversion/SecondPrincipalCaller.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseSecondPrincipalCaller.principalWindow line 14
  2. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.principalWindow_apply line 19
  3. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.principalWindow_norm line 28
  4. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.principalWindow_support line 34
  5. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.principalWindow_seminorm_zero line 41
  6. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.principalWindow_upper line 55
  7. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.whole_columnLog line 70
  8. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.primeMark_union_of_lists_disjoint line 78
  9. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.firstCoreTest_markedRadial line 92
  10. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.secondInputCoefficient_overlap_zero line 116
  11. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.firstCoreTest_coefficient line 128
  12. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.input_diagonal line 146
  13. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.input_norm_product line 157
  14. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.zero_congr_input line 164
  15. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.restoration_congr_input line 175
  16. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.firstCoreInputRow_principal_test line 195
  17. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.firstFreshSecondPoisson_markedRadial line 217
  18. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.residual_lists_pairwise line 256
  19. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.residual_lists_avoid line 265
  20. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.residual_coeff_bound line 271
  21. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.firstCore_principal_energy line 280
  22. theorem OAI.SevenEighths.InverseSecondPrincipalCaller.priority_principal_energy line 322