Continuous biased bisect problem

We explore a variation of the original biased bisect problem. We find a function $E: ℝ → ℝ$ that satisfies the functional equation $$ E(n) = \min_{0 < w < n} \{E(w) + E(n - w) + w t + (n - w) s\} $$ for all positive $n$. We will see that $E(n) = n \log n/ρ$, and the optimal strategy is linear to $n$.

Main statements

• IsOptimalCostℝ, IsOptimalStratℝ are the target properties of the solution.
• Eℝ is the optimal cost function.
  • Eℝ_IsOptimalCostℝ verifies this is the solution to IsOptimalCostℝ.
  • ρ is the coefficient in Eℝ.
• wℝ is the optimal strategy function.
  • wℝ_IsOptimalStratℝ verifies this is the solution to IsOptimalStratℝ.
  • g is the coefficient in wℝ.

ρ is the unique real solution to the equation $ρf(ρ) = 1$, where $ρf(ρ) = e^{-s ρ} + e^{-t ρ}$.

noncomputable def ρf (s t : ℝ) [PosReal s] [PosReal t] (ρ : ℝ) : ℝ

Equations

• ρf s t ρ = Real.exp (-s * ρ) + Real.exp (-t * ρ)

theorem ρf_anti (s t : ℝ) [PosReal s] [PosReal t] : StrictAnti (ρf s t)

theorem ρ_exist (s t : ℝ) [PosReal s] [PosReal t] : ∃! ρ : ℝ, ρ ≥ 0 ∧ ρf s t ρ = 1

noncomputable def ρ (s t : ℝ) [PosReal s] [PosReal t] : ℝ

Equations

• ρ s t = Exists.choose ⋯

theorem ρ_satisfies (s t : ℝ) [PosReal s] [PosReal t] : ρf s t (ρ s t) = 1

theorem ρ_range (s t : ℝ) [PosReal s] [PosReal t] : 0 < ρ s t

g is the unique real solution to the equation $g^s = (1-g)^t$.

theorem g_exist (s t : ℝ) [PosReal s] [PosReal t] : ∃! g : ℝ, g ∈ Set.Icc 0 1 ∧ g ^ s = (1 - g) ^ t

noncomputable def g (s t : ℝ) [PosReal s] [PosReal t] : ℝ

Equations

• g s t = Exists.choose ⋯

theorem g_satisfies (s t : ℝ) [PosReal s] [PosReal t] : g s t ^ s = (1 - g s t) ^ t

theorem g_range (s t : ℝ) [PosReal s] [PosReal t] : g s t ∈ Set.Ioo 0 1

theorem g_unique (s t : ℝ) [PosReal s] [PosReal t] (g' : ℝ) (grange : g' ∈ Set.Icc 0 1) (satisfies : g' ^ s = (1 - g') ^ t) : g' = g s t

g is homogeneous.

theorem g_homo (s t l : ℝ) [PosReal s] [PosReal t] [PosReal l] : g s t = g (l * s) (l * t)

The two coefficients ρ and g are closely related

theorem g_ρ_agree (s t : ℝ) [PosReal s] [PosReal t] : g s t = Real.exp (-t * ρ s t)

We define the goal of the continuous version of the problem.

def IsOptimalCostℝ (Efun : ℝ → ℝ) (s t : ℝ) : Prop

Equations

• IsOptimalCostℝ Efun s t = ∀ n > 0, IsLeast (StratEval Efun s t n '' Set.Ioo 0 n) (Efun n)

def IsOptimalStratℝ (Efun : ℝ → ℝ) (wfun : ℝ → Set ℝ) (s t : ℝ) : Prop

Equations

• IsOptimalStratℝ Efun wfun s t = ∀ n > 0, ∀ w ∈ Set.Ioo 0 n, StratEval Efun s t n w = Efun n ↔ w ∈ wfun n

The proposed solution Eℝ and wℝ are simple functions with coefficients ρ and g.

noncomputable def Eℝ (s t : ℝ) [PosReal s] [PosReal t] : ℝ → ℝ

Equations

• Eℝ s t n = n * Real.log n / ρ s t

noncomputable def wℝ (s t : ℝ) [PosReal s] [PosReal t] : ℝ → ℝ

Equations

• wℝ s t x✝ = g s t * x✝

We also verify wℝ is always between 0 and n

theorem wℝ_range (s t : ℝ) [PosReal s] [PosReal t] (n : ℝ) (npos : 0 < n) : wℝ s t n ∈ Set.Ioo 0 n

Similar to the discrete problem, we define the auxiliary Dℝ function and discuss its derivative. It turns out Dℝ is a convex function with a unique minimum.

noncomputable def Dℝ (s t : ℝ) [PosReal s] [PosReal t] (n w : ℝ) : ℝ

Equations

• Dℝ s t n w = Eℝ s t w + Eℝ s t (n - w) + t * w + s * (n - w)

noncomputable def D'ℝ (s t : ℝ) [PosReal s] [PosReal t] (n w : ℝ) : ℝ

Equations

• D'ℝ s t n w = (Real.log w - Real.log (n - w)) / ρ s t + t - s

theorem Dℝ_derive (s t : ℝ) [PosReal s] [PosReal t] (n w : ℝ) (wleft : 0 < w) (wright : w < n) : HasDerivAt (Dℝ s t n) (D'ℝ s t n w) w

theorem D'ℝ_mono (s t : ℝ) [PosReal s] [PosReal t] (n : ℝ) : StrictMonoOn (D'ℝ s t n) (Set.Ioo 0 n)

theorem D'ℝ_continuous (s t : ℝ) [PosReal s] [PosReal t] (n : ℝ) : ContinuousOn (D'ℝ s t n) (Set.Ioo 0 n)

theorem D'ℝ_zero (s t : ℝ) [PosReal s] [PosReal t] (n : ℝ) (npos : 0 < n) : D'ℝ s t n (wℝ s t n) = 0

theorem Dℝ_left (s t : ℝ) [PosReal s] [PosReal t] (n w : ℝ) (wleft : 0 < w) (wright : w < wℝ s t n) : Dℝ s t n (wℝ s t n) < Dℝ s t n w

theorem Dℝ_right (s t : ℝ) [PosReal s] [PosReal t] (n w : ℝ) (wleft : wℝ s t n < w) (wright : w < n) : Dℝ s t n (wℝ s t n) < Dℝ s t n w

theorem Dℝ_min (s t : ℝ) [PosReal s] [PosReal t] (n : ℝ) (npos : 0 < n) : Dℝ s t n (wℝ s t n) = Eℝ s t n

Finally, we verify Eℝ and wℝ are indeed the solution.

theorem Eℝ_IsOptimalCostℝ (s t : ℝ) [PosReal s] [PosReal t] : IsOptimalCostℝ (Eℝ s t) s t

theorem wℝ_IsOptimalStratℝ (s t : ℝ) [PosReal s] [PosReal t] : IsOptimalStratℝ (Eℝ s t) (fun (n : ℝ) => {wℝ s t n}) s t