OAI/NumberTheory/DirichletL/Eisenstein/CompactProfiles.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.cosetHeight_continuous line 79
  2. lemma OAI.CubicEisenstein.cuspCutoffCorrection_measurable line 88
  3. lemma OAI.CubicEisenstein.cuspCutoffCorrection_norm_le line 98
  4. lemma OAI.CubicEisenstein.smoothCuspSeedDefect_measurable line 114
  5. lemma OAI.CubicEisenstein.smoothCuspSeedDefect_bounded line 118
  6. lemma OAI.CubicEisenstein.kernelQuotientDefect_measurable line 125
  7. theorem OAI.CubicEisenstein.kernelQuotientDefect_memLp line 129
  8. def OAI.CubicEisenstein.kernelL2Defect line 138
  9. lemma OAI.CubicEisenstein.kernelL2Defect_ae_eq line 141
  10. lemma OAI.CubicEisenstein.cuspCutoffCorrection_add line 151
  11. lemma OAI.CubicEisenstein.cuspCutoffCorrection_smul line 160
  12. def OAI.CubicEisenstein.compactHeightProfile line 169
  13. lemma OAI.CubicEisenstein.compactHeightProfile_measurable line 172
  14. lemma OAI.CubicEisenstein.compactHeightProfile_norm_le line 176
  15. lemma OAI.CubicEisenstein.compactHeightProfile_add line 185
  16. lemma OAI.CubicEisenstein.compactHeightProfile_smul line 190
  17. def OAI.CubicEisenstein.kernelCompactProfile line 195
  18. lemma OAI.CubicEisenstein.kernelCompactProfile_measurable line 206
  19. lemma OAI.CubicEisenstein.kernelCompactProfile_norm_le line 211
  20. lemma OAI.CubicEisenstein.kernelCompactProfile_memLp line 218
  21. lemma OAI.CubicEisenstein.kernelCompactProfile_add line 223
  22. lemma OAI.CubicEisenstein.kernelCompactProfile_smul line 232
  23. def OAI.CubicEisenstein.compactProfileL2Linear line 241
  24. lemma OAI.CubicEisenstein.compactProfileL2Linear_bound line 253
  25. def OAI.CubicEisenstein.compactProfileL2 line 262
  26. lemma OAI.CubicEisenstein.compactProfileL2_ae_eq line 267
  27. def OAI.CubicEisenstein.compactLogProfile line 272
  28. def OAI.CubicEisenstein.compactDefectSecond line 276
  29. def OAI.CubicEisenstein.compactDefectFirst line 284
  30. def OAI.CubicEisenstein.compactDefectProfile line 291
  31. lemma OAI.CubicEisenstein.compactDefectProfile_apply line 295
  32. lemma OAI.CubicEisenstein.compactDefectProfile_entire line 309
  33. lemma OAI.CubicEisenstein.compactHeightProfile_actual_defect line 316
  34. lemma OAI.CubicEisenstein.compactProfileL2_actual_defect line 326
  35. theorem OAI.CubicEisenstein.kernelL2Defect_entire line 338
  36. theorem OAI.SecondPassIntegration.full_uniform_normalized_child_tests line 352
  37. theorem OAI.SecondPassIntegration.full_uniform_twisted_normalized_child_tests line 400
  38. def OAI.SecondPassArithmetic.globalSecondLiteralTerm line 488
  39. theorem OAI.SecondPassArithmetic.globalResidualScale_eq line 501
  40. theorem OAI.SecondPassArithmetic.globalSecondLiteralTerm_fixed_profiles line 510
  41. theorem OAI.SecondPassArithmetic.globalSecondLiteralTerm_twisted_profiles line 598