CollisionAlgebra.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Cancellation and the strict-slack comparison for the surviving prime indices.

lemma OAI.TotientAsymptotic.log_le_a line 12
lemma OAI.TotientAsymptotic.a_monotone_positive line 21

theorem OAI.TotientAsymptotic.cancel_equal_shifts line 29

Source documentation

Deleting matching primes cancels exactly their shifts, retaining all multiplicity in the residual integer.

theorem cancel_equal_shifts {ι : Type*} [DecidableEq ι]
    (I : Finset ι) (p q : ι → ℕ) (D D' : ℕ)
    (hp : ∀ i ∈ I, 2 ≤ p i)
    (hprod : D*(∏ i ∈ I, (p i-1)) = D'*(∏ i ∈ I, (q i-1))) :
    D*(∏ i ∈ I.filter (fun i => p i ≠ q i), (p i-1)) =
      D'*(∏ i ∈ I.filter (fun i => p i ≠ q i), (q i-1)) := by
…

Mentions: OAI.TotientAsymptotic.D

theorem OAI.TotientAsymptotic.reindexed_slack_sum_le line 58

Source documentation

Removing matched indices and renumbering the survivors cannot increase the renewal-weighted sum. This is the monotonicity step in collision-slack.

theorem reindexed_slack_sum_le (b J : ℕ) (j : ℕ → ℕ) (u : ℕ → ℝ)
    (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) :
    (∑ k ∈ Finset.Icc 1 b, a k*u (j k)) ≤ ∑ k ∈ Finset.Icc 1 J, a k*u k := by
…

Mentions: OAI.TotientAsymptotic.a