← Mathematical handbook

theorem Verification.kendallTau_ofContinuousMarginals_probability (μ : MeasureTheory.ProbabilityMeasure (Fin 2 → ℝ)) (hc : ∀ (i : Fin 2), Continuous ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal μ i))) (hm : ∀ (i : Fin 2), StrictMono ↑(ProbabilityTheory.cdf (ProbabilityTheory.Copula.marginal μ i))) : (ProbabilityTheory.Copula.ofContinuousMarginals μ hc).kendallTau = 4 * ((↑μ).prod ↑μ).real {p : (Fin 2 → ℝ) × (Fin 2 → ℝ) | p.1 ≤ p.2} - 1

theorem Verification.gaussianScaleMixture_kendallTau {r : ℝ} (hr : r ∈ Set.Icc (-1) 1) (μ : MeasureTheory.ProbabilityMeasure ℝ) (s : ℝ → ℝ) (hs : Measurable s) (hp : ∀ᵐ (t : ℝ) ∂↑μ, 0 < s t) : (ProbabilityTheory.Copula.gaussianScaleMixture (bivariateCorrelation r) ⋯ ⋯ μ s hs hp).kendallTau = 2 / Real.pi * Real.arcsin r