OAI/NumberTheory/DirichletL/Fourier/TupleWeights.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.JointLogSeparation.finite_triple_bounded_integral line 78
  2. def OAI.SecondPassIntegration.tupleOuterWeight line 113
  3. lemma OAI.SecondPassIntegration.tupleOuterWeight_continuous line 118
  4. lemma OAI.SecondPassIntegration.tupleOuterWeight_norm line 130
  5. def OAI.SecondPassIntegration.tupleSourceSum line 141
  6. theorem OAI.SecondPassIntegration.tupleSource_eq_integratedSecondMode line 147
  7. theorem OAI.SecondPassIntegration.tupleSource_uniform_transfer line 215
  8. def OAI.JointLogSeparation.halfNormalizationMultiplier line 265
  9. lemma OAI.JointLogSeparation.halfNormalization_temperate line 268
  10. def OAI.JointLogSeparation.halfNormalizationCLM line 275
  11. lemma OAI.JointLogSeparation.halfNormalizationCLM_apply line 278
  12. lemma OAI.JointLogSeparation.sqrt_exp_half line 283
  13. theorem OAI.JointLogSeparation.halfNormalization_exact line 289
  14. lemma OAI.JointLogSeparation.halfNormalization_twist line 303
  15. theorem OAI.JointLogSeparation.halfNormalization_source_control line 310
  16. lemma OAI.SecondPassIntegration.sqrtProductNorm line 321
  17. theorem OAI.SecondPassIntegration.columnLog_union_scale line 325
  18. lemma OAI.SecondPassIntegration.halfNormalization_at_ratio line 338
  19. theorem OAI.SecondPassIntegration.normalizedColumn_union_test line 349
  20. lemma OAI.CanonicalQuadraticSieve.lambdaIdeal_maximal line 372
  21. lemma OAI.CanonicalQuadraticSieve.twoIdeal_maximal line 375
  22. lemma OAI.CanonicalQuadraticSieve.twoIdeal_characteristic line 378
  23. theorem OAI.CanonicalQuadraticSieve.supported_span_iff line 382
  24. def OAI.CanonicalQuadraticSieve.badPrime line 423
  25. instance OAI.CanonicalQuadraticSieve.badPrime_maximal line 425
  26. theorem OAI.CanonicalQuadraticSieve.badPrime_mask line 430
  27. theorem OAI.CanonicalQuadraticSieve.highKernelNorm_mono line 439
  28. theorem OAI.CanonicalQuadraticSieve.highKernel_family_squared_norm_le line 451
  29. theorem OAI.CanonicalQuadraticSieve.highKernel_quotient_family_squared_norm_le line 465
  30. theorem OAI.CanonicalQuadraticSieve.highKernel_quotientMatrix_squared_norm_le line 483
  31. def OAI.CanonicalQuadraticSieve.totalQuotient line 526
  32. theorem OAI.CanonicalQuadraticSieve.totalQuotient_ne_zero line 528
  33. theorem OAI.CanonicalQuadraticSieve.totalQuotient_norm_le line 533
  34. theorem OAI.CanonicalQuadraticSieve.gcd_eq_iff_quotient_coprime line 543
  35. def OAI.CanonicalQuadraticSieve.gcdTerm line 558
  36. def OAI.CanonicalQuadraticSieve.gcdBlock line 564
  37. theorem OAI.CanonicalQuadraticSieve.gcdTerm_eq_quotient line 568
  38. theorem OAI.CanonicalQuadraticSieve.highKernel_gcdBlock_bound line 597