OriginalCommonCenter.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A common rational center from the original positive lift family

theorem OAI.Ostmann.eventual_original_commonCenter line 15

Source documentation

The scalar hypotheses of the finite common-center theorem have now been discharged at the original scales. The input probability is supplied by eventual_original_lift_probability.

theorem eventual_original_commonCenter (Cpop : ℝ) (hCpop : 500 ≤ Cpop) :
    ∀ᶠ T : ℝ in atTop, ∀ (P : Finset ℕ) (t : ℕ → ℤ) (k : ℕ) (K X : ℝ),
      ∀ hP : ∀ p ∈ P, p.Prime, (∀ p ∈ P, Real.exp T ≤ (p : ℝ)) →
      Real.exp T ≤ Cpop * T * P.card → (P.card : ℝ) ≤ Real.exp (T + 1) →
      10 ≤ k + 1 → 2 * (k + 1) ^ 2 ≤ P.card →
      ((k + 1 : ℕ) : ℝ) ≤ 2 * T ^ (3 / 5 : ℝ) →
      T ^ (9999999 / 10000000 : ℝ) / 1000 ≤ K → K ≤ T →
      1 ≤ X → X ≤ Real.exp (((k + 1 - 10 : ℕ) : ℝ) * T) →
      Real.exp (-K / 5) ≤ (Fintype.card (Fin (k + 1) ↪ P) : ℝ)⁻¹ *
        (tupleLiftFamily P (k + 1) ⌈Real.exp (13 * T / 100)⌉₊
          ⌈X * Real.exp (13 * T / 100)⌉₊ t).card →
      ∃ a ∈ Finset.Icc 1 ⌈Real.exp (13 * T / 100)⌉₊,
…

Mentions: OAI.Ostmann.tupleLiftFamily