OAI/Combinatorics/HadwigerCounterexample/EmpiricalInformation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HadwigerCounterexample.draw_pick line 15
2. theorem OAI.HadwigerCounterexample.draw_elem line 25
3. theorem OAI.HadwigerCounterexample.tension_traj line 28
4. abbrev OAI.HadwigerCounterexample.Track line 47
5. def OAI.HadwigerCounterexample.traceTraj line 48
6. theorem OAI.HadwigerCounterexample.draws_trace line 53
7. theorem OAI.HadwigerCounterexample.traj_charge line 65
8. theorem OAI.HadwigerCounterexample.traj_cap line 89

   Source documentation

   If components are coarse with no tiny positive atoms, their repeat law has a corresponding cap cost for any submeasure.

   theorem traj_cap (p : Wgt B) (hp : IsLaw p) (u : ℝ)
       (h : ∀ i, p i≠0 → bp (-u)≤p i) :
       ∀ x, draws (Fin l) p x≠0 → bp (-u*l) ≤ draws (Fin l) p x := by
   …

   Mentions: OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.IsLaw, OAI.HadwigerCounterexample.bp, OAI.HadwigerCounterexample.draws