← Mathematical handbook

A copula on a forward graph and its transpose is unique

noncomputable def Verification.upperGraph (τ : ↑unitInterval → ↑unitInterval) (u : ↑unitInterval) : Fin 2 → ↑unitInterval

Equations

• Verification.upperGraph τ u = ![u, τ u]

noncomputable def Verification.lowerGraph (τ : ↑unitInterval → ↑unitInterval) (u : ↑unitInterval) : Fin 2 → ↑unitInterval

Equations

• Verification.lowerGraph τ u = ![τ u, u]

def Verification.ForwardGraphSupport (C : ProbabilityTheory.Copula 2) (τ : ↑unitInterval → ↑unitInterval) (q : ℝ) : Prop

Equations

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

theorem Verification.copula_forward_graph_unique (C D : ProbabilityTheory.Copula 2) (τ : ↑unitInterval → ↑unitInterval) (hτ : Measurable τ) (q : ℝ) (hq : 0 < q) (hC : ForwardGraphSupport C τ q) (hD : ForwardGraphSupport D τ q) : C = D

Uniform marginals determine a copula supported on a forward graph and its transpose.