← Mathematical handbook

theorem Verification.convexOn_clip_left {f : ℝ → ℝ} {c : ℝ} (hc : ConvexOn ℝ (Set.Ici c) f) (hm : MonotoneOn f (Set.Ici c)) : ConvexOn ℝ Set.univ fun (x : ℝ) => f (max c x)

noncomputable def Verification.powerCut (θ a k : ℝ) : ℝ

Equations

• Verification.powerCut θ a k = (a / k) ^ θ⁻¹

noncomputable def Verification.powerBranch (θ a k x : ℝ) : ℝ

Equations

• Verification.powerBranch θ a k x = (k * x ^ θ - a) ^ θ⁻¹

theorem Verification.powerCut_nonneg {a k : ℝ} (ha : 0 ≤ a) (hk : 0 < k) (θ : ℝ) : 0 ≤ powerCut θ a k

theorem Verification.powerCut_pow {θ a k : ℝ} (hθ : 0 < θ) (ha : 0 ≤ a) (hk : 0 < k) : powerCut θ a k ^ θ = a / k

theorem Verification.powerBranch_base_pos {θ a k x : ℝ} (hθ : 0 < θ) (ha : 0 ≤ a) (hk : 0 < k) (hx : powerCut θ a k < x) : 0 < k * x ^ θ - a

theorem Verification.powerBranch_deriv {θ a k x : ℝ} (hθ : 0 < θ) (ha : 0 ≤ a) (hk : 0 < k) (hx : powerCut θ a k < x) : HasDerivAt (powerBranch θ a k) (k * (k - a / x ^ θ) ^ (θ⁻¹ - 1)) x

theorem Verification.powerBranch_convex {θ a k : ℝ} (hθ : 0 < θ) (hθ1 : θ ≤ 1) (ha : 0 ≤ a) (hk : 0 < k) : ConvexOn ℝ (Set.Ici (powerCut θ a k)) (powerBranch θ a k)

theorem Verification.truncatedPower_convex {θ a k : ℝ} (hθ : 0 < θ) (hθ1 : θ ≤ 1) (ha : 0 ≤ a) (hk : 0 < k) : ConvexOn ℝ (Set.Ici 0) fun (x : ℝ) => max 0 (k * x ^ θ - a) ^ θ⁻¹