OAI/NumberTheory/JointDickman/Counting/SamplingRateEnvelope.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A vanishing error envelope for the adaptive cut comparison

  1. def OAI.JointDickman.samplingDegreeEnvelope line 11
  2. def OAI.JointDickman.samplingSquareEnvelope line 14
  3. def OAI.JointDickman.samplingEntropyEnvelope line 17
  4. def OAI.JointDickman.samplingRateEnvelope line 20
  5. theorem OAI.JointDickman.samplingDegreeEnvelope_tendsto line 26
  6. theorem OAI.JointDickman.samplingSquareEnvelope_tendsto line 33
  7. theorem OAI.JointDickman.samplingRateEnvelope_tendsto line 40
  8. theorem OAI.JointDickman.sampling_parameters_eventually line 53