Documentation

Verification.Nelsen21Comparison

← Mathematical handbook

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

Equations

Verification.n21Y θ t = 1 - (1 - t) ^ θ

Instances For

noncomputable def Verification.n21Z (θ η t : ℝ) :

Equations

Verification.n21Z θ η t = 1 - Verification.n21Y θ t ^ (η / θ)

Instances For

noncomputable def Verification.n21Comparison (θ η t : ℝ) :

Equations

Verification.n21Comparison θ η t = 1 - Verification.n21Z θ η t ^ η⁻¹

Instances For

noncomputable def Verification.n21ComparisonPrime (θ η t : ℝ) :

Equations

Verification.n21ComparisonPrime θ η t = (1 - t) ^ (θ - 1) * Verification.n21Y θ t ^ (η / θ - 1) * Verification.n21Z θ η t ^ (η⁻¹ - 1)

Instances For

noncomputable def Verification.n21ComparisonLog (θ η t : ℝ) :

Equations

Verification.n21ComparisonLog θ η t = (θ - 1) * Real.log (1 - t) + (η / θ - 1) * Real.log (Verification.n21Y θ t) + (η⁻¹ - 1) * Real.log (Verification.n21Z θ η t)

Instances For

theorem Verification.n21YZ_pos {θ η t : ℝ} (hθ : 0 < θ) (hη : 0 < η) (ht : t ∈ Set.Ioo 0 1) :

0 < n21Y θ t ∧ 0 < n21Z θ η t

theorem Verification.n21Y_deriv {θ t : ℝ} (ht : t < 1) :

HasDerivAt (n21Y θ) (θ * (1 - t) ^ (θ - 1)) t

theorem Verification.n21Z_deriv {θ η t : ℝ} (hθ : 0 < θ) (hη : 0 < η) (ht : t ∈ Set.Ioo 0 1) :

HasDerivAt (n21Z θ η) (-η * (1 - t) ^ (θ - 1) * n21Y θ t ^ (η / θ - 1)) t

theorem Verification.n21Comparison_deriv {θ η t : ℝ} (hθ : 0 < θ) (hη : 0 < η) (ht : t ∈ Set.Ioo 0 1) :

HasDerivAt (n21Comparison θ η) (n21ComparisonPrime θ η t) t

theorem Verification.n21ComparisonLog_deriv {θ η t : ℝ} (hθ : 0 < θ) (hη : 0 < η) (ht : t ∈ Set.Ioo 0 1) :

HasDerivAt (n21ComparisonLog θ η) ((η - θ - (η - 1) * n21Y θ t + (θ - 1) * n21Y θ t ^ (η / θ)) / ((1 - t) * n21Y θ t * n21Z θ η t)) t

theorem Verification.n21ComparisonLog_monotone {θ η : ℝ} (hθ : 1 ≤ θ) (hθη : θ ≤ η) :

MonotoneOn (n21ComparisonLog θ η) (Set.Ioo 0 1)

theorem Verification.n21ComparisonPrime_exp {θ η t : ℝ} (hθ : 0 < θ) (hη : 0 < η) (ht : t ∈ Set.Ioo 0 1) :

n21ComparisonPrime θ η t = Real.exp (n21ComparisonLog θ η t)

theorem Verification.n21Comparison_convex {θ η : ℝ} (hθ : 1 ≤ θ) (hθη : θ ≤ η) :

ConvexOn ℝ (Set.Icc 0 1) (n21Comparison θ η)

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

n21Comparison θ η t = n21Core η (n21Core θ t)

theorem Verification.n21Comparison_zero {θ η : ℝ} (hθ : 0 < θ) (hη : 0 < η) :

n21Comparison θ η 0 = 0

theorem Verification.n21Comparison_superadd {θ η s t : ℝ} (hθ : 1 ≤ θ) (hθη : θ ≤ η) (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t ≤ 1) :

n21Comparison θ η s + n21Comparison θ η t ≤ n21Comparison θ η (s + t)