OAI/NumberTheory/EgyptianFractions/FinitePowerSaving.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.finite_uniform_rpow_saving line 10

   Source documentation

   A finite collection of eventual power-saving estimates admits a single positive saving, coefficient, and threshold. Auxiliary parameters are left arbitrary, so an interval and a reciprocal-phase numerator can be included.

   theorem finite_uniform_rpow_saving {ι α : Type*} (s : Finset ι)
       (f : ι → ℝ → α → ℝ) (P : ι → ℝ → α → Prop) (p : ℝ)
       (h : ∀ i ∈ s, ∃ A δ : ℝ, 0 < A ∧ 0 < δ ∧ ∃ T : ℝ,
         ∀ U : ℝ, T ≤ U → ∀ z : α, P i U z → f i U z ≤ A * U ^ (p - δ)) :
       ∃ A δ : ℝ, 0 < A ∧ 0 < δ ∧ ∃ T : ℝ, 1 ≤ T ∧
         ∀ i ∈ s, ∀ U : ℝ, T ≤ U → ∀ z : α,
           P i U z → f i U z ≤ A * U ^ (p - δ) := by
   …

2. theorem OAI.Problem337.finite_derivative_order_power_saving line 54

   Source documentation

   Uniformisation over the bounded collection of derivative orders used for reciprocal phases. This also covers an empty order interval.

   theorem finite_derivative_order_power_saving {α : Type*} (Q : ℕ)
       (f : ℕ → ℝ → α → ℝ) (P : ℕ → ℝ → α → Prop)
       (h : ∀ k : ℕ, 4 ≤ k → k ≤ Q →
         ∃ A δ : ℝ, 0 < A ∧ 0 < δ ∧ ∃ T : ℝ,
           ∀ U : ℝ, T ≤ U → ∀ z : α, P k U z → f k U z ≤ A * U ^ (1 - δ)) :
       ∃ A δ : ℝ, 0 < A ∧ 0 < δ ∧ ∃ T : ℝ, 1 ≤ T ∧
         ∀ k : ℕ, 4 ≤ k → k ≤ Q → ∀ U : ℝ, T ≤ U → ∀ z : α,
           P k U z → f k U z ≤ A * U ^ (1 - δ) := by
   …