← Copula mathematical handbook

Straight shuffles of M from weight vectors with zero entries

Nelsen, An Introduction to Copulas, 2nd ed., §3.2.3, describes a straight shuffle of M by a partition of [0,1] into consecutive source intervals together with a permutation that puts the intervals into a new order. In approximation arguments (Nelsen, Theorem 3.2.2) the natural partitions contain intervals of length zero, which IntervalPartition excludes.

Here a straight shuffle is described by a weight vector w : Fin M → ℝ (nonnegative, summing to one; zero entries allowed) listing the source intervals from left to right, and a permutation π of Fin M giving the order of the pieces on the target axis. Piece k is the diagonal segment of the square [s_k, s_k + w_k] × [t_k, t_k + w_k], where s_k = ∑_{j < k} w_j and t_k = ∑_{π j < π k} w_j.

weightShuffle w hw0 hw1 π is defined as an honest shuffleOfMin after the zero-length pieces are discarded (the positive pieces are enumerated in increasing order by Finset.orderIsoOfFin), so it is a shuffle of M in the sense of the library. Its CDF is ∑_k min (clipLength (u - s_k) w_k) (clipLength (v - t_k) w_k) with clipLength x w = min (max x 0) w (cdf_weightShuffle).

Main declarations

• IsShuffleOfMin, IsStraightShuffleOfMin: the classes of (straight) shuffles of M.
• clipLength, prefixSum, sum_clipLength_prefixSum: telescoping of consecutive intervals.
• IntervalPartition.ofWeights: the partition formed by the positive weights.
• weightShuffle, cdf_weightShuffle, isStraightShuffleOfMin_weightShuffle.

Shuffles of M as a class of copulas

def ProbabilityTheory.Copula.IsShuffleOfMin (S : Copula 2) : Prop

S is a shuffle of M: a finite shuffle of min in the sense of shuffleOfMin, with an arbitrary orientation of every segment (Nelsen, §3.2.3).

Equations

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

def ProbabilityTheory.Copula.IsStraightShuffleOfMin (S : Copula 2) : Prop

S is a straight shuffle of M: a finite shuffle of min in which every segment keeps its increasing orientation.

Equations

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

theorem ProbabilityTheory.Copula.IsStraightShuffleOfMin.isShuffleOfMin {S : Copula 2} (h : S.IsStraightShuffleOfMin) : S.IsShuffleOfMin

theorem ProbabilityTheory.Copula.isStraightShuffleOfMin_shuffleOfMin {n : ℕ} (P Q : IntervalPartition n) (perm : Equiv.Perm (Fin n)) (hwidth : ∀ (i : Fin n), P.width i = Q.width (perm i)) : (shuffleOfMin P Q perm hwidth fun (x : Fin n) => false).IsStraightShuffleOfMin

theorem ProbabilityTheory.Copula.isShuffleOfMin_shuffleOfMin {n : ℕ} (P Q : IntervalPartition n) (perm : Equiv.Perm (Fin n)) (hwidth : ∀ (i : Fin n), P.width i = Q.width (perm i)) (flipped : Fin n → Bool) : (shuffleOfMin P Q perm hwidth flipped).IsShuffleOfMin

theorem ProbabilityTheory.Copula.isStraightShuffleOfMin_comonotonic : (comonotonic 2).IsStraightShuffleOfMin

M itself is the trivial straight shuffle.

Clipped lengths and prefix sums

def ProbabilityTheory.Copula.clipLength (x w : ℝ) : ℝ

The length of the part of a segment of length w that lies below x, when the segment starts at 0: min (max x 0) w.

Equations

• ProbabilityTheory.Copula.clipLength x w = min (max x 0) w

theorem ProbabilityTheory.Copula.clipLength_nonneg (x : ℝ) {w : ℝ} (hw : 0 ≤ w) : 0 ≤ clipLength x w

theorem ProbabilityTheory.Copula.clipLength_le (x w : ℝ) : clipLength x w ≤ w

theorem ProbabilityTheory.Copula.clipLength_of_nonpos {x : ℝ} (w : ℝ) (hx : x ≤ 0) (hw : 0 ≤ w) : clipLength x w = 0

theorem ProbabilityTheory.Copula.clipLength_of_le {x w : ℝ} (hwx : w ≤ x) (hw : 0 ≤ w) : clipLength x w = w

@[simp]

theorem ProbabilityTheory.Copula.clipLength_zero_right (x : ℝ) : clipLength x 0 = 0

theorem ProbabilityTheory.Copula.monotone_clipLength (w : ℝ) : Monotone fun (x : ℝ) => clipLength x w

theorem ProbabilityTheory.Copula.clipLength_min (x y w : ℝ) : clipLength (min x y) w = min (clipLength x w) (clipLength y w)

theorem ProbabilityTheory.Copula.clipLength_add (x : ℝ) {W w : ℝ} (hW : 0 ≤ W) (hw : 0 ≤ w) : clipLength x W + clipLength (x - W) w = clipLength x (W + w)

Two consecutive segments of lengths W and w form one segment of length W + w.

theorem ProbabilityTheory.Copula.min_sub_min_eq_clipLength (u s : ℝ) {w : ℝ} (hw : 0 ≤ w) : min u (s + w) - min u s = clipLength (u - s) w

The CDF contribution of a segment starting at s of length w, written with minima.

def ProbabilityTheory.Copula.prefixSum {M : ℕ} (w : Fin M → ℝ) (t : ℕ) : ℝ

The sum of the weights with index below t.

Equations

• ProbabilityTheory.Copula.prefixSum w t = ∑ j : Fin M, if ↑j < t then w j else 0

@[simp]

theorem ProbabilityTheory.Copula.prefixSum_zero {M : ℕ} (w : Fin M → ℝ) : prefixSum w 0 = 0

theorem ProbabilityTheory.Copula.prefixSum_of_le {M : ℕ} (w : Fin M → ℝ) {t : ℕ} (ht : M ≤ t) : prefixSum w t = ∑ j : Fin M, w j

theorem ProbabilityTheory.Copula.prefixSum_nonneg {M : ℕ} {w : Fin M → ℝ} (hw : ∀ (k : Fin M), 0 ≤ w k) (t : ℕ) : 0 ≤ prefixSum w t

theorem ProbabilityTheory.Copula.prefixSum_le_sum {M : ℕ} {w : Fin M → ℝ} (hw : ∀ (k : Fin M), 0 ≤ w k) (t : ℕ) : prefixSum w t ≤ ∑ j : Fin M, w j

theorem ProbabilityTheory.Copula.prefixSum_mono {M : ℕ} {w : Fin M → ℝ} (hw : ∀ (k : Fin M), 0 ≤ w k) : Monotone (prefixSum w)

theorem ProbabilityTheory.Copula.prefixSum_succ {M : ℕ} (w : Fin M → ℝ) (k : Fin M) : prefixSum w (↑k + 1) = prefixSum w ↑k + w k

theorem ProbabilityTheory.Copula.prefixSum_castSucc {M : ℕ} (w : Fin (M + 1) → ℝ) {t : ℕ} (ht : t ≤ M) : prefixSum w t = prefixSum (fun (j : Fin M) => w j.castSucc) t

theorem ProbabilityTheory.Copula.sum_clipLength_prefixSum {M : ℕ} (w : Fin M → ℝ) (hw : ∀ (k : Fin M), 0 ≤ w k) (x : ℝ) : ∑ k : Fin M, clipLength (x - prefixSum w ↑k) (w k) = clipLength x (∑ k : Fin M, w k)

Consecutive segments with lengths w 0, w 1, … fill a segment of the total length.

The partition of the positive weights

noncomputable def ProbabilityTheory.Copula.posWeights {M : ℕ} (w : Fin M → ℝ) : Finset (Fin M)

The indices of the positive weights.

Equations

• ProbabilityTheory.Copula.posWeights w = {k : Fin M | 0 < w k}

theorem ProbabilityTheory.Copula.mem_posWeights {M : ℕ} {w : Fin M → ℝ} {k : Fin M} : k ∈ posWeights w ↔ 0 < w k

noncomputable def ProbabilityTheory.Copula.posIndex {M : ℕ} (w : Fin M → ℝ) {N : ℕ} (hN : (posWeights w).card = N) (j : Fin N) : Fin M

The jth positive weight index, in increasing order.

Equations

• ProbabilityTheory.Copula.posIndex w hN j = ↑(((ProbabilityTheory.Copula.posWeights w).orderIsoOfFin hN) j)

theorem ProbabilityTheory.Copula.posIndex_strictMono {M : ℕ} (w : Fin M → ℝ) {N : ℕ} (hN : (posWeights w).card = N) : StrictMono (posIndex w hN)

theorem ProbabilityTheory.Copula.posIndex_pos {M : ℕ} (w : Fin M → ℝ) {N : ℕ} (hN : (posWeights w).card = N) (j : Fin N) : 0 < w (posIndex w hN j)

theorem ProbabilityTheory.Copula.exists_posIndex_eq {M : ℕ} (w : Fin M → ℝ) {N : ℕ} (hN : (posWeights w).card = N) {k : Fin M} (hk : 0 < w k) : ∃ (j : Fin N), posIndex w hN j = k

theorem ProbabilityTheory.Copula.sum_posIndex {M : ℕ} (w : Fin M → ℝ) (hw0 : ∀ (k : Fin M), 0 ≤ w k) {N : ℕ} (hN : (posWeights w).card = N) (g : Fin M → ℝ) (hg : ∀ (k : Fin M), w k = 0 → g k = 0) : ∑ j : Fin N, g (posIndex w hN j) = ∑ k : Fin M, g k

Sums over all indices reduce to sums over the positive weights.

theorem ProbabilityTheory.Copula.prefixSum_posIndex {M : ℕ} (w : Fin M → ℝ) (hw0 : ∀ (k : Fin M), 0 ≤ w k) {N : ℕ} (hN : (posWeights w).card = N) (j : Fin N) : prefixSum (fun (j : Fin N) => w (posIndex w hN j)) ↑j = prefixSum w ↑(posIndex w hN j)

theorem ProbabilityTheory.Copula.prefixSum_posIndex_le_one {M : ℕ} (w : Fin M → ℝ) (hw0 : ∀ (k : Fin M), 0 ≤ w k) (hw1 : ∑ k : Fin M, w k = 1) {N : ℕ} (hN : (posWeights w).card = N) (t : ℕ) : prefixSum (fun (j : Fin N) => w (posIndex w hN j)) t ≤ 1

noncomputable def ProbabilityTheory.Copula.IntervalPartition.ofWeights {M : ℕ} (w : Fin M → ℝ) (hw0 : ∀ (k : Fin M), 0 ≤ w k) (hw1 : ∑ k : Fin M, w k = 1) {N : ℕ} (hN : (posWeights w).card = N) : IntervalPartition N

The interval partition whose cells are the positive weights, in increasing order.

Equations

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

theorem ProbabilityTheory.Copula.IntervalPartition.width_ofWeights {M : ℕ} (w : Fin M → ℝ) (hw0 : ∀ (k : Fin M), 0 ≤ w k) (hw1 : ∑ k : Fin M, w k = 1) {N : ℕ} (hN : (posWeights w).card = N) (j : Fin N) : (ofWeights w hw0 hw1 hN).width j = w (posIndex w hN j)

theorem ProbabilityTheory.Copula.IntervalPartition.point_ofWeights_castSucc {M : ℕ} (w : Fin M → ℝ) (hw0 : ∀ (k : Fin M), 0 ≤ w k) (hw1 : ∑ k : Fin M, w k = 1) {N : ℕ} (hN : (posWeights w).card = N) (j : Fin N) : ↑((ofWeights w hw0 hw1 hN).point j.castSucc) = prefixSum w ↑(posIndex w hN j)

theorem ProbabilityTheory.Copula.IntervalPartition.width_mul_coord_ofWeights {M : ℕ} (w : Fin M → ℝ) (hw0 : ∀ (k : Fin M), 0 ≤ w k) (hw1 : ∑ k : Fin M, w k = 1) {N : ℕ} (hN : (posWeights w).card = N) (j : Fin N) (u : ↑unitInterval) : (ofWeights w hw0 hw1 hN).width j * ↑((ofWeights w hw0 hw1 hN).coord j u) = clipLength (↑u - prefixSum w ↑(posIndex w hN j)) (w (posIndex w hN j))

The shuffle of a weight vector

def ProbabilityTheory.Copula.targetWeights {M : ℕ} (w : Fin M → ℝ) (π : Equiv.Perm (Fin M)) (k : Fin M) : ℝ

The weights listed in target order.

Equations

• ProbabilityTheory.Copula.targetWeights w π k = w ((Equiv.symm π) k)

theorem ProbabilityTheory.Copula.targetWeights_nonneg {M : ℕ} (w : Fin M → ℝ) (hw0 : ∀ (k : Fin M), 0 ≤ w k) (π : Equiv.Perm (Fin M)) (k : Fin M) : 0 ≤ targetWeights w π k

theorem ProbabilityTheory.Copula.sum_targetWeights {M : ℕ} (w : Fin M → ℝ) (hw1 : ∑ k : Fin M, w k = 1) (π : Equiv.Perm (Fin M)) : ∑ k : Fin M, targetWeights w π k = 1

theorem ProbabilityTheory.Copula.mem_posWeights_iff_perm {M : ℕ} (w : Fin M → ℝ) (π : Equiv.Perm (Fin M)) (k : Fin M) : k ∈ posWeights w ↔ π k ∈ posWeights (targetWeights w π)

theorem ProbabilityTheory.Copula.card_posWeights_targetWeights {M : ℕ} (w : Fin M → ℝ) (π : Equiv.Perm (Fin M)) : (posWeights (targetWeights w π)).card = (posWeights w).card

def ProbabilityTheory.Copula.targetOffset {M : ℕ} (w : Fin M → ℝ) (π : Equiv.Perm (Fin M)) (k : Fin M) : ℝ

The target offset of piece k: the total weight of the pieces placed before it.

Equations

• ProbabilityTheory.Copula.targetOffset w π k = ProbabilityTheory.Copula.prefixSum (ProbabilityTheory.Copula.targetWeights w π) ↑(π k)

theorem ProbabilityTheory.Copula.targetOffset_eq {M : ℕ} (w : Fin M → ℝ) (π : Equiv.Perm (Fin M)) (k : Fin M) : targetOffset w π k = ∑ j : Fin M, if ↑(π j) < ↑(π k) then w j else 0

noncomputable def ProbabilityTheory.Copula.shuffleSource {M : ℕ} (w : Fin M → ℝ) (hw0 : ∀ (k : Fin M), 0 ≤ w k) (hw1 : ∑ k : Fin M, w k = 1) : IntervalPartition (posWeights w).card

The source partition of the positive pieces.

Equations

• ProbabilityTheory.Copula.shuffleSource w hw0 hw1 = ProbabilityTheory.Copula.IntervalPartition.ofWeights w hw0 hw1 ⋯

noncomputable def ProbabilityTheory.Copula.shuffleTarget {M : ℕ} (w : Fin M → ℝ) (hw0 : ∀ (k : Fin M), 0 ≤ w k) (hw1 : ∑ k : Fin M, w k = 1) (π : Equiv.Perm (Fin M)) : IntervalPartition (posWeights w).card

The target partition of the positive pieces.

Equations

• ProbabilityTheory.Copula.shuffleTarget w hw0 hw1 π = ProbabilityTheory.Copula.IntervalPartition.ofWeights (ProbabilityTheory.Copula.targetWeights w π) ⋯ ⋯ ⋯

noncomputable def ProbabilityTheory.Copula.shufflePerm {M : ℕ} (w : Fin M → ℝ) (π : Equiv.Perm (Fin M)) : Equiv.Perm (Fin (posWeights w).card)

The permutation of the positive pieces induced by π.

Equations

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

theorem ProbabilityTheory.Copula.posIndex_shufflePerm {M : ℕ} (w : Fin M → ℝ) (π : Equiv.Perm (Fin M)) (j : Fin (posWeights w).card) : posIndex (targetWeights w π) ⋯ ((shufflePerm w π) j) = π (posIndex w ⋯ j)

theorem ProbabilityTheory.Copula.shuffle_hwidth {M : ℕ} (w : Fin M → ℝ) (hw0 : ∀ (k : Fin M), 0 ≤ w k) (hw1 : ∑ k : Fin M, w k = 1) (π : Equiv.Perm (Fin M)) (j : Fin (posWeights w).card) : (shuffleSource w hw0 hw1).width j = (shuffleTarget w hw0 hw1 π).width ((shufflePerm w π) j)

noncomputable def ProbabilityTheory.Copula.weightShuffle {M : ℕ} (w : Fin M → ℝ) (hw0 : ∀ (k : Fin M), 0 ≤ w k) (hw1 : ∑ k : Fin M, w k = 1) (π : Equiv.Perm (Fin M)) : Copula 2

The straight shuffle of M with source weights w (in order) and target order π. Pieces of weight zero are discarded, so this is a genuine shuffleOfMin.

Equations

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

theorem ProbabilityTheory.Copula.isStraightShuffleOfMin_weightShuffle {M : ℕ} (w : Fin M → ℝ) (hw0 : ∀ (k : Fin M), 0 ≤ w k) (hw1 : ∑ k : Fin M, w k = 1) (π : Equiv.Perm (Fin M)) : (weightShuffle w hw0 hw1 π).IsStraightShuffleOfMin

theorem ProbabilityTheory.Copula.cdf_weightShuffle {M : ℕ} (w : Fin M → ℝ) (hw0 : ∀ (k : Fin M), 0 ≤ w k) (hw1 : ∑ k : Fin M, w k = 1) (π : Equiv.Perm (Fin M)) (u v : ↑unitInterval) : (weightShuffle w hw0 hw1 π).cdf ![u, v] = ∑ k : Fin M, min (clipLength (↑u - prefixSum w ↑k) (w k)) (clipLength (↑v - targetOffset w π k) (w k))

CDF of a weight shuffle: piece k contributes the length of its diagonal segment below (u, v).