OAI/NumberTheory/DirichletL/MeanSquare/ReflectedDyadicSeries.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.InitialMeanSquare.star_normalizedColumn line 84
  2. lemma OAI.InitialMeanSquare.conjugateProfile_support_bound line 91
  3. theorem OAI.InitialMeanSquare.initial_nonzero_source_eq_bins line 106
  4. theorem OAI.InitialMeanSquare.initial_nonzero_source_norm_le_bins line 133
  5. def OAI.InitialMeanSquare.initialBinCost line 162
  6. theorem OAI.InitialMeanSquare.initial_nonzero_source_transfer line 177
  7. theorem OAI.CompletedGauss.completed_smooth_series_rowPhase line 235
  8. theorem OAI.CompletedGauss.completed_fiber_scalar_cost line 340
  9. theorem OAI.CompletedGauss.completed_conductor_norm_bound line 402
  10. theorem OAI.CompletedGauss.completed_actual_fiber_cost line 413
  11. def OAI.CompletedGauss.completedShellWindow line 448
  12. theorem OAI.CompletedGauss.completedShellWindow_support line 451
  13. theorem OAI.CompletedGauss.completedShellWindow_norm line 459
  14. theorem OAI.CompletedGauss.completedShellWindow_log line 463
  15. theorem OAI.CompletedGauss.dyadic_root_product_bound line 473
  16. def OAI.CompletedGauss.reflectedDyadicCoefficient line 484
  17. theorem OAI.CompletedGauss.reflectedDyadicCoefficient_norm line 494
  18. def OAI.CompletedGauss.reflectedBranchBlock line 548
  19. theorem OAI.CompletedGauss.completed_reflected_branch_series line 557