← Mathematical handbook

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

Equations

• Verification.frankDen θ u v = 1 - Real.exp (-θ) - (1 - Real.exp (-θ * u)) * (1 - Real.exp (-θ * v))

theorem Verification.frankDen_pos {θ : ℝ} (hθ : 0 < θ) {u v : ℝ} (hu : u ∈ Set.Icc 0 1) (hv : v ∈ Set.Icc 0 1) : 0 < frankDen θ u v

noncomputable def Verification.frankDensity (θ : ℝ) (x : Fin 2 → ↑unitInterval) : ℝ

Equations

• Verification.frankDensity θ x = θ * (1 - Real.exp (-θ)) * Real.exp (-θ * ↑(x 0)) * Real.exp (-θ * ↑(x 1)) / Verification.frankDen θ ↑(x 0) ↑(x 1) ^ 2

theorem Verification.frankDensity_nonneg {θ : ℝ} (hθ : 0 < θ) (x : Fin 2 → ↑unitInterval) : 0 ≤ frankDensity θ x

theorem Verification.continuous_frankDensity {θ : ℝ} (hθ : 0 < θ) : Continuous (frankDensity θ)

theorem Verification.frankDen_inv_tp2 {θ : ℝ} (hθ : 0 < θ) : ProbabilityTheory.IsTP2 fun (u v : ↑unitInterval) => 1 / frankDen θ ↑u ↑v

theorem Verification.isMTP2_frankDensity {θ : ℝ} (hθ : 0 < θ) : ProbabilityTheory.IsMTP2 (frankDensity θ)

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

Equations

• Verification.frankPartial θ u v = Real.exp (-θ * u) * (1 - Real.exp (-θ * v)) / Verification.frankDen θ u v

theorem Verification.frank_partial_derivative {θ u v : ℝ} (hd : frankDen θ u v ≠ 0) : HasDerivAt (fun (y : ℝ) => frankPartial θ u y) (θ * (1 - Real.exp (-θ)) * Real.exp (-θ * u) * Real.exp (-θ * v) / frankDen θ u v ^ 2) v

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

Equations

• Verification.frankRealCDF θ u v = -Real.log (Verification.frankDen θ u v / (1 - Real.exp (-θ))) / θ

theorem Verification.frank_cdf_derivative {θ u v : ℝ} (hθ : θ ≠ 0) (hd : frankDen θ u v ≠ 0) (he : 1 - Real.exp (-θ) ≠ 0) : HasDerivAt (fun (x : ℝ) => frankRealCDF θ x v) (frankPartial θ u v) u

theorem Verification.integral_frankDensity_second {θ : ℝ} (hθ : 0 < θ) (u v : ↑unitInterval) : ∫ (y : ↑unitInterval) in Set.Iic v, frankDensity θ ![u, y] = frankPartial θ ↑u ↑v

theorem Verification.integral_frankPartial_first {θ : ℝ} (hθ : 0 < θ) (u v : ↑unitInterval) : ∫ (x : ↑unitInterval) in Set.Iic u, frankPartial θ ↑x ↑v = frankRealCDF θ ↑u ↑v

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

theorem Verification.frank_toMeasure_density {θ : ℝ} (hθ : 0 < θ) : (ProbabilityTheory.Copula.frank θ hθ).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (frankDensity θ x)

theorem Verification.frank_hasMTP2Density {θ : ℝ} (hθ : 0 < θ) : (ProbabilityTheory.Copula.frank θ hθ).HasMTP2Density