OAI/Combinatorics/HadwigerCounterexample/CollisionInequality.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HadwigerCounterexample.density line 15
2. def OAI.HadwigerCounterexample.overlap line 16
3. theorem OAI.HadwigerCounterexample.overlap_count line 19
4. def OAI.HadwigerCounterexample.Volley.hist line 43

   Source documentation

   law of accepted keys as an unnormalized histogram

   def hist (v : A → Volley p n I) (t : Tagging p I)
       (μ : Wgt (UnitType p n N)) (rho' : Wgt A) (U : A → UnitType p n N → Prop) :
       Wgt (Keys (p:=p) t N) :=
   …

   Mentions: OAI.HadwigerCounterexample.Volley, OAI.HadwigerCounterexample.Tagging, OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.UnitType, OAI.HadwigerCounterexample.Keys

5. theorem OAI.HadwigerCounterexample.Volley.record_sum line 49
6. theorem OAI.HadwigerCounterexample.Volley.collision line 100
7. theorem OAI.HadwigerCounterexample.collision_scales line 174