OAI/Combinatorics/UniformKServer/CausalLevelAux.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The integrated auxiliary function is adapted to the old request history.

  1. lemma OAI.UniformKServer.LevelMap.Data.heavyPotential_inputs line 18
  2. lemma OAI.UniformKServer.LevelMap.Data.auxiliary_inputs line 32