OAI/NumberTheory/JointDickman/Probability/ChannelGrid.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's refining logarithmic grid

  1. def OAI.JointDickman.channelFineCount line 12
  2. def OAI.JointDickman.channelMesh line 15
  3. def OAI.JointDickman.channelLower line 17
  4. def OAI.JointDickman.channelUpper line 20
  5. theorem OAI.JointDickman.channelFineCount_pos line 23
  6. theorem OAI.JointDickman.channelFineCount_upper line 30
  7. theorem OAI.JointDickman.channelFineCount_eventually_le_square line 39
  8. theorem OAI.JointDickman.channelMesh_pos line 55
  9. theorem OAI.JointDickman.channel_width line 58
  10. theorem OAI.JointDickman.channelLower_ge line 62
  11. theorem OAI.JointDickman.channelUpper_le line 66
  12. theorem OAI.JointDickman.channelCells_disjoint line 76
  13. theorem OAI.JointDickman.channel_total_mass line 94
  14. theorem OAI.JointDickman.channel_atom_lower line 102