OAI/Combinatorics/UniformKServer/KeyEdits.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniformKServer.KeyEdits.overlay line 15

   Source documentation

   Fixed earlier and later structures implement precedence. Label recycling is immaterial to this one-edit operation: an unchanged record has its old label and both other structures are held fixed.

   def overlay (earlier : Option J) (label : I → J) (later : J) (o : Option I) : J :=
   …

2. def OAI.UniformKServer.KeyEdits.changed line 18
3. def OAI.UniformKServer.KeyEdits.uncovered line 21
4. def OAI.UniformKServer.KeyEdits.retirement line 23
5. def OAI.UniformKServer.KeyEdits.next line 28
6. theorem OAI.UniformKServer.KeyEdits.first_persists line 29
7. theorem OAI.UniformKServer.KeyEdits.changed_bounds line 44
8. theorem OAI.UniformKServer.KeyEdits.changed_self line 49
9. theorem OAI.UniformKServer.KeyEdits.uncovered_bounds line 52
10. theorem OAI.UniformKServer.KeyEdits.none_charge line 55
11. theorem OAI.UniformKServer.KeyEdits.insertion_stationary line 65

    Source documentation

    All three rows of the source noncoverage table, including changes hidden by higher-priority structures. Covers/radii are persistent for old records.

    theorem insertion_stationary (old : List I) (keep cover : I → Bool) (n : I)
        (earlier : Option J) (label : I → J) (later : J) :
        changed earlier label later (old.find? cover) ((next old keep n).find? cover) +
          uncovered ((next old keep n).find? cover)-uncovered (old.find? cover) ≤
            2*retirement (old.find? cover) keep
     := by
    …

    Mentions: OAI.UniformKServer.KeyEdits.changed, OAI.UniformKServer.KeyEdits.next, OAI.UniformKServer.KeyEdits.uncovered, OAI.UniformKServer.KeyEdits.retirement

12. theorem OAI.UniformKServer.KeyEdits.insertion_mover line 84
13. theorem OAI.UniformKServer.KeyEdits.shadowed line 100