Documentation

Verification.FrankDependence

← Mathematical handbook

noncomputable def Verification.frankSection (θ a b x : ℝ) :

Equations

Verification.frankSection θ a b x = -Real.log (a + b * Real.exp (-θ * x)) / θ

Instances For

theorem Verification.frankSection_pos {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : 0 < a + b) (θ x : ℝ) :

0 < a + b * Real.exp (-θ * x)

theorem Verification.frankSection_deriv {θ a b : ℝ} (hθ : θ ≠ 0) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : 0 < a + b) (x : ℝ) :

HasDerivAt (frankSection θ a b) (b * Real.exp (-θ * x) / (a + b * Real.exp (-θ * x))) x

theorem Verification.frankSection_concave {θ a b : ℝ} (hθ : 0 < θ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : 0 < a + b) :

ConcaveOn ℝ Set.univ (frankSection θ a b)

noncomputable def Verification.frankA (θ : ℝ) (v : ↑unitInterval) :

Equations

Verification.frankA θ v = (Real.exp (-θ * ↑v) - Real.exp (-θ)) / (1 - Real.exp (-θ))

Instances For

noncomputable def Verification.frankB (θ : ℝ) (v : ↑unitInterval) :

Equations

Verification.frankB θ v = (1 - Real.exp (-θ * ↑v)) / (1 - Real.exp (-θ))

Instances For

theorem Verification.frankAB {θ : ℝ} (hθ : 0 < θ) (v : ↑unitInterval) :

0 ≤ frankA θ v ∧ 0 ≤ frankB θ v ∧ frankA θ v + frankB θ v = 1

theorem Verification.frank_cdf_section (θ : ℝ) (hθ : 0 < θ) (u v : ↑unitInterval) :

(ProbabilityTheory.Copula.frank θ hθ).cdf ![u, v] = frankSection θ (frankA θ v) (frankB θ v) ↑u

theorem Verification.frank_positive_isSI (θ : ℝ) (hθ : 0 < θ) :

(ProbabilityTheory.Copula.frank θ hθ).IsSI

theorem Verification.frank_positive_isCI (θ : ℝ) (hθ : 0 < θ) :

(ProbabilityTheory.Copula.frank θ hθ).IsCI

theorem Verification.frank_negative_transpose (θ : ℝ) (hθ : θ < 0) :

(ProbabilityTheory.Copula.frankNegative θ hθ).transpose = ProbabilityTheory.Copula.frankNegative θ hθ

theorem Verification.frank_negative_isCD (θ : ℝ) (hθ : θ < 0) :

(ProbabilityTheory.Copula.frankNegative θ hθ).IsCD

theorem Verification.frank_positive_ne_independence (θ : ℝ) (hθ : 0 < θ) :

ProbabilityTheory.Copula.frank θ hθ ≠ ProbabilityTheory.Copula.independence 2

theorem Verification.frank_positive_not_cd (θ : ℝ) (hθ : 0 < θ) :

¬(ProbabilityTheory.Copula.frank θ hθ).IsCD

theorem Verification.frank_negative_not_ci (θ : ℝ) (hθ : θ < 0) :

¬(ProbabilityTheory.Copula.frankNegative θ hθ).IsCI

theorem Verification.frank_positive_not_nqd (θ : ℝ) (hθ : 0 < θ) :

¬(ProbabilityTheory.Copula.frank θ hθ).IsNQD

theorem Verification.frank_negative_not_pqd (θ : ℝ) (hθ : θ < 0) :

¬(ProbabilityTheory.Copula.frankNegative θ hθ).IsPQD

theorem Verification.frank_negative_not_density_tp2 (θ : ℝ) (hθ : θ < 0) :

¬(ProbabilityTheory.Copula.frankNegative θ hθ).HasMTP2Density