OAI/NumberTheory/EgyptianFractions/DeterministicSubsetMean.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.subsetEntry_le_exp_of_power_pool line 13

   Source documentation

   All entries of the canonical deterministic binary block have the right size for the high-level reciprocal-phase theorem.

   theorem subsetEntry_le_exp_of_power_pool {S : ℝ} (hS : 1 < S)
       {m : ℕ} (hm : (m : ℝ) ≤ S / Real.log S) (p : Fin m → ℕ)
       (hp : ∀ j, (p j).Prime) (hsize : ∀ j, (p j : ℝ) ≤ S ^ (101 : ℕ))
       (I : Fin m → Fin 2) :
       (ResidueConstruction.subsetEntry p I : ℝ) ≤ Real.exp (101 * S) := by
   …

   Mentions: OAI.Problem337.ResidueConstruction.subsetEntry

2. theorem OAI.Problem337.deterministic_subset_mean_two_errors line 37

   Source documentation

   The unconditional deterministic second moment specialized to the actual prime-subset block. Its exact 2^m normalization and distinctness are proved, rather than left as hypotheses for the residue-family assembler.

   theorem deterministic_subset_mean_two_errors (D : ℝ) (hD : 255 ≤ D) :
       ∃ A c : ℝ, 0 < A ∧ 0 < c ∧
         ∀ᶠ S : ℝ in atTop, ∀ (m : ℕ) (X C ell : ℝ),
           (m : ℝ) ≤ S / Real.log 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) →
           ∀ p : Fin m → ℕ, (∀ j, (p j).Prime) → Function.Injective p →
             (∀ j, (p j : ℝ) ≤ S ^ (101 : ℕ)) →
             (∑ u ∈ Finset.Icc (⌊Real.exp (-(m : ℝ) / 10000) * X⌋₊ + 1) ⌊X⌋₊,
               ‖(∑ I : Fin m → Fin 2,
                   differencingPhase (ell * C * (ResidueConstruction.subsetEntry p I : ℝ) /
   …

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

3. theorem OAI.Problem337.eventually_deterministic_subset_mean line 72

   Source documentation

   The high-level deterministic moment estimate for the actual binary prime-product block, with the manuscript's final exponential rate.

   theorem eventually_deterministic_subset_mean (D : ℝ) (hD : 255 ≤ D) :
       ∀ᶠ S : ℝ in atTop, ∀ (m : ℕ) (X C ell : ℝ),
         S / (2 * Real.log S) ≤ (m : ℝ) → (m : ℝ) ≤ S / Real.log 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) →
         ∀ p : Fin m → ℕ, (∀ j, (p j).Prime) → Function.Injective p →
           (∀ j, (p j : ℝ) ≤ S ^ (101 : ℕ)) →
           (∑ u ∈ Finset.Icc (⌊Real.exp (-(m : ℝ) / 10000) * X⌋₊ + 1) ⌊X⌋₊,
             ‖(∑ I : Fin m → Fin 2,
                 differencingPhase (ell * C * (ResidueConstruction.subsetEntry p I : ℝ) /
                   (u : ℝ))) / (2 : ℂ) ^ m‖ ^ 2) ≤
   …

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