OAI/NumberTheory/DirichletL/MeanSquare/PoissonSource.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InitialMeanSquare.outside_mean_square_source line 80
  2. lemma OAI.InitialMeanSquare.initial_actual_row_norm line 147
  3. lemma OAI.InitialMeanSquare.initialLogIndex_eq_second line 155
  4. theorem OAI.InitialMeanSquare.initial_sector_coordinates line 159
  5. theorem OAI.InitialMeanSquare.initial_bin_transfer line 179
  6. theorem OAI.FiniteOverlapDecomposition.sum_powerset_split line 243
  7. theorem OAI.FiniteOverlapDecomposition.sum_pair_split_cube line 279
  8. def OAI.SecondPassArithmetic.canonicalSourceCoefficient line 308
  9. theorem OAI.SecondPassArithmetic.canonicalSourceCoefficient_union line 314
  10. theorem OAI.SecondPassArithmetic.canonicalCube_pair_row line 329
  11. theorem OAI.SecondPassArithmetic.canonicalSourceCoefficient_cube_split line 375
  12. def OAI.FirstPassCubeLabels.canonicalPairMode line 420
  13. lemma OAI.FirstPassCubeLabels.canonicalPairMode_summable line 429
  14. lemma OAI.FirstPassCubeLabels.actualFirstKernel_summable line 459
  15. theorem OAI.FirstPassCubeLabels.canonicalPair_first_poisson line 475
  16. lemma OAI.FirstPassCubeLabels.tsum_actualFirstKernel line 515
  17. def OAI.FirstPassCubeLabels.disjointCanonicalSource line 538
  18. theorem OAI.FirstPassCubeLabels.disjointCanonicalSource_poisson line 547
  19. def OAI.SecondPassArithmetic.canonicalCubeSourcePair line 586
  20. def OAI.SecondPassArithmetic.canonicalCubeOuter line 596
  21. def OAI.SecondPassArithmetic.canonicalCubeResidual line 601
  22. def OAI.SecondPassArithmetic.canonicalCubeBeforePoisson line 607
  23. lemma OAI.SecondPassArithmetic.cube_filter_left line 618
  24. lemma OAI.SecondPassArithmetic.cube_filter_right line 624
  25. theorem OAI.SecondPassArithmetic.canonicalCubeSourcePair_factor line 630
  26. def OAI.SecondPassArithmetic.canonicalCubeCorrelation line 661
  27. theorem OAI.SecondPassArithmetic.canonicalCubeCorrelation_eq_blocks line 667
  28. theorem OAI.SecondPassArithmetic.canonicalCubeBeforePoisson_eq_all_modes line 714
  29. lemma OAI.SecondPassArithmetic.canonicalSourceCoefficient_norm_le_one line 733
  30. lemma OAI.SecondPassArithmetic.canonicalCubeOuter_norm_le_one line 751