← Mathematical handbook

theorem Verification.frank_exp_den_ne_zero {θ : ℝ} (hθ : θ ≠ 0) : 1 - Real.exp (-θ) ≠ 0

theorem Verification.frankDen_ne_zero {θ : ℝ} (hθ : θ ≠ 0) (u v : ↑unitInterval) : frankDen θ ↑u ↑v ≠ 0

theorem Verification.frankRegularCDF_eq_real {θ : ℝ} (hθ : θ ≠ 0) (u v : ℝ) : frankRegularCDF u v θ = frankRealCDF θ u v

theorem Verification.frank_conditionalCDF_of_cdf (C : ProbabilityTheory.Copula 2) {θ : ℝ} (hθ : θ ≠ 0) (hc : ∀ (u v : ↑unitInterval), C.cdf ![u, v] = frankRealCDF θ ↑u ↑v) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => C.conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => frankPartial θ ↑u ↑v

theorem Verification.frank_kendallTau_integral_of_cdf (C : ProbabilityTheory.Copula 2) {θ : ℝ} (hθ : θ ≠ 0) (hc : ∀ (u v : ↑unitInterval), C.cdf ![u, v] = frankRealCDF θ ↑u ↑v) : C.kendallTau = 1 - 4 * ∫ (v : ↑unitInterval) (u : ↑unitInterval), frankPartial θ ↑u ↑v * frankPartial θ ↑v ↑u