← Copula mathematical handbook

Reducing symmetric square-gap tails to a single radical integral

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.square_gap_tail_reduction (r : ℝ) (hr : r ∈ Set.Ioo 0 1) (f : ℝ → ℝ) (hf : Continuous f) (hz : ∀ t ≤ r ^ 2, f t = 0) : ∫ (p : ↑unitInterval × ↑unitInterval), f |↑p.1 ^ 2 - ↑p.2 ^ 2| = 2 * ∫ (x : ℝ) in r..1, ∫ (y : ℝ) in 0..√(x ^ 2 - r ^ 2), f (x ^ 2 - y ^ 2)

A continuous function vanishing below r² has only the two symmetric triangular tails.