Documentation

Oeis.FibonacciUnionsMinkowskiSums

@[reducible, inline]

abbrev FibonacciMinkowski.Point :

Equations

FibonacciMinkowski.Point = (ℤ × ℤ)

Instances For

def FibonacciMinkowski.xy :

ℕ → Finset Point × Finset Point

The pair (xₙ,yₙ) from the document.

Equations

FibonacciMinkowski.xy 0 = ({(1, 0)}, {(0, 1)})
FibonacciMinkowski.xy n.succ = ((FibonacciMinkowski.xy n).1 ∪ (FibonacciMinkowski.xy n).2, (FibonacciMinkowski.xy n).1 + (FibonacciMinkowski.xy n).2)

Instances For

def FibonacciMinkowski.env (n : ℕ) (v : ℤ) :

The lower envelope Eₙ(v). For n < 2, the second branch is a harmless junk value, as prescribed in the document.

Equations

FibonacciMinkowski.env n v = if h : (Finset.range (n - 1)).Nonempty then (Finset.range (n - 1)).inf' h fun (k : ℕ) => (↑n - 1 - ↑k) * v + ↑(Nat.fib (k + 3)) else v + 2

Instances For

theorem FibonacciMinkowski.lam_exists (n : ℕ) (d : ℤ) :

∃ (j : ℕ), d ≤ env n (1 + ↑j)

theorem FibonacciMinkowski.env_mono_strong (n : ℕ) (hn : 2 ≤ n) (v' v : ℤ) (hvv : v' ≤ v) :

env n v' + (v - v') ≤ env n v

theorem FibonacciMinkowski.env_eq_line (n k : ℕ) (v : ℤ) (hn : 2 ≤ n) (hk : k ≤ n - 2) (hl : ↑(Nat.fib (k + 1)) ≤ v) (hu : v ≤ ↑(Nat.fib (k + 2))) :

env n v = (↑n - 1 - ↑k) * v + ↑(Nat.fib (k + 3))

theorem FibonacciMinkowski.env_one (n : ℕ) (hn : 2 ≤ n) :

env n 1 = ↑n + 1

theorem FibonacciMinkowski.env_fib (n : ℕ) (hn : 2 ≤ n) :

env n ↑(Nat.fib n) = ↑(Nat.fib (n + 2))

def FibonacciMinkowski.lam (n : ℕ) (d : ℤ) :

The lower profile λₙ(d), defined as the least positive integer whose image under env n is at least d.

Equations

FibonacciMinkowski.lam n d = 1 + ↑(Nat.find ⋯)

Instances For

theorem FibonacciMinkowski.lam_galois (n : ℕ) (hn : 2 ≤ n) (d v : ℤ) (hv : 1 ≤ v) :

lam n d ≤ v ↔ d ≤ env n v

theorem FibonacciMinkowski.lam_ge_one (n : ℕ) (d : ℤ) :

1 ≤ lam n d

theorem FibonacciMinkowski.lam_le_fib_iff (n : ℕ) (hn : 2 ≤ n) (d : ℤ) :

lam n d ≤ ↑(Nat.fib n) ↔ d ≤ ↑(Nat.fib (n + 2))

theorem FibonacciMinkowski.env_shift_low (n : ℕ) (hn : 2 ≤ n) (u : ℤ) (hu1 : 1 ≤ u) (hu2 : u ≤ ↑(Nat.fib n)) :

env (n + 1) u = env n u + u

theorem FibonacciMinkowski.env_shift_high (n : ℕ) (hn : 2 ≤ n) (u : ℤ) (hu1 : ↑(Nat.fib n) ≤ u) (hu2 : u ≤ ↑(Nat.fib (n + 1))) :

env (n + 1) u = u + ↑(Nat.fib (n + 2))

theorem FibonacciMinkowski.lam_eq_one_iff (n : ℕ) (hn : 2 ≤ n) (d : ℤ) :

lam n d = 1 ↔ d ≤ ↑n + 1

theorem FibonacciMinkowski.lam_half (n : ℕ) (hn : 2 ≤ n) (d : ℤ) (hlo : ↑n + 1 ≤ d) (hhi : d ≤ ↑(Nat.fib (n + 2))) :

2 * lam n d ≤ d

def FibonacciMinkowski.mu (n : ℕ) (d : ℤ) :

The upper profile μₙ(d).

Equations

FibonacciMinkowski.mu n d = if d ≤ 1 then 0 else FibonacciMinkowski.lam (n - 1) (max d ↑n)

Instances For

theorem FibonacciMinkowski.mu_values (n : ℕ) (hn : 3 ≤ n) (d : ℤ) :

(d ≤ 1 → mu n d = 0) ∧ (2 ≤ d → d ≤ ↑n → mu n d = 1) ∧ (↑n ≤ d → mu n d = lam (n - 1) d)

theorem FibonacciMinkowski.mu_galois (n : ℕ) (hn : 3 ≤ n) (d v : ℤ) (hv : 1 ≤ v) :

mu n d ≤ v ↔ d ≤ env (n - 1) v

theorem FibonacciMinkowski.mu_nonneg (n : ℕ) (d : ℤ) :

0 ≤ mu n d

theorem FibonacciMinkowski.mu_ge_one (n : ℕ) (hn : 3 ≤ n) (d : ℤ) (hd : 2 ≤ d) :

1 ≤ mu n d

theorem FibonacciMinkowski.mu_half (n : ℕ) (hn : 3 ≤ n) (d : ℤ) (hlo : 1 ≤ d) (hhi : d ≤ ↑(Nat.fib (n + 1))) :

2 * mu n d ≤ d

noncomputable def FibonacciMinkowski.fiberSet (s t : ℤ) (L : ℤ → ℤ) :

A finite staircase set, presented as a disjoint union of diagonal fibers.

Equations

FibonacciMinkowski.fiberSet s t L = (Finset.Icc s t).biUnion fun (d : ℤ) => Finset.image (fun (a : ℤ) => (a, d - a)) (Finset.Icc (L d) (d - L d))

Instances For

theorem FibonacciMinkowski.structure_base :

(xy 3).1 = fiberSet 1 (↑(Nat.fib 4)) (mu 3) ∧ (xy 3).2 = fiberSet 4 (↑(Nat.fib 5)) (lam 3)

theorem FibonacciMinkowski.fiber_union_step (n : ℕ) (hn : 3 ≤ n) :

fiberSet 1 (↑(Nat.fib (n + 1))) (mu n) ∪ fiberSet (↑n + 1) (↑(Nat.fib (n + 2))) (lam n) = fiberSet 1 (↑(Nat.fib (n + 2))) (mu (n + 1))

theorem FibonacciMinkowski.profile_superadd (n : ℕ) (hn : 3 ≤ n) (d d' : ℤ) (hd1 : 1 ≤ d) (hd2 : d ≤ ↑(Nat.fib (n + 1))) (hd'1 : ↑n + 1 ≤ d') (hd'2 : d' ≤ ↑(Nat.fib (n + 2))) :

d + d' ≤ env (n + 1) (mu n d + lam n d')

theorem FibonacciMinkowski.fib_group_index (n : ℕ) (hn : 3 ≤ n) (w : ℤ) (hw1 : 3 ≤ w) (hw2 : w ≤ ↑(Nat.fib (n + 1))) :

∃ (k : ℕ), 2 ≤ k ∧ k ≤ n - 1 ∧ ↑(Nat.fib (k + 1)) ≤ w ∧ w ≤ ↑(Nat.fib (k + 2))

theorem FibonacciMinkowski.diagonal_witness_one (n : ℕ) (hn : 3 ≤ n) (e : ℤ) (he1 : ↑n + 2 ≤ e) (hw : lam (n + 1) e = 1) :

∃ (d : ℤ) (d' : ℤ), 1 ≤ d ∧ d ≤ ↑(Nat.fib (n + 1)) ∧ ↑n + 1 ≤ d' ∧ d' ≤ ↑(Nat.fib (n + 2)) ∧ d + d' = e ∧ mu n d + lam n d' ≤ lam (n + 1) e

theorem FibonacciMinkowski.diagonal_witness_two (n : ℕ) (hn : 3 ≤ n) (e : ℤ) (he1 : ↑n + 2 ≤ e) (hw : lam (n + 1) e = 2) :

∃ (d : ℤ) (d' : ℤ), 1 ≤ d ∧ d ≤ ↑(Nat.fib (n + 1)) ∧ ↑n + 1 ≤ d' ∧ d' ≤ ↑(Nat.fib (n + 2)) ∧ d + d' = e ∧ mu n d + lam n d' ≤ lam (n + 1) e

theorem FibonacciMinkowski.diagonal_witness_large (n : ℕ) (hn : 3 ≤ n) (e : ℤ) (he1 : ↑n + 2 ≤ e) (he2 : e ≤ ↑(Nat.fib (n + 3))) (hw : 3 ≤ lam (n + 1) e) :

∃ (d : ℤ) (d' : ℤ), 1 ≤ d ∧ d ≤ ↑(Nat.fib (n + 1)) ∧ ↑n + 1 ≤ d' ∧ d' ≤ ↑(Nat.fib (n + 2)) ∧ d + d' = e ∧ mu n d + lam n d' ≤ lam (n + 1) e

theorem FibonacciMinkowski.diagonal_witnesses (n : ℕ) (hn : 3 ≤ n) (e : ℤ) (he1 : ↑n + 2 ≤ e) (he2 : e ≤ ↑(Nat.fib (n + 3))) :

∃ (d : ℤ) (d' : ℤ), 1 ≤ d ∧ d ≤ ↑(Nat.fib (n + 1)) ∧ ↑n + 1 ≤ d' ∧ d' ≤ ↑(Nat.fib (n + 2)) ∧ d + d' = e ∧ mu n d + lam n d' ≤ lam (n + 1) e

theorem FibonacciMinkowski.interval_split (l₁ u₁ l₂ u₂ A : ℤ) (h₁ : l₁ ≤ u₁) (h₂ : l₂ ≤ u₂) (hlo : l₁ + l₂ ≤ A) (hhi : A ≤ u₁ + u₂) :

∃ (a : ℤ) (a' : ℤ), l₁ ≤ a ∧ a ≤ u₁ ∧ l₂ ≤ a' ∧ a' ≤ u₂ ∧ a + a' = A

theorem FibonacciMinkowski.fiber_sum_step (n : ℕ) (hn : 3 ≤ n) :

fiberSet 1 (↑(Nat.fib (n + 1))) (mu n) + fiberSet (↑n + 1) (↑(Nat.fib (n + 2))) (lam n) = fiberSet (↑n + 2) (↑(Nat.fib (n + 3))) (lam (n + 1))

theorem FibonacciMinkowski.structure_pair (n : ℕ) (hn : 3 ≤ n) :

(xy n).1 = fiberSet 1 (↑(Nat.fib (n + 1))) (mu n) ∧ (xy n).2 = fiberSet (↑n + 1) (↑(Nat.fib (n + 2))) (lam n)

theorem FibonacciMinkowski.structure_x (n : ℕ) (hn : 3 ≤ n) :

(xy n).1 = fiberSet 1 (↑(Nat.fib (n + 1))) (mu n)

Explicit staircase description of xₙ.

theorem FibonacciMinkowski.structure_y (n : ℕ) (hn : 3 ≤ n) :

(xy n).2 = fiberSet (↑n + 1) (↑(Nat.fib (n + 2))) (lam n)

Explicit staircase description of yₙ.

noncomputable def FibonacciMinkowski.envSum (m : ℕ) :

Equations

FibonacciMinkowski.envSum m = ∑ u ∈ Finset.Icc 1 ↑(Nat.fib m), FibonacciMinkowski.env m u

Instances For

noncomputable def FibonacciMinkowski.lamSum (m : ℕ) :

Equations

FibonacciMinkowski.lamSum m = ∑ d ∈ Finset.Icc (↑m + 1) ↑(Nat.fib (m + 2)), FibonacciMinkowski.lam m d

Instances For

noncomputable def FibonacciMinkowski.stairSum (m : ℕ) :

Equations

FibonacciMinkowski.stairSum m = ∑ d ∈ Finset.Icc (↑m + 1) ↑(Nat.fib (m + 2)), (d + 1 - 2 * FibonacciMinkowski.lam m d)

Instances For

theorem FibonacciMinkowski.fiberSet_card (s t : ℤ) (L : ℤ → ℤ) (hst : s ≤ t) (hwide : ∀ d ∈ Finset.Icc s t, 2 * L d ≤ d) :

↑(fiberSet s t L).card = ∑ d ∈ Finset.Icc s t, (d + 1 - 2 * L d)

theorem FibonacciMinkowski.join_intervals (a c b : ℤ) (h : a ≤ c ∧ c ≤ b) :

Finset.Icc a b = Finset.Icc a c ∪ Finset.Icc (c + 1) b

theorem FibonacciMinkowski.envSum_formula (m : ℕ) (hm : 2 ≤ m) :

2 * envSum m = ↑(Nat.fib m) * ↑(Nat.fib (m + 2)) + ↑(Nat.fib m) ^ 2 + ↑(Nat.fib (m + 2)) - 1

theorem FibonacciMinkowski.lamSum_formula (m : ℕ) (hm : 2 ≤ m) :

2 * lamSum m = ↑(Nat.fib m) * ↑(Nat.fib (m + 1)) + ↑(Nat.fib (m + 2)) + 1 - 2 * ↑m

theorem FibonacciMinkowski.stairSum_formula (m : ℕ) (hm : 2 ≤ m) :

2 * stairSum m = ↑(Nat.fib (2 * m + 1)) + ↑(Nat.fib (m + 2)) - ↑m * (↑m - 1) - 2

theorem FibonacciMinkowski.card_y_large (n : ℕ) (hn : 3 ≤ n) :

2 * (xy n).2.card + n * (n - 1) + 2 = Nat.fib (2 * n + 1) + Nat.fib (n + 2)

theorem FibonacciMinkowski.card_x_large (n : ℕ) (hn : 3 ≤ n) :

2 * (xy n).1.card = Nat.fib (2 * n - 1) + Nat.fib (n + 1) + 2

theorem FibonacciMinkowski.card_x (n : ℕ) (hn : 1 ≤ n) :

2 * (xy n).1.card = Nat.fib (2 * n - 1) + Nat.fib (n + 1) + 2

theorem FibonacciMinkowski.card_y (n : ℕ) (hn : 1 ≤ n) :

2 * (xy n).2.card + n * (n - 1) + 2 = Nat.fib (2 * n + 1) + Nat.fib (n + 2)

theorem FibonacciMinkowski.main_theorem (n : ℕ) (hn : 1 ≤ n) :

2 * (xy n).1.card = Nat.fib (2 * n - 1) + Nat.fib (n + 1) + 2 ∧ 2 * (xy n).2.card + n * (n - 1) + 2 = Nat.fib (2 * n + 1) + Nat.fib (n + 2)

The two doubled cardinality identities, exactly as stated in the paper.