OAI/NumberTheory/TotientAsymptotic/CollisionSlack.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.sum_a_Icc line 13
2. lemma OAI.TotientAsymptotic.gridded_weighted_slack line 24

   Source documentation

   Moving each surviving cutoff by at most e loses only e * sum a_k of the strict simplex slack. The weights are compared at the original indices.

   lemma gridded_weighted_slack (b J : ℕ) (j : ℕ → ℕ) (u ν : ℕ → ℝ)
       (B σ e : ℝ) (hB : 0 < B)
       (hj : Set.InjOn j (↑(Finset.Icc 1 b) : Set ℕ))
       (hidx : ∀ k ∈ Finset.Icc 1 b, k ≤ j k ∧ j k ≤ J)
       (hu : ∀ k ∈ Finset.Icc 1 J, 0 ≤ u k)
       (hslack : (∑ k ∈ Finset.Icc 1 J, a k*u k) ≤ (1-σ)*B)
       (hgrid : ∀ k ∈ Finset.Icc 1 b, ν k ≤ u (j k)/B+e) :
       (∑ k ∈ Finset.Icc 1 b, a k*ν k) ≤ 1-σ+e*(∑ k ∈ Finset.Icc 1 b, a k) := by
   …

   Mentions: OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.a

3. lemma OAI.TotientAsymptotic.comparisonError_le line 49
4. lemma OAI.TotientAsymptotic.comparisonExponent_le line 60
5. lemma OAI.TotientAsymptotic.comparison_log_power_saving line 72