OAI/NumberTheory/JointDickman/Amplification/CoarseGrid.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Grouping the manuscript grid into equal coarse cells

  1. def OAI.JointDickman.channelBlockCount line 13
  2. theorem OAI.JointDickman.channelFineCount_eq line 16
  3. def OAI.JointDickman.groupedLower line 18
  4. def OAI.JointDickman.groupedUpper line 21
  5. theorem OAI.JointDickman.grouped_width line 24
  6. theorem OAI.JointDickman.groupedLower_ge line 27
  7. theorem OAI.JointDickman.groupedUpper_le line 30
  8. theorem OAI.JointDickman.groupedCells_disjoint line 33
  9. theorem OAI.JointDickman.groupedLower_diameter line 39
  10. theorem OAI.JointDickman.grouped_total_mass line 65
  11. theorem OAI.JointDickman.channelFineCount_lower line 72
  12. theorem OAI.JointDickman.channelMesh_fine_upper line 79