Stability.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The finite collision-stability inequality

This is the finite quantitative calculation in Lemma 2.5 of the manuscript. The final theorem takes the exact numerical consequences of Chebyshev's bound and Mertens' first theorem at the chosen cutoff as explicit hypotheses. No main theorem of the manuscript is assumed here.

def OAI.Ostmann.collisionDefect line 19
Source documentation
The three nonnegative terms in the collision stability estimate.
```
noncomputable def collisionDefect (p : ℕ) (s t : Finset ℕ) (μ ν : ℕ → ℝ) : ℝ :=
…
```
theorem OAI.Ostmann.collisionDefect_nonneg line 24
theorem OAI.Ostmann.collisionDefect_eq line 38

theorem OAI.Ostmann.weighted_collisionDefect_eq line 49

Source documentation

The sum of stability defects is the sum of the collision energies minus the universal baseline 4 ∑ log p / p.

theorem weighted_collisionDefect_eq (P : Finset ℕ) (s t : ℕ → Finset ℕ)
    (μ ν : ℕ → ℕ → ℝ)
    (hs : ∀ p ∈ P, (s p).Nonempty) (ht : ∀ p ∈ P, (t p).Nonempty)
    (hμ : ∀ p ∈ P, ∑ r ∈ s p, μ p r = 1)
    (hν : ∀ p ∈ P, ∑ r ∈ t p, ν p r = 1) :
    (∑ p ∈ P, Real.log (p : ℝ) * collisionDefect p (s p) (t p) (μ p) (ν p)) =
      (∑ p ∈ P, Real.log (p : ℝ) * ∑ r ∈ s p, μ p r ^ 2) +
      (∑ p ∈ P, Real.log (p : ℝ) * ∑ r ∈ t p, ν p r ^ 2) -
      4 * ∑ p ∈ P, Real.log (p : ℝ) / (p : ℝ) := by
…

Mentions: OAI.Ostmann.collisionDefect

theorem OAI.Ostmann.collision_stability_of_prime_sums line 75

Source documentation

A finite, explicit form of collision stability. The two energy bounds come from residue_collision_bound; the last two hypotheses are exactly the prime-sum estimates needed at the cutoff, rather than full asymptotic theories. Mertens' first theorem (1874) supplies the lower prime sum.

theorem collision_stability_of_prime_sums (P : Finset ℕ)
    (s t : ℕ → Finset ℕ) (μ ν : ℕ → ℕ → ℝ)
    (X Q : ℕ) (m K C : ℝ)
    (hs : ∀ p ∈ P, (s p).Nonempty) (ht : ∀ p ∈ P, (t p).Nonempty)
    (hμ : ∀ p ∈ P, ∑ r ∈ s p, μ p r = 1)
    (hν : ∀ p ∈ P, ∑ r ∈ t p, ν p r = 1)
    (hm : 0 ≤ m)
    (henergyμ : (∑ p ∈ P, Real.log (p : ℝ) * ∑ r ∈ s p, μ p r ^ 2) ≤
      Real.log (X : ℝ) + m * ∑ p ∈ P, Real.log (p : ℝ))
    (henergyν : (∑ p ∈ P, Real.log (p : ℝ) * ∑ r ∈ t p, ν p r ^ 2) ≤
      Real.log (X : ℝ) + m * ∑ p ∈ P, Real.log (p : ℝ))
    (hchebyshev : (∑ p ∈ P, Real.log (p : ℝ)) ≤ K * Q)
…

theorem OAI.Ostmann.finite_measure_collision_stability line 99

Source documentation

Apply the stability inequality to two actual finite measures on integers. The maps f and g label their residue classes; allowing a relabeling is needed for the negative second summand. The prime-sum hypotheses are the finite specializations of the published inputs used here.

theorem finite_measure_collision_stability (P A B : Finset ℕ)
    (μ ν : ℕ → ℝ) (s t : ℕ → Finset ℕ) (f g : ℕ → ℕ → ℕ)
    (X Q : ℕ) (m K C : ℝ)
    (hX : 1 ≤ X) (hP : ∀ p ∈ P, p.Prime)
    (hA : ∀ a ∈ A, a ≤ X) (hB : ∀ b ∈ B, b ≤ X)
    (hμ : ∀ a ∈ A, 0 ≤ μ a) (hν : ∀ b ∈ B, 0 ≤ ν b)
    (hmassμ : ∑ a ∈ A, μ a = 1) (hmassν : ∑ b ∈ B, ν b = 1)
    (hatomμ : ∀ a ∈ A, μ a ≤ m) (hatomν : ∀ b ∈ B, ν b ≤ m)
    (hs : ∀ p ∈ P, (s p).Nonempty) (ht : ∀ p ∈ P, (t p).Nonempty)
    (hf : ∀ p ∈ P, ∀ a ∈ A, f p a ∈ s p)
    (hg : ∀ p ∈ P, ∀ b ∈ B, g p b ∈ t p)
    (hcongrf : ∀ p ∈ P, ∀ a ∈ A, ∀ b ∈ A, f p a = f p b ↔ a ≡ b [MOD p])
…