OAI/NumberTheory/EgyptianFractions/ResidueRegimeSplice.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem337.GeometricDensity.residueData_of_two_lists line 15

   Source documentation

   Combine the deterministic and sampled lists according to the level cutoff. The index set is kept fixed, so repeated sampled products retain their full multiplicity. The same choice also changes the auxiliary factor from C to 1. The shifted moment input is uniform over all positive divisors of the common denominator; no moment assumption about the chosen list is added.

   def residueData_of_two_lists
       {DM D₀ η c r S loss : ℝ} {C M : ℕ}
       (I : Finset ℕ) (hI : I.Nonempty) (t₀ t₁ : ℕ → ℕ)
       (hpos₀ : ∀ i ∈ I, 0 < t₀ i) (hpos₁ : ∀ i ∈ I, 0 < t₁ i)
       (hdvd₀ : ∀ i ∈ I, t₀ i ∣ M) (hdvd₁ : ∀ i ∈ I, t₁ i ∣ M)
       (E₀ E₁ : ℕ → Finset ℕ)
       (hcount₀ : ∀ j < depth DM η S, Real.exp S < cutoff DM η S j →
         ∀ u ∈ Finset.Icc 1 ⌊cutoff DM η S j⌋₊, u ∉ E₀ j →
           cutoff DM η S (j + 1) < (u : ℝ) →
           contraction η S * (I.card : ℝ) / loss ≤
             ((I.filter (fun i => Int.fract (-((C * t₀ i : ℕ) : ℝ) / u) <
               contraction η S)).card : ℝ))
   …

   Mentions: OAI.Problem337.GeometricDensity.depth, OAI.Problem337.GeometricDensity.cutoff, OAI.Problem337.GeometricDensity.contraction