OAI/NumberTheory/DirichletL/CubicSieve/RadialWindows.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SecondPassArithmetic.columnLog_three_split line 87
  2. lemma OAI.SecondPassArithmetic.canonicalCubeResidual_log line 99
  3. lemma OAI.SecondPassArithmetic.actualFirstKernel_insert_windows line 120
  4. lemma OAI.FirstPassCubeLabels.conductor_zero_swap line 156
  5. lemma OAI.FirstPassCubeLabels.conductor_parity_swap line 160
  6. lemma OAI.FirstPassCubeLabels.dilationExponent_swap line 164
  7. lemma OAI.FirstPassCubeLabels.retained_swap line 168
  8. lemma OAI.FirstPassCubeLabels.b0Exponent_swap line 171
  9. lemma OAI.FirstPassCubeLabels.cubeActiveSupport_swap line 176
  10. lemma OAI.FirstPassCubeLabels.cubeOddSupport_swap line 185
  11. lemma OAI.FirstPassCubeLabels.dilationLabel_swap line 189
  12. lemma OAI.FirstPassCubeLabels.jLabel_swap line 196
  13. lemma OAI.FirstPassCubeLabels.b0Label_swap line 203
  14. theorem OAI.SecondPassArithmetic.firstInputFamilyEnergy_swap line 216
  15. def OAI.SecondPassArithmetic.CubeCoordinates.swap line 227
  16. lemma OAI.SecondPassArithmetic.CubeCoordinates.swap_swap line 229
  17. def OAI.SecondPassArithmetic.orientedCubeFirstBlock line 244
  18. theorem OAI.SecondPassArithmetic.orientedCubeFirstBlock_input_transfer line 261
  19. theorem OAI.SecondPassArithmetic.orientedTwoPassage_quantitative line 396
  20. def OAI.CubicEisenstein.euclideanC1cToH1 line 477
  21. lemma OAI.CubicEisenstein.euclideanC1cToH1_norm line 483
  22. lemma OAI.CubicEisenstein.euclideanC1c_supported_range line 486
  23. def OAI.CubicEisenstein.euclideanC1cToSupportedH1 line 508
  24. lemma OAI.CubicEisenstein.compact_clm_closedBall line 513
  25. theorem OAI.CubicEisenstein.euclidean_C1c_family_precompact line 518
  26. abbrev OAI.CubicEisenstein.KernelFundamentalVolume line 545
  27. abbrev OAI.CubicEisenstein.KernelGradientL2 line 548
  28. lemma OAI.CubicEisenstein.kernelTestPartial_continuous line 550
  29. lemma OAI.CubicEisenstein.kernelGradientAt_continuous line 558
  30. lemma OAI.CubicEisenstein.kernelGradientAt_memLp line 566
  31. def OAI.CubicEisenstein.kernelGradientToL2 line 578
  32. lemma OAI.CubicEisenstein.kernelGradientToL2_coe line 581
  33. lemma OAI.CubicEisenstein.kernelGradientToL2_inner line 585
  34. lemma OAI.CubicEisenstein.kernelGradientToL2_norm_sq line 593
  35. def OAI.CubicEisenstein.kernelGradientLinear line 600
  36. def OAI.CubicEisenstein.kernelInitialGradientGraph line 614
  37. lemma OAI.CubicEisenstein.kernelInitialGradientGraph_unique line 617
  38. def OAI.CubicEisenstein.kernelInitialGradient line 627
  39. lemma OAI.CubicEisenstein.kernelInitialGradient_graph line 630
  40. lemma OAI.CubicEisenstein.kernelInitialGradient_dense_domain line 634