OAI/NumberTheory/DirichletL/GaussSum/ReflectionBrackets.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LocalReflectionBrackets.bracket_eq_zero_iff line 79
  2. theorem OAI.LocalReflectionBrackets.norm_bracket_nonexceptional_le_one line 88
  3. theorem OAI.LocalReflectionBrackets.norm_bracket_zero_le line 93
  4. theorem OAI.LocalReflectionBrackets.canonical_A5_norm_cases line 103
  5. theorem OAI.LocalReflectionBrackets.actual_trace_A5_normalized line 131
  6. theorem OAI.LocalReflectionBrackets.actual_bracket_four_divisibility_split line 141
  7. theorem OAI.LocalReflectionBrackets.actual_bracket_zero_iff line 149
  8. theorem OAI.LocalReflectionBrackets.rootCard_span line 154
  9. def OAI.LocalReflectionBrackets.zeroFourierCoefficient line 164
  10. theorem OAI.LocalReflectionBrackets.zeroFourierCoefficient_zero line 167
  11. theorem OAI.LocalReflectionBrackets.zeroFourierCoefficient_nontrivial line 175
  12. theorem OAI.LocalReflectionBrackets.zeroFourierCoefficient_zero_norm_le_one line 179
  13. theorem OAI.LocalReflectionBrackets.canonical_zeroFourierCoefficient line 198
  14. theorem OAI.LocalReflectionBrackets.finite_active_scalar_norm_one line 208
  15. theorem OAI.EisensteinSchwartzPoisson.complex_radial_norm_sq_integral line 230
  16. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_zero_eq_halfline line 257
  17. theorem OAI.EisensteinSchwartzPoisson.quadratic_principal_zero_modes_equal line 267
  18. def OAI.EisensteinSchwartzPoisson.quadraticSquareProfile line 273
  19. theorem OAI.EisensteinSchwartzPoisson.quadraticSquareProfile_apply line 276
  20. def OAI.EisensteinSchwartzPoisson.quadraticTransformedSquareProfile line 281
  21. theorem OAI.EisensteinSchwartzPoisson.quadraticTransformedSquareProfile_apply line 287
  22. theorem OAI.EisensteinSchwartzPoisson.quadraticSquareProfile_principal_equal line 297
  23. theorem OAI.ActualEisensteinCubic.primeSubsetGenerator_norm_sq line 312
  24. theorem OAI.ActualEisensteinCubic.masked_principal_radial_poisson line 317
  25. def OAI.ActualEisensteinCubic.maskedPrincipalRemainder line 339
  26. theorem OAI.ActualEisensteinCubic.masked_principal_radial_poisson_zero_split line 347
  27. theorem OAI.ActualEisensteinCubic.quadratic_square_poisson_main_cancel line 378
  28. abbrev OAI.PrimaryIdealUnitReindex.O line 398
  29. abbrev OAI.PrimaryIdealUnitReindex.GoodIdeal line 401
  30. abbrev OAI.PrimaryIdealUnitReindex.GoodElement line 402
  31. theorem OAI.PrimaryIdealUnitReindex.finite_units line 404
  32. theorem OAI.PrimaryIdealUnitReindex.span_unit_primary line 411
  33. def OAI.PrimaryIdealUnitReindex.unitIdealToElement line 416
  34. theorem OAI.PrimaryIdealUnitReindex.unitIdealToElement_injective line 419
  35. theorem OAI.PrimaryIdealUnitReindex.unitIdealToElement_surjective line 432
  36. def OAI.PrimaryIdealUnitReindex.unitIdealEquiv line 442
  37. theorem OAI.PrimaryIdealUnitReindex.tsum_good_elements_product line 445
  38. theorem OAI.PrimaryIdealUnitReindex.tsum_good_elements_unit_invariant line 450
  39. theorem OAI.PrimaryIdealUnitReindex.lambda_prime_actual line 463
  40. theorem OAI.PrimaryIdealUnitReindex.primaryGenerator_ne_zero_of_good_factors line 467
  41. theorem OAI.PrimaryIdealUnitReindex.primaryGenerator_span_ne_zero_iff line 478
  42. theorem OAI.PrimaryIdealUnitReindex.tsum_ramified_mask line 508
  43. theorem OAI.PrimaryIdealUnitReindex.tsum_ramified_mask_unit_invariant line 518
  44. abbrev OAI.QuadraticUnitInvariance.O line 529
  45. theorem OAI.QuadraticUnitInvariance.principalNormalizedGauss_three_eq_quadraticGamma line 533
  46. theorem OAI.QuadraticUnitInvariance.principalNormalizedGauss_three_eq_rayValue line 555
  47. theorem OAI.QuadraticUnitInvariance.quadratic_unit_phase line 564
  48. theorem OAI.QuadraticUnitInvariance.finiteSexticRow_three_star line 583
  49. theorem OAI.QuadraticUnitInvariance.quadratic_unit_value_eq_of_same_ray line 593
  50. theorem OAI.QuadraticUnitInvariance.quadratic_pair_unit_invariant line 614