← Mathematical handbook

Attaining transport on the right half of each contact interval

The three path families are the A, B and C segments of Ansari–Rockel, Section 4. Their symmetric mixture has uniform marginals.

structure ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData : Type

• N : ℕ
• N_pos : 0 < self.N
• v : ℝ
• w : ℝ
• v_nonneg : 0 ≤ self.v
• w_nonneg : 0 ≤ self.w
• normalized : 2 * (↑self.N + 1) * (self.w + ↑self.N * self.v) = 1

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData.period_nonneg (S : RightData) : 0 ≤ UpperSpline.period (↑S.N) S.v S.w

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData.end_eq_one (S : RightData) : ↑S.N * UpperSpline.period (↑S.N) S.v S.w + 2 * S.w + ↑S.N * S.v = 1

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData.period_pos (S : RightData) : 0 < UpperSpline.period (↑S.N) S.v S.w

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData.phase_mem (S : RightData) (k : ℕ) (i : Fin 4) (s : ↑unitInterval) (hk : k ≤ S.N) (hi : i = 3 → k < S.N) : ↑k * UpperSpline.period (↑S.N) S.v S.w + UpperSpline.piecePoint (↑S.N) S.v S.w i ↑s ∈ Set.Icc 0 1

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData.point (S : RightData) (k : ℕ) (i : Fin 4) (hk : k ≤ S.N) (hi : i = 3 → k < S.N) (s : ↑unitInterval) : ↑unitInterval

Equations

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

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData.continuous_point (S : RightData) (k : ℕ) (i : Fin 4) (hk : k ≤ S.N) (hi : i = 3 → k < S.N) : Continuous (S.point k i hk hi)

@[reducible, inline]

abbrev ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData.Index (S : RightData) : Type

Equations

• S.Index = (Fin (S.N + 1) ⊕ Fin S.N ⊕ Fin S.N)

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData.weight (S : RightData) : S.Index → ℝ

Equations

• S.weight (Sum.inl val) = S.w
• S.weight (Sum.inr (Sum.inl k)) = (↑S.N - ↑↑k) * S.v
• S.weight (Sum.inr (Sum.inr k)) = (↑↑k + 1) * S.v

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData.weight_nonneg (S : RightData) (i : S.Index) : 0 ≤ S.weight i

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData.path (S : RightData) : S.Index → ↑unitInterval → Fin 2 → ↑unitInterval

Equations

• S.path (Sum.inl k) x✝ = ![S.point (↑k) 0 ⋯ ⋯ x✝, S.point (↑k) 2 ⋯ ⋯ x✝]
• S.path (Sum.inr (Sum.inl k)) x✝ = ![S.point (↑k) 1 ⋯ ⋯ x✝, S.point (↑k) 3 ⋯ ⋯ x✝]
• S.path (Sum.inr (Sum.inr k)) x✝ = ![S.point (↑k) 3 ⋯ ⋯ x✝, S.point (↑k + 1) 1 ⋯ ⋯ x✝]

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData.continuous_path (S : RightData) (i : S.Index) : Continuous (S.path i)

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData.symmetricPath (S : RightData) (i : S.Index × Bool) (s : ↑unitInterval) : Fin 2 → ↑unitInterval

Equations

• S.symmetricPath i s = if i.2 = true then ![S.path i.1 s 1, S.path i.1 s 0] else S.path i.1 s

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData.continuous_symmetricPath (S : RightData) (i : S.Index × Bool) : Continuous (S.symmetricPath i)