OAI/NumberTheory/JointDickman/Probability/HistogramProductError.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The product error for the actual two endpoint histograms

  1. def OAI.JointDickman.manuscriptFourier line 11
  2. def OAI.JointDickman.manuscriptApproxFourier line 16
  3. def OAI.JointDickman.manuscriptAmplitudeEnergy line 21
  4. theorem OAI.JointDickman.manuscriptAmplitudeEnergy_nonneg line 27
  5. theorem OAI.JointDickman.manuscriptFourier_square_bounds line 34
  6. theorem OAI.JointDickman.manuscript_histogram_product_error line 60