OAI/NumberTheory/DirichletL/Inversion/InitialPoissonBridge.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.InverseInitialPoissonBridge.rowPolynomial line 14
  2. lemma OAI.SevenEighths.InverseInitialPoissonBridge.pool_positive line 17
  3. lemma OAI.SevenEighths.InverseInitialPoissonBridge.pool_good line 20
  4. lemma OAI.SevenEighths.InverseInitialPoissonBridge.pool_char line 24
  5. theorem OAI.SevenEighths.InverseInitialPoissonBridge.idealRowHom_eq_idealSexticRow line 29
  6. theorem OAI.SevenEighths.InverseInitialPoissonBridge.rowPolynomial_eq_finite line 43
  7. theorem OAI.SevenEighths.InverseInitialPoissonBridge.rowPolynomial_smoothed_summable line 51
  8. theorem OAI.SevenEighths.InverseInitialPoissonBridge.rowPolynomial_smoothed_expand line 62
  9. theorem OAI.SevenEighths.InverseInitialPoissonBridge.rowPolynomial_smoothed_poisson line 81
  10. theorem OAI.SevenEighths.InverseInitialPoissonBridge.indexed_smoothed_poisson line 100
  11. theorem OAI.SevenEighths.InverseInitialPoissonBridge.indexed_conjugate_smoothed_poisson line 133
  12. theorem OAI.SevenEighths.InverseInitialPoissonBridge.indexed_smoothed_summable line 151
  13. theorem OAI.SevenEighths.InverseInitialPoissonBridge.supported_of_dvd line 171
  14. theorem OAI.SevenEighths.InverseInitialPoissonBridge.columns_admissible line 175
  15. theorem OAI.SevenEighths.InverseInitialPoissonBridge.masked_columns_admissible line 187
  16. theorem OAI.SevenEighths.InverseInitialPoissonBridge.norm_idealRowHom_four_eq_two line 197
  17. def OAI.SevenEighths.InverseInitialPoissonBridge.heckeIdealCharacter line 215
  18. theorem OAI.SevenEighths.InverseInitialPoissonBridge.heckeIdealCharacter_apply line 218
  19. def OAI.SevenEighths.InverseInitialPoissonBridge.originalFixedPolynomial line 221
  20. def OAI.SevenEighths.InverseInitialPoissonBridge.overlapResidualCoefficient line 228
  21. def OAI.SevenEighths.InverseInitialPoissonBridge.overlapPrefactor line 234
  22. theorem OAI.SevenEighths.InverseInitialPoissonBridge.originalFixedPolynomial_eq line 238
  23. theorem OAI.SevenEighths.InverseInitialPoissonBridge.maskedResidual_eq line 253
  24. lemma OAI.SevenEighths.InverseInitialPoissonBridge.norm_sq_square_factor line 262
  25. theorem OAI.SevenEighths.InverseInitialPoissonBridge.originalFixedPolynomial_norm_sq line 268
  26. theorem OAI.SevenEighths.InverseInitialPoissonBridge.norm_overlapPrefactor_sq line 280
  27. theorem OAI.SevenEighths.InverseInitialPoissonBridge.original_fixed_overlap_smoothed_poisson line 299
  28. theorem OAI.SevenEighths.InverseInitialPoissonBridge.original_fixed_overlap_smoothed_poisson_zero_split line 328
  29. def OAI.SevenEighths.InverseInitialPoissonBridge.residualNormalizedPolynomial line 350
  30. lemma OAI.SevenEighths.InverseInitialPoissonBridge.norm_rpow_half_sq line 356
  31. theorem OAI.SevenEighths.InverseInitialPoissonBridge.residual_normalized_smoothed_poisson line 363
  32. theorem OAI.SevenEighths.InverseInitialPoissonBridge.residual_normalized_smoothed_poisson_zero_split line 391
  33. theorem OAI.SevenEighths.InverseInitialPoissonBridge.original_fixed_overlap_smoothed_summable line 413
  34. theorem OAI.SevenEighths.InverseInitialPoissonBridge.original_normalized_polynomial_hecke_rows line 429
  35. theorem OAI.SevenEighths.InverseInitialPoissonBridge.indexed_conjugate_smoothed_summable line 449
  36. theorem OAI.SevenEighths.InverseInitialPoissonBridge.residual_normalized_smoothed_summable line 460