Behavior of $E_{s,t}(n)$ and $w_{s,t}(n)$ for fixed $n$ and varying $s,t$

We will see that $w$ consists of a bunch of "blocks", whose interior displays Inert behavior, while edges display Split behavior. We will explicitly construct this block list, where each block is represented by inert tuples $(a, b, c, d)$.

Main statements

• wₗᵢMono: wₗᵢ is weakly monotone w.r.t. $s/t$.

This encodes an inert tuple $(a, b, c, d)$, though on its own it is not necessarily one.

structure InertSeg : Type

• a : ℕ+
• b : ℕ+
• c : ℕ+
• d : ℕ+

theorem InertSeg.ext {x y : InertSeg} (a : x.a = y.a) (b : x.b = y.b) (c : x.c = y.c) (d : x.d = y.d) : x = y

theorem InertSeg.ext_iff {x y : InertSeg} : x = y ↔ x.a = y.a ∧ x.b = y.b ∧ x.c = y.c ∧ x.d = y.d

instance instReprInertSeg : Repr InertSeg

Equations

• instReprInertSeg = { reprPrec := instReprInertSeg.repr }

def instReprInertSeg.repr : InertSeg → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

An inert tuple must satisfy $ad - bc = 1$

def InertSeg.det1 (seg : InertSeg) : Prop

Equations

• seg.det1 = (seg.a * seg.d = seg.b * seg.c + 1)

An inert tuple always creates a non-empty interval $[b/a, d/c]$.

theorem InertSeg.det1.lt {seg : InertSeg} (h : seg.det1) : ↑↑seg.b / ↑↑seg.a < ↑↑seg.d / ↑↑seg.c

An inert tuple is actually inert if n is below the branching point.

def InertSeg.inert (n : ℕ+) (seg : InertSeg) : Prop

Equations

• InertSeg.inert n seg = (↑n ≤ nBranching (seg.a + seg.c) (seg.b + seg.d))

Given a list of potentially inert tuple list, the function genSeg divides those whose branching point is too small to hopefully make the entire list actually inert.

def genSeg (n : ℕ+) (input : List InertSeg) : List InertSeg

Equations

• One or more equations did not get rendered due to their size.
• genSeg n [] = []

genSeg preserves $ad - bc = 1$.

theorem genSegDet (n : ℕ+) (input : List InertSeg) (h : List.Forall InertSeg.det1 input) : List.Forall InertSeg.det1 (genSeg n input)

If the input list is inert for $n$, then the output is inert for $n + 1$.

theorem genSegInert (n : ℕ+) (input : List InertSeg) (h : List.Forall (InertSeg.inert n) input) : List.Forall (InertSeg.inert (n + 1)) (genSeg (n + 1) input)

The explict inert tuple list is constructed as follows:

• $n < 3$ is special cased and we will skip them here.
  • $n = 1$ is undefined for w.
  • $n = 2$ gives a constant function w.
• $n = 3$ gives an empty list. This is also a special case but also serves as the base case.
• starting from $n = 4$, we append $(n - 2, 1, n - 3, 1)$ and $(1, n - 3, 1, n - 2)$ to the two ends of the list and divide tuples to keep them inert.

def segList (n : ℕ+) : List InertSeg

Equations

• One or more equations did not get rendered due to their size.

The first non-empty list is at $n = 4$

theorem segList4 : segList 4 = [{ a := 2, b := 1, c := 1, d := 1 }, { a := 1, b := 1, c := 1, d := 2 }]

Restating the recursive definition of segList as a themorem.

theorem segListSucc (n : ℕ+) (h : ¬n < 3) : segList (n + 1) = genSeg (n + 1) ([{ a := n - 1, b := 1, c := n - 2, d := 1 }] ++ segList n ++ [{ a := 1, b := n - 2, c := 1, d := n - 1 }])

segList always has $ad - bc = 1$ for all elements.

theorem segListDet (n : ℕ+) : List.Forall InertSeg.det1 (segList n)

segList's elements are all inert.

theorem segListInert (n : ℕ+) : List.Forall (InertSeg.inert n) (segList n)

We will specialize $w$ function with $s = 1$ and varying $t$.

segToInterval converts inert tuple to intervals of $t$.

def segToInterval (seg : InertSeg) : Set ℝ

Equations

• segToInterval seg = Set.Icc (↑↑seg.b / ↑↑seg.a) (↑↑seg.d / ↑↑seg.c)

def intervalList (n : ℕ+) : List (Set ℝ)

Equations

• intervalList n = List.map segToInterval (segList n)

All these intervals are positive numbers.

theorem intervalPositive (n : ℕ+) : List.Forall (fun (x : Set ℝ) => x ⊆ Set.Ioi 0) (intervalList n)

Define a wₗᵢ function without PosReal to help formulating theorems later

noncomputable def wₗᵢex (s t n : ℝ) : ℝ

Equations

• wₗᵢex s t n = if hs : s > 0 then if ht : t > 0 then have this := ⋯; have this_1 := ⋯; wₗᵢ s t n else 0 else 0

wₗᵢ is antitonic w.r.t $t$ in each closed interval. This comes from the following two facts:

• in the open interior, wₗᵢ is a constant, from Inert lemmas.
• The left and right boundary Splits into the interior, inducing inequialities.

theorem wₗᵢAntiOnInterval (N : ℕ+) (n : ℝ) (hn : n ≤ ↑↑N) (n2 : 2 ≤ n) : List.Forall (AntitoneOn fun (t : ℝ) => wₗᵢex 1 t n) (intervalList N)

Now that we have AntitoneOn in each interval, we'd like to glue them together.

The core theorem we want to use is AntitoneOn.union_right, but we need to apply it repeatedly on the list. To do so, we will need to formalize some properties about the list.

A list of sets is called SetsCover iff

• all the sets are non-empty Icc intervals, and
• they connect to each other at boundaries.

def SetsCover (list : List (Set ℝ)) (a b : ℝ) : Prop

Equations

• SetsCover [] a b = False
• SetsCover [single] a b = (single = Set.Icc a b ∧ a ≤ b)
• SetsCover (head :: tail) a b = ∃ (c : ℝ), head = Set.Icc a c ∧ a ≤ c ∧ SetsCover tail c b

A SetsCover list covers a large non-empty Set.Icc interval.

theorem LeOfSetsCover (list : List (Set ℝ)) (a b : ℝ) (cover : SetsCover list a b) : a ≤ b

Two SetsCover lists can be glued together.

def SetsCoverAppend {l1 l2 : List (Set ℝ)} {a b c : ℝ} (h1 : SetsCover l1 a b) (h2 : SetsCover l2 b c) : SetsCover (l1 ++ l2) a c

Equations

• ⋯ = ⋯

The list version of AntitoneOn.union_right.

theorem antitoneListUnion (f : ℝ → ℝ) (list : List (Set ℝ)) (a b : ℝ) (cover : SetsCover list a b) (antitone : List.Forall (AntitoneOn f) list) : AntitoneOn f (Set.Icc a b)

theorem IccEq {a b a' b' : ℝ} (h : Set.Icc a b = Set.Icc a' b') (le : a ≤ b) : a = a' ∧ b = b'

genSeg preserves the SetsCover property.

theorem genSegPreserveCovers (n : ℕ+) (list : List InertSeg) (a b : ℝ) (hdet : List.Forall InertSeg.det1 list) (hcover : SetsCover (List.map segToInterval list) a b) : SetsCover (List.map segToInterval (genSeg n list)) a b

Our interval list is indeed SetsCover.

theorem intervalListCover (n : ℕ+) : SetsCover (intervalList (n + 3)) (1 / (↑↑n + 1)) (↑↑n + 1)

Combining everything above, we show that wₗᵢ 1 t n is antitone on $[1 / (n - 2), n - 2]$ for integer $n$ (for non integer $n$, we just need to take a larger interger).

theorem wₗᵢAntiOnMiddle (N : ℕ+) (n : ℝ) (hn : n ≤ ↑↑N + 3) (n2 : 2 ≤ n) : AntitoneOn (fun (t : ℝ) => wₗᵢex 1 t n) (Set.Icc (1 / (↑↑N + 1)) (↑↑N + 1))

With Inert edge theories, we can show wₗᵢ 1 t n is antitone on $(0, 1 / (n - 2)]$ and on $[n - 2, ∞)$.

theorem wₗᵢAntiOnLeft (N : ℕ+) (n : ℝ) (hn : n ≤ ↑↑N + 3) (n2 : 2 ≤ n) : AntitoneOn (fun (t : ℝ) => wₗᵢex 1 t n) (Set.Ioc 0 (1 / (↑↑N + 1)))

theorem wₗᵢAntiOnRight (N : ℕ+) (n : ℝ) (hn : n ≤ ↑↑N + 3) (n2 : 2 ≤ n) : AntitoneOn (fun (t : ℝ) => wₗᵢex 1 t n) (Set.Ici (↑↑N + 1))

Gluing all them together, wₗᵢ 1 t n is antitone on all positive $t$. We also drops the bounding N here as it is no longer in the result.

theorem wₗᵢAnti (n : ℝ) (n2 : 2 ≤ n) : AntitoneOn (fun (t : ℝ) => wₗᵢex 1 t n) (Set.Ioi 0)

Restating the previous theorem for general $s$ and $t$.

theorem wₗᵢMono (s1 t1 s2 t2 n : ℝ) (n2 : 2 ≤ n) [PosReal s1] [PosReal t1] [PosReal s2] [PosReal t2] (h : s1 / t1 ≤ s2 / t2) : wₗᵢ s1 t1 n ≤ wₗᵢ s2 t2 n