Documentation

Copula.Rank.Region.MeanVariance.Support.EqualBlocks

← Copula mathematical handbook

Equal diagonal blocks of every positive size #

The index n represents n+1 cells, so no zero-cell convention is needed.

noncomputable def ProbabilityTheory.Copula.RankRegion.MeanVariance.Support.equalSplit (n : ℕ) :

↑unitInterval

Equations

ProbabilityTheory.Copula.RankRegion.MeanVariance.Support.equalSplit n = ⟨1 / (↑n + 2), ⋯⟩

Instances For

noncomputable def ProbabilityTheory.Copula.RankRegion.MeanVariance.Support.equalBlocks :

ℕ → Copula 2 → Copula 2

Equations

One or more equations did not get rendered due to their size.
ProbabilityTheory.Copula.RankRegion.MeanVariance.Support.equalBlocks 0 x✝ = x✝

Instances For

theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.Support.equalBlocks_rho (n : ℕ) (C : Copula 2) :

(equalBlocks n C).spearmanRho = 1 - (1 - C.spearmanRho) / (↑n + 1) ^ 2

theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.Support.equalBlocks_tau (n : ℕ) (C : Copula 2) :

(equalBlocks n C).kendallTau = 1 - (1 - C.kendallTau) / (↑n + 1)

theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.Support.equalBlocks_footrule (n : ℕ) (C : Copula 2) :

(equalBlocks n C).spearmanFootrule = 1 - (1 - C.spearmanFootrule) / (↑n + 1)

theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.Support.HasFunctionalWitness.equalBlocks {C : Copula 2} (hC : HasFunctionalWitness C) (n : ℕ) :

HasFunctionalWitness (Support.equalBlocks n C)

theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.Support.equalBlocks_lower_tail (C : Copula 2) {l : ℝ} (hC : C.HasLowerTailDependence l) (n : ℕ) :

(equalBlocks n C).HasLowerTailDependence l

theorem ProbabilityTheory.Copula.RankRegion.MeanVariance.Support.equalBlocks_upper_tail (C : Copula 2) {l : ℝ} (hC : C.HasUpperTailDependence l) (n : ℕ) :

(equalBlocks n C).HasUpperTailDependence l