lean_workbook_plus_34622
ProvedLet then ,\nwere if , if and if , then ..\nIt is easy to proof by induction.\nBut I don't calculate . These representation give expressions .\nBecause we get
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_34622 (x : ℝ)
(h₀ : x = 18 / 1991)
: ∃ (a : ℕ → ℕ),
∀ (k : ℕ),
(a k) = 0 ∨ (a k) = 1 ∨ (a k) = 2 ∧
∑' k : ℕ, (a k) / 3^k = x ∧
∑' k : ℕ, (a k) / 2^k = 5 / 128 := by sorrySource