← Copula mathematical handbook

Proposition 3.3: the six-strip upper seed

These are exactly the six positive-slope segments in the paper, including the degenerate endpoint shuffles. All coefficients use the resulting copula.

noncomputable def ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.upperSeedStrip (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 4)) (i : Fin 6) : Common.ShuffleStrip

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.upperSeedShuffle (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 4)) : Common.PositiveShuffle 6

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.upperSeed (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 4)) : Copula 2

Equations

• ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.upperSeed q hq = (ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.upperSeedShuffle q hq).copula

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.upperSeed_footrule (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 4)) : (upperSeed q hq).spearmanFootrule = 12 * q ^ 2 - 1 / 2

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.upperSeed_beta (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 4)) : (upperSeed q hq).blomqvistBeta = 8 * q - 1

def ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.upperSeedPermutation : Equiv.Perm (Fin 6)

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.upperSeed_tau (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 4)) : (upperSeed q hq).kendallTau = 8 * q ^ 2

theorem ProbabilityTheory.Copula.RankRegion.TauFootruleBeta.upperSeed_coefficients (q : ℝ) (hq : q ∈ Set.Icc 0 (1 / 4)) : (upperSeed q hq).kendallTau = 8 * q ^ 2 ∧ (upperSeed q hq).spearmanFootrule = 12 * q ^ 2 - 1 / 2 ∧ (upperSeed q hq).blomqvistBeta = 8 * q - 1