OAI/NumberTheory/DirichletL/QuadraticSieve/SpatialDerivatives.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalQuadraticSieve.column_sqrt_ratio_bounds line 77
  2. theorem OAI.CanonicalQuadraticSieve.dual_middle_sqrt_identity line 86
  3. theorem OAI.CanonicalQuadraticSieve.dual_middle_argument line 97
  4. theorem OAI.CanonicalQuadraticSieve.actual_dual_middle_radial_block_bound line 124
  5. theorem OAI.CanonicalQuadraticSieve.principal_middle_prefactor_bound line 176
  6. theorem OAI.CanonicalQuadraticSieve.principal_middle_prefactor_sum line 199
  7. def OAI.CanonicalQuadraticSieve.originalMiddleConstant line 220
  8. def OAI.CanonicalQuadraticSieve.dualMiddleConstant line 222
  9. theorem OAI.CanonicalQuadraticSieve.dual_principal_prefactor_identity line 224
  10. theorem OAI.CanonicalQuadraticSieve.actual_original_middle_weighted_bound line 247
  11. theorem OAI.CanonicalQuadraticSieve.actual_dual_middle_weighted_bound line 269
  12. lemma OAI.CubicEisenstein.abs_le_inv_of_mul_sq_le_one line 299
  13. lemma OAI.CubicEisenstein.heightLog_first_bounds line 305
  14. lemma OAI.CubicEisenstein.heightLog_second_bounds line 319
  15. lemma OAI.CubicEisenstein.actual_quadraticHeight_nonneg line 357
  16. abbrev OAI.CubicEisenstein.SpatialCoordinates line 369
  17. def OAI.CubicEisenstein.axisSlice line 371
  18. def OAI.CubicEisenstein.spatialLogD line 374
  19. def OAI.CubicEisenstein.spatialLogDD line 378
  20. lemma OAI.CubicEisenstein.spatial_axis_hasDerivAt line 383
  21. lemma OAI.CubicEisenstein.spatial_axis_hasDerivAt_deriv line 399
  22. def OAI.CubicEisenstein.rowSmoothPower line 434
  23. def OAI.CubicEisenstein.rowLogD line 438
  24. def OAI.CubicEisenstein.rowLogDD line 442
  25. lemma OAI.CubicEisenstein.row_denominator_pos line 446
  26. lemma OAI.CubicEisenstein.rowLogD_bound line 452
  27. lemma OAI.CubicEisenstein.rowLogDD_bound line 461
  28. lemma OAI.CubicEisenstein.row_axis_hasDerivAt line 471
  29. lemma OAI.CubicEisenstein.row_axis_hasDerivAt_deriv line 477
  30. lemma OAI.CubicEisenstein.hasDerivAt_deriv_tsum_of_bounds line 490
  31. lemma OAI.CubicEisenstein.norm_row_axis_deriv line 511
  32. lemma OAI.CubicEisenstein.norm_row_axis_deriv2 line 522
  33. def OAI.CubicEisenstein.smoothSummand line 537
  34. lemma OAI.CubicEisenstein.smoothSummand_eq_actual line 540
  35. lemma OAI.CubicEisenstein.smooth_axis_differentiable line 548
  36. lemma OAI.CubicEisenstein.smooth_axis_deriv_differentiable line 553
  37. lemma OAI.CubicEisenstein.norm_smooth_axis_deriv line 561
  38. lemma OAI.CubicEisenstein.norm_smooth_axis_deriv2 line 570
  39. lemma OAI.CubicEisenstein.smoothSummand_axis_update line 579
  40. def OAI.CubicEisenstein.clampedCoordinates line 593
  41. lemma OAI.CubicEisenstein.continuous_clampedCoordinates line 596
  42. lemma OAI.CubicEisenstein.continuous_axis_update line 603
  43. lemma OAI.CubicEisenstein.smoothSummand_eq_clamped line 613
  44. theorem OAI.CubicEisenstein.axis_summable_derivative_bounds line 619
  45. lemma OAI.CubicEisenstein.smooth_axis_differentiable_at line 668
  46. lemma OAI.CubicEisenstein.smooth_axis_deriv_differentiable_at line 674