← Copula mathematical handbook

Bivariate Archimedean generators

We use the decreasing inverse-generator convention: ψ is convex on [0,∞) and φ is its inverse on (0,1]. Zero coordinates are handled separately. Convexity is sufficient in dimension two; this constructor makes no claim of admissibility in higher dimensions.

structure ProbabilityTheory.Copula.BivariateGenerator : Type

The analytic conditions sufficient for a bivariate Archimedean copula.

• toFun : ℝ → ℝ

  Decreasing inverse generator.

• invFun : ↑unitInterval → ℝ

  Generator on positive unit-interval arguments; its value at zero is unused.

• nonneg (t : ℝ) : 0 ≤ t → 0 ≤ self.toFun t
• antitone : AntitoneOn self.toFun (Set.Ici 0)
• convex : ConvexOn ℝ (Set.Ici 0) self.toFun
• inv_nonneg (u : ↑unitInterval) : u ≠ 0 → 0 ≤ self.invFun u
• inv_antitone (u v : ↑unitInterval) : u ≠ 0 → u ≤ v → self.invFun v ≤ self.invFun u
• inv_one : self.invFun 1 = 0
• right_inv (u : ↑unitInterval) : u ≠ 0 → self.toFun (self.invFun u) = ↑u

theorem ProbabilityTheory.Copula.BivariateGenerator.convex_increment {f : ℝ → ℝ} (hf : ConvexOn ℝ (Set.Ici 0) f) {a b c e : ℝ} (ha : 0 ≤ a) (hc : 0 ≤ c) (hab : a ≤ b) (hce : c ≤ e) : 0 ≤ f (b + e) - f (a + e) - f (b + c) + f (a + c)

noncomputable def ProbabilityTheory.Copula.BivariateGenerator.cdf (g : BivariateGenerator) (u v : ↑unitInterval) : ℝ

The Archimedean formula, with grounded boundary values.

Equations

• g.cdf u v = if u = 0 ∨ v = 0 then 0 else g.toFun (g.invFun u + g.invFun v)

@[simp]

theorem ProbabilityTheory.Copula.BivariateGenerator.cdf_zero_left (g : BivariateGenerator) (v : ↑unitInterval) : g.cdf 0 v = 0

@[simp]

theorem ProbabilityTheory.Copula.BivariateGenerator.cdf_zero_right (g : BivariateGenerator) (u : ↑unitInterval) : g.cdf u 0 = 0

@[simp]

theorem ProbabilityTheory.Copula.BivariateGenerator.cdf_one_left (g : BivariateGenerator) (v : ↑unitInterval) : g.cdf 1 v = ↑v

@[simp]

theorem ProbabilityTheory.Copula.BivariateGenerator.cdf_one_right (g : BivariateGenerator) (u : ↑unitInterval) : g.cdf u 1 = ↑u

theorem ProbabilityTheory.Copula.BivariateGenerator.cdf_nonneg (g : BivariateGenerator) (u v : ↑unitInterval) : 0 ≤ g.cdf u v

theorem ProbabilityTheory.Copula.BivariateGenerator.cdf_mono_left (g : BivariateGenerator) (v : ↑unitInterval) : Monotone fun (u : ↑unitInterval) => g.cdf u v

theorem ProbabilityTheory.Copula.BivariateGenerator.cdf_comm (g : BivariateGenerator) (u v : ↑unitInterval) : g.cdf u v = g.cdf v u

theorem ProbabilityTheory.Copula.BivariateGenerator.isClassical_cdf (g : BivariateGenerator) : IsClassical fun (u : Fin 2 → ↑unitInterval) => g.cdf (u 0) (u 1)

noncomputable def ProbabilityTheory.Copula.BivariateGenerator.copula (g : BivariateGenerator) : Copula 2

The copula measure represented by a bivariate Archimedean generator.

Equations

• g.copula = ProbabilityTheory.Copula.ofClassical (fun (u : Fin 2 → ↑unitInterval) => g.cdf (u 0) (u 1)) ⋯

@[simp]

theorem ProbabilityTheory.Copula.BivariateGenerator.cdf_copula (g : BivariateGenerator) (u : Fin 2 → ↑unitInterval) : g.copula.cdf u = g.cdf (u 0) (u 1)

def ProbabilityTheory.Copula.HasArchimedeanGenerator {d : ℕ} (C : Copula d) (g : BivariateGenerator) : Prop

Identification of a copula's Archimedean generator in its given dimension. The copula already supplies validity; bivariate convexity alone is not used to construct higher-dimensional copulas. Grounded boundary values follow from C.

Equations

• C.HasArchimedeanGenerator g = ∀ (u : Fin d → ↑unitInterval), (∀ (i : Fin d), u i ≠ 0) → C.cdf u = g.toFun (∑ i : Fin d, g.invFun (u i))

def ProbabilityTheory.Copula.IsArchimedean {d : ℕ} (C : Copula d) : Prop

A copula with an identified decreasing Archimedean generator.

Equations

• C.IsArchimedean = ∃ (g : ProbabilityTheory.Copula.BivariateGenerator), C.HasArchimedeanGenerator g

theorem ProbabilityTheory.Copula.BivariateGenerator.hasArchimedeanGenerator (g : BivariateGenerator) : g.copula.HasArchimedeanGenerator g

theorem ProbabilityTheory.Copula.BivariateGenerator.isArchimedean (g : BivariateGenerator) : g.copula.IsArchimedean