FavorableBlockEndpoint.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

An integral endpoint chosen after the favorable logarithmic block

theorem OAI.Ostmann.eventual_favorable_block_endpoint line 13

Source documentation

Rounding the endpoint up changes its logarithm by at most one. The reserve in the block leaves every giant-cell prime below the collision cutoff.

theorem eventual_favorable_block_endpoint (k : ℕ) :
    ∀ᶠ L : ℝ in atTop, ∀ lo : ℝ,
      Real.exp ((5 / 100 : ℝ) * L) ≤ lo → lo ≤ Real.exp ((9 / 10 : ℝ) * L) →
      ∃ Y : ℝ, ∃ hi : ℕ, (hi : ℝ) = Real.exp Y ∧
        2 * lo + 2 ^ (k + 1) * (12 * Real.exp ((1 / 100 : ℝ) * L)) ≤ Y ∧
        Y ≤ 2 * lo + 2 ^ (k + 1) * (12 * Real.exp ((1 / 100 : ℝ) * L)) + 1 ∧
        Real.exp ((4 / 100 : ℝ) * L) ≤ Y ∧ Y ≤ Real.exp L ∧
        ⌈Real.exp (lo + 10 * Real.exp ((1 / 100 : ℝ) * L) + 3)⌉₊ ≤
          tailCollisionCutoff Y := by
…

Mentions: OAI.Ostmann.tailCollisionCutoff