Asymptotics

We show that E and wₗᵢ, the solution to the original biased bisect problem, are asymptotically equivalent to Eℝ and wℝ, the solution to the continuous biased bisect problem.

Main statements

• E_Asymptotic states the asymptotic behavior of E.
• w_Asymtotic states the asymptotic behavior of wₗᵢ.

We start with a few lemma concerning the asymptotic behavior of δₖ and φ.

Although intuitively obvious, we need to show that δₖ grows unbounded.

theorem δₖ_infinity (s t : ℝ) [PosReal s] [PosReal t] : Filter.Tendsto (δₖ s t) Filter.atTop Filter.atTop

We restate φ_bound in terms of asymptotic behavior: log φ has linear growth.

theorem φ_Asymptotic (s t : ℝ) [PosReal s] [PosReal t] : Filter.Tendsto (fun (x : ℝ) => x * ρ s t / Real.log ↑(φ s t x)) Filter.atTop (nhds 1)

Composing two above, we show δₖ and log nₖ grow at the same rate.

theorem δₖ_Asymptotic (s t : ℝ) [PosReal s] [PosReal t] : Filter.Tendsto (fun (k : ℕ) => δₖ s t k * ρ s t / Real.log ↑(nₖ s t (k + 1))) Filter.atTop (nhds 1)

We also show that δₖ grows sub-exponentially w.r.t k.

theorem δₖ_slowGrow (s t : ℝ) [PosReal s] [PosReal t] : Filter.Tendsto (fun (k : ℕ) => δₖ s t (k + 1) / δₖ s t k) Filter.atTop (nhds 1)

With all lemmas above, we show dE grows like log.

theorem dE_Asymptotic' (s t : ℝ) [PosReal s] [PosReal t] : Filter.Tendsto (fun (n : ℝ) => dE s t n * ρ s t / Real.log n) Filter.atTop (nhds 1)

Restating dE_Asymptotic in terms of asymptotic equivalence.

theorem dE_Asymptotic (s t : ℝ) [PosReal s] [PosReal t] : Asymptotics.IsEquivalent Filter.atTop (dE s t) fun (x : ℝ) => Real.log x / ρ s t

Integrating boths sides of dE_Asymptotic, we show E is equivalent to Eℝ.

theorem E_Asymptotic (s t : ℝ) [PosReal s] [PosReal t] : Asymptotics.IsEquivalent Filter.atTop (E s t) (Eℝ s t)

To study the asymptotic behavior of w, we extend the result w_Asymtotic_int to real $s$ and $t$.

As the starter, g agrees with ξ₀, allowing us to translate the coefficient from the integer case to the real case.

theorem g_eq (s t : ℕ+) : ξ₀ s t ^ ↑t = g ↑↑s ↑↑t

A corollary of w_Asymtotic_int: the limit holds for rational $s / t$.

theorem w_Asymtotic_rat (s t : ℝ) [PosReal s] [PosReal t] (rational : s / t ∈ Set.range Rat.cast) : Filter.Tendsto (fun (n : ℝ) => wₗᵢ s t n / n) Filter.atTop (nhds (g s t))

To generalize the limit to all real s and t, we will utilize the following facts:

• g is antitone and continuous.
• w is monotone w.r.t $s$ and $t$.

To help with the proof, we define the inverse function of g w.r.t $t$, fixing $s = 1$.

noncomputable def ginv (g : ℝ) : ℝ

Equations

• ginv g = Real.log g / Real.log (1 - g)

ginv is antitone.

theorem ginv_anti : StrictAntiOn ginv (Set.Ioo 0 1)

And as expected, ginv inverts g.

theorem ginv_comp (r : ℝ) [PosReal r] : ginv (g 1 r) = r

We generalize w's asymtotic behavior to all positive $s$ and $t$

theorem w_Asymtotic' (s t : ℝ) [PosReal s] [PosReal t] : Filter.Tendsto (fun (n : ℝ) => wₗᵢ s t n / n) Filter.atTop (nhds (g s t))

Lastly, we restate w_Asymtotic in terms of asymptotic equivalence.

theorem w_Asymtotic (s t : ℝ) [PosReal s] [PosReal t] : Asymptotics.IsEquivalent Filter.atTop (wₗᵢ s t) (wℝ s t)