OAI/NumberTheory/DirichletL/QuadraticSieve/GreenIntegrals.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalQuadraticSieve.norm_double_sum_real_factor_fun line 77
  2. def OAI.CanonicalQuadraticSieve.dualPrincipalKernel line 93
  3. def OAI.CanonicalQuadraticSieve.dualProductDivisorMiddleAt line 100
  4. theorem OAI.CanonicalQuadraticSieve.dualProductDivisorMiddleAt_nonneg line 109
  5. theorem OAI.CanonicalQuadraticSieve.dualProductDivisorMiddleAt_le_window line 118
  6. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.dual_product_divisor_middle line 148
  7. theorem OAI.SecondPassArithmetic.secondChildColumn_norm_le_test line 199
  8. theorem OAI.SecondPassArithmetic.fixedChildRow_elementary line 217
  9. theorem OAI.DescentFiberCost.finite_element_count_real line 246
  10. theorem OAI.DescentFiberCost.finite_label_row_count line 262
  11. theorem OAI.SecondPassIntegration.childEnergy_elementary_normalized line 297
  12. theorem OAI.ShortDraftLatticeCount.rowNormBall_norm_sq_le line 358
  13. theorem OAI.SecondPassArithmetic.secondFrequencyCutoff_norm_sq_le line 377
  14. lemma OAI.CubicEisenstein.green_identity_interval line 389
  15. lemma OAI.CubicEisenstein.axisSlice_update line 411
  16. theorem OAI.CubicEisenstein.actual_axis_local_regular line 416
  17. lemma OAI.CubicEisenstein.intervalIntegrable_second_of_bound line 437
  18. theorem OAI.CubicEisenstein.actual_eisenstein_local_green line 445
  19. lemma OAI.CubicEisenstein.actual_axis_differentiable_at line 477
  20. lemma OAI.CubicEisenstein.actual_axis_second_locallyIntegrable line 486
  21. theorem OAI.CubicEisenstein.actual_eisenstein_green_interval line 499
  22. lemma OAI.CubicEisenstein.periodic_deriv line 533
  23. lemma OAI.CubicEisenstein.embedding_rectangular_period line 540
  24. lemma OAI.CubicEisenstein.actual_axis_periodic_zero line 548
  25. lemma OAI.CubicEisenstein.actual_axis_periodic_one line 561
  26. lemma OAI.CubicEisenstein.green_periodic_zero line 578
  27. theorem OAI.CubicEisenstein.actual_green_real_period_zero line 588
  28. theorem OAI.CubicEisenstein.actual_green_imag_period_zero line 600
  29. def OAI.CubicEisenstein.cuspRectangle line 612
  30. lemma OAI.CubicEisenstein.cuspRectangle_volume line 614
  31. lemma OAI.CubicEisenstein.cuspRectangle_volume_twice_period line 621
  32. lemma OAI.CubicEisenstein.rectangular_period_change_of_basis line 628
  33. lemma OAI.CubicEisenstein.rectangular_period_matrix_det line 638