Inert behavior when changing $s,t$

We prove a family of "inert" theorems. The w function, along with many underlying structures, demonstrate a behavior where for a fixed $n$, the function value doesn't change along $s/t$ line within a small interval Such interval is always between a pair of Farey neighbours.

To be specific, for positive integers $a$, $b$, $c$, and $d$ such that $ad - bc = 1$, and for all $s$ and $t$ usch that $c/d < s/t < a/b$, the $w$ function is a constant as long as $n$ isn't too large (we will find the bound for $n$ soon)

We will use such tuple $(a, b, c, d)$ a lot in the following theorems, which we call an inert tuple.

Intuitively, changing $s/t$ slightly is to rotate Λline little bit. When such rotation doesn't hit any lattice points, a lot of functions we have constructed stay constant.

Main statements

• wₘᵢₙ_inert, wₘₐₓ_inert, and wₗᵢ_inert state that $w$ doesnt't change along with small change to $s,t$ as long as $n$ isn't too large.
• wₘᵢₙ_inert_edge, wₘₐₓ_inert_edge and wₗᵢ_inert_edge explicitly calculates $w$ when $t$ is very large.
• wₘᵢₙ_inert_edge', wₘₐₓ_inert_edge' and wₗᵢ_inert_edge' explicitly calculates $w$ when $s$ is very large.

We start with a simple lemma: for rational $s/t$, the scanning line can pass multiple points, but this can only happen after the s * t threshold.

theorem unique_pq (s t : ℕ+) (pq pq' : ℕ × ℕ) (coprime : s.Coprime t) (eq : δₚ (↑↑s) (↑↑t) pq = δₚ (↑↑s) (↑↑t) pq') (bound : δₚ (↑↑s) (↑↑t) pq < ↑↑s * ↑↑t) : pq = pq'

The property of Farey neighbors: a new fraction between a Farey neighbor must have a large denominator.

theorem slopeBound (a b c d s t : ℕ+) (det : a * d = b * c + 1) (left : c * t < d * s) (right : b * s < a * t) : t ≥ b + d

Some inert theorems on Λceiled: below the threshold, one can slightly rotate the ceiling without changing the set members.

We divide the proof into three parts:

• Λceiled_inert_half: only look at one side of the delta area.
• Λceiled_inert: prove for the full set, but requires an ordering between two ceilings.
• Λceiled_inert': remove the requirement on the ordering.

theorem Λceiled_inert_half (a b c d : ℕ+) (s1 t1 s2 t2 : ℝ) (p q : ℕ) [PosReal s1] [PosReal t1] [PosReal s2] [PosReal t2] (det : a * d = b * c + 1) (left : ↑↑a * t1 > ↑↑b * s1) (mid : s1 * t2 > s2 * t1) (right : ↑↑d * s2 > ↑↑c * t2) (pBound : p < ↑b + ↑d) (p' q' : ℕ) (qless : q < q') (pmore : p' < p) : ↑p' * s1 + ↑q' * t1 ≤ ↑p * s1 + ↑q * t1 ↔ ↑p' * s2 + ↑q' * t2 ≤ ↑p * s2 + ↑q * t2

theorem Λceiled_inert (a b c d : ℕ+) (s1 t1 s2 t2 : ℝ) (p q : ℕ) [PosReal s1] [PosReal t1] [PosReal s2] [PosReal t2] (det : a * d = b * c + 1) (left : ↑↑a * t1 > ↑↑b * s1) (mid : s1 * t2 > s2 * t1) (right : ↑↑d * s2 > ↑↑c * t2) (pBound : p < ↑b + ↑d) (qBound : q < ↑a + ↑c) : Λceiled s1 t1 (↑p * s1 + ↑q * t1) = Λceiled s2 t2 (↑p * s2 + ↑q * t2)

theorem Λceiled_inert' (a b c d : ℕ+) (s1 t1 s2 t2 : ℝ) (p q : ℕ) [PosReal s1] [PosReal t1] [PosReal s2] [PosReal t2] (det : a * d = b * c + 1) (left1 : ↑↑a * t1 > ↑↑b * s1) (right1 : ↑↑d * s1 > ↑↑c * t1) (left2 : ↑↑a * t2 > ↑↑b * s2) (right2 : ↑↑d * s2 > ↑↑c * t2) (pBound : p < ↑b + ↑d) (qBound : q < ↑a + ↑c) : Λceiled s1 t1 (↑p * s1 + ↑q * t1) = Λceiled s2 t2 (↑p * s2 + ↑q * t2)

The δₚ evaluation is inert within the threshold, as in the ordering doesn't change for changing $s/t$.

theorem Δceiled_lt_inert (a b c d : ℕ+) (s1 t1 s2 t2 : ℝ) (p1 q1 p2 q2 : ℕ) [PosReal s1] [PosReal t1] [PosReal s2] [PosReal t2] (det : a * d = b * c + 1) (left1 : ↑↑a * t1 > ↑↑b * s1) (right1 : ↑↑d * s1 > ↑↑c * t1) (left2 : ↑↑a * t2 > ↑↑b * s2) (right2 : ↑↑d * s2 > ↑↑c * t2) (p1Bound : p1 < ↑b + ↑d) (q1Bound : q1 < ↑a + ↑c) (p2Bound : p2 < ↑b + ↑d) (q2Bound : q2 < ↑a + ↑c) : δₚ s1 t1 (p1, q1) < δₚ s1 t1 (p2, q2) → δₚ s2 t2 (p1, q1) < δₚ s2 t2 (p2, q2)

A variation of Λceiled_inert, concering about a ceiling created by lattice point below ℕ, and with Λceiled_inert_t' that removes the ordering requirement. This will be used for w related theories.

theorem Λceiled_inert_t (a b c d : ℕ+) (s1 t1 s2 t2 : ℝ) (p : ℕ) [PosReal s1] [PosReal t1] [PosReal s2] [PosReal t2] (det : a * d = b * c + 1) (left : ↑↑a * t1 > ↑↑b * s1) (mid : s1 * t2 > s2 * t1) (right : ↑↑d * s2 > ↑↑c * t2) (pBound : p < ↑b + ↑d) : Λceiled s1 t1 (↑p * s1 - t1) = Λceiled s2 t2 (↑p * s2 - t2)

theorem Λceiled_inert_t' (a b c d : ℕ+) (s1 t1 s2 t2 : ℝ) (p : ℕ) [PosReal s1] [PosReal t1] [PosReal s2] [PosReal t2] (det : a * d = b * c + 1) (left1 : ↑↑a * t1 > ↑↑b * s1) (right1 : ↑↑d * s1 > ↑↑c * t1) (left2 : ↑↑a * t2 > ↑↑b * s2) (right2 : ↑↑d * s2 > ↑↑c * t2) (pBound : p < ↑b + ↑d) : Λceiled s1 t1 (↑p * s1 - t1) = Λceiled s2 t2 (↑p * s2 - t2)

The mediant of Farey neighbors is within the inert interval.

theorem abcdLeftRight (a b c d : ℕ+) (det : a * d = b * c + 1) : ↑↑a * (↑↑b + ↑↑d) > ↑↑b * (↑↑a + ↑↑c) ∧ ↑↑d * (↑↑a + ↑↑c) > ↑↑c * (↑↑b + ↑↑d)

δₖ sequence is inert within an inert interval. This version is a bit primitive, where it requires a sequence of lattice points that generates δₖ to exist first, and we don't have an explicit bound yet.

theorem δₖ_inert (a b c d : ℕ+) (s1 t1 s2 t2 : ℝ) (kbound : ℕ) (pqₖ : ℕ → ℕ × ℕ) [PosReal s1] [PosReal t1] [PosReal s2] [PosReal t2] (det : a * d = b * c + 1) (left1 : ↑↑a * t1 > ↑↑b * s1) (right1 : ↑↑d * s1 > ↑↑c * t1) (left2 : ↑↑a * t2 > ↑↑b * s2) (right2 : ↑↑d * s2 > ↑↑c * t2) (pqMatch1 : ∀ k ≤ kbound, δₖ s1 t1 k = δₚ s1 t1 (pqₖ k)) (pqBound : ∀ k ≤ kbound, (pqₖ k).1 * (↑a + ↑c) + (pqₖ k).2 * (↑b + ↑d) < (↑a + ↑c) * (↑b + ↑d)) (k : ℕ) : k ≤ kbound → δₖ s2 t2 k = δₚ s2 t2 (pqₖ k)

Here we have series of little lemma to eventually prove the cardinality of all lattice points in an inert interval.

def FintypeIcc (L : ℕ) : Type

Equations

• FintypeIcc L = ↑(Set.Icc 0 L)

def Λrectangle (s t : ℕ+) : Finset (ℕ × ℕ)

Equations

• Λrectangle s t = Finset.range (↑t + 1) ×ˢ Finset.range (↑s + 1)

instance Λrectangle_fintype (s t : ℕ+) : Fintype { x : ℕ × ℕ // x ∈ Λrectangle s t }

Equations

• Λrectangle_fintype s t = id (Finset.range (↑t + 1) ×ˢ Finset.range (↑s + 1)).fintypeCoeSort

theorem Λrectangle_card (s t : ℕ+) : Fintype.card { x : ℕ × ℕ // x ∈ Λrectangle s t } = (↑t + 1) * (↑s + 1)

def Λtriangle (s t : ℕ+) : Set (ℕ × ℕ)

Equations

• Λtriangle s t = {pq : ℕ × ℕ | pq.1 * ↑s + pq.2 * ↑t < ↑s * ↑t}

def ΛtriangleFinset (s t : ℕ+) : Finset (ℕ × ℕ)

Equations

• ΛtriangleFinset s t = (Finset.range ↑t).biUnion fun (p : ℕ) => {p} ×ˢ Finset.range ((↑s * (↑t - p) + (↑t - 1)) / ↑t)

theorem Λtriangle_is_Finset (s t : ℕ+) (pq : ℕ × ℕ) : pq ∈ ΛtriangleFinset s t ↔ pq ∈ Λtriangle s t

instance ΛtriangleFintype (s t : ℕ+) : Fintype ↑(Λtriangle s t)

Equations

• ΛtriangleFintype s t = Fintype.ofFinset (ΛtriangleFinset s t) ⋯

noncomputable instance ΛtriangleDecidable (s t : ℕ+) : DecidablePred fun (x : ℕ × ℕ) => x ∈ Λtriangle s t

Equations

• ΛtriangleDecidable s t = Classical.decPred fun (x : ℕ × ℕ) => x ∈ Λtriangle s t

def ΛtriangleUpper (s t : ℕ+) : Set (ℕ × ℕ)

Equations

• ΛtriangleUpper s t = {pq : ℕ × ℕ | pq.1 * ↑s + pq.2 * ↑t > ↑s * ↑t} ∩ ↑(Λrectangle s t)

def ΛtriangleUpperSubset (s t : ℕ+) : ΛtriangleUpper s t ⊆ ↑(Λrectangle s t)

Equations

• ⋯ = ⋯

noncomputable instance ΛtriangleUpperDecidable (s t : ℕ+) : DecidablePred fun (x : ℕ × ℕ) => x ∈ ΛtriangleUpper s t

Equations

• ΛtriangleUpperDecidable s t = Classical.decPred fun (x : ℕ × ℕ) => x ∈ ΛtriangleUpper s t

noncomputable instance ΛtriangleUpperFintype (s t : ℕ+) : Fintype ↑(ΛtriangleUpper s t)

Equations

• ΛtriangleUpperFintype s t = (↑(Λrectangle s t)).fintypeSubset ⋯

def BoundDecomposite (p q : ℕ) {s t : ℕ+} (h : p * ↑s + q * ↑t < ↑s * ↑t) : p < ↑t ∧ q < ↑s

Equations

• ⋯ = ⋯

theorem ΛtriangleCardEq (s t : ℕ+) : (Λtriangle s t).toFinset.card = (ΛtriangleUpper s t).toFinset.card

def ΛrectangleCut (s t : ℕ+) : Finset (ℕ × ℕ)

Equations

• ΛrectangleCut s t = (Λrectangle s t \ {(↑t, 0)}) \ {(0, ↑s)}

instance ΛrectangleCutFintype (s t : ℕ+) : Fintype { x : ℕ × ℕ // x ∈ ΛrectangleCut s t }

Equations

• ΛrectangleCutFintype s t = id ((Λrectangle s t \ {(↑t, 0)}) \ {(0, ↑s)}).fintypeCoeSort

theorem ΛrectangleCutCard (s t : ℕ+) : Fintype.card { x : ℕ × ℕ // x ∈ ΛrectangleCut s t } = (↑t + 1) * (↑s + 1) - 2

theorem ΛrectangleDecompose (s t : ℕ+) (coprime : s.Coprime t) : ΛrectangleCut s t = (Λtriangle s t).toFinset ∪ (ΛtriangleUpper s t).toFinset

theorem ΛrectangleDisjoint (s t : ℕ+) : (Λtriangle s t).toFinset ∩ (ΛtriangleUpper s t).toFinset = ∅

Here we finally get the value of the cardinality, which we will use to character rise the bound of n.

theorem ΛtriangleCard (s t : ℕ+) (coprime : s.Coprime t) : (Λtriangle s t).toFinset.card = ((↑s + 1) * (↑t + 1) - 2) / 2

We define the the sequence of lattice points that will generate δₖ

theorem pqOfδₖ_exist (s t : ℕ+) (k : ℕ) : ∃ (pq : ℕ × ℕ), δₚ (↑↑s) (↑↑t) pq = δₖ (↑↑s) (↑↑t) k

noncomputable def pqOfδₖ (s t : ℕ+) (k : ℕ) : ℕ × ℕ

Equations

• pqOfδₖ s t k = ⋯.choose

theorem pqOfδₖ_bound (s t : ℕ+) (k : ℕ) (coprime : s.Coprime t) (h : k < ((↑s + 1) * (↑t + 1) - 2) / 2) : (pqOfδₖ s t k).1 * ↑s + (pqOfδₖ s t k).2 * ↑t < ↑s * ↑t

theorem abcdCoprime (a b c d : ℕ+) (det : a * d = b * c + 1) : (a + c).Coprime (b + d)

Now we can prove a stronger version of δₖ_inert, because we know the sequence of lattice points always exists, and we have the explicit bound.

theorem δₖ_inert_fixed (a b c d : ℕ+) (s t : ℝ) (k : ℕ) [PosReal s] [PosReal t] (det : a * d = b * c + 1) (left : ↑↑a * t > ↑↑b * s) (right : ↑↑d * s > ↑↑c * t) (kbound : k < ((↑a + ↑c + 1) * (↑b + ↑d + 1) - 2) / 2) : δₖ s t k = δₚ s t (pqOfδₖ (a + c) (b + d) k)

From δₖ, we can prove nₖ is inert,

theorem nₖ_inert (a b c d : ℕ+) (s1 t1 s2 t2 : ℝ) (k : ℕ) [PosReal s1] [PosReal t1] [PosReal s2] [PosReal t2] (det : a * d = b * c + 1) (left1 : ↑↑a * t1 > ↑↑b * s1) (right1 : ↑↑d * s1 > ↑↑c * t1) (left2 : ↑↑a * t2 > ↑↑b * s2) (right2 : ↑↑d * s2 > ↑↑c * t2) (kbound : k < (↑a + ↑c + 1) * (↑b + ↑d + 1) / 2) : nₖ s1 t1 k = nₖ s2 t2 k

...and wₖ is inert. This prove is longer because one need to consider some wₖ might corresponds to a ceiling generated by a lattice point below ℕ.

theorem wₖ_inert (a b c d : ℕ+) (s1 t1 s2 t2 : ℝ) (k : ℕ) [PosReal s1] [PosReal t1] [PosReal s2] [PosReal t2] (det : a * d = b * c + 1) (left1 : ↑↑a * t1 > ↑↑b * s1) (right1 : ↑↑d * s1 > ↑↑c * t1) (left2 : ↑↑a * t2 > ↑↑b * s2) (right2 : ↑↑d * s2 > ↑↑c * t2) (kbound : k < (↑a + ↑c + 1) * (↑b + ↑d + 1) / 2) : wₖ s1 t1 k = wₖ s2 t2 k

We define the bound for n The first definition allows explicit computation, but we also immediately prove a formula that's more useful for theorem proving.

def nBranching (s t : ℕ+) : ℕ

Equations

• nBranching s t = 1 + ∑ pq ∈ (Λtriangle s t).toFinset, Jₚ pq

theorem nBranchingFormula (s t : ℕ+) (coprime : s.Coprime t) : nBranching s t = nₖ (↑↑s) (↑↑t) ((↑s + 1) * (↑t + 1) / 2 - 1)

kceiled is inert within the bound of n.

theorem kceiled_inert (a b c d : ℕ+) (s1 t1 s2 t2 n : ℝ) [PosReal s1] [PosReal t1] [PosReal s2] [PosReal t2] (det : a * d = b * c + 1) (left1 : ↑↑a * t1 > ↑↑b * s1) (right1 : ↑↑d * s1 > ↑↑c * t1) (left2 : ↑↑a * t2 > ↑↑b * s2) (right2 : ↑↑d * s2 > ↑↑c * t2) (nbound : n ≤ ↑(nBranching (a + c) (b + d))) : kceiled s1 t1 n = kceiled s2 t2 n

... so is kₙ

theorem kₙ_inert (a b c d : ℕ+) (s1 t1 s2 t2 n : ℝ) [PosReal s1] [PosReal t1] [PosReal s2] [PosReal t2] (det : a * d = b * c + 1) (left1 : ↑↑a * t1 > ↑↑b * s1) (right1 : ↑↑d * s1 > ↑↑c * t1) (left2 : ↑↑a * t2 > ↑↑b * s2) (right2 : ↑↑d * s2 > ↑↑c * t2) (nbound : n ≤ ↑(nBranching (a + c) (b + d))) : kₙ s1 t1 n = kₙ s2 t2 n

Here come our main theorems: wₘᵢₙ, wₘₐₓ, and wₗᵢ are all inert.

theorem wₘᵢₙ_inert (a b c d : ℕ+) (s1 t1 s2 t2 n : ℝ) [PosReal s1] [PosReal t1] [PosReal s2] [PosReal t2] (det : a * d = b * c + 1) (left1 : ↑↑a * t1 > ↑↑b * s1) (right1 : ↑↑d * s1 > ↑↑c * t1) (left2 : ↑↑a * t2 > ↑↑b * s2) (right2 : ↑↑d * s2 > ↑↑c * t2) (h : n ≥ 2) (nbound : n ≤ ↑(nBranching (a + c) (b + d))) : wₘᵢₙ s1 t1 n = wₘᵢₙ s2 t2 n

theorem wₘₐₓ_inert (a b c d : ℕ+) (s1 t1 s2 t2 n : ℝ) [PosReal s1] [PosReal t1] [PosReal s2] [PosReal t2] (det : a * d = b * c + 1) (left1 : ↑↑a * t1 > ↑↑b * s1) (right1 : ↑↑d * s1 > ↑↑c * t1) (left2 : ↑↑a * t2 > ↑↑b * s2) (right2 : ↑↑d * s2 > ↑↑c * t2) (h : n ≥ 2) (nbound : n ≤ ↑(nBranching (a + c) (b + d))) : wₘₐₓ s1 t1 n = wₘₐₓ s2 t2 n

theorem wₗᵢ_inert (a b c d : ℕ+) (s1 t1 s2 t2 n : ℝ) [PosReal s1] [PosReal t1] [PosReal s2] [PosReal t2] (det : a * d = b * c + 1) (left1 : ↑↑a * t1 > ↑↑b * s1) (right1 : ↑↑d * s1 > ↑↑c * t1) (left2 : ↑↑a * t2 > ↑↑b * s2) (right2 : ↑↑d * s2 > ↑↑c * t2) (_h : n ≥ 2) (nbound : n ≤ ↑(nBranching (a + c) (b + d))) : wₗᵢ s1 t1 n = wₗᵢ s2 t2 n

We start proving another family ot theorems: inert at edge These are essentially saying w functions are inert for $(a=1,b=N,c=0,d=1)$ and for $(a=1,b=0,c=N,d=1)$ But as we have been developing our theory for positive inters only, these need special treatment.

We will also prove stronger theorems where we find the value of w explicity. In fact, they are at the edge $1$ or $n - 1$, hence the name.

theorem δₖ_inert_edge (N : ℕ+) (s t : ℝ) (k : ℕ) [PosReal s] [PosReal t] (left : t > ↑↑N * s) (kbound : k < ↑N + 1) : δₖ s t k = ↑k * s

theorem nₖ_inert_edge (N : ℕ+) (s t : ℝ) (k : ℕ) [PosReal s] [PosReal t] (left : t > ↑↑N * s) (kbound : k < ↑N + 2) : nₖ s t k = k + 1

theorem wₖ_inert_edge (N : ℕ+) (s t : ℝ) (k : ℕ) [PosReal s] [PosReal t] (left : t > ↑↑N * s) (kbound : k < ↑N + 2) : wₖ s t k = 1

theorem wₘᵢₙ_inert_edge (N : ℕ+) (s t n : ℝ) [PosReal s] [PosReal t] (left : t > ↑↑N * s) (h : n ≥ 2) (nbound : n ≤ ↑↑N + 2) : wₘᵢₙ s t n = 1

theorem wₘₐₓ_inert_edge (N : ℕ+) (s t n : ℝ) [PosReal s] [PosReal t] (left : t > ↑↑N * s) (h : n ≥ 2) (nbound : n ≤ ↑↑N + 2) : wₘₐₓ s t n = 1

theorem wₗᵢ_inert_edge (N : ℕ+) (s t n : ℝ) [PosReal s] [PosReal t] (left : t > ↑↑N * s) (h : n ≥ 2) (nbound : n ≤ ↑↑N + 2) : wₗᵢ s t n = 1

theorem wₘᵢₙ_inert_edge' (N : ℕ+) (s t n : ℝ) [PosReal s] [PosReal t] (left : s > ↑↑N * t) (h : n ≥ 2) (nbound : n ≤ ↑↑N + 2) : wₘᵢₙ s t n = n - 1

theorem wₘₐₓ_inert_edge' (N : ℕ+) (s t n : ℝ) [PosReal s] [PosReal t] (left : s > ↑↑N * t) (h : n ≥ 2) (nbound : n ≤ ↑↑N + 2) : wₘₐₓ s t n = n - 1

theorem wₗᵢ_inert_edge' (N : ℕ+) (s t n : ℝ) [PosReal s] [PosReal t] (left : s > ↑↑N * t) (h : n ≥ 2) (nbound : n ≤ ↑↑N + 2) : wₗᵢ s t n = n - 1