← Copula mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.gridCollision (n : ℕ) (x y : Fin 2 → ↑unitInterval) : ℝ

Equations

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

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.measurable_gridCollision (n : ℕ) : Measurable fun (p : (Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval)) => gridCollision n p.1 p.2

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.norm_gridCollision (n : ℕ) (x y : Fin 2 → ↑unitInterval) : ‖gridCollision n x y‖ ≤ 1

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

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.grid_collision_eq (C : Copula 2) (n : ℕ) : ∫ (p : (Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval)), gridCollision n p.1 p.2 ∂C.toMeasure.prod C.toMeasure = ∑ i : Fin ((n + 1) * (n + 1)), gridWeights C n i ^ 2

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.tendsto_grid_squares (C : Copula 2) : Filter.Tendsto (fun (n : ℕ) => ∑ i : Fin ((n + 1) * (n + 1)), gridWeights C n i ^ 2) Filter.atTop (nhds 0)

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.gridWeights_le_one (C : Copula 2) (n : ℕ) (i : Fin ((n + 1) * (n + 1))) : gridWeights C n i ≤ 1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.tendsto_grid_cubes (C : Copula 2) : Filter.Tendsto (fun (n : ℕ) => ∑ i : Fin ((n + 1) * (n + 1)), gridWeights C n i ^ 3) Filter.atTop (nhds 0)