OAI/NumberTheory/JointDickman/Probability/SampledHistogram.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Residue projection of the sampled endpoint histogram

  1. theorem OAI.JointDickman.unitResidueFourier_projected_sub_contract line 11
  2. def OAI.JointDickman.sampledProjectedValue line 20
  3. def OAI.JointDickman.sampledProjectedFourier line 27
  4. theorem OAI.JointDickman.sampledProjectedValue_eq_sum line 35
  5. theorem OAI.JointDickman.sampledProjectedFourier_eq line 52
  6. theorem OAI.JointDickman.sampledProjectedFourier_square_le line 60
  7. theorem OAI.JointDickman.projected_averaged_to_sampled_square_error line 70