Derivative computations for the Phi function

First and second derivative computations for the entropy expressions defining the Phi functions.

First derivatives of hEntropy components

theorem KaltonRoberts.hasDerivAt_binEntropy (x : ℝ) (hx : 0 < x) (hx1 : x < 1) : HasDerivAt (fun (x : ℝ) => -x * Real.log x - (1 - x) * Real.log (1 - x)) (Real.log (1 - x) - Real.log x) x

theorem KaltonRoberts.hasDerivAt_h_entropy_second (θ x : ℝ) (hx : 0 < x) (hxθ : x < θ) : HasDerivAt (fun (x : ℝ) => θ * Real.log θ - x * Real.log x - (θ - x) * Real.log (θ - x)) (Real.log (θ - x) - Real.log x) x

theorem KaltonRoberts.hasDerivAt_neg_entropy_scaled (r x : ℝ) (hx : 0 < x) (hx1 : x < 1) : HasDerivAt (fun (x : ℝ) => r * x * Real.log x + r * (1 - x) * Real.log (1 - x)) (r * (Real.log x - Real.log (1 - x))) x

Second derivatives

theorem KaltonRoberts.hasDerivAt_binEntropy_deriv (x : ℝ) (hx : 0 < x) (hx1 : x < 1) : HasDerivAt (fun (x : ℝ) => Real.log (1 - x) - Real.log x) (-1 / (1 - x) - 1 / x) x

theorem KaltonRoberts.hasDerivAt_h_entropy_second_deriv (θ x : ℝ) (hx : 0 < x) (hxθ : x < θ) : HasDerivAt (fun (x : ℝ) => Real.log (θ - x) - Real.log x) (-1 / (θ - x) - 1 / x) x

theorem KaltonRoberts.hasDerivAt_neg_entropy_scaled_deriv (r x : ℝ) (hx : 0 < x) (hx1 : x < 1) : HasDerivAt (fun (x : ℝ) => r * (Real.log x - Real.log (1 - x))) (r * (1 / x + 1 / (1 - x))) x

Derivative of Phi

theorem KaltonRoberts.hasDerivAt_Phi (r θ x : ℝ) (hx : 0 < x) (hxθ : x < θ) (hx1 : x < 1) (hθ0 : 0 < θ) (hθ1 : θ < 1) (hr : 0 < r) : HasDerivAt (fun (x : ℝ) => Phi r θ x) (Real.log (1 - x) - Real.log x + (Real.log (θ - x) - Real.log x) + (r / θ * Real.log (r / θ) - r * Real.log r - (r / θ - r) * Real.log (r / θ - r)) + r * (Real.log x - Real.log (1 - x))) x

theorem KaltonRoberts.hasDerivAt_Phi_second (r θ x : ℝ) (hx : 0 < x) (hxθ : x < θ) (hx1 : x < 1) (_hθ0 : 0 < θ) (_hr : 2 < r) : HasDerivAt (fun (x : ℝ) => Real.log (1 - x) - Real.log x + (Real.log (θ - x) - Real.log x) + (r / θ * Real.log (r / θ) - r * Real.log r - (r / θ - r) * Real.log (r / θ - r)) + r * (Real.log x - Real.log (1 - x))) (Phi'' r θ x) x

The second derivative of Phi equals Phi'' r θ x.

Generic ConvexOn for Phi

theorem KaltonRoberts.convexOn_Phi_of_Phi''_nonneg {r θ δ α : ℝ} (hδ : 0 < δ) (hαθ : α < θ) (hθ1 : θ < 1) (hr : 2 < r) (hθ0 : 0 < θ) (hδα : δ ≤ α) (hPhi'' : ∀ (x : ℝ), δ ≤ x → x ≤ α → 0 ≤ Phi'' r θ x) : ConvexOn ℝ (Set.Icc δ α) fun (x : ℝ) => Phi r θ x