← Mathematical handbook

noncomputable def Verification.frankOrderCoordinate (u : ↑unitInterval) : ↑unitInterval

Equations

• Verification.frankOrderCoordinate u = ⟨2 ^ ↑u - 1, ⋯⟩

theorem Verification.frank_log_base_pos {θ : ℝ} (hθ : θ ≠ 0) (u v : ↑unitInterval) : 0 < 1 + (Real.exp (-θ * ↑u) - 1) * (Real.exp (-θ * ↑v) - 1) / (Real.exp (-θ) - 1)

theorem Verification.frank_nelsen17_identity {θ : ℝ} (hθ : θ ≠ 0) (u v : ↑unitInterval) : frankRegularCDF (↑u) (↑v) θ = Real.log (1 + (nelsen17 (θ / Real.log 2) ⋯).cdf ![frankOrderCoordinate u, frankOrderCoordinate v]) / Real.log 2

theorem Verification.frankRegularCDF_monotone_nonzero {θ η : ℝ} (hθ : θ ≠ 0) (hη : η ≠ 0) (hθη : θ ≤ η) (u v : ↑unitInterval) : frankRegularCDF (↑u) (↑v) θ ≤ frankRegularCDF (↑u) (↑v) η