OAI/NumberTheory/Ostmann/Construction/RepeatRemovalBudget.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.moment_small_shift line 14

   Source documentation

   A shift of at most one quarter of the inverse moment order changes the moment by a factor less than 3/2.

   theorem moment_small_shift (A B : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B)
       (k : ℕ) (hk : 0 < k) (hsmall : 4 * k * B ≤ A) :
       (A + B) ^ k ≤ (3 / 2 : ℝ) * A ^ k := by
   …

2. theorem OAI.Ostmann.repeat_shift_of_squared_budget line 46

   Source documentation

   The squared form avoids logarithms of either moment and is convenient when inserting I≥sqrt(X)*exp(.016K) and I₀≤C*X.

   theorem repeat_shift_of_squared_budget (I I₀ : ℝ) (hI : 0 ≤ I) (hI₀ : 0 ≤ I₀)
       (J k : ℕ) (hJ : 0 < J) (hk : 0 < k)
       (hbudget : ((16 * (k : ℝ) ^ 3 / J) ^ k) * I₀ ^ 2 ≤ I ^ 2) :
       4 * k * ((Real.sqrt ((k : ℝ) * J) / J) * I₀ ^ (1 / (k : ℝ))) ≤
         I ^ (1 / (k : ℝ)) := by
   …