← Copula mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.quantize (n : ℕ) (x : ↑unitInterval) : Fin (n + 1)

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.quantize n x = ⟨⌊↑n * ↑x⌋₊, ⋯⟩

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.measurable_quantize (n : ℕ) : Measurable (quantize n)

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.eventually_quantize_lt {x y : ↑unitInterval} (h : x < y) : ∀ᶠ (n : ℕ) in Filter.atTop, quantize n x < quantize n y

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.gridCode (n : ℕ) (x : Fin 2 → ↑unitInterval) : Fin ((n + 1) * (n + 1))

Equations

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

def ProbabilityTheory.Copula.RankRegion.RhoTau.gridSwap (n : ℕ) : Equiv.Perm (Fin ((n + 1) * (n + 1)))

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.gridSwap n = finProdFinEquiv.symm.trans ((Equiv.prodComm (Fin (n + 1)) (Fin (n + 1))).trans finProdFinEquiv)

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.gridSwap_code (n : ℕ) (x : Fin 2 → ↑unitInterval) : (gridSwap n) (gridCode n x) = finProdFinEquiv (quantize n (x 1), quantize n (x 0))

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.measurable_gridCode (n : ℕ) : Measurable (gridCode n)

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.finProdFinEquiv_lt {m n : ℕ} (a b : Fin m × Fin n) (h : a.1 < b.1) : finProdFinEquiv a < finProdFinEquiv b

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.eventually_grid_order {x y : Fin 2 → ↑unitInterval} (h : x 0 ≠ y 0) : ∀ᶠ (n : ℕ) in Filter.atTop, orderSign (gridCode n x) (gridCode n y) = orderSign (x 0) (y 0)

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.eventually_grid_swap_order {x y : Fin 2 → ↑unitInterval} (h : x 1 ≠ y 1) : ∀ᶠ (n : ℕ) in Filter.atTop, orderSign ((gridSwap n) (gridCode n x)) ((gridSwap n) (gridCode n y)) = orderSign (x 1) (y 1)