OAI/NumberTheory/EgyptianFractions/DeterministicReciprocal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem337.sum_nat_interval_eq_int line 11

   Source documentation

   The natural and integer closed interval sums agree under the canonical cast.

   lemma sum_nat_interval_eq_int (f : ℤ → ℂ) (L R : ℕ) :
       (∑ n ∈ Finset.Icc L R, f n) = ∑ n ∈ Finset.Icc (L : ℤ) (R : ℤ), f n := by
   …

2. lemma OAI.Problem337.reciprocal_sum_dyadic_piece line 29

   Source documentation

   Integer-interval reciprocal cancellation in a natural dyadic piece.

   lemma reciprocal_sum_dyadic_piece (A δ U Z : ℝ) (u L R : ℕ)
       (hu : 0 < u) (hU : U = (u : ℝ))
       (hlocal : ∀ L R : ℤ, U ≤ (L : ℝ) → (R : ℝ) ≤ 2 * U →
         ‖∑ n ∈ Finset.Icc L R, differencingPhase (Z / (n : ℝ))‖ ≤ A * U ^ (1 - δ)) :
       ‖∑ n ∈ (Finset.Ico u (2 * u) ∩ Finset.Icc L R),
         differencingPhase (Z / (n : ℝ))‖ ≤ A * U ^ (1 - δ) := by
   …

   Mentions: OAI.Problem337.differencingPhase

3. theorem OAI.Problem337.deterministic_reciprocal_sum_bound line 55

   Source documentation

   The local reciprocal-phase theorem gives a uniform exponential saving over an entire high residue level. The denominator range and local frequency range are explicit, and no cancellation hypothesis remains.

   theorem deterministic_reciprocal_sum_bound (D : ℝ) (hD : 255 ≤ D) :
       ∃ A c : ℝ, 0 < A ∧ 0 < c ∧
         ∀ᶠ S : ℝ in atTop, ∀ (m X Z : ℝ) (L R : ℕ),
           m ≤ S → Real.exp S ≤ X → X ≤ Real.exp (D * S / 4) →
           Real.exp (-m / 10000) * X ≤ (L : ℝ) → (R : ℝ) ≤ X →
           Real.exp (D * S) ≤ |Z| → |Z| ≤ Real.exp ((2 * D + 102) * S) →
           ‖∑ n ∈ Finset.Icc L R, differencingPhase (Z / (n : ℝ))‖ ≤
             A * X * Real.exp (-c * S) := by
   …

   Mentions: OAI.Problem337.D, OAI.Problem337.differencingPhase