← Mathematical handbook

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

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

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

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

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

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.phase (S : LeftData) (k : ℕ) (i : Fin 4) (s : ℝ) : ℝ

Equations

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

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.phase_mem (S : LeftData) (k : ℕ) (i : Fin 4) (s : ↑unitInterval) (hk : k ≤ S.N) (hi0 : i = 0 → 0 < k) (hi2 : i = 2 ∨ i = 3 → k < S.N) : S.phase k i ↑s ∈ Set.Icc 0 1

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.point (S : LeftData) (k : ℕ) (i : Fin 4) (hk : k ≤ S.N) (hi0 : i = 0 → 0 < k) (hi2 : i = 2 ∨ i = 3 → k < S.N) (s : ↑unitInterval) : ↑unitInterval

Equations

• S.point k i hk hi0 hi2 s = ⟨S.phase k i ↑s, ⋯⟩

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.continuous_point (S : LeftData) (k : ℕ) (i : Fin 4) (hk : k ≤ S.N) (hi0 : i = 0 → 0 < k) (hi2 : i = 2 ∨ i = 3 → k < S.N) : Continuous (S.point k i hk hi0 hi2)

@[reducible, inline]

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

Equations

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

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.weight (S : LeftData) : 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.LeftData.weight_nonneg (S : LeftData) (i : S.Index) : 0 ≤ S.weight i

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

Equations

• S.path (Sum.inl k) x✝ = ![S.point (↑k) 2 ⋯ ⋯ ⋯ x✝, S.point (↑k + 1) 0 ⋯ ⋯ ⋯ 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.LeftData.continuous_path (S : LeftData) (i : S.Index) : Continuous (S.path i)

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.symmetricPath (S : LeftData) (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.LeftData.continuous_symmetricPath (S : LeftData) (i : S.Index × Bool) : Continuous (S.symmetricPath i)