OAI/NumberTheory/DirichletL/GaussSum/ReflectedBranches.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompletedGauss.reflectedLocalPiece line 79
  2. def OAI.CompletedGauss.reflectedLocalSize line 84
  3. def OAI.CompletedGauss.reflectedBranch line 88
  4. theorem OAI.CompletedGauss.bracket_eq_sum_reflectedLocalPiece line 92
  5. theorem OAI.CompletedGauss.prod_bracket_eq_full_branches line 101
  6. theorem OAI.CompletedGauss.reflectedLocalPiece_norm_le line 111
  7. theorem OAI.CompletedGauss.sqrt_norm_reflectionExtractedDivisor line 128
  8. theorem OAI.CompletedGauss.reflectedBranch_norm_bound line 142
  9. theorem OAI.CompletedGauss.reflectionExtractedDivisor_ne_zero line 166
  10. theorem OAI.CompletedGauss.reflectedBranch_normalized_bound line 177
  11. theorem OAI.CompletedGauss.reflectedBranch_divisibility line 197
  12. theorem OAI.CompletedGauss.Vstar_contDiff line 249
  13. theorem OAI.CompletedGauss.Vstar_support line 267
  14. def OAI.CompletedGauss.vstarSchwartz line 274
  15. theorem OAI.CompletedGauss.vstarSchwartz_apply line 279
  16. theorem OAI.CompletedGauss.completed_kernel_log_separation line 283
  17. theorem OAI.InitialMeanSquare.initial_bin_invariant line 314
  18. theorem OAI.InitialMeanSquare.initial_bin_invariant_le line 322
  19. theorem OAI.InitialMeanSquare.initial_small_radial_admissible line 332
  20. def OAI.CubicEisenstein.hyperbolicEuclideanCoordinates line 366
  21. lemma OAI.CubicEisenstein.hyperbolicEuclideanCoordinates_upperPoint line 369
  22. lemma OAI.CubicEisenstein.euclideanToHyperbolic_coordinates line 374
  23. lemma OAI.CubicEisenstein.hyperbolicEuclideanCoordinates_toHyperbolic line 382
  24. def OAI.CubicEisenstein.euclideanAction line 389
  25. lemma OAI.CubicEisenstein.euclideanAction_positive line 392
  26. lemma OAI.CubicEisenstein.euclideanAction_mul line 397
  27. lemma OAI.CubicEisenstein.euclideanAction_translation line 402
  28. lemma OAI.CubicEisenstein.euclideanAction_diagonal line 410
  29. lemma OAI.CubicEisenstein.euclideanAction_weyl line 422
  30. lemma OAI.CubicEisenstein.euclideanWeylReflection_norm line 444
  31. lemma OAI.CubicEisenstein.euclideanComplexDilation_norm line 450
  32. lemma OAI.CubicEisenstein.euclideanInversionDeriv_norm line 462
  33. def OAI.CubicEisenstein.HyperbolicDifferentialIsometry line 468
  34. lemma OAI.CubicEisenstein.hyperbolicDifferentialIsometry_mul line 473
  35. lemma OAI.CubicEisenstein.hyperbolicDifferentialIsometry_translation line 492
  36. lemma OAI.CubicEisenstein.hyperbolicDifferentialIsometry_diagonal line 504
  37. lemma OAI.CubicEisenstein.hyperbolicDifferentialIsometry_weyl line 517
  38. theorem OAI.CubicEisenstein.hyperbolicDifferentialIsometry line 532
  39. lemma OAI.CubicEisenstein.norm_comp_scaled_isometry line 553
  40. lemma OAI.CubicEisenstein.hyperbolic_cotangent_energy_comp line 572
  41. def OAI.CubicEisenstein.euclideanScalarDirichletDensity line 586
  42. lemma OAI.CubicEisenstein.euclideanScalarDirichletDensity_invariant line 589
  43. lemma OAI.CubicEisenstein.hyperbolicEuclideanCoordinates_continuous line 604
  44. lemma OAI.CubicEisenstein.hyperbolicSpatialChart_toHyperbolic line 608
  45. lemma OAI.CubicEisenstein.euclideanToHyperbolic_contMDiffAt line 612
  46. def OAI.CubicEisenstein.kernelTestField line 629
  47. lemma OAI.CubicEisenstein.kernelTestField_contDiffAt line 632
  48. lemma OAI.CubicEisenstein.kernelTestField_re_contDiffAt line 637
  49. lemma OAI.CubicEisenstein.kernelTestField_im_contDiffAt line 641
  50. lemma OAI.CubicEisenstein.kernelTestField_invariant line 645
  51. def OAI.CubicEisenstein.kernelTestEnergyDensity line 649
  52. lemma OAI.CubicEisenstein.kernelTestEnergyDensity_nonneg line 653
  53. lemma OAI.CubicEisenstein.kernelTestEnergyDensity_invariant line 658
  54. def OAI.CubicEisenstein.kernelQuotientEnergyDensity line 676
  55. lemma OAI.CubicEisenstein.kernelTestEnergyDensity_continuous line 683
  56. lemma OAI.CubicEisenstein.kernelQuotientEnergyDensity_continuous line 693
  57. lemma OAI.CubicEisenstein.kernelQuotientEnergyDensity_nonneg line 696
  58. lemma OAI.CubicEisenstein.kernelQuotientEnergyDensity_support line 701
  59. lemma OAI.CubicEisenstein.kernelQuotientEnergyDensity_hasCompactSupport line 727
  60. lemma OAI.CubicEisenstein.kernelQuotientEnergyDensity_integrable line 731
  61. def OAI.CubicEisenstein.kernelDirichletEnergy line 736
  62. lemma OAI.CubicEisenstein.kernelDirichletEnergy_nonneg line 739