OAI/NumberTheory/DirichletL/GaussSum/MixedConversion.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MixedGaussConversion.O line 70
  2. def OAI.MixedGaussConversion.localGauss line 73
  3. def OAI.MixedGaussConversion.localCoefficient line 77
  4. def OAI.MixedGaussConversion.localG line 81
  5. theorem OAI.MixedGaussConversion.norm_localGauss line 85
  6. theorem OAI.MixedGaussConversion.canonicalSextic_fifth_eq_inverse line 98
  7. theorem OAI.MixedGaussConversion.localGauss_five_eq line 108
  8. theorem OAI.MixedGaussConversion.local_sign_conversion line 114
  9. theorem OAI.MixedGaussConversion.norm_localG line 131
  10. def OAI.MixedGaussConversion.convertedLocal line 141
  11. theorem OAI.MixedGaussConversion.neg_localGauss_eq_converted line 148
  12. theorem OAI.MixedGaussConversion.moebius_mixed_gauss_conversion line 162
  13. theorem OAI.GaussGeneratorTransport.pair_moebius_eq_active line 200
  14. def OAI.GaussGeneratorTransport.activeConvertedGauss line 226
  15. def OAI.GaussGeneratorTransport.activePairDualSeries line 238
  16. def OAI.GaussGeneratorTransport.convertedPairPoissonKernel line 253
  17. theorem OAI.GaussGeneratorTransport.moebius_squarefreePairPoissonKernel_conversion line 261
  18. theorem OAI.GaussGeneratorTransport.moebius_pair_radial_poisson_converted line 298
  19. theorem OAI.GaussGeneratorTransport.moebius_pair_kernel_conversion_of_generators line 316
  20. def OAI.ConcretePrimeRowBridge.mobiusIdealColumn line 341
  21. def OAI.ConcretePrimeRowBridge.conjugateIdealRowSum line 344
  22. theorem OAI.ConcretePrimeRowBridge.conjugateIdealRowSum_eq_star line 351
  23. theorem OAI.ConcretePrimeRowBridge.conjugateIdealRowSum_smoothed_summable line 360
  24. theorem OAI.ConcretePrimeRowBridge.conjugateIdealRowSum_smoothed_poisson line 373
  25. theorem OAI.ConcretePrimeRowBridge.mobiusIdealColumn_eq_zero_of_not_squarefree line 404
  26. theorem OAI.ConcretePrimeRowBridge.conjugateIdealRowSum_zeroMode_offDiagonal line 410
  27. theorem OAI.ConcretePrimeRowBridge.conjugateIdealRowSum_zeroMode_formula line 430
  28. theorem OAI.ConcretePrimeRowBridge.conjugateIdealRowSum_smoothed_poisson_zero_split line 451
  29. theorem OAI.ConcretePrimeRowBridge.norm_mobiusIdealColumn_le line 469
  30. theorem OAI.ConcretePrimeRowBridge.norm_conjugateIdealRowSum_zeroMode_le line 477
  31. theorem OAI.ConcretePrimeRowBridge.norm_secondPoisson_zeroMode_fixed_factors line 498
  32. theorem OAI.EisensteinSchwartzPoisson.scaled_cauchy_antitone line 527
  33. theorem OAI.EisensteinSchwartzPoisson.scaled_cauchy_nat_bound line 536
  34. theorem OAI.EisensteinSchwartzPoisson.summable_scaled_cauchy_nat line 548
  35. theorem OAI.EisensteinSchwartzPoisson.summable_scaled_cauchy_int line 553
  36. theorem OAI.EisensteinSchwartzPoisson.scaled_cauchy_int_bound line 560
  37. theorem OAI.EisensteinSchwartzPoisson.scaled_eisenstein_cauchy_summable line 589
  38. theorem OAI.EisensteinSchwartzPoisson.scaled_eisenstein_cauchy_bound line 609
  39. theorem OAI.EisensteinSchwartzPoisson.scaled_eisenstein_cauchy_small line 639
  40. theorem OAI.EisensteinSchwartzPoisson.one_le_eisenstein_norm_sq line 654
  41. theorem OAI.EisensteinSchwartzPoisson.cauchy_large_scale_pointwise line 661
  42. theorem OAI.EisensteinSchwartzPoisson.lattice_profile_nonzero_scaled_bound line 673
  43. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_nonzero_lattice_uniform line 723