← Copula mathematical handbook

Finite shuffles of min

Two partitions and a permutation describe the source and target strips. Corresponding strips must have equal lengths. A Boolean for each strip allows its diagonal to be reflected, giving both orientations of the classical shuffle construction. Equal-width straight shuffles are included.

noncomputable def ProbabilityTheory.Copula.shuffleData {n : ℕ} (P Q : IntervalPartition n) (perm : Equiv.Perm (Fin n)) (hwidth : ∀ (i : Fin n), P.width i = Q.width (perm i)) : PatchworkData (Fin n)

Coordinate data of a length-preserving permutation of interval strips.

Equations

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

noncomputable def ProbabilityTheory.Copula.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) : Copula 2

A shuffle of M, with optional reflection of each segment.

Equations

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

theorem ProbabilityTheory.Copula.cdf_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) (u v : ↑unitInterval) : (shuffleOfMin P Q perm hwidth flipped).cdf ![u, v] = ∑ i : Fin n, P.width i * if flipped i = true then max (↑(P.coord i u) + ↑(Q.coord (perm i) v) - 1) 0 else min ↑(P.coord i u) ↑(Q.coord (perm i) v)

noncomputable def ProbabilityTheory.Copula.uniformShuffleOfMin (n : ℕ) (hn : 0 < n) (perm : Equiv.Perm (Fin n)) : Copula 2

Equal-width straight shuffle, requiring only a positive order and a permutation.

Equations

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

@[simp]

theorem ProbabilityTheory.Copula.shuffleOfMin_refl {n : ℕ} (P : IntervalPartition n) : (shuffleOfMin P P (Equiv.refl (Fin n)) ⋯ fun (x : Fin n) => false) = comonotonic 2