OAI/NumberTheory/EgyptianFractions/DeterministicMean.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.finite_second_moment_cutoff line 12

   Source documentation

   A version of the finite second moment normalized by an arbitrary upper cutoff, valid also when the ambient integer interval is empty.

   theorem finite_second_moment_cutoff {α β : Type*}
       (U : Finset α) (T : Finset β) (z : α → β → ℂ) (X E : ℝ)
       (hT : T.Nonempty) (hX : 0 ≤ X) (hE : 0 ≤ E) (hU : (U.card : ℝ) ≤ X)
       (hunit : ∀ u ∈ U, ∀ t ∈ T, ‖z u t‖ = 1)
       (hcorr : ∀ t ∈ T, ∀ s ∈ T, t ≠ s →
         ‖∑ u ∈ U, z u t * conj (z u s)‖ ≤ X * E) :
       (∑ u ∈ U, ‖(∑ t ∈ T, z u t) / (T.card : ℂ)‖ ^ 2) ≤
         X * (1 / (T.card : ℝ) + E) := by
   …

2. theorem OAI.Problem337.deterministic_mean_two_errors line 41

   Source documentation

   The full deterministic high-level second moment, with its two explicit error terms. Distinctness of the indexed natural entries is the only arithmetic property used in the off-diagonal estimate.

   theorem deterministic_mean_two_errors (D : ℝ) (hD : 255 ≤ D) :
       ∃ A c : ℝ, 0 < A ∧ 0 < c ∧
         ∀ᶠ S : ℝ in atTop, ∀ (m X C ell : ℝ),
           m ≤ S → Real.exp S ≤ X → X ≤ Real.exp (D * S / 4) →
           Real.exp (D * S) ≤ C → C ≤ Real.exp (2 * D * S) →
           1 ≤ ell → ell ≤ Real.exp (m / 2500) →
           ∀ {β : Type*} (T : Finset β) (t : β → ℕ),
             Set.InjOn t (T : Set β) →
             Real.exp (Real.log 2 * m) ≤ (T.card : ℝ) →
             (∀ i ∈ T, (t i : ℝ) ≤ Real.exp (101 * S)) →
             (∑ u ∈ Finset.Icc (⌊Real.exp (-m / 10000) * X⌋₊ + 1) ⌊X⌋₊,
               ‖(∑ i ∈ T, differencingPhase (ell * C * (t i : ℝ) / (u : ℝ))) /
   …

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