OAI/Combinatorics/UniformKServer/ParkCapacity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Shared subtree capacity for parks at many depths. The geometry enters only through nested regions, same-depth disjointness, and actual validity witnesses.

  1. theorem OAI.UniformKServer.ParkCapacity.grouped line 17
  2. structure OAI.UniformKServer.ParkCapacity.Geometry line 36
  3. def OAI.UniformKServer.ParkCapacity.ball line 45
  4. def OAI.UniformKServer.ParkCapacity.mass line 46
  5. theorem OAI.UniformKServer.ParkCapacity.ancestor_region line 48
  6. theorem OAI.UniformKServer.ParkCapacity.disjoint_mass line 63
  7. theorem OAI.UniformKServer.ParkCapacity.cumulative line 81