OAI/Combinatorics/HadwigerCounterexample/GroupedQueryIndependence.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Grouped Query Independence

  1. instance OAI.HadwigerCounterexample.knFin line 15
  2. def OAI.HadwigerCounterexample.freePart line 16
  3. def OAI.HadwigerCounterexample.frozenZ line 18
  4. theorem OAI.HadwigerCounterexample.spin_scan_free line 21
  5. theorem OAI.HadwigerCounterexample.fresh_Z line 28
  6. theorem OAI.HadwigerCounterexample.scopedZ_bit line 61
  7. theorem OAI.HadwigerCounterexample.scopedZ_scan line 66
  8. def OAI.HadwigerCounterexample.freeNet line 70
  9. theorem OAI.HadwigerCounterexample.law_probes line 74
  10. def OAI.HadwigerCounterexample.bloom line 95
  11. theorem OAI.HadwigerCounterexample.buds line 98
  12. theorem OAI.HadwigerCounterexample.inject_column_slice line 109
  13. theorem OAI.HadwigerCounterexample.ray_bloom line 118
  14. def OAI.HadwigerCounterexample.Template.queryLaw line 134
  15. theorem OAI.HadwigerCounterexample.Template.queries_bloom line 140

    Source documentation

    covers endpoint variants whenever a position only visits each port once

    theorem queries_bloom (x : Jā†’ Inputs p n I) (g : Route (KeySlots p v.t) G)
    (h : bloom p x) (he : āˆ€ e : G,Injective (fun i : Port g e => i.val.1))
    (i : G) :
    Injective (pooled (fun i => queryLaw v (x i) (g:=g)) i).mulVec := by
ā€¦

    Mentions: OAI.HadwigerCounterexample.Inputs, OAI.HadwigerCounterexample.Route, OAI.HadwigerCounterexample.KeySlots, OAI.HadwigerCounterexample.bloom, OAI.HadwigerCounterexample.Port, OAI.HadwigerCounterexample.pooled, OAI.HadwigerCounterexample.Template.queryLaw