ManyUnlitCatalog.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Sum a finite actual designation catalog with varying extra reciprocal exponents.

theorem OAI.TwoPointCorrelations.eventually_many_unlit_catalog line 13

theorem OAI.TwoPointCorrelations.eventually_many_unlit_designations line 39

Source documentation

The input is the literal unlit set in each word's nonsingleton expansion. The exponent is derived from those occurrences internally.

theorem eventually_many_unlit_designations {I ι τ : Type*}
    [Fintype I] [Fintype ι] [Fintype τ] [DecidableEq ι]
    (C : ℝ) (hC : 0 ≤ C) :
    ∀ᶠ L : ℝ in atTop, ∀ (label : I → τ → ι) (U : I → Finset τ)
      (H : ℝ) (weight : I → ℝ),
      (∀ i, U i ⊆ nonsingletonSlots (label i)) →
      (∀ i, L ^ (1 / 50 : ℝ) < (U i).card) →
      (∀ i, 0 ≤ weight i) →
      (∑ i, weight i) ≤ Real.exp (C * L * (Real.log L) ^ 2) →
      Real.exp (L ^ (199 / 200 : ℝ)) ≤ H →
      (∑ i, weight i * (H⁻¹) ^
        (∑ a ∈ nonsingletonLabels (label i),
…

Mentions: OAI.TwoPointCorrelations.nonsingletonSlots, OAI.TwoPointCorrelations.nonsingletonLabels