OAI/NumberTheory/DirichletL/MeanSquare/CanonicalDensity.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InitialMeanSquare.outsideIdealsUpTo_mono line 80
  2. theorem OAI.InitialMeanSquare.outside_row_cutoff_stable line 86
  3. def OAI.SecondPassArithmetic.canonicalCubeDualFinite line 132
  4. def OAI.SecondPassArithmetic.canonicalCubeDualTail line 145
  5. theorem OAI.SecondPassArithmetic.canonicalCubeBeforePoisson_split line 158
  6. theorem OAI.SecondPassArithmetic.canonicalCubeDualFinite_eq_raw_blocks line 181
  7. def OAI.SecondPassArithmetic.canonicalSourceBlocks line 212
  8. theorem OAI.SecondPassArithmetic.canonicalSourceBlocks_mem line 217
  9. theorem OAI.SecondPassArithmetic.sum_canonicalSourceBlocks line 223
  10. theorem OAI.SecondPassArithmetic.canonicalSourceBlocks_admissible line 255
  11. theorem OAI.SecondPassArithmetic.canonicalSourceBlocks_cube_norms line 278
  12. def OAI.SecondPassArithmetic.canonicalSourceCutoff line 302
  13. lemma OAI.SecondPassArithmetic.canonicalSourceCutoff_zero line 306
  14. def OAI.SecondPassArithmetic.canonicalSourceTotal line 313
  15. def OAI.SecondPassArithmetic.canonicalSourceZero line 321
  16. def OAI.SecondPassArithmetic.canonicalSourceFinite line 329
  17. def OAI.SecondPassArithmetic.canonicalSourceTail line 337
  18. def OAI.SecondPassArithmetic.canonicalBlockFrequencies line 345
  19. def OAI.SecondPassArithmetic.canonicalBlockCoefficient line 348
  20. theorem OAI.SecondPassArithmetic.canonicalSourceFinite_eq_raw line 353
  21. theorem OAI.SecondPassArithmetic.canonicalSourceTotal_split line 375
  22. theorem OAI.SecondPassArithmetic.canonicalBlockCoefficient_bound line 394
  23. theorem OAI.SecondPassArithmetic.canonicalSource_twoPassage_quantitative line 416
  24. theorem OAI.InitialMeanSquare.initial_subunit_row_le_label line 495
  25. theorem OAI.InitialMeanSquare.initial_subunit_density_bound line 506
  26. lemma OAI.InitialMeanSquare.initialErrorFrequencyBound_ge_one line 537
  27. lemma OAI.InitialMeanSquare.initialErrorRowBound_ge_one line 546
  28. abbrev OAI.InitialMeanSquare.OutsidePrimeIndex line 562
  29. def OAI.InitialMeanSquare.outsidePrime line 565
  30. lemma OAI.InitialMeanSquare.outsidePrime_ne_zero line 568
  31. lemma OAI.InitialMeanSquare.outsidePrime_maximal line 572
  32. lemma OAI.InitialMeanSquare.outsidePrime_coprime line 579
  33. lemma OAI.InitialMeanSquare.outsidePrime_good line 583
  34. lemma OAI.InitialMeanSquare.outsidePrime_odd line 587
  35. lemma OAI.InitialMeanSquare.outsidePrime_injective line 591
  36. lemma OAI.InitialMeanSquare.outsidePrime_primary line 597
  37. def OAI.InitialMeanSquare.initialExcludedNorm line 602
  38. lemma OAI.InitialMeanSquare.initialExcludedNorm_ge_one line 605
  39. def OAI.InitialMeanSquare.outsideCanonicalDensity line 608
  40. def OAI.InitialMeanSquare.HasInitialCanonicalDensity line 619