OAI/Combinatorics/HadwigerCounterexample/UltrafilterRates.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Ultrafilter Rates

  1. def OAI.HadwigerCounterexample.slight line 16

    Source documentation

    Upper target thresholds, without claiming nonnegativity.

    def slight (l : Filter A) (x : A→ℝ) := ∀ δ:ℝ,0<δ→∀ᶠ n in l,x n≤δ
  2. theorem OAI.HadwigerCounterexample.slight_gap line 18
  3. def OAI.HadwigerCounterexample.warm line 30

    Source documentation

    At least subexponential mass.

    def warm (l : Filter A) (z x : A→ℝ) :=
…
  4. theorem OAI.HadwigerCounterexample.warm.const line 35
  5. theorem OAI.HadwigerCounterexample.warm.mono line 38
  6. theorem OAI.HadwigerCounterexample.warm.positive line 40
  7. theorem OAI.HadwigerCounterexample.warm.mul line 43
  8. theorem OAI.HadwigerCounterexample.warm.inv_cap line 48
  9. theorem OAI.HadwigerCounterexample.warm.survive line 54
  10. theorem OAI.HadwigerCounterexample.ExpSmall.bp_n line 66
  11. theorem OAI.HadwigerCounterexample.ExpSmall.poly line 69
  12. theorem OAI.HadwigerCounterexample.taking line 80
  13. theorem OAI.HadwigerCounterexample.diagonal_gains line 88
  14. theorem OAI.HadwigerCounterexample.slight_inv_stage line 102
  15. theorem OAI.HadwigerCounterexample.trend_sizes line 109