← Copula mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.width (S : LeftData) : Fin 4 → ℝ

Equations

• S.width 0 = S.w
• S.width 1 = ↑S.N * S.v
• S.width 2 = S.w
• S.width 3 = (↑S.N + 1) * S.v

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.phase_affine (S : LeftData) (k : ℕ) (i : Fin 4) (s : ℝ) : S.phase k i s = S.phase k i 0 + S.width i * s

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.integral_piece (S : LeftData) (f : ℝ → ℝ) (k : ℕ) (i : Fin 4) : S.width i * ∫ (s : ↑unitInterval), f (S.phase k i ↑s) = ∫ (x : ℝ) in S.phase k i 0..S.phase k i 1, f x

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.path_density_sum (S : LeftData) (F : ℕ → Fin 4 → ℝ) : ∑ k ∈ Finset.range S.N, S.w * (F k 2 + F (k + 1) 0) + ∑ k ∈ Finset.range S.N, (↑S.N - ↑k) * S.v * (F k 1 + F k 3) + ∑ k ∈ Finset.range S.N, (↑k + 1) * S.v * (F k 3 + F (k + 1) 1) = ∑ k ∈ Finset.range S.N, (↑S.N * S.v * F k 1 + S.w * F k 2 + (↑S.N + 1) * S.v * F k 3 + S.w * F (k + 1) 0) + ↑S.N * S.v * F S.N 1

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.phase_adjacent (S : LeftData) (k : ℕ) : S.phase k 0 1 = S.phase k 1 0 ∧ S.phase k 1 1 = S.phase k 2 0 ∧ S.phase k 2 1 = S.phase k 3 0 ∧ S.phase k 3 1 = S.phase (k + 1) 0 0

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.integral_four (S : LeftData) (f : ℝ → ℝ) (hf : Continuous f) (k : ℕ) : (((↑S.N * S.v * ∫ (s : ↑unitInterval), f (S.phase k 1 ↑s)) + S.w * ∫ (s : ↑unitInterval), f (S.phase k 2 ↑s)) + (↑S.N + 1) * S.v * ∫ (s : ↑unitInterval), f (S.phase k 3 ↑s)) + S.w * ∫ (s : ↑unitInterval), f (S.phase (k + 1) 0 ↑s) = ∫ (x : ℝ) in S.phase k 1 0..S.phase (k + 1) 1 0, f x

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.integral_periods (S : LeftData) (f : ℝ → ℝ) (hf : Continuous f) (m : ℕ) : ∑ k ∈ Finset.range m, ∫ (x : ℝ) in S.phase k 1 0..S.phase (k + 1) 1 0, f x = ∫ (x : ℝ) in 0..S.phase m 1 0, f x

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.phase_density_integral (S : LeftData) (f : ℝ → ℝ) (hf : Continuous f) : ∑ k ∈ Finset.range S.N, S.w * ((∫ (s : ↑unitInterval), f (S.phase k 2 ↑s)) + ∫ (s : ↑unitInterval), f (S.phase (k + 1) 0 ↑s)) + ∑ k ∈ Finset.range S.N, (↑S.N - ↑k) * S.v * ((∫ (s : ↑unitInterval), f (S.phase k 1 ↑s)) + ∫ (s : ↑unitInterval), f (S.phase k 3 ↑s)) + ∑ k ∈ Finset.range S.N, (↑k + 1) * S.v * ((∫ (s : ↑unitInterval), f (S.phase k 3 ↑s)) + ∫ (s : ↑unitInterval), f (S.phase (k + 1) 1 ↑s)) = ∫ (x : ℝ) in 0..1, f x

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.symmetric_marginal_sum (S : LeftData) (j : Fin 2) (f : ↑unitInterval → ℝ) : ∑ i : S.Index × Bool, S.weight i.1 * ∫ (s : ↑unitInterval), f (S.symmetricPath i s j) = ∑ i : S.Index, S.weight i * ((∫ (s : ↑unitInterval), f (S.path i s 0)) + ∫ (s : ↑unitInterval), f (S.path i s 1))

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.marginal_integral (S : LeftData) (j : Fin 2) (f : ↑unitInterval → ℝ) (hf : Continuous f) : ∑ i : S.Index × Bool, S.weight i.1 * ∫ (s : ↑unitInterval), f (S.symmetricPath i s j) = ∫ (s : ↑unitInterval), f s

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.copula (S : LeftData) : Copula 2

Equations

• S.copula = ProbabilityTheory.Copula.RankRegion.FinitePathCoupling.copula (fun (i : S.Index × Bool) => S.weight i.1) ⋯ S.symmetricPath ⋯ ⋯

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.LeftData.integral_copula (S : LeftData) {f : (Fin 2 → ↑unitInterval) → ℝ} (hf : Continuous f) : ∫ (x : Fin 2 → ↑unitInterval), f x ∂S.copula.toMeasure = ∑ i : S.Index × Bool, S.weight i.1 * ∫ (s : ↑unitInterval), f (S.symmetricPath i s)