← Mathematical handbook

A one-dimensional Kendall integral for the actual sampled band

noncomputable def Verification.bandTauIntegrand (b : ℝ) (t : ↑unitInterval) : ℝ

Equations

• Verification.bandTauIntegrand b t = max 0 (1 - b * ↑t) ^ 2

theorem Verification.bandTauIntegrand_mem {b : ℝ} (hb : 0 ≤ b) (t : ↑unitInterval) : bandTauIntegrand b t ∈ Set.Icc 0 1

theorem Verification.diagonalBand_cdf_noise_integral (b : ℝ) (hb : 0 ≤ b) (u : ↑unitInterval) : ∫ (z : ↑unitInterval), (diagonalBand b hb).cdf (bandSample b (u, z)) = ↑u - (∫ (t : ↑unitInterval) in Set.Iic u, bandTauIntegrand b t) / 2

Average the CDF over the independent noise while holding the first rank fixed.

theorem Verification.diagonalBand_tau_integral (b : ℝ) (hb : 0 ≤ b) : (diagonalBand b hb).kendallTau = 1 - 2 * ∫ (t : ↑unitInterval), (1 - ↑t) * bandTauIntegrand b t

Kendall's tau reduces to a bounded, one-dimensional polynomial-ramp integral.