OAI/Geometry/CylinderCovering/Nilpotent/GridMeasure.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.NilpotentGrid.coarseCell_volume line 10
  2. lemma OAI.NilpotentGrid.coordinate_zero_volume line 23
  3. lemma OAI.NilpotentGrid.unequal_cell_coordinate line 37
  4. lemma OAI.NilpotentGrid.coarseCell_aeDisjoint line 44
  5. lemma OAI.NilpotentGrid.coarseUnion_volume line 64
  6. lemma OAI.NilpotentGrid.coarseUnion_integral line 73
  7. lemma OAI.NilpotentGrid.coarseCell_integral_error line 91
  8. theorem OAI.NilpotentGrid.coarseUnion_integral_error line 115
  9. lemma OAI.NilpotentGrid.coarseUnion_integral_le line 142
  10. theorem OAI.NilpotentGrid.tagged_sum_le_domain_integral line 160
  11. lemma OAI.NilpotentGrid.coarseCell_integral_error_of_oscillation line 176
  12. theorem OAI.NilpotentGrid.coarseUnion_integral_error_of_oscillation line 197
  13. theorem OAI.NilpotentGrid.tagged_sum_le_domain_integral_of_oscillation line 223