PrescribedInversion.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.exists_positive_slack line 9

Source documentation

Slack in a reciprocal bound, including nonpositive slopes.

theorem exists_positive_slack {A c : ℝ} (hA : 0 < A) (hc : c < 1 / A) :
    ∃ ε : ℝ, 0 < ε ∧ c * (A + ε) < 1 := by
…

theorem OAI.Problem337.eventual_double_exp_lower_of_short_markers line 28

Source documentation

Abstract inversion of a short marked-expansion bound.

The hypotheses isolate the combinatorial work: finite initial intervals are eventually covered, marked expansions can be padded from length at least three, and large markers have asymptotically short expansions.

theorem eventual_double_exp_lower_of_short_markers
    (D : ℕ → Set ℕ) (v : ℕ → ℕ) (A : ℝ) (hA : 0 < A)
    (hmissing : ∀ k, 2 ≤ v k ∧ v k ∉ D k)
    (hsmall : ∀ M : ℕ, ∃ K : ℕ, ∀ k : ℕ, K ≤ k →
      ∀ m : ℕ, 2 ≤ m → m < M → m ∈ D k)
    (hpad : ∀ r k : ℕ, 3 ≤ r → r ≤ k → D r ⊆ D k)
    (hshort : ∀ ε : ℝ, 0 < ε → ∃ M : ℕ, 2 ≤ M ∧
      ∀ m : ℕ, M ≤ m → ∃ r : ℕ, 3 ≤ r ∧ m ∈ D r ∧
        (r : ℝ) ≤ (A + ε) * Real.log (Real.log (m : ℝ))) :
    ∀ c : ℝ, c < 1 / A → ∃ K : ℕ, ∀ k : ℕ, K ≤ k →
      Real.exp (Real.exp (c * (k : ℝ))) ≤ (v k : ℝ) := by
…

Mentions: OAI.Problem337.D, OAI.Problem337.v