OAI/Combinatorics/HadwigerCounterexample/SingletonPhaseTests.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HadwigerCounterexample.avg_on_support line 13
2. theorem OAI.HadwigerCounterexample.Bazaar.single_pitch line 24
3. def OAI.HadwigerCounterexample.Bazaar.frequent line 58
4. theorem OAI.HadwigerCounterexample.Bazaar.calm_pitch line 62
5. def OAI.HadwigerCounterexample.Bazaar.bids line 91

   Source documentation

   fixed companion Z restrict frequent pair to this list of small Φ values

   def bids (w : Wgt (UnitType p n N)) (S : Party) (i : Bool)
       (M G : Atlas p r T) (Z : Batch G N) : Finset (Batch M N) :=
   …

   Mentions: OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.UnitType, OAI.HadwigerCounterexample.Party, OAI.HadwigerCounterexample.Atlas, OAI.HadwigerCounterexample.Batch

6. theorem OAI.HadwigerCounterexample.Bazaar.bids_mem line 96
7. theorem OAI.HadwigerCounterexample.Bazaar.bids_bound line 104