OAI/Combinatorics/BalancedRyser/Profiles/ProfileCoordinates.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.clippedProfileCoordinate line 13
  2. theorem OAI.Balanced.clippedProfileCoordinate_apply line 21
  3. theorem OAI.Balanced.clippedProfileCoordinate_nonneg line 24
  4. theorem OAI.Balanced.clippedProfileCoordinate_eq line 27
  5. theorem OAI.Balanced.boundedProfile_coordinate_bounds line 32
  6. theorem OAI.Balanced.clippedProfileCoordinate_eq_of_bounded line 38
  7. def OAI.Balanced.profileCoordinateDeviation line 44
  8. lemma OAI.Balanced.profileCoordinateDeviation_nonneg line 53
  9. lemma OAI.Balanced.profileCoordinateDeviation_zero_iff line 56
  10. theorem OAI.Balanced.profile_coordinate_bounds_weak_limit line 69
  11. theorem OAI.Balanced.ambient_profile_incidence_weak_limit line 86
  12. theorem OAI.Balanced.boundedProfile_incidence_weak_limit line 110
  13. theorem OAI.Balanced.boundedProfile_zero_coordinate_weak_limit line 135