Inverse function φ

We explore more about the function φ, which is the "inverse function" of dE.

Main statements

• φ_inv shows the inverse relation between φ and dE.
• φ_neg and φ_rec characterize the function φ as generated by a recurrence relation.
• φ_bound shows φ grows exponentially and gives a bound on the coefficient.

φ is simply defined as Jceiled shifted by 1.

noncomputable def φ (s t : ℝ) [PosReal s] [PosReal t] (δ : ℝ) : ℕ

Equations

• φ s t δ = 1 + Jceiled s t δ

theorem φ_mono (s t : ℝ) [PosReal s] [PosReal t] : Monotone (φ s t)

theorem φ_pos (s t : ℝ) [PosReal s] [PosReal t] (δ : ℝ) : 0 < φ s t δ

φ is also a stair-case like function. It doesn't really have a inverse function in the strict sense, but we can describe its relation ship with dE by the following.

noncomputable def δceiledByφ (s t n : ℝ) [PosReal s] [PosReal t] : Set ℝ

Equations

• δceiledByφ s t n = {δ : ℝ | ↑(φ s t δ) ≤ n}

theorem φ_inv (s t n : ℝ) (n1 : n ≥ 1) [PosReal s] [PosReal t] : δceiledByφ s t n = Set.Iio (dE s t n)

Another way to show this, is that φ maps δₖ back to nₖ, though the index k is shifted due to our convention of close/open intervals.

theorem φδₖ (s t : ℝ) (k : ℕ) [PosReal s] [PosReal t] : φ s t (δₖ s t k) = nₖ s t (k + 1)

Analog to w_eq/w_lt/w_gt lemmas, φ maps δₖ - t back to wₖ (again with shifted k).

theorem φδₖt (s t : ℝ) (k : ℕ) [PosReal s] [PosReal t] : φ s t (δₖ s t k - t) = wₖ s t (k + 1)

Two lemmas similar to Jline_s and Jline_t

theorem Jceiled_s (s t δ : ℝ) [PosReal s] [PosReal t] : Jceiled s t (δ - s) = ∑ x ∈ (Λceiled s t δ).toFinset, match x with | (p, q) => shut p (Jₚ (p - 1, q))

theorem Jceiled_t (s t δ : ℝ) [PosReal s] [PosReal t] : Jceiled s t (δ - t) = ∑ x ∈ (Λceiled s t δ).toFinset, match x with | (p, q) => shut q (Jₚ (p, q - 1))

φ(δ) is the unique function that satifies the following conditions:

• φ(< 0) = 1
• φ(δ ≥ 0) = φ(δ - s) + φ(δ - t)

theorem φ_neg (s t δ : ℝ) (dneg : δ < 0) [PosReal s] [PosReal t] : φ s t δ = 1

theorem φ_rec (s t δ : ℝ) (dpos : δ ≥ 0) [PosReal s] [PosReal t] : φ s t δ = φ s t (δ - s) + φ s t (δ - t)

φ grows as fast as exponential, and the rate is ρ. Here we show the exponential growth with an undetermined, but bounded coefficient.

theorem φ_bound (s t x : ℝ) (h : -max s t ≤ x) [PosReal s] [PosReal t] : ↑(φ s t x) ∈ Set.Icc (Real.exp (ρ s t * x)) (Real.exp (ρ s t * (x + max s t)))