← Mathematical handbook

noncomputable def Verification.n21Core (θ t : ℝ) : ℝ

Equations

• Verification.n21Core θ t = 1 - (1 - (1 - t) ^ θ) ^ θ⁻¹

noncomputable def Verification.n21CorePrime (θ t : ℝ) : ℝ

Equations

• Verification.n21CorePrime θ t = -(1 - t) ^ (θ - 1) * (1 - (1 - t) ^ θ) ^ (θ⁻¹ - 1)

theorem Verification.n21_inner_mem {θ t : ℝ} (hθ : 0 < θ) (ht : t ∈ Set.Icc 0 1) : 1 - (1 - t) ^ θ ∈ Set.Icc 0 1

theorem Verification.n21Core_mem {θ t : ℝ} (hθ : 0 < θ) (ht : t ∈ Set.Icc 0 1) : n21Core θ t ∈ Set.Icc 0 1

theorem Verification.n21Core_antitone {θ : ℝ} (hθ : 0 < θ) : AntitoneOn (n21Core θ) (Set.Icc 0 1)

theorem Verification.n21Core_involutive {θ t : ℝ} (hθ : 0 < θ) (ht : t ∈ Set.Icc 0 1) : n21Core θ (n21Core θ t) = t

theorem Verification.n21Core_deriv {θ t : ℝ} (hθ : 0 < θ) (ht : t ∈ Set.Ioo 0 1) : HasDerivAt (n21Core θ) (n21CorePrime θ t) t

theorem Verification.n21Core_deriv2 {θ t : ℝ} (hθ : 0 < θ) (ht : t ∈ Set.Ioo 0 1) : HasDerivAt (n21CorePrime θ) ((θ - 1) * (1 - t) ^ (θ - 2) * (1 - (1 - t) ^ θ) ^ (θ⁻¹ - 2)) t

theorem Verification.n21Core_continuous {θ : ℝ} (hθ : 0 < θ) : Continuous (n21Core θ)

theorem Verification.n21Core_convex {θ : ℝ} (hθ : 1 ≤ θ) : ConvexOn ℝ (Set.Icc 0 1) (n21Core θ)