← Mathematical handbook

noncomputable def Verification.frankExpSlope (x θ : ℝ) : ℝ

Equations

• Verification.frankExpSlope x θ = dslope (fun (t : ℝ) => Real.exp (-t * x)) 0 θ

theorem Verification.frankExpSlope_zero (x : ℝ) : frankExpSlope x 0 = -x

theorem Verification.continuousAt_frankExpSlope (x : ℝ) : ContinuousAt (frankExpSlope x) 0

theorem Verification.frankExpSlope_ne {θ : ℝ} (hθ : θ ≠ 0) (x : ℝ) : frankExpSlope x θ = (Real.exp (-θ * x) - 1) / θ

noncomputable def Verification.frankSlopeQuotient (u v θ : ℝ) : ℝ

Equations

• Verification.frankSlopeQuotient u v θ = Verification.frankExpSlope u θ * Verification.frankExpSlope v θ / Verification.frankExpSlope 1 θ

theorem Verification.frankSlopeQuotient_zero (u v : ℝ) : frankSlopeQuotient u v 0 = -u * v

theorem Verification.continuousAt_frankSlopeQuotient (u v : ℝ) : ContinuousAt (frankSlopeQuotient u v) 0

noncomputable def Verification.frankRegularCDF (u v θ : ℝ) : ℝ

Equations

• Verification.frankRegularCDF u v θ = -dslope Real.log 1 (1 + θ * Verification.frankSlopeQuotient u v θ) * Verification.frankSlopeQuotient u v θ

theorem Verification.frankRegularCDF_zero (u v : ℝ) : frankRegularCDF u v 0 = u * v

theorem Verification.continuousAt_frankRegularCDF (u v : ℝ) : ContinuousAt (frankRegularCDF u v) 0

theorem Verification.frankRegularCDF_formula {θ : ℝ} (hθ : θ ≠ 0) (u v : ℝ) : frankRegularCDF u v θ = -Real.log (1 + (Real.exp (-θ * u) - 1) * (Real.exp (-θ * v) - 1) / (Real.exp (-θ) - 1)) / θ

theorem Verification.frankRegularCDF_positive (θ : ℝ) (hθ : 0 < θ) (u v : ↑unitInterval) : frankRegularCDF (↑u) (↑v) θ = (ProbabilityTheory.Copula.frank θ hθ).cdf ![u, v]

theorem Verification.frankRegularCDF_negative (θ : ℝ) (hθ : θ < 0) (u v : ↑unitInterval) : frankRegularCDF (↑u) (↑v) θ = (ProbabilityTheory.Copula.frankNegative θ hθ).cdf ![u, v]