FiniteDesignationSum.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite designation catalogs may be indexed by numerical words of varying length.

lemma OAI.TwoPointCorrelations.designation_catalog_weight line 15

Source documentation

Each admissible designation set is a subset of all slots. The complete catalog therefore costs at most one binary choice per slot.

lemma designation_catalog_weight {I τ : Type*} [DecidableEq I] [Fintype τ]
    (F : Finset I) (allowed : I → Finset (Finset τ)) (weight : I → ℝ)
    (hw : ∀ i, 0 ≤ weight i) :
    (∑ a ∈ F.sigma allowed, weight a.1) ≤
      (2 : ℝ) ^ Fintype.card τ * ∑ i ∈ F, weight i := by
…

theorem OAI.TwoPointCorrelations.eventually_many_unlit_finsets line 31

Source documentation

The threshold is uniform in the finite catalog and in its index type. It can therefore be used for word lengths and prime pools varying with L.

theorem eventually_many_unlit_finsets (C : ℝ) (hC : 0 ≤ C) :
    ∀ᶠ L : ℝ in atTop, ∀ (I : Type) [DecidableEq I] (F : Finset I)
      (E : I → ℕ) (H : ℝ) (weight : I → ℝ),
      (∀ i ∈ F, 0 ≤ weight i) →
      (∑ i ∈ F, weight i) ≤ Real.exp (C * L * (Real.log L) ^ 2) →
      (∀ i ∈ F, L ^ (1 / 50 : ℝ) ≤ 2 * E i) →
      Real.exp (L ^ (199 / 200 : ℝ)) ≤ H →
      (∑ i ∈ F, weight i * (H⁻¹) ^ E i) ≤ Real.exp (-L ^ (101 / 100 : ℝ)) := by
…