OAI/NumberTheory/EgyptianFractions/GeometricHighResidues.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.GeometricDensity.mem_high_residue_interval line 13

   Source documentation

   The open lower cutoff of a geometric level is precisely the natural interval required by deterministic residue localization.

   theorem mem_high_residue_interval {DM S : ℝ} {j u : ℕ}
       (hu : u ∈ Finset.Icc 1 ⌊cutoff DM (1 / 10000) S j⌋₊)
       (hnext : cutoff DM (1 / 10000) S (j + 1) < (u : ℝ)) :
       u ∈ Finset.Icc
         (⌊Real.exp (-(ResidueLevels.scale S : ℝ) / 10000) *
           cutoff DM (1 / 10000) S j⌋₊ + 1)
         ⌊cutoff DM (1 / 10000) S j⌋₊ := by
   …

   Mentions: OAI.Problem337.GeometricDensity.cutoff, OAI.Problem337.ResidueLevels.scale

2. theorem OAI.Problem337.GeometricDensity.eventually_high_geometric_subset_residues line 37

   Source documentation

   The actual deterministic block supplies all high geometric levels at one common onset, with a single exceptional-set function. No Fourier estimate or cutoff-window hypothesis is left to the final arithmetic assembly.

   theorem eventually_high_geometric_subset_residues
       (DM : ℝ) (hDM : 255 ≤ 4 * (DM + 2)) :
       ∀ᶠ S : ℝ in atTop, ∀ C : ℕ,
         Real.exp (4 * (DM + 2) * S) ≤ (C : ℝ) →
         (C : ℝ) ≤ Real.exp (2 * (4 * (DM + 2)) * S) →
         ∀ p : Fin (ResidueLevels.scale S) → ℕ,
           (∀ i, (p i).Prime) → Function.Injective p →
           (∀ i, (p i : ℝ) ≤ S ^ (101 : ℕ)) →
           ∃ E : ℕ → Finset ℕ, ∀ j : ℕ,
             Real.exp S < cutoff DM (1 / 10000) S j →
             ((E j).card : ℝ) ≤ cutoff DM (1 / 10000) S j *
                 Real.exp (-(ResidueLevels.scale S : ℝ) / 1000) ∧
   …

   Mentions: OAI.Problem337.ResidueLevels.scale, OAI.Problem337.GeometricDensity.cutoff