noncomputable def Misc.Seq1.seq₁ : ℕ → ℕ

Equations

• Misc.Seq1.seq₁ = Classical.epsilon fun (a : ℕ → ℕ) => a 0 = 1 ∧ ∀ (n : ℕ), n ≠ 0 → a n = (List.filter (fun (x : ℕ) => decide ¬n ∣ x) (List.map a (List.range n))).sum

noncomputable def Misc.Seq1.N₁ : ℕ

Equations

• Misc.Seq1.N₁ = Misc.Seq1.seq₁ (Nat.find! fun (i : ℕ) => have n := Misc.Seq1.seq₁ i; 0 < n ∧ ∀ (k : ℕ), 2 ^ k ≠ n)

@[irreducible]

def Misc.Seq1.seq₁Comp (n : ℕ) : ℕ

Equations

• Misc.Seq1.seq₁Comp n = if n = 0 then 1 else (List.filter (fun (x : ℕ) => decide ¬n ∣ x) (List.map (fun (x : { x : ℕ // x ∈ List.range n }) => Misc.Seq1.seq₁Comp ↑x) (List.range n).attach)).sum

def Misc.Seq1.N₁Comp : ℕ

Equations

• Misc.Seq1.N₁Comp = 72

@[simp]

theorem Misc.Seq1.seq₁Comp_zero : seq₁Comp 0 = 1

@[simp]

theorem Misc.Seq1.seq₁Comp_eq_seq₁ : seq₁Comp = seq₁

@[csimp]

theorem Misc.Seq1.seq₁_eq_seq₁Comp : seq₁ = seq₁Comp

theorem Misc.Seq1.map_seq₁_range_10 : List.map seq₁ (List.range 10) = [1, 0, 1, 2, 4, 8, 16, 32, 8, 72]

@[simp]

theorem Misc.Seq1.seq₁_9 : seq₁ 9 = 72

@[simp]

theorem Misc.Seq1.N₁Comp_eq : N₁Comp = 72

@[simp]

theorem Misc.Seq1.N₁_eq : N₁ = 72

@[csimp]

theorem Misc.Seq1.N₁_eq_N₁Comp : N₁ = N₁Comp