← Mathematical handbook

Finite shuffles with increasing strips

The construction is a sum of actual uniform segment laws. The tiling conditions state that the horizontal and vertical strips partition the unit interval; zero-width strips are allowed throughout.

noncomputable def Verification.stripCut (s a u : ℝ) : ℝ

Equations

• Verification.stripCut s a u = min s (max 0 (u - a))

theorem Verification.stripCut_eq_min_sub {s a u : ℝ} (hs : 0 ≤ s) : stripCut s a u = min u (a + s) - min u a

theorem Verification.stripCut_zero {s a u : ℝ} (hs : 0 ≤ s) (hu : u ≤ a) : stripCut s a u = 0

theorem Verification.stripCut_full {s a u : ℝ} (hu : a + s ≤ u) : stripCut s a u = s

theorem Verification.stripCut_inside {s a u : ℝ} (h0 : a ≤ u) (h1 : u ≤ a + s) : stripCut s a u = u - a

structure Verification.ShuffleStrip : Type

• x : ℝ
• y : ℝ
• width : ℝ
• x_nonneg : 0 ≤ self.x
• y_nonneg : 0 ≤ self.y
• width_nonneg : 0 ≤ self.width
• x_end : self.x + self.width ≤ 1
• y_end : self.y + self.width ≤ 1

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

Equations

• S.point u = ![⟨S.x + S.width * ↑u, ⋯⟩, ⟨S.y + S.width * ↑u, ⋯⟩]

theorem Verification.ShuffleStrip.continuous_point (S : ShuffleStrip) : Continuous S.point

noncomputable def Verification.ShuffleStrip.law (S : ShuffleStrip) : MeasureTheory.Measure (Fin 2 → ↑unitInterval)

Equations

• S.law = ENNReal.ofReal S.width • MeasureTheory.Measure.map S.point MeasureTheory.volume

instance Verification.ShuffleStrip.instIsFiniteMeasureForallFinOfNatNatElemRealUnitIntervalLaw (S : ShuffleStrip) : MeasureTheory.IsFiniteMeasure S.law

theorem Verification.ShuffleStrip.law_univ (S : ShuffleStrip) : S.law Set.univ = ENNReal.ofReal S.width

theorem Verification.ShuffleStrip.law_Iic (S : ShuffleStrip) (u : Fin 2 → ↑unitInterval) : S.law (Set.Iic u) = ENNReal.ofReal (min (stripCut S.width S.x ↑(u 0)) (stripCut S.width S.y ↑(u 1)))

theorem Verification.ShuffleStrip.integral_law (S : ShuffleStrip) {f : (Fin 2 → ↑unitInterval) → ℝ} (hf : Continuous f) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂S.law = S.width * ∫ (u : ↑unitInterval), f (S.point u)

structure Verification.PositiveShuffle (n : ℕ) : Type

• strip : Fin n → ShuffleStrip
• total : ∑ i : Fin n, (self.strip i).width = 1
• tile_x (u : ↑unitInterval) : ∑ i : Fin n, stripCut (self.strip i).width (self.strip i).x ↑u = ↑u
• tile_y (u : ↑unitInterval) : ∑ i : Fin n, stripCut (self.strip i).width (self.strip i).y ↑u = ↑u

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

Equations

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

instance Verification.PositiveShuffle.instIsFiniteMeasureForallFinOfNatNatElemRealUnitIntervalLaw {n : ℕ} (S : PositiveShuffle n) : MeasureTheory.IsFiniteMeasure S.law

instance Verification.PositiveShuffle.instIsProbabilityMeasureForallFinOfNatNatElemRealUnitIntervalLaw {n : ℕ} (S : PositiveShuffle n) : MeasureTheory.IsProbabilityMeasure S.law

theorem Verification.PositiveShuffle.law_Iic {n : ℕ} (S : PositiveShuffle n) (u : Fin 2 → ↑unitInterval) : S.law (Set.Iic u) = ENNReal.ofReal (∑ i : Fin n, min (stripCut (S.strip i).width (S.strip i).x ↑(u 0)) (stripCut (S.strip i).width (S.strip i).y ↑(u 1)))

theorem Verification.PositiveShuffle.marginal {n : ℕ} (S : PositiveShuffle n) (j : Fin 2) : MeasureTheory.Measure.map (fun (x : Fin 2 → ↑unitInterval) => x j) S.law = MeasureTheory.volume

noncomputable def Verification.PositiveShuffle.copula {n : ℕ} (S : PositiveShuffle n) : ProbabilityTheory.Copula 2

Equations

• S.copula = { measure := ⟨S.law, ⋯⟩, marginal_eq := ⋯ }

theorem Verification.PositiveShuffle.cdf {n : ℕ} (S : PositiveShuffle n) (u : Fin 2 → ↑unitInterval) : S.copula.cdf u = ∑ i : Fin n, min (stripCut (S.strip i).width (S.strip i).x ↑(u 0)) (stripCut (S.strip i).width (S.strip i).y ↑(u 1))

theorem Verification.PositiveShuffle.integral_copula {n : ℕ} (S : PositiveShuffle n) {f : (Fin 2 → ↑unitInterval) → ℝ} (hf : Continuous f) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂S.copula.toMeasure = ∑ i : Fin n, (S.strip i).width * ∫ (u : ↑unitInterval), f ((S.strip i).point u)

theorem Verification.PositiveShuffle.footrule {n : ℕ} (S : PositiveShuffle n) : S.copula.spearmanFootrule = 1 - 3 * ∑ i : Fin n, (S.strip i).width * |(S.strip i).x - (S.strip i).y|

theorem Verification.PositiveShuffle.cdf_point {n : ℕ} (S : PositiveShuffle n) (π : 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 : ↑unitInterval) : S.copula.cdf ((S.strip i).point u) = (S.strip i).width * ↑u + ∑ j : Fin n, if j < i ∧ π j < π i then (S.strip j).width else 0

theorem Verification.PositiveShuffle.tau {n : ℕ} (S : PositiveShuffle n) (π : 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.copula.kendallTau = 4 * ∑ i : Fin n, (S.strip i).width * ((S.strip i).width / 2 + ∑ j : Fin n, if j < i ∧ π j < π i then (S.strip j).width else 0) - 1