OAI/Geometry/CylinderCovering/Physical/WeightLipschitz.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RuledApproximation.inverse_difference_le line 8
  2. lemma OAI.RuledApproximation.physicalDirection_norm_one_le line 19
  3. lemma OAI.RuledApproximation.physicalDirection_difference_bound line 25
  4. theorem OAI.RuledApproximation.physicalWeight_difference_le line 51
  5. theorem OAI.RuledApproximation.physicalWeight_lipschitzWith line 58
  6. lemma OAI.RuledApproximation.physicalWeight_le_one line 66
  7. lemma OAI.RuledApproximation.affine_physicalWeight_error line 70
  8. theorem OAI.NilpotentRate.collar_area_bound line 90
  9. theorem OAI.NilpotentRate.weighted_cell_bound line 107
  10. theorem OAI.NilpotentRate.sum_cell_errors line 119