OAI/Computability/FourierTransform/Asymptotics.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PowerSaving.Skies.Tm line 12
2. abbrev OAI.PowerSaving.Skies.Qm line 13
3. lemma OAI.PowerSaving.Skies.Ttop line 15
4. lemma OAI.PowerSaving.Skies.Qtop line 16
5. lemma OAI.PowerSaving.Skies.log2_min line 17
6. lemma OAI.PowerSaving.Skies.stack_lim line 23

   Source comment

   n is problem size, N allowed between n and 2n

   lemma stack_lim (n N : ℕ) (hn : 0<n) (h : n≤N) (hk : N ≤ 2*n) (ht : 1≤Tm n) :
       (stackN N:ℝ) ≤ 10 * Tm n := by
   …

   Mentions: OAI.PowerSaving.Skies.Tm

7. lemma OAI.PowerSaving.Skies.order_pow_lim line 38
8. lemma OAI.PowerSaving.Skies.order_lim line 48
9. lemma OAI.PowerSaving.Skies.score_lim line 59
10. lemma OAI.PowerSaving.Skies.hills_lim line 69
11. def OAI.PowerSaving.Skies.flight line 86
12. lemma OAI.PowerSaving.Skies.leg_lim line 88
13. lemma OAI.PowerSaving.Skies.flight_big line 106
14. lemma OAI.PowerSaving.Skies.dwarf line 115

    Source comment

    little o fournishes eventual caps.

    lemma dwarf {v : ℕ→ℝ} (h : Tendsto v atTop atTop) (d : ℕ) {p c : ℝ} (hp : 0<p) (hc : 0<c) :
        ∀ᶠ n in atTop, log (v n)^d ≤ c*v n^p := by
    …

15. lemma OAI.PowerSaving.Skies.docks_ev line 128

    Source comment

    initial branch disappears

    lemma docks_ev (h : ∀ n:ℕ,n ≤ N n ∧ N n ≤ 2*n) :
        ∀ᶠ n in atTop, Ports (N n) := by
    …

16. lemma OAI.PowerSaving.Skies.polylog_ev line 139
17. lemma OAI.PowerSaving.Skies.wind_ev line 156
18. lemma OAI.PowerSaving.Skies.lunch_big line 169