← Mathematical handbook

Table 6: Frank Kendall tau and the first Debye function

theorem Papers.AnsariRockel2024.frank_conditionalCDF {θ : ℝ} (hθ : θ ≠ 0) (v : ↑unitInterval) : (fun (u : ↑unitInterval) => (frankSigned θ).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => Verification.frankPartial θ ↑u ↑v

theorem Papers.AnsariRockel2024.frank_kendallTau {θ : ℝ} (hθ : θ ≠ 0) : (frankSigned θ).kendallTau = 1 - 4 / θ * (1 - Verification.debyeOne θ)

theorem Papers.AnsariRockel2024.frank_kendallTau_zero : (frankSigned 0).kendallTau = 0

theorem Papers.AnsariRockel2024.frank_debyeTwo_kernel_integral {θ : ℝ} (hθ : θ ≠ 0) : Verification.debyeTwo θ = ∫ (v : ↑unitInterval), 2 * ↑v * Verification.debyeKernel (θ * ↑v)

theorem Papers.AnsariRockel2024.frank_debyeOne_neg {θ : ℝ} (hθ : θ ≠ 0) : Verification.debyeOne (-θ) = Verification.debyeOne θ + θ / 2

theorem Papers.AnsariRockel2024.frank_debyeTwo_neg {θ : ℝ} (hθ : θ ≠ 0) : Verification.debyeTwo (-θ) = Verification.debyeTwo θ + 2 * θ / 3

theorem Papers.AnsariRockel2024.frank_kendallTau_neg (θ : ℝ) : (frankSigned (-θ)).kendallTau = -(frankSigned θ).kendallTau

theorem Papers.AnsariRockel2024.frank_spearmanRho_zero : (frankSigned 0).spearmanRho = 0

theorem Papers.AnsariRockel2024.frank_spearmanRho_neg (θ : ℝ) : (frankSigned (-θ)).spearmanRho = -(frankSigned θ).spearmanRho

theorem Papers.AnsariRockel2024.frank_spearmanRho {θ : ℝ} (hθ : θ ≠ 0) : (frankSigned θ).spearmanRho = 1 - 12 / θ * (Verification.debyeOne θ - Verification.debyeTwo θ)