OAI/NumberTheory/DirichletL/QuadraticSieve/FiniteOperator.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteSieveOperator.operator line 77
  2. theorem OAI.FiniteSieveOperator.operator_apply line 81
  3. theorem OAI.FiniteSieveOperator.operator_conjTranspose line 84
  4. theorem OAI.FiniteSieveOperator.operator_conjTranspose_norm line 89
  5. theorem OAI.FiniteSieveOperator.operator_zero line 95
  6. theorem OAI.FiniteSieveOperator.operator_add line 100
  7. theorem OAI.FiniteSieveOperator.operator_smul line 105
  8. theorem OAI.FiniteSieveOperator.operator_sum line 110
  9. theorem OAI.FiniteSieveOperator.diagonal_twist_norm_le line 118
  10. theorem OAI.FiniteSieveOperator.separated_phase_norm_le line 151
  11. theorem OAI.FiniteSieveOperator.energy_bound line 178
  12. def OAI.QuadraticInitialBound.quadraticMatrix line 192
  13. def OAI.QuadraticInitialBound.quadraticSieveNorm line 198
  14. theorem OAI.QuadraticInitialBound.quadraticSieveNorm_energy line 205
  15. theorem OAI.QuadraticInitialBound.quadratic_matrix_norm_reverse_le line 214
  16. theorem OAI.QuadraticInitialBound.quadraticSieveNorm_reverse_le line 260
  17. abbrev OAI.IdealDivisorBound.O line 279
  18. theorem OAI.IdealDivisorBound.divisor_ne_zero line 281
  19. theorem OAI.IdealDivisorBound.divisor_card_le_product line 287
  20. theorem OAI.IdealDivisorBound.linear_le_geometric line 305
  21. theorem OAI.IdealDivisorBound.support_norm_two_le line 317
  22. theorem OAI.IdealDivisorBound.norm_factor_product line 331
  23. theorem OAI.IdealDivisorBound.ideal_divisor_small_power line 339
  24. abbrev OAI.SecondPassFiber.O line 417
  25. structure OAI.SecondPassFiber.OldTuple line 419
  26. structure OAI.SecondPassFiber.Valid line 426
  27. def OAI.SecondPassFiber.divisorTarget line 435
  28. theorem OAI.SecondPassFiber.core_dvd_target line 437
  29. theorem OAI.SecondPassFiber.target_ne_zero line 473
  30. theorem OAI.SecondPassFiber.core_ne_zero line 476
  31. theorem OAI.SecondPassFiber.valid_core_injective line 484
  32. theorem OAI.SecondPassFiber.valid_tuple_card_le line 517
  33. theorem OAI.SecondPassFiber.valid_tuple_small_power line 533
  34. def OAI.SecondPassFiber.newLabel line 553
  35. def OAI.SecondPassFiber.newRow line 554
  36. theorem OAI.SecondPassFiber.second_energy_pushforward line 557
  37. theorem OAI.FirstPassCubeLabels.conductorExponent_val line 600
  38. theorem OAI.FirstPassCubeLabels.cube_pair_exponent_mod line 604
  39. def OAI.FirstPassCubeLabels.cubePairLocal line 612
  40. theorem OAI.FirstPassCubeLabels.cubePairLocal_eq_character line 617
  41. def OAI.FirstPassCubeLabels.cubeConductorSupport line 652
  42. def OAI.FirstPassCubeLabels.cubePrincipalSupport line 656
  43. theorem OAI.FirstPassCubeLabels.cubeConductorExponent_ne_zero line 660
  44. theorem OAI.FirstPassCubeLabels.cubeConductorExponent_lt_six line 665
  45. def OAI.FirstPassCubeLabels.multiplicityRow line 670
  46. def OAI.FirstPassCubeLabels.cubePairRow line 674
  47. theorem OAI.FirstPassCubeLabels.row_filter_eq_power_product line 681
  48. theorem OAI.FirstPassCubeLabels.cubePairRow_eq_product line 691
  49. theorem OAI.FirstPassCubeLabels.principal_product_eq_mask line 702
  50. theorem OAI.FirstPassCubeLabels.cubePairRow_conductor_selection line 719
  51. theorem OAI.FirstPassCubeLabels.cubeConductorPrimes_pairwise_coprime line 748
  52. def OAI.FirstPassCubeLabels.cubePairPoissonKernel line 761
  53. theorem OAI.FirstPassCubeLabels.cubePairRow_radial_poisson line 780