OAI/NumberTheory/EgyptianFractions/DilationRecurrenceUpper.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.DilationRecurrence.exists_affine_upper_bound line 12

   Source documentation

   An eventual dilation recurrence has a global affine barrier whenever its linear drift fits the proposed slope. The finitely many initial values are absorbed in one constant, without a positivity assumption on the sequence.

   theorem exists_affine_upper_bound
       (f g : ℕ → ℝ) (d : ℕ) (hd : 2 ≤ d) (a b : ℝ) (hb : 0 ≤ b)
       (hmargin : a + b / (d : ℝ) ≤ b)
       (hrec : ∀ᶠ n : ℕ in atTop, f n ≤ g n + f (n / d))
       (hstep : ∀ᶠ n : ℕ in atTop, g n ≤ a * (n : ℝ)) :
       ∃ B : ℝ, 0 ≤ B ∧ ∀ n : ℕ, f n ≤ b * (n : ℝ) + B := by
   …

2. theorem OAI.Problem337.DilationRecurrence.eventually_linear_of_affine line 46

   Source documentation

   Any strict enlargement of an affine barrier is eventually a linear bound.

   theorem eventually_linear_of_affine
       (f : ℕ → ℝ) (b B c : ℝ) (hbc : b < c)
       (hbound : ∀ n : ℕ, f n ≤ b * (n : ℝ) + B) :
       ∀ᶠ n : ℕ in atTop, f n ≤ c * (n : ℝ) := by
   …

3. theorem OAI.Problem337.DilationRecurrence.eventually_upper_bound line 59

   Source documentation

   A fixed strict slack in the slope removes the initial-value constant.

   theorem eventually_upper_bound
       (f g : ℕ → ℝ) (d : ℕ) (hd : 2 ≤ d) (a b c : ℝ) (hb : 0 ≤ b)
       (hmargin : a + b / (d : ℝ) ≤ b) (hbc : b < c)
       (hrec : ∀ᶠ n : ℕ in atTop, f n ≤ g n + f (n / d))
       (hstep : ∀ᶠ n : ℕ in atTop, g n ≤ a * (n : ℝ)) :
       ∀ᶠ n : ℕ in atTop, f n ≤ c * (n : ℝ) := by
   …

4. theorem OAI.Problem337.DilationRecurrence.eventually_upper_of_ratio_limit line 71

   Source documentation

   The asymptotic slope of the forcing term gives the geometric-series slope for the recursively bounded sequence. This needs a limit only for g, not for f, and handles the natural-number rounding in n / d exactly.

   theorem eventually_upper_of_ratio_limit
       (f g : ℕ → ℝ) (d : ℕ) (hd : 2 ≤ d) (c : ℝ) (hc : 0 ≤ c)
       (hrec : ∀ᶠ n : ℕ in atTop, f n ≤ g n + f (n / d))
       (hlim : Tendsto (fun n : ℕ => g n / (n : ℝ)) atTop (nhds c))
       (ε : ℝ) (hε : 0 < ε) :
       ∀ᶠ n : ℕ in atTop,
         f n ≤ (c / (1 - 1 / (d : ℝ)) + ε) * (n : ℝ) := by
   …