CommonCenterProbability.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Common-center extraction directly from the original lift probability

theorem OAI.Ostmann.pow_le_twice_descFactorial line 13

theorem OAI.Ostmann.exists_commonCenter_of_lift_probability line 23

Source documentation

All combinatorial moments are computed from actual congruence lifts. The remaining assumptions are explicit scalar inequalities.

theorem exists_commonCenter_of_lift_probability (P : Finset ℕ)
    (t : ℕ → ℤ) (k d K H Z Amax : ℕ) (hd : d ≤ k + 1)
    (A V ρ : ℝ) (hA : 0 < A) (hV : 0 < V) (hρ : 0 < ρ)
    (hZ : 0 < Z) (hAmax : 0 < Amax)
    (hprime : ∀ p ∈ P, p.Prime) (hap : ∀ p ∈ P, Amax < p)
    (hmin : ∀ p ∈ P, Z ≤ p) (hlog : ∀ p ∈ P, V ≤ Real.log (p : ℝ))
    (hbudget : Real.log (2 * (H : ℝ)) < (K + 1 : ℕ) * V)
    (hsmall : 2 * K * (P.card : ℝ) ≤ A ^ 2)
    (hsize : 2 * (k + 1) ^ 2 ≤ P.card)
    (hprob : ρ ≤ (Fintype.card (Fin (k + 1) ↪ P) : ℝ)⁻¹ *
      (tupleLiftFamily P (k + 1) Amax H t).card)
    (hdiscard : A ^ d * liftMomentUpper P.card (k + 1 - d) H Z ≤
…

Mentions: OAI.Ostmann.tupleLiftFamily, OAI.Ostmann.liftMomentUpper