← Mathematical handbook

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

Equations

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

noncomputable def ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData.width (S : RightData) : 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.RightData.phase_affine (S : RightData) (k : ℕ) (i : Fin 4) (s : ℝ) : S.phase k i s = S.phase k i 0 + S.width i * s

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData.integral_piece (S : RightData) (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.RightData.path_density_sum (S : RightData) (F : ℕ → Fin 4 → ℝ) : ∑ k ∈ Finset.range (S.N + 1), S.w * (F k 0 + F k 2) + ∑ 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 + 1), (S.w * F k 0 + ↑S.N * S.v * F k 1 + S.w * F k 2) + ∑ k ∈ Finset.range S.N, (↑S.N + 1) * S.v * F k 3

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData.phase_adjacent (S : RightData) (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.RightData.integral_three (S : RightData) (f : ℝ → ℝ) (hf : Continuous f) (k : ℕ) : ((S.w * ∫ (s : ↑unitInterval), f (S.phase k 0 ↑s)) + ↑S.N * S.v * ∫ (s : ↑unitInterval), f (S.phase k 1 ↑s)) + S.w * ∫ (s : ↑unitInterval), f (S.phase k 2 ↑s) = ∫ (x : ℝ) in S.phase k 0 0..S.phase k 2 1, f x

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

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

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData.phase_density_integral (S : RightData) (f : ℝ → ℝ) (hf : Continuous f) : ∑ k ∈ Finset.range (S.N + 1), S.w * ((∫ (s : ↑unitInterval), f (S.phase k 0 ↑s)) + ∫ (s : ↑unitInterval), f (S.phase k 2 ↑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.RightData.symmetric_marginal_sum (S : RightData) (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.RightData.marginal_integral (S : RightData) (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.RightData.copula (S : RightData) : Copula 2

The upper-bound transport is a copula, with zero-weight paths permitted.

Equations

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

theorem ProbabilityTheory.Copula.RankRegion.RhoFootrule.RightData.integral_copula (S : RightData) {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)