← Mathematical handbook

Permuted finite copula blocks

Allowing arbitrary copulas inside the permuted squares proves the signed shuffle formula by taking each component to be M or W. Degenerate blocks have zero measure and require no limiting argument.

noncomputable def Verification.ShuffleStrip.blockPoint (S : ShuffleStrip) (u : Fin 2 → ↑unitInterval) : Fin 2 → ↑unitInterval

Equations

• S.blockPoint u j = S.point (u j) j

theorem Verification.ShuffleStrip.continuous_blockPoint (S : ShuffleStrip) : Continuous S.blockPoint

noncomputable def Verification.ShuffleStrip.blockLaw (S : ShuffleStrip) (C : ProbabilityTheory.Copula 2) : MeasureTheory.Measure (Fin 2 → ↑unitInterval)

Equations

• S.blockLaw C = ENNReal.ofReal S.width • MeasureTheory.Measure.map S.blockPoint C.toMeasure

theorem Verification.ShuffleStrip.blockLaw_univ (S : ShuffleStrip) (C : ProbabilityTheory.Copula 2) : (S.blockLaw C) Set.univ = ENNReal.ofReal S.width

instance Verification.ShuffleStrip.instIsFiniteMeasureForallFinOfNatNatElemRealUnitIntervalBlockLaw (S : ShuffleStrip) (C : ProbabilityTheory.Copula 2) : MeasureTheory.IsFiniteMeasure (S.blockLaw C)

theorem Verification.ShuffleStrip.blockLaw_marginal (S : ShuffleStrip) (C : ProbabilityTheory.Copula 2) (j : Fin 2) : MeasureTheory.Measure.map (fun (x : Fin 2 → ↑unitInterval) => x j) (S.blockLaw C) = MeasureTheory.Measure.map (fun (x : Fin 2 → ↑unitInterval) => x j) S.law

theorem Verification.ShuffleStrip.blockLaw_Iic_self (S : ShuffleStrip) (C : ProbabilityTheory.Copula 2) (u : Fin 2 → ↑unitInterval) : (S.blockLaw C).real (Set.Iic (S.blockPoint u)) = S.width * C.cdf u

theorem Verification.ShuffleStrip.blockPoint_bounds (S : ShuffleStrip) (u : Fin 2 → ↑unitInterval) (j : Fin 2) : S.point 0 j ≤ S.blockPoint u j ∧ S.blockPoint u j ≤ S.point 1 j

theorem Verification.ShuffleStrip.blockLaw_Iic_full (S : ShuffleStrip) (C : ProbabilityTheory.Copula 2) (z : Fin 2 → ↑unitInterval) (hz : S.point 1 ≤ z) : (S.blockLaw C).real (Set.Iic z) = S.width

theorem Verification.ShuffleStrip.blockLaw_Iic_zero (S : ShuffleStrip) (C : ProbabilityTheory.Copula 2) (z : Fin 2 → ↑unitInterval) (j : Fin 2) (hz : z j ≤ S.point 0 j) : (S.blockLaw C).real (Set.Iic z) = 0

theorem Verification.ShuffleStrip.integral_blockLaw (S : ShuffleStrip) (C : ProbabilityTheory.Copula 2) {f : (Fin 2 → ↑unitInterval) → ℝ} (hf : Continuous f) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂S.blockLaw C = S.width * ∫ (u : Fin 2 → ↑unitInterval), f (S.blockPoint u) ∂C.toMeasure

noncomputable def Verification.PositiveShuffle.blockLaw {n : ℕ} (S : PositiveShuffle n) (C : Fin n → ProbabilityTheory.Copula 2) : MeasureTheory.Measure (Fin 2 → ↑unitInterval)

Equations

• S.blockLaw C = ∑ i : Fin n, (S.strip i).blockLaw (C i)

instance Verification.PositiveShuffle.instIsFiniteMeasureForallFinOfNatNatElemRealUnitIntervalBlockLaw {n : ℕ} (S : PositiveShuffle n) (C : Fin n → ProbabilityTheory.Copula 2) : MeasureTheory.IsFiniteMeasure (S.blockLaw C)

instance Verification.PositiveShuffle.instIsProbabilityMeasureForallFinOfNatNatElemRealUnitIntervalBlockLaw {n : ℕ} (S : PositiveShuffle n) (C : Fin n → ProbabilityTheory.Copula 2) : MeasureTheory.IsProbabilityMeasure (S.blockLaw C)

noncomputable def Verification.PositiveShuffle.blockCopula {n : ℕ} (S : PositiveShuffle n) (C : Fin n → ProbabilityTheory.Copula 2) : ProbabilityTheory.Copula 2

Equations

• S.blockCopula C = { measure := ⟨S.blockLaw C, ⋯⟩, marginal_eq := ⋯ }

theorem Verification.PositiveShuffle.block_cdf {n : ℕ} (S : PositiveShuffle n) (C : Fin n → ProbabilityTheory.Copula 2) (z : Fin 2 → ↑unitInterval) : (S.blockCopula C).cdf z = ∑ i : Fin n, ((S.strip i).blockLaw (C i)).real (Set.Iic z)

theorem Verification.PositiveShuffle.block_cdf_point {n : ℕ} (S : PositiveShuffle n) (C : Fin n → ProbabilityTheory.Copula 2) (π : Equiv.Perm (Fin n)) (hx : ∀ (i j : Fin n), i < j → (S.strip i).x + (S.strip i).width ≤ (S.strip j).x) (hy : ∀ (i j : Fin n), π i < π j → (S.strip i).y + (S.strip i).width ≤ (S.strip j).y) (i : Fin n) (u : Fin 2 → ↑unitInterval) : (S.blockCopula C).cdf ((S.strip i).blockPoint u) = (S.strip i).width * (C i).cdf u + ∑ j : Fin n, if j < i ∧ π j < π i then (S.strip j).width else 0

theorem Verification.PositiveShuffle.integral_blockCopula {n : ℕ} (S : PositiveShuffle n) (C : Fin n → ProbabilityTheory.Copula 2) {f : (Fin 2 → ↑unitInterval) → ℝ} (hf : Continuous f) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂(S.blockCopula C).toMeasure = ∑ i : Fin n, (S.strip i).width * ∫ (u : Fin 2 → ↑unitInterval), f ((S.strip i).blockPoint u) ∂(C i).toMeasure

theorem Verification.PositiveShuffle.block_tau_raw {n : ℕ} (S : PositiveShuffle n) (C : Fin n → ProbabilityTheory.Copula 2) (π : Equiv.Perm (Fin n)) (hx : ∀ (i j : Fin n), i < j → (S.strip i).x + (S.strip i).width ≤ (S.strip j).x) (hy : ∀ (i j : Fin n), π i < π j → (S.strip i).y + (S.strip i).width ≤ (S.strip j).y) : (S.blockCopula C).kendallTau = ∑ i : Fin n, ((S.strip i).width ^ 2 * ((C i).kendallTau + 1) + 4 * (S.strip i).width * ∑ j : Fin n, if j < i ∧ π j < π i then (S.strip j).width else 0) - 1

theorem Verification.PositiveShuffle.block_tau {n : ℕ} (S : PositiveShuffle n) (C : Fin n → ProbabilityTheory.Copula 2) (π : Equiv.Perm (Fin n)) (hx : ∀ (i j : Fin n), i < j → (S.strip i).x + (S.strip i).width ≤ (S.strip j).x) (hy : ∀ (i j : Fin n), π i < π j → (S.strip i).y + (S.strip i).width ≤ (S.strip j).y) : (S.blockCopula C).kendallTau = ∑ i : Fin n, (C i).kendallTau * (S.strip i).width ^ 2 + 2 * ∑ i : Fin n, ∑ j : Fin n, if j < i then (if π j < π i then 1 else -1) * (S.strip j).width * (S.strip i).width else 0

noncomputable def Verification.PositiveShuffle.signedCopula {n : ℕ} (S : PositiveShuffle n) (ε : Fin n → Bool) : ProbabilityTheory.Copula 2

A signed shuffle of M: true selects a diagonal and false an antidiagonal.

Equations

• S.signedCopula ε = S.blockCopula fun (i : Fin n) => if ε i = true then ProbabilityTheory.Copula.comonotonic 2 else ProbabilityTheory.Copula.countermonotonic

theorem Verification.PositiveShuffle.signed_tau {n : ℕ} (S : PositiveShuffle n) (ε : Fin n → Bool) (π : Equiv.Perm (Fin n)) (hx : ∀ (i j : Fin n), i < j → (S.strip i).x + (S.strip i).width ≤ (S.strip j).x) (hy : ∀ (i j : Fin n), π i < π j → (S.strip i).y + (S.strip i).width ≤ (S.strip j).y) : (S.signedCopula ε).kendallTau = ∑ i : Fin n, (if ε i = true then 1 else -1) * (S.strip i).width ^ 2 + 2 * ∑ i : Fin n, ∑ j : Fin n, if j < i then (if π j < π i then 1 else -1) * (S.strip j).width * (S.strip i).width else 0

The signed shuffle identity, with the pair sum written over j < i.