TypicalEndpoints.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Few endpoints fail a positive prime test

The argument tests the uniform measure on the actual exceptional set. This turns the collision estimate for every large subset into a cardinality bound.

theorem OAI.Ostmann.weighted_real_sum_sq line 16
theorem OAI.Ostmann.weighted_mean_commute line 36
def OAI.Ostmann.badEndpoints line 43

theorem OAI.Ostmann.badEndpoints_card_lt line 49

Source documentation

No large subset can consist entirely of endpoints whose weighted mean is less than half the positive reference mean.

theorem badEndpoints_card_lt (A P : Finset ℕ) (w g : ℕ → ℝ)
    (f : ℕ → ℕ → ℝ) (δ E : ℝ) (K : ℕ) (hK : 0 < K) (hδ : 0 < δ)
    (hw : ∀ p ∈ P, 0 ≤ w p) (hmass : 0 < ∑ p ∈ P, w p)
    (href : δ * (∑ p ∈ P, w p) ≤ ∑ p ∈ P, w p * g p)
    (hsmall : 4 * E < δ ^ 2 * ∑ p ∈ P, w p)
    (htest : ∀ B ⊆ A, K ≤ B.card →
      (∑ p ∈ P, w p * (residueTestMean B (fun a => f a p) - g p) ^ 2) ≤ E) :
    (badEndpoints A P w f δ).card < K := by
…

Mentions: OAI.Ostmann.residueTestMean, OAI.Ostmann.badEndpoints

theorem OAI.Ostmann.simultaneous_good_endpoints line 86

Source documentation

Finitely many prime tests hold simultaneously after deleting at most the sum of their exceptional-set bounds.

theorem simultaneous_good_endpoints {ι : Type*} [DecidableEq ι]
    (E : Finset ℕ) (J : Finset ι) (bad : ι → Finset ℕ) (K : ℕ)
    (hbad : ∀ j ∈ J, (bad j).card ≤ K) :
    ∃ G ⊆ E, E.card ≤ G.card + J.card * K ∧
      ∀ a ∈ G, ∀ j ∈ J, a ∉ bad j := by
…