OAI/NumberTheory/DirichletL/MeanSquare/HarmonicAggregation.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InitialMeanSquare.initialRayMass line 81
  2. lemma OAI.InitialMeanSquare.initialRayMass_nonneg line 83
  3. theorem OAI.InitialMeanSquare.initial_complementary_harmonic line 91
  4. theorem OAI.InitialMeanSquare.initial_harmonic_aggregation line 112
  5. def OAI.SecondPassArithmetic.sourceGlobalBlock line 164
  6. lemma OAI.SecondPassArithmetic.cube_swap_support line 167
  7. lemma OAI.SecondPassArithmetic.cube_swap_sum line 171
  8. lemma OAI.SecondPassArithmetic.orientedCubeFirstBlock_single_source line 177
  9. lemma OAI.SecondPassArithmetic.canonical_log_kernel line 204
  10. def OAI.SecondPassArithmetic.commonProductUnit line 240
  11. lemma OAI.SecondPassArithmetic.commonProductUnit_spec line 245
  12. def OAI.SecondPassArithmetic.commonCubePhase line 250
  13. lemma OAI.SecondPassArithmetic.commonCubePhase_norm line 255
  14. theorem OAI.SecondPassArithmetic.canonicalSource_mode_attachment line 260
  15. lemma OAI.SecondPassArithmetic.orientedCubeFirstBlock_eq_sum_single line 298
  16. def OAI.SecondPassArithmetic.rawCanonicalBlock line 311
  17. def OAI.SecondPassArithmetic.sourceFrequencyEquiv line 326
  18. def OAI.SecondPassArithmetic.sourceRotatedCoefficient line 329
  19. lemma OAI.SecondPassArithmetic.sourceFrequencyEquiv_label line 334
  20. lemma OAI.SecondPassArithmetic.sourceFrequencyEquiv_row_norm line 338
  21. lemma OAI.SecondPassArithmetic.sourceFrequencyEquiv_row_ne_zero line 344
  22. lemma OAI.SecondPassArithmetic.sourceRotatedCoefficient_norm line 349
  23. theorem OAI.SecondPassArithmetic.rawCanonicalBlock_eq_oriented line 362
  24. theorem OAI.SecondPassArithmetic.rawCanonicalTwoPassage_quantitative line 413
  25. theorem OAI.SecondPassArithmetic.padded_orientedCubeFirstBlock_input_transfer line 498