← Mathematical handbook

Rectangle probabilities and increasing distribution functions

Rectangle increments use lower endpoints on the selected coordinates, hence the sign is (-1)^s.card. The probability identity requires ordered endpoints. The empty-dimensional rectangle has probability one.

def ProbabilityTheory.Copula.corner {d : ℕ} (a b : Fin d → ↑unitInterval) (s : Finset (Fin d)) (i : Fin d) : ↑unitInterval

A corner of a rectangle, choosing the lower endpoint on s.

Equations

• ProbabilityTheory.Copula.corner a b s i = if i ∈ s then a i else b i

@[simp]

theorem ProbabilityTheory.Copula.corner_empty {d : ℕ} (a b : Fin d → ↑unitInterval) : corner a b ∅ = b

def ProbabilityTheory.Copula.partialIncrement {d : ℕ} (F : (Fin d → ↑unitInterval) → ℝ) (a b : Fin d → ↑unitInterval) (s : Finset (Fin d)) : ℝ

Apply finite differences in the coordinates of s.

Equations

• ProbabilityTheory.Copula.partialIncrement F a b s = ∑ t ∈ s.powerset, (-1) ^ t.card * F (ProbabilityTheory.Copula.corner a b t)

def ProbabilityTheory.Copula.rectangleIncrement {d : ℕ} (F : (Fin d → ↑unitInterval) → ℝ) (a b : Fin d → ↑unitInterval) : ℝ

The alternating sum of a function over all corners of a rectangle.

Equations

• ProbabilityTheory.Copula.rectangleIncrement F a b = ProbabilityTheory.Copula.partialIncrement F a b Finset.univ

@[simp]

theorem ProbabilityTheory.Copula.partialIncrement_empty {d : ℕ} (F : (Fin d → ↑unitInterval) → ℝ) (a b : Fin d → ↑unitInterval) : partialIncrement F a b ∅ = F b

theorem ProbabilityTheory.Copula.partialIncrement_insert {d : ℕ} (F : (Fin d → ↑unitInterval) → ℝ) (a b : Fin d → ↑unitInterval) (s : Finset (Fin d)) (i : Fin d) (hi : i ∉ s) : partialIncrement F a b (insert i s) = partialIncrement F a b s - partialIncrement F a (Function.update b i (a i)) s

theorem ProbabilityTheory.Copula.partialIncrement_singleton {d : ℕ} (F : (Fin d → ↑unitInterval) → ℝ) (a b : Fin d → ↑unitInterval) (i : Fin d) : partialIncrement F a b {i} = F b - F (Function.update b i (a i))

theorem ProbabilityTheory.Copula.rectangleIncrement_two (F : (Fin 2 → ↑unitInterval) → ℝ) (a b : Fin 2 → ↑unitInterval) : rectangleIncrement F a b = F b - F ![a 0, b 1] - F ![b 0, a 1] + F a

The familiar four-term increment in dimension two.

theorem ProbabilityTheory.Copula.rectangleIncrement_cdf {d : ℕ} (C : Copula d) (a b : Fin d → ↑unitInterval) (hab : a ≤ b) : rectangleIncrement C.cdf a b = C.toMeasure.real (Set.univ.pi fun (i : Fin d) => Set.Ioc (a i) (b i))

The alternating CDF sum equals the probability of the half-open rectangle.

theorem ProbabilityTheory.Copula.rectangleIncrement_cdf_nonneg {d : ℕ} (C : Copula d) (a b : Fin d → ↑unitInterval) (hab : a ≤ b) : 0 ≤ rectangleIncrement C.cdf a b

Nonnegative rectangle increments: the classical d-increasing property.

theorem ProbabilityTheory.Copula.measureReal_rectangle_two (C : Copula 2) (a b : Fin 2 → ↑unitInterval) (hab : a ≤ b) : C.toMeasure.real (Set.univ.pi fun (i : Fin 2) => Set.Ioc (a i) (b i)) = C.cdf b - C.cdf ![a 0, b 1] - C.cdf ![b 0, a 1] + C.cdf a

Bivariate rectangle probabilities written as four CDF evaluations.