OAI/NumberTheory/DirichletL/GaussSum/BranchScaling.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CompletedGauss.completedResidualScale line 78
  2. def OAI.CompletedGauss.completedBranchScale line 81
  3. theorem OAI.CompletedGauss.completed_reflected_fiber line 87
  4. def OAI.LocalReflectionBrackets.unitArgumentFactor line 138
  5. theorem OAI.LocalReflectionBrackets.bracket_mul_unit line 141
  6. theorem OAI.LocalReflectionBrackets.unitArgumentFactor_norm line 152
  7. theorem OAI.CompletedGauss.unit_ramified_quotient_ne_zero line 163
  8. def OAI.CompletedGauss.ramifiedBranchPhase line 171
  9. theorem OAI.CompletedGauss.ramifiedBranchPhase_norm line 177
  10. theorem OAI.CompletedGauss.ramified_bracket_full_expansion line 185
  11. def OAI.InitialMeanSquare.sourceLabelUnit line 215
  12. lemma OAI.InitialMeanSquare.sourceLabelUnit_spec line 218
  13. def OAI.InitialMeanSquare.sourceIdealPoint line 221
  14. def OAI.InitialMeanSquare.sourceUnitPoint line 223
  15. lemma OAI.InitialMeanSquare.sourceUnitPoint_injective line 226
  16. def OAI.InitialMeanSquare.sourceIdealTarget line 234
  17. theorem OAI.InitialMeanSquare.sourceChildEnergy_le_ideal line 243
  18. theorem OAI.InitialMeanSquare.sourceGeometricMean_le_ideal line 266
  19. theorem OAI.InitialMeanSquare.sourceIdealTarget_bounds line 277
  20. theorem OAI.InitialMeanSquare.positive_nested_density_bound line 292
  21. theorem OAI.InitialMeanSquare.polynomial_density_cost line 319
  22. theorem OAI.InitialMeanSquare.initialBinCost_of_child_bound line 347
  23. lemma OAI.FirstPassCubeLabels.blockRow_mul line 421
  24. lemma OAI.FirstPassCubeLabels.blockRow_unit_mul_star line 426
  25. lemma OAI.FirstPassCubeLabels.originalLabelColumn_unit_c line 432
  26. lemma OAI.FirstPassCubeLabels.row_four_eq_star_square line 441
  27. theorem OAI.FirstPassCubeLabels.threeGaussRowFactor_common_unit line 448
  28. theorem OAI.FirstPassCubeLabels.actualFirstKernel_common_unit line 474
  29. theorem OAI.FirstPassCubeLabels.commonUnitPhase_norm line 501
  30. def OAI.FirstPassCubeLabels.unitSquareRowEquiv line 511
  31. theorem OAI.FirstPassCubeLabels.tsum_actualFirstKernel_common_unit line 523
  32. lemma OAI.FirstPassCubeLabels.blockRow_at_zero line 559
  33. lemma OAI.FirstPassCubeLabels.threeGaussRowFactor_zero_nonempty line 568
  34. theorem OAI.FirstPassCubeLabels.actualFirstKernel_zero line 575
  35. theorem OAI.FirstPassCubeLabels.actualFirstKernel_truncate line 616