← Copula mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.gridTau (C : Copula 2) (n : ℕ) : ℝ

Equations

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

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.gridRho (C : Copula 2) (n : ℕ) : ℝ

Equations

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

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.tendsto_gridTau (C : Copula 2) : Filter.Tendsto (gridTau C) Filter.atTop (nhds C.kendallTau)

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.tendsto_gridRho (C : Copula 2) : Filter.Tendsto (gridRho C) Filter.atTop (nhds C.spearmanRho)

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.grid_prototype (C : Copula 2) (n : ℕ) : ∃ (p : LowerParameter), p.tau = gridTau C n ∧ p.rho ≤ gridRho C n

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.gridTau_mem (C : Copula 2) (n : ℕ) : gridTau C n ∈ Set.Icc (-1) 1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.boundaryMap_grid_le (C : Copula 2) (n : ℕ) : ↑(boundaryMap ⟨gridTau C n, ⋯⟩) ≤ gridRho C n

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.boundaryMap_le_rho (C : Copula 2) : ↑(boundaryMap ⟨C.kendallTau, ⋯⟩) ≤ C.spearmanRho

The universal sharp Schreyer–Paulin–Trutschnig lower bound.

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.universal_lower (C : Copula 2) : ∃ (p : LowerParameter), p.tau = C.kendallTau ∧ p.rho ≤ C.spearmanRho