← Copula mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.gridWeights (C : Copula 2) (n : ℕ) (i : Fin ((n + 1) * (n + 1))) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.RhoTau.gridWeights C n = ProbabilityTheory.Copula.RankRegion.RhoTau.finiteWeight C.toMeasure (ProbabilityTheory.Copula.RankRegion.RhoTau.gridCode n)

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

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.gridWeights_sum (C : Copula 2) (n : ℕ) : ∑ i : Fin ((n + 1) * (n + 1)), gridWeights C n i = 1

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

Equations

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

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoTau.gridSecond (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_gridFirst (n : ℕ) : Measurable fun (p : (Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval)) => gridFirst n p.1 p.2

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

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

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

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.norm_gridProduct (n : ℕ) (x y : Fin 2 → ↑unitInterval) : ‖gridFirst n x y * gridSecond n x y‖ ≤ 1

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.tendsto_gridFirst_mean (C : Copula 2) (x : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (n : ℕ) => ∫ (y : Fin 2 → ↑unitInterval), gridFirst n x y ∂C.toMeasure) Filter.atTop (nhds (1 - 2 * ↑(x 0)))

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.tendsto_gridSecond_mean (C : Copula 2) (x : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (n : ℕ) => ∫ (y : Fin 2 → ↑unitInterval), gridSecond n x y ∂C.toMeasure) Filter.atTop (nhds (1 - 2 * ↑(x 1)))

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.tendsto_grid_rank_moment (C : Copula 2) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : Fin 2 → ↑unitInterval), (∫ (y : Fin 2 → ↑unitInterval), gridFirst n x y ∂C.toMeasure) * ∫ (y : Fin 2 → ↑unitInterval), gridSecond n x y ∂C.toMeasure ∂C.toMeasure) Filter.atTop (nhds (∫ (x : Fin 2 → ↑unitInterval), (1 - 2 * ↑(x 0)) * (1 - 2 * ↑(x 1)) ∂C.toMeasure))

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.tendsto_grid_pair_moment (C : Copula 2) : Filter.Tendsto (fun (n : ℕ) => ∫ (p : (Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval)), gridFirst n p.1 p.2 * gridSecond n p.1 p.2 ∂C.toMeasure.prod C.toMeasure) Filter.atTop (nhds C.kendallTau)

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.grid_pair_moment_eq (C : Copula 2) (n : ℕ) : ∫ (p : (Fin 2 → ↑unitInterval) × (Fin 2 → ↑unitInterval)), gridFirst n p.1 p.2 * gridSecond n p.1 p.2 ∂C.toMeasure.prod C.toMeasure = weighted2 (gridWeights C n) fun (i j : Fin ((n + 1) * (n + 1))) => orderSign i j * orderSign ((gridSwap n) i) ((gridSwap n) j)

theorem ProbabilityTheory.Copula.RankRegion.RhoTau.grid_rank_moment_eq (C : Copula 2) (n : ℕ) : ∫ (x : Fin 2 → ↑unitInterval), (∫ (y : Fin 2 → ↑unitInterval), gridFirst n x y ∂C.toMeasure) * ∫ (y : Fin 2 → ↑unitInterval), gridSecond n x y ∂C.toMeasure ∂C.toMeasure = ∑ i : Fin ((n + 1) * (n + 1)), (gridWeights C n i * ∑ j : Fin ((n + 1) * (n + 1)), orderSign i j * gridWeights C n j) * ∑ k : Fin ((n + 1) * (n + 1)), orderSign ((gridSwap n) i) ((gridSwap n) k) * gridWeights C n k