OAI/Combinatorics/HadwigerCounterexample/InformationSmallSetBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Information Small Set Bounds

  1. structure OAI.HadwigerCounterexample.Ultra line 15

    Source documentation

    Family of orientation/flag-conditional laws (μ already realizes joint flag law).

    structure Ultra (μ : Wgt A) (p : A→Wgt B) : Prop where
…

    Mentions: OAI.HadwigerCounterexample.Wgt

  2. def OAI.HadwigerCounterexample.budget line 21
  3. def OAI.HadwigerCounterexample.tariffs line 23
  4. def OAI.HadwigerCounterexample.catalog line 27
  5. theorem OAI.HadwigerCounterexample.Ultra.maxCat line 34
  6. theorem OAI.HadwigerCounterexample.Ultra.cat_dom line 36
  7. theorem OAI.HadwigerCounterexample.Ultra.cat_sub line 43
  8. theorem OAI.HadwigerCounterexample.binary_info line 50
  9. theorem OAI.HadwigerCounterexample.expand_event line 62
  10. theorem OAI.HadwigerCounterexample.ui_threshold line 89