Split behavior when changing $s,t$

We prove a family of "split" theorems.

When applying perturbation to $s$ and $t$, a single Λline set that pass through multiple lattice points will split into several sets. Consequently, more nₖ are inserted, and the piecewise function $E$ and $w$ split into finer pieces. We describe the behavior of $w$ during this process.

Finally, we will prove that wₗᵢ uniformly shifts towards one direction during splitting, which is a prerequisite for monocity of wₗᵢ over $s/t$.

While these are true for all positive $s$ and $t$, it is only interesting when $s/t$ is rational. If $s/t$ is irrational, all Λline are already singletons, so they won't split further.

Main statements

• wₗᵢsSplit and wₗᵢtSplit state wₗᵢ moves in the direction monotonic to $s/t$.
• wₘᵢₙsSplit and wₘᵢₙtSplit state wₘᵢₙ stays or moves upwards when $s/t$ moves in either direction.
• wₘₐₓsSplit and wₘₐₓtSplit state wₘₐₓ stays or moves downwards when $s/t$ moves in either direction.

Implementation note

We describe perturbation in δ-ε-like language. The larger $n$ or $k$ we look at, the smaller perturbation is allowed. We will develope an allowed bound for $ε$ for the given range of $k$. By convention, we use capital $K$ to represent the bound for $k$

For simplicity, we will mostly only consider a positive perturbation on t, and leave the rest to symmetry.

def Λₖ (s t : ℝ) (k : ℕ) [PosReal s] [PosReal t] : Set (ℕ × ℕ)

Equations

• Λₖ s t k = Λline s t (δₖ s t k)

theorem ΛₖNonempty (s t : ℝ) (k : ℕ) [PosReal s] [PosReal t] : (Λₖ s t k).Nonempty

noncomputable instance instFintypeElemProdNatΛₖ (s t : ℝ) (k : ℕ) [PosReal s] [PosReal t] : Fintype ↑(Λₖ s t k)

Equations

• instFintypeElemProdNatΛₖ s t k = id inferInstance

def Λfloored (s t : ℝ) (K : ℕ) [PosReal s] [PosReal t] : Set (ℕ × ℕ)

Equations

• Λfloored s t K = {pq : ℕ × ℕ | δₚ s t pq > δₖ s t K}

noncomputable def minGap (s t : ℝ) (K : ℕ) [PosReal s] [PosReal t] : ℝ

Equations

• minGap s t K = (Finset.image (fun (k : ℕ) => δₖ s t (k + 1) - δₖ s t k) (Finset.range (K + 1))).min' ⋯

noncomputable def εBound (s t : ℝ) (K : ℕ) [PosReal s] [PosReal t] : ℝ

Equations

• εBound s t K = minGap s t K / δₖ s t (K + 1)

theorem εBoundPos (s t : ℝ) (K : ℕ) [PosReal s] [PosReal t] : 0 < εBound s t K

theorem ΛₖIsolated (s t ε : ℝ) (k K : ℕ) (kbound : k < K) [PosReal s] [PosReal t] (εpos : 0 ≤ ε) (εbound : ε < t * εBound s t K) (pq : ℕ × ℕ) : pq ∈ Λₖ s t k → ∀ pq' ∈ Λₖ s t (k + 1), δₚ s (t + ε) pq < δₚ s (t + ε) pq'

theorem ΛflooredIsolated (s t ε : ℝ) (K : ℕ) [PosReal s] [PosReal t] (εpos : 0 ≤ ε) (εbound : ε < t * εBound s t K) (pq : ℕ × ℕ) : pq ∈ Λₖ s t K → ∀ pq' ∈ Λfloored s t K, δₚ s (t + ε) pq < δₚ s (t + ε) pq'

theorem ΛₖMono (s t ε : ℝ) (k1 k2 K : ℕ) (kh : k1 < k2) (kbound : k1 ≤ K) [PosReal s] [PosReal t] (εpos : 0 ≤ ε) (εbound : ε < t * εBound s t K) (pq : ℕ × ℕ) : pq ∈ Λₖ s t k1 → ∀ pq' ∈ Λₖ s t k2, δₚ s (t + ε) pq < δₚ s (t + ε) pq'

theorem ΛₖSplit (s t ε : ℝ) (k : ℕ) [PosReal s] [PosReal t] [PosReal ε] (pq : ℕ × ℕ) : pq ∈ Λₖ s t k → ∀ pq' ∈ Λₖ s t k, pq = pq' ↔ δₚ s (t + ε) pq = δₚ s (t + ε) pq'

theorem ΛₖSplit' (s t ε : ℝ) (k K : ℕ) (kbound : k ≤ K) [PosReal s] [PosReal t] [PosReal ε] (εbound : ε < t * εBound s t K) (pq : ℕ × ℕ) : pq ∈ Λₖ s t k → ∀ (pq' : ℕ × ℕ), pq = pq' ↔ δₚ s (t + ε) pq = δₚ s (t + ε) pq'

theorem ΛₖtoδNonempty (s t ε : ℝ) (k : ℕ) [PosReal s] [PosReal t] : (Finset.image (δₚ s (t + ε)) (Λₖ s t k).toFinset).Nonempty

noncomputable def δₚSplitMax (s t ε : ℝ) (k : ℕ) [PosReal s] [PosReal t] [PosReal ε] : ℝ

Equations

• δₚSplitMax s t ε k = (Finset.image (δₚ s (t + ε)) (Λₖ s t k).toFinset).max' ⋯

theorem δₚSplitMaxInΔ (s t ε : ℝ) (k : ℕ) [PosReal s] [PosReal t] [PosReal ε] : δₚSplitMax s t ε k ∈ Δ s (t + ε)

theorem δₚSplitMaxSpec (s t ε : ℝ) (k : ℕ) [PosReal s] [PosReal t] [PosReal ε] (pq : ℕ × ℕ) : pq ∈ Λₖ s t k → δₚ s (t + ε) pq ≤ δₚSplitMax s t ε k

noncomputable def kSplitMax (s t ε : ℝ) (k : ℕ) [PosReal s] [PosReal t] [PosReal ε] : ℕ

Equations

• kSplitMax s t ε k = ⋯.choose

def kSplitMaxSpec (s t ε : ℝ) (k : ℕ) [PosReal s] [PosReal t] [PosReal ε] (pq : ℕ × ℕ) : pq ∈ Λₖ s t k → δₚ s (t + ε) pq ≤ δₖ s (t + ε) (kSplitMax s t ε k)

Equations

• ⋯ = ⋯

theorem ΛceiledSplit (s t ε : ℝ) (k K : ℕ) [PosReal s] [PosReal t] [PosReal ε] (kBound : k ≤ K) (εbound : ε < t * εBound s t K) : Λceiled s t (δₖ s t k) = Λceiled s (t + ε) (δₖ s (t + ε) (kSplitMax s t ε k))

theorem ΛceiledSplit_s (s t ε : ℝ) (k K : ℕ) [PosReal s] [PosReal t] [PosReal ε] (kBound : k ≤ K) (εbound : ε < t * εBound s t K) : Λceiled s t (δₖ s t k - s) = Λceiled s (t + ε) (δₖ s (t + ε) (kSplitMax s t ε k) - s)

theorem nₖSplit (s t ε : ℝ) (k K : ℕ) [PosReal s] [PosReal t] [PosReal ε] (kBound : k ≤ K) (εbound : ε < t * εBound s t K) : nₖ s t (k + 1) = nₖ s (t + ε) (kSplitMax s t ε k + 1)

theorem wₖ'Split (s t ε : ℝ) (k K : ℕ) [PosReal s] [PosReal t] [PosReal ε] (kBound : k ≤ K) (εbound : ε < t * εBound s t K) : wₖ' s t (k + 1) = wₖ' s (t + ε) (kSplitMax s t ε k + 1)

theorem wₖSplit (s t ε : ℝ) (k K : ℕ) [PosReal s] [PosReal t] [PosReal ε] (kBound : k ≤ K) (εbound : ε < t * εBound s t K) : wₖ s t (k + 1) = wₖ s (t + ε) (kSplitMax s t ε k + 1)

theorem wₘᵢₙSplit (s t ε : ℝ) (k K : ℕ) (n : ℝ) [PosReal s] [PosReal t] [PosReal ε] (kBound : k < K) (εbound : ε < t * εBound s t K) (nleft : ↑(nₖ s t (k + 1)) ≤ n) (nright : n < ↑(nₖ s t (k + 2))) : wₘᵢₙ s t n ≤ wₘᵢₙ s (t + ε) n

theorem wₘₐₓSplit (s t ε : ℝ) (k K : ℕ) (n : ℝ) [PosReal s] [PosReal t] [PosReal ε] (kBound : k < K) (εbound : ε < t * εBound s t K) (nleft : ↑(nₖ s t (k + 1)) ≤ n) (nright : n < ↑(nₖ s t (k + 2))) : wₘₐₓ s (t + ε) n ≤ wₘₐₓ s t n

theorem δₖSplitBetween (s t ε : ℝ) (k K k' : ℕ) [PosReal s] [PosReal t] [PosReal ε] (kBound : k < K) (εbound : ε < t * εBound s t K) (k'left : kSplitMax s t ε k < k') (k'right : k' ≤ kSplitMax s t ε (k + 1)) : ∃ pq ∈ Λₖ s t (k + 1), δₖ s (t + ε) k' = δₚ s (t + ε) pq

noncomputable def pqOfδₖSplit (s t ε : ℝ) (k K k' : ℕ) [PosReal s] [PosReal t] [PosReal ε] (kBound : k < K) (εbound : ε < t * εBound s t K) (k'left : kSplitMax s t ε k < k') (k'right : k' ≤ kSplitMax s t ε (k + 1)) : ℕ × ℕ

Equations

• pqOfδₖSplit s t ε k K k' kBound εbound k'left k'right = ⋯.choose

noncomputable def pqslope (pq : ℕ × ℕ) : ℝ

Equations

• pqslope pq = ↑pq.2 / (↑pq.1 + ↑pq.2)

theorem Jslope (pq : ℕ × ℕ) (h : pq.2 ≠ 0) : ↑(Jₚ (pq.1, pq.2 - 1)) / ↑(Jₚ pq) = pqslope pq

theorem wslope (s t ε : ℝ) (k K k' : ℕ) [PosReal s] [PosReal t] [PosReal ε] (kBound : k < K) (εbound : ε < t * εBound s t K) (k'left : kSplitMax s t ε k < k') (k'right : k' ≤ kSplitMax s t ε (k + 1)) : ↑(Jtₖ s (t + ε) k') / ↑(Jₖ s (t + ε) k') = pqslope (pqOfδₖSplit s t ε k K k' kBound εbound k'left k'right)

noncomputable def slopeₖ (s t : ℝ) [PosReal s] [PosReal t] (k : ℕ) : ℝ

Equations

• slopeₖ s t k = (↑(wₖ s t (k + 1)) - ↑(wₖ s t k)) / (↑(nₖ s t (k + 1)) - ↑(nₖ s t k))

theorem wslopeMono (s t ε : ℝ) (k K : ℕ) [PosReal s] [PosReal t] [PosReal ε] (kBound : k < K) (εbound : ε < t * εBound s t K) : StrictMonoOn (slopeₖ s (t + ε)) (Set.Ioc (kSplitMax s t ε k) (kSplitMax s t ε (k + 1)))

theorem wₗᵢunder (s t ε : ℝ) (k K k' : ℕ) [PosReal s] [PosReal t] [PosReal ε] (kBound : k < K) (εbound : ε < t * εBound s t K) (k'left : kSplitMax s t ε k < k') (k'right : k' < kSplitMax s t ε (k + 1)) : ↑(wₖ s (t + ε) (k' + 1)) < wₗᵢ s t ↑(nₖ s (t + ε) (k' + 1))

theorem wₗᵢSplit (s t ε : ℝ) (k K : ℕ) (n : ℝ) [PosReal s] [PosReal t] [PosReal ε] (kBound : k < K) (εbound : ε < t * εBound s t K) (nleft : ↑(nₖ s t (k + 1)) ≤ n) (nright : n < ↑(nₖ s t (k + 2))) : wₗᵢ s (t + ε) n ≤ wₗᵢ s t n

theorem generalizeSplit (prop : (s t ε : ℝ) → [PosReal s] → [PosReal t] → [PosReal ε] → ℝ → Prop) (localSplit : ∀ (s t ε : ℝ) (k K : ℕ) (n : ℝ) [inst : PosReal s] [inst_1 : PosReal t] [inst_2 : PosReal ε], k < K → ε < t * εBound s t K → ↑(nₖ s t (k + 1)) ≤ n → n < ↑(nₖ s t (k + 2)) → prop s t ε n) (s t n : ℝ) (n2 : 2 ≤ n) [PosReal s] [PosReal t] : ∃ εbound > 0, ∀ (ε : ℝ) (εpos : 0 < ε), ε < εbound → have this := ⋯; prop s t ε n

theorem wₗᵢtSplit (s t n : ℝ) (n2 : 2 ≤ n) [PosReal s] [PosReal t] : ∃ εbound > 0, ∀ (ε : ℝ) (εpos : 0 < ε), ε < εbound → have this := ⋯; wₗᵢ s (t + ε) n ≤ wₗᵢ s t n

theorem wₘᵢₙtSplit (s t n : ℝ) (n2 : 2 ≤ n) [PosReal s] [PosReal t] : ∃ εbound > 0, ∀ (ε : ℝ) (εpos : 0 < ε), ε < εbound → have this := ⋯; wₘᵢₙ s t n ≤ wₘᵢₙ s (t + ε) n

theorem wₘₐₓtSplit (s t n : ℝ) (n2 : 2 ≤ n) [PosReal s] [PosReal t] : ∃ εbound > 0, ∀ (ε : ℝ) (εpos : 0 < ε), ε < εbound → have this := ⋯; wₘₐₓ s (t + ε) n ≤ wₘₐₓ s t n

theorem wₗᵢsSplit (s t n : ℝ) (n2 : 2 ≤ n) [PosReal s] [PosReal t] : ∃ εbound > 0, ∀ (ε : ℝ) (εpos : 0 < ε), ε < εbound → have this := ⋯; wₗᵢ s t n ≤ wₗᵢ (s + ε) t n

theorem wₘᵢₙsSplit (s t n : ℝ) (n2 : 2 ≤ n) [PosReal s] [PosReal t] : ∃ εbound > 0, ∀ (ε : ℝ) (εpos : 0 < ε), ε < εbound → have this := ⋯; wₘᵢₙ s t n ≤ wₘᵢₙ (s + ε) t n

theorem wₘₐₓsSplit (s t n : ℝ) (n2 : 2 ≤ n) [PosReal s] [PosReal t] : ∃ εbound > 0, ∀ (ε : ℝ) (εpos : 0 < ε), ε < εbound → have this := ⋯; wₘₐₓ (s + ε) t n ≤ wₘₐₓ s t n