OAI/Computability/FourierTransform/TensorSaving.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PowerSaving.RAM.allot_bound line 11

   Source documentation

   Work bound for the flat recursion. k=0 treated with k+1 in the conclusion.

   theorem allot_bound (u a D : ℕ) (hu : 3≤u) (z : ℝ) (hz : 0≤z)
       (hD : (D:ℝ)/(2:ℝ)^a < (u:ℝ)^z) :
       ∃ C : ℝ, 1≤C ∧ ∀ k : ℕ,
         (allot u a D k : ℝ) ≤ C*(2:ℝ)^k*((k:ℝ)+1)^z := by
   …

   Mentions: OAI.PowerSaving.RAM.allot

2. def OAI.PowerSaving.alpha line 81
3. theorem OAI.PowerSaving.alpha_pos line 83
4. theorem OAI.PowerSaving.alpha_lt line 84
5. lemma OAI.PowerSaving.network_rate line 88
6. def OAI.PowerSaving.hills line 114

   Source documentation

   Natural envelopes using a ceiling for real powers.

   def hills (k : ℕ) := Nat.ceil (((k:ℝ)+1)^alpha)

   Mentions: OAI.PowerSaving.alpha

7. lemma OAI.PowerSaving.hills_pos line 116
8. lemma OAI.PowerSaving.hills_mono line 119
9. lemma OAI.PowerSaving.hills_le line 124
10. lemma OAI.PowerSaving.hills_real line 129
11. lemma OAI.PowerSaving.total_hills line 135