OAI/NumberTheory/DirichletL/CubicSieve/PaddedPassage.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SecondPassArithmetic.padded_orientedTwoPassage_quantitative line 84
  2. theorem OAI.SecondPassArithmetic.padded_rawCanonicalTwoPassage_quantitative line 154
  3. def OAI.SecondPassArithmetic.firstFrequencyDisk line 238
  4. lemma OAI.SecondPassArithmetic.mem_firstFrequencyDisk line 241
  5. lemma OAI.SecondPassArithmetic.firstFrequencyDisk_zero line 252
  6. lemma OAI.SecondPassArithmetic.outside_firstFrequencyDisk line 256
  7. lemma OAI.SecondPassArithmetic.firstFrequencyDisk_unit_invariant line 259
  8. lemma OAI.CubicEisenstein.euclideanCoordinateVector_eq_basis line 269
  9. lemma OAI.CubicEisenstein.schwartz_toL2_norm_sq line 274
  10. def OAI.CubicEisenstein.kernelLocalizedDensity line 285
  11. lemma OAI.CubicEisenstein.kernelLocalizedDensity_eq_schwartz line 290
  12. lemma OAI.CubicEisenstein.kernelLocalizedDensity_integrable line 298
  13. lemma OAI.CubicEisenstein.kernelLocalizedH1_norm_sq line 306
  14. lemma OAI.CubicEisenstein.kernelLocalizedDensity_zero line 316
  15. lemma OAI.CubicEisenstein.kernelLocalizedDensity_le line 324
  16. lemma OAI.CubicEisenstein.kernelEuclideanProjection_volume_integrable line 351
  17. theorem OAI.CubicEisenstein.kernelLocalizedH1_norm_sq_le line 362
  18. theorem OAI.CubicEisenstein.kernelLocalizedH1_bounded line 404
  19. def OAI.CubicEisenstein.kernelLocalizedSchwartzLinear line 446
  20. def OAI.CubicEisenstein.kernelLocalizedH1Linear line 458
  21. abbrev OAI.CubicEisenstein.KernelEnergyAmbient line 480
  22. def OAI.CubicEisenstein.kernelEnergyCore line 482
  23. def OAI.CubicEisenstein.kernelEnergyGraphSubmodule line 486
  24. abbrev OAI.CubicEisenstein.KernelEnergyGraph line 489
  25. instance OAI.CubicEisenstein.kernelEnergyGraph_complete line 491
  26. example OAI.CubicEisenstein.(example at line 494) line 494
  27. def OAI.CubicEisenstein.kernelEnergyGraphCore line 496
  28. lemma OAI.CubicEisenstein.kernelEnergyGraphCore_dense line 500
  29. def OAI.CubicEisenstein.kernelEnergyMass line 505
  30. def OAI.CubicEisenstein.kernelEnergyGradient line 510
  31. lemma OAI.CubicEisenstein.kernelEnergyMass_core line 515
  32. lemma OAI.CubicEisenstein.kernelEnergyGradient_core line 518
  33. lemma OAI.CubicEisenstein.kernelEnergyGraph_norm_sq line 521
  34. lemma OAI.CubicEisenstein.kernelEnergyGraphCore_norm_sq line 525
  35. lemma OAI.CubicEisenstein.kernelEnergyMass_dense line 530
  36. lemma OAI.CubicEisenstein.kernelLocalizedH1_graph_bound line 535
  37. def OAI.CubicEisenstein.kernelEnergyLocalize line 548
  38. lemma OAI.CubicEisenstein.kernelEnergyLocalize_core line 551
  39. def OAI.CubicEisenstein.kernelLocalizedL2Linear line 563
  40. lemma OAI.CubicEisenstein.kernelLocalizedL2Linear_apply line 566
  41. lemma OAI.CubicEisenstein.kernelLocalizedL2_bounded line 569
  42. lemma OAI.CubicEisenstein.kernelLocalizedL2_bound line 614
  43. def OAI.CubicEisenstein.kernelL2Localize line 624
  44. lemma OAI.CubicEisenstein.kernelL2Localize_core line 627
  45. lemma OAI.CubicEisenstein.kernelEnergyLocalize_mass line 632
  46. lemma OAI.CubicEisenstein.kernelEnergyLocalize_eq_zero_of_mass_zero line 643