OAI/Combinatorics/HadwigerCounterexample/ConcentrationScales.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HadwigerCounterexample.pay_nat line 15

   Source documentation

   pay slack for any fixed multiple of exponentially smaller term.

   theorem pay_nat {a b : ℝ} (c : ℝ) (hab : b < a) :
       ∀ᶠ n : ℕ in atTop,c * bp (-a*n) ≤ bp (-b*n) := by
   …

   Mentions: OAI.HadwigerCounterexample.bp

2. theorem OAI.HadwigerCounterexample.pay_div_nat line 23
3. theorem OAI.HadwigerCounterexample.cast_tops line 29
4. theorem OAI.HadwigerCounterexample.port_limit line 42
5. def OAI.HadwigerCounterexample.Program.makeData line 50

   Source documentation

   empirical input-and-image law

   def makeData (s : Program p n g A) (w : Wgt A) (o : Forum p n N G) :
       Wgt (A×Rack J N) :=
   …

   Mentions: OAI.HadwigerCounterexample.Program, OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.Forum, OAI.HadwigerCounterexample.Rack

6. theorem OAI.HadwigerCounterexample.Program.data_law line 54
7. theorem OAI.HadwigerCounterexample.Program.view_data line 57
8. theorem OAI.HadwigerCounterexample.Program.freq_data line 61
9. theorem OAI.HadwigerCounterexample.Program.variance_calendar line 66
10. theorem OAI.HadwigerCounterexample.Program.approx_calendar line 106
11. theorem OAI.HadwigerCounterexample.Program.thin_calendar line 123