SingletonDecay.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The selected singleton savings dominate the complete crude trace cost.

lemma OAI.TwoPointCorrelations.eventually_singleton_floor_bounds line 11

theorem OAI.TwoPointCorrelations.eventually_singleton_decay line 34

Source documentation

647/600 = 1/12 + 199/200 exceeds the desired exponent 21/20. All fixed coefficients in the enumeration affect only the threshold.

theorem eventually_singleton_decay (C : ℝ) (hC : 0 ≤ C) :
    ∀ᶠ L : ℝ in atTop, ∀ r : ℕ,
      L ^ (1 / 12 : ℝ) / 32 ≤ (r : ℝ) → (r : ℝ) ≤ L →
      Real.exp (C * L * (Real.log L) ^ 2) *
        (Real.exp (C * Real.log L - L ^ (199 / 200 : ℝ))) ^ r ≤
          Real.exp (-L ^ (21 / 20 : ℝ)) := by
…

lemma OAI.TwoPointCorrelations.progression_factor_le_exp line 74

Source documentation

The one-coordinate progression factor in exponential form.

lemma progression_factor_le_exp (N : ℕ) (H T D : ℝ)
    (hH : Real.exp T ≤ H) (hN : 2 + Real.log N ≤ Real.exp D) :
    H⁻¹ + (1 + Real.log N) / H ≤ Real.exp (D - T) := by
…

lemma OAI.TwoPointCorrelations.eventually_singleton_progression_factor line 88

Source documentation

The actual cutoffs N ≤ exp L and H ≥ exp(L^(199/200)) give a progression factor at most one for all sufficiently large L.

lemma eventually_singleton_progression_factor :
    ∀ᶠ L : ℝ in atTop, ∀ (N : ℕ) (H : ℝ), 1 ≤ N → (N : ℝ) ≤ Real.exp L →
      Real.exp (L ^ (199 / 200 : ℝ)) ≤ H →
      H⁻¹ + (1 + Real.log N) / H ≤ Real.exp (2 * Real.log L - L ^ (199 / 200 : ℝ)) ∧
        H⁻¹ + (1 + Real.log N) / H ≤ 1 := by
…

theorem OAI.TwoPointCorrelations.eventually_singleton_total line 119

Source documentation

Transfer the finite progression estimate to the same exponential scale. Its harmless numerator 2 + log N is kept explicitly.

theorem eventually_singleton_total (C : ℝ) (hC : 0 ≤ C) :
    ∀ᶠ L : ℝ in atTop, ∀ (r N : ℕ) (H cost total : ℝ),
      L ^ (1 / 12 : ℝ) / 32 ≤ (r : ℝ) → (r : ℝ) ≤ L →
      Real.exp (L ^ (199 / 200 : ℝ)) ≤ H →
      2 + Real.log N ≤ Real.exp (C * Real.log L) →
      0 ≤ cost → cost ≤ Real.exp (C * L * (Real.log L) ^ 2) →
      total ≤ cost * (H⁻¹ + (1 + Real.log N) / H) ^ r →
      total ≤ Real.exp (-L ^ (21 / 20 : ℝ)) := by
…