OAI/NumberTheory/DirichletL/CubicSieve/ReopenedFibers.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SecondPassArithmetic.globalChildBudget_canonical_bound line 85
  2. def OAI.SecondPassArithmetic.reopenedCubeFiber line 146
  3. lemma OAI.SecondPassArithmetic.mem_reopenedCubeFiber line 151
  4. def OAI.SecondPassArithmetic.reopenedCubeFamily line 167
  5. lemma OAI.SecondPassArithmetic.mem_reopenedCubeFamily line 170
  6. lemma OAI.SecondPassArithmetic.reopenedCubeFamily_admissible line 181
  7. lemma OAI.SecondPassArithmetic.reopenedCubeFamily_support line 185
  8. theorem OAI.SecondPassArithmetic.sum_reopenedCubeFamily line 192
  9. lemma OAI.SecondPassArithmetic.primeProduct_finsupp_support line 220
  10. lemma OAI.SecondPassArithmetic.reopenedCubeFamily_cube_norms line 229
  11. def OAI.SecondPassArithmetic.reopenedPairCoefficient line 240
  12. lemma OAI.SecondPassArithmetic.reopenedPairCoefficient_independent_common line 245
  13. lemma OAI.SecondPassArithmetic.reopenedPairCoefficient_bound line 249
  14. theorem OAI.SecondPassArithmetic.reopenedCanonicalRow_smoothed_eq_source line 266
  15. theorem OAI.SecondPassArithmetic.reopenedCubeFamily_card line 324
  16. theorem OAI.SecondPassArithmetic.reopenedCubeFamily_card_le line 330
  17. theorem OAI.SecondPassArithmetic.reopenedSourceBlocks_bounds line 344
  18. theorem OAI.SecondPassArithmetic.reopenedCubeFamily_small_power line 357
  19. theorem OAI.SecondPassArithmetic.reopenedCanonicalRow_smoothed_split line 395
  20. theorem OAI.SecondPassArithmetic.reopenedCanonicalBlockCoefficient_bound line 419
  21. lemma OAI.CubicEisenstein.euclideanIntegral_borel_transport line 441
  22. lemma OAI.CubicEisenstein.euclideanIntegrable_borel_transport line 453
  23. lemma OAI.CubicEisenstein.euclideanNativeIntegral_eq_borel line 465
  24. lemma OAI.CubicEisenstein.euclideanNativeIntegrable_iff_borel line 472
  25. def OAI.CubicEisenstein.euclideanLp_borel_transport line 479
  26. def OAI.CubicEisenstein.euclideanNativeLpBorelEquiv line 491
  27. lemma OAI.CubicEisenstein.euclideanLp_borel_transport_schwartz line 497
  28. lemma OAI.CubicEisenstein.euclideanNativeLpBorelEquiv_schwartz line 510
  29. lemma OAI.CubicEisenstein.euclideanOriginalMeasurable_eq_borel line 525
  30. def OAI.CubicEisenstein.kernelLocalizedRealTest line 532
  31. lemma OAI.CubicEisenstein.sourceC1c_toL2_norm_sq line 538
  32. lemma OAI.CubicEisenstein.sourceC1c_toL2Grad_norm_sq line 551
  33. lemma OAI.CubicEisenstein.kernelLocalizedRealTest_grad_le line 564
  34. lemma OAI.CubicEisenstein.kernelLocalizedRealTest_energy_le line 581
  35. lemma OAI.CubicEisenstein.kernelLocalizedRealTest_support line 604
  36. theorem OAI.CubicEisenstein.kernelLocalizedReal_family_precompact line 615
  37. abbrev OAI.CubicEisenstein.RellichRealL2 line 650
  38. abbrev OAI.CubicEisenstein.RellichComplexL2 line 651
  39. def OAI.CubicEisenstein.kernelComplexL2Assemble line 653
  40. lemma OAI.CubicEisenstein.kernelComplexL2Assemble_localized line 659
  41. theorem OAI.CubicEisenstein.kernelLocalizedComplex_family_precompact line 681
  42. theorem OAI.CubicEisenstein.kernelLocalizedNative_family_precompact line 698
  43. def OAI.CubicEisenstein.kernelEnergyLocalizeL2 line 712
  44. theorem OAI.CubicEisenstein.kernelEnergyLocalizeL2_isCompact line 715