PrescribedCorollary.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.prescribed_lower_of_marked line 15

Source documentation

The combinatorial hypotheses of the prescribed-denominator corollary imply all its eventual double-exponential lower bounds.

theorem prescribed_lower_of_marked
    (padding : ∀ r : ℕ, 3 ≤ r → ∀ n : Fin r → ℕ, IsOneExpansion n →
      ∀ m : ℕ, (∃ i : Fin r, n i = m) →
        ∃ n' : Fin (r + 1) → ℕ,
          IsOneExpansion n' ∧ ∃ i : Fin (r + 1), n' i = m)
    (occurs : ∀ m : ℕ, 2 ≤ m → ∃ k : ℕ, m ∈ D k)
    (short : ∀ ε : ℝ, 0 < ε → ∃ M : ℕ, 2 ≤ M ∧
      ∀ m : ℕ, M ≤ m → ∃ k : ℕ, ∃ n : Fin k → ℕ,
        IsOneExpansion n ∧ (∃ i : Fin k, n i = m) ∧
          (k : ℝ) ≤ (257 / Real.log 2 + ε) * Real.log (Real.log (m : ℝ)))
    (missing : ∀ k : ℕ, 2 ≤ v k ∧ v k ∉ D k) :
    ∀ c : ℝ, c < Real.log 2 / 257 → ∃ K : ℕ,
…

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

theorem OAI.Problem337.prescribed_denominator_corollary_of_inputs line 52

Source documentation

Full assembly of the prescribed-denominator consequence, conditional only on its exact combinatorial construction and elementary denominator inputs.

theorem prescribed_denominator_corollary_of_inputs
    (padding : ∀ r : ℕ, 3 ≤ r → ∀ n : Fin r → ℕ, IsOneExpansion n →
      ∀ m : ℕ, (∃ i : Fin r, n i = m) →
        ∃ n' : Fin (r + 1) → ℕ,
          IsOneExpansion n' ∧ ∃ i : Fin (r + 1), n' i = m)
    (occurs : ∀ m : ℕ, 2 ≤ m → ∃ k : ℕ, m ∈ D k)
    (short : ∀ ε : ℝ, 0 < ε → ∃ M : ℕ, 2 ≤ M ∧
      ∀ m : ℕ, M ≤ m → ∃ k : ℕ, ∃ n : Fin k → ℕ,
        IsOneExpansion n ∧ (∃ i : Fin k, n i = m) ∧
          (k : ℝ) ≤ (257 / Real.log 2 + ε) * Real.log (Real.log (m : ℝ)))
    (missing : ∀ k : ℕ, 2 ≤ v k ∧ v k ∉ D k)
    (upper : ∀ k : ℕ, 1 ≤ k → v k ≤ 1 + k ^ (2 ^ (k - 1))) :
…

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