OAI/Combinatorics/UniformKServer/SideParameterChanges.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Prepared parameter jumps charged only to changed size coordinates (§04). Constants are independent of the number of children and of the smallest size.

  1. def OAI.UniformKServer.SideParameterChanges.size line 17
  2. theorem OAI.UniformKServer.SideParameterChanges.same_sizes line 20
  3. theorem OAI.UniformKServer.SideParameterChanges.coordinate_bound_all line 40
  4. theorem OAI.UniformKServer.SideParameterChanges.parameter_jump line 50
  5. theorem OAI.UniformKServer.SideParameterChanges.prepared_upper line 72