OAI/Geometry/Cannon/Flows/Lower.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CannonNode.lower line 22
  2. def OAI.CannonNode.upper line 25
  3. lemma OAI.CannonNode.ball_range line 30
  4. lemma OAI.CannonNode.ball_extrema line 37
  5. lemma OAI.CannonNode.lower_le_upper line 45
  6. lemma OAI.CannonNode.ball_range_mono line 49
  7. def OAI.CannonNode.childLower line 56
  8. def OAI.CannonNode.childUpper line 58
  9. def OAI.CannonNode.fraction line 60
  10. lemma OAI.CannonNode.fraction_nonneg line 62
  11. lemma OAI.CannonNode.fraction_le_one line 65
  12. lemma OAI.CannonNode.fraction_pos_iff line 73
  13. lemma OAI.CannonNode.child_nested line 78
  14. lemma OAI.CannonNode.positive_child_length line 84