OAI/NumberTheory/DirichletL/Inversion/PrincipalEnergy.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.InversePrincipalEnergy.zero_norm_le line 21
  2. def OAI.SevenEighths.InversePrincipalEnergy.supportIdeal line 33
  3. lemma OAI.SevenEighths.InversePrincipalEnergy.supportIdeal_ne_zero line 36
  4. lemma OAI.SevenEighths.InversePrincipalEnergy.supportIdeal_norm_pos line 40
  5. theorem OAI.SevenEighths.InversePrincipalEnergy.mask_card_le_divisors line 45
  6. def OAI.SevenEighths.InversePrincipalEnergy.principalFrequency line 54
  7. theorem OAI.SevenEighths.InversePrincipalEnergy.principalFrequency_eq line 61
  8. theorem OAI.SevenEighths.InversePrincipalEnergy.principalFrequency_eq_secondFrequencyKernel_empty line 70
  9. def OAI.SevenEighths.InversePrincipalEnergy.restorationTerm line 78
  10. theorem OAI.SevenEighths.InversePrincipalEnergy.restorationTerm_eq_principal_kernel line 87
  11. theorem OAI.SevenEighths.InversePrincipalEnergy.restorationTerm_eq line 98
  12. theorem OAI.SevenEighths.InversePrincipalEnergy.restorationTerm_mask_norm_le line 117
  13. theorem OAI.SevenEighths.InversePrincipalEnergy.restorationTerm_mask_summable_norm line 136
  14. theorem OAI.SevenEighths.InversePrincipalEnergy.restoration_divisor_abs_le line 149
  15. def OAI.SevenEighths.InversePrincipalEnergy.principalRestoration line 180
  16. theorem OAI.SevenEighths.InversePrincipalEnergy.principalRestoration_abs_le line 187
  17. theorem OAI.SevenEighths.InversePrincipalEnergy.principalRestoration_norm_le line 210
  18. def OAI.SevenEighths.InversePrincipalEnergy.markedRadial line 228
  19. lemma OAI.SevenEighths.InversePrincipalEnergy.markedRadial_support line 234
  20. theorem OAI.SevenEighths.InversePrincipalEnergy.radial_mass_from_pointwise line 247
  21. lemma OAI.SevenEighths.InversePrincipalEnergy.mass_le_divisor_mass line 278
  22. theorem OAI.SevenEighths.InversePrincipalEnergy.marked_radial_divisor_mass line 291
  23. lemma OAI.SevenEighths.InversePrincipalEnergy.radial_support_of_annular line 343
  24. def OAI.SevenEighths.InversePrincipalEnergy.outsideCutoff line 349
  25. lemma OAI.SevenEighths.InversePrincipalEnergy.outsideCutoff_norm_le_one line 353
  26. lemma OAI.SevenEighths.InversePrincipalEnergy.outsideCutoff_mul_norm_le_one line 359
  27. theorem OAI.SevenEighths.InversePrincipalEnergy.uniform_row_control line 366
  28. theorem OAI.SevenEighths.InversePrincipalEnergy.principal_energy_le line 394
  29. theorem OAI.SevenEighths.InversePrincipalEnergy.marked_principal_energy line 426