ManyUnlitDecay.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The extra reciprocal powers of many unlit occurrences beat every crude cost.

theorem OAI.TwoPointCorrelations.eventually_many_unlit_decay line 14

Source documentation

Here E is the number of extra reciprocal powers. The bound L^(1/50) ≤ 2E follows from the exact nonsingleton count.

theorem eventually_many_unlit_decay (C : ℝ) (hC : 0 ≤ C) :
    ∀ᶠ L : ℝ in atTop, ∀ (E : ℕ) (H : ℝ),
      L ^ (1 / 50 : ℝ) ≤ 2 * E → Real.exp (L ^ (199 / 200 : ℝ)) ≤ H →
      Real.exp (C * L * (Real.log L) ^ 2) * (H⁻¹) ^ E ≤
        Real.exp (-L ^ (101 / 100 : ℝ)) := by
…

theorem OAI.TwoPointCorrelations.eventually_many_unlit_total line 56

Source documentation

Transfer a finite designated-term estimate, with its complete crude weight retained, to the many-unlit negligible bound.

theorem eventually_many_unlit_total (C : ℝ) (hC : 0 ≤ C) :
    ∀ᶠ L : ℝ in atTop, ∀ (U E : ℕ) (H cost total : ℝ),
      L ^ (1 / 50 : ℝ) < U → U ≤ 2 * E →
      Real.exp (L ^ (199 / 200 : ℝ)) ≤ H →
      cost ≤ Real.exp (C * L * (Real.log L) ^ 2) →
      total ≤ cost * (H⁻¹) ^ E →
      total ≤ Real.exp (-L ^ (101 / 100 : ℝ)) := by
…