OAI/NumberTheory/EgyptianFractions/DeterministicPhaseWindow.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.deterministic_phase_window line 11

   Source documentation

   The dyadic pieces of a high residue level lie in the range where the uniform reciprocal-phase estimate applies.

   theorem deterministic_phase_window (S m D X U Z : ℝ)
       (hS : 0 ≤ S) (hSlarge : 10 * Real.log 2 ≤ S)
       (hm : m ≤ S) (hD : 255 ≤ D)
       (hXlower : Real.exp S ≤ X) (hXupper : X ≤ Real.exp (D * S / 4))
       (hUlower : Real.exp (-m / 10000) * X / 2 ≤ U) (hUupper : U ≤ X)
       (hZlower : Real.exp (D * S) ≤ |Z|)
       (hZupper : |Z| ≤ Real.exp ((2 * D + 102) * S)) :
       Real.exp (4 * S / 5) ≤ U ∧ U ^ 4 ≤ |Z| ∧ |Z| ≤ U ^ (3 * D) := by
   …

   Mentions: OAI.Problem337.D

2. theorem OAI.Problem337.power_saving_le_exponential line 51

   Source documentation

   A local power saving becomes a uniform exponential saving throughout the high-level dyadic window.

   theorem power_saving_le_exponential (S U A δ : ℝ)
       (hU : Real.exp (4 * S / 5) ≤ U) (hA : 0 ≤ A) (hδ : 0 ≤ δ) :
       A * U ^ (1 - δ) ≤ A * U * Real.exp (-(4 * δ * S / 5)) := by
   …

3. theorem OAI.Problem337.deterministic_frequency_bounds line 72

   Source documentation

   The frequency occurring in an off-diagonal prime-subset pair has the required exponential bounds. Distinctness, not primality, is needed here.

   theorem deterministic_frequency_bounds (S m D C l : ℝ) (t t' : ℕ)
       (hS : 0 ≤ S) (hm : m ≤ S) (hlower : 1 ≤ l)
       (hlupper : l ≤ Real.exp (m / 2500))
       (hClower : Real.exp (D * S) ≤ C) (hCupper : C ≤ Real.exp (2 * D * S))
       (ht : (t : ℝ) ≤ Real.exp (101 * S))
       (ht' : (t' : ℝ) ≤ Real.exp (101 * S)) (hne : t ≠ t') :
       Real.exp (D * S) ≤ |l * C * ((t : ℝ) - t')| ∧
         |l * C * ((t : ℝ) - t')| ≤ Real.exp ((2 * D + 102) * S) := by
   …

   Mentions: OAI.Problem337.D

4. theorem OAI.Problem337.deterministic_phase_sum_bound line 107

   Source documentation

   Summation over dyadic pieces preserves the uniform exponential saving.

   theorem deterministic_phase_sum_bound {E : Type*} [NormedAddCommGroup E]
       (f : ℕ → E) (Y X : ℕ) (S A δ : ℝ) (hY : 1 ≤ Y)
       (hA : 0 ≤ A) (hδ : 0 ≤ δ)
       (hYlarge : Real.exp (4 * S / 5) ≤ (Y : ℝ) / 2)
       (hlocal : ∀ U : ℕ, 0 < U → Y ≤ 2 * U → U ≤ X →
         ‖∑ n ∈ (Finset.Ico U (2 * U) ∩ Finset.Icc Y X), f n‖ ≤
           A * (U : ℝ) ^ (1 - δ)) :
       ‖∑ n ∈ Finset.Icc Y X, f n‖ ≤
         2 * A * (X : ℝ) * Real.exp (-(4 * δ * S / 5)) := by
   …