← Copula mathematical handbook

Non-strict generators by clamping

A non-strict Archimedean generator φ has a finite value φ(0) = a; its pseudo-inverse is ψ(t) = F(min t a), where F is the inverse of φ on [0, a] (Nelsen, An Introduction to Copulas, second edition, Definition 4.1.1 and Theorem 4.1.4). This file packages the verification that such a clamped function is an admissible bivariate inverse generator: F convex and antitone on [0, a] with F a = 0 suffices, because t ↦ min t a is concave and a convex antitone function of a concave function is convex.

The constructor BivariateGenerator.ofClamp is used for the non-strict families 11, 18, 21 and 22 of Nelsen's Table 4.1.

theorem ProbabilityTheory.Copula.convexOn_comp_concaveOn_of_mapsTo {g f : ℝ → ℝ} {D T : Set ℝ} (hg : ConvexOn ℝ T g) (hanti : AntitoneOn g T) (hf : ConcaveOn ℝ D f) (hmaps : Set.MapsTo f D T) : ConvexOn ℝ D fun (x : ℝ) => g (f x)

A convex antitone function of a concave function is convex (sets in ℝ, with an explicit MapsTo hypothesis instead of an image set).

theorem ProbabilityTheory.Copula.concaveOn_min_const (a : ℝ) : ConcaveOn ℝ Set.univ fun (t : ℝ) => min t a

t ↦ min t a is concave on the whole line.

theorem ProbabilityTheory.Copula.convexOn_clamp {F : ℝ → ℝ} {a : ℝ} (ha : 0 ≤ a) (hconv : ConvexOn ℝ (Set.Icc 0 a) F) (hanti : AntitoneOn F (Set.Icc 0 a)) : ConvexOn ℝ (Set.Ici 0) fun (t : ℝ) => F (min t a)

Clamping a convex function that is antitone on [0, a] at a gives a convex function on [0, ∞).

noncomputable def ProbabilityTheory.Copula.BivariateGenerator.ofClamp (F : ℝ → ℝ) (a : ℝ) (ha : 0 ≤ a) (hconv : ConvexOn ℝ (Set.Icc 0 a) F) (hanti : AntitoneOn F (Set.Icc 0 a)) (hFa : F a = 0) (φ : ↑unitInterval → ℝ) (hφ : ∀ (u : ↑unitInterval), u ≠ 0 → φ u ∈ Set.Icc 0 a) (hφanti : ∀ (u v : ↑unitInterval), u ≠ 0 → u ≤ v → φ v ≤ φ u) (hφ1 : φ 1 = 0) (hright : ∀ (u : ↑unitInterval), u ≠ 0 → F (φ u) = ↑u) : BivariateGenerator

A non-strict bivariate generator from the inverse F of the generator on [0, a], extended by zero beyond a (as F (min t a)). The generator φ must take values in [0, a], be antitone, vanish at one, and be inverted by F.

Equations

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

theorem ProbabilityTheory.Copula.BivariateGenerator.ofClamp_toFun {F : ℝ → ℝ} {a : ℝ} {ha : 0 ≤ a} {hconv : ConvexOn ℝ (Set.Icc 0 a) F} {hanti : AntitoneOn F (Set.Icc 0 a)} {hFa : F a = 0} {φ : ↑unitInterval → ℝ} {hφ : ∀ (u : ↑unitInterval), u ≠ 0 → φ u ∈ Set.Icc 0 a} {hφanti : ∀ (u v : ↑unitInterval), u ≠ 0 → u ≤ v → φ v ≤ φ u} {hφ1 : φ 1 = 0} {hright : ∀ (u : ↑unitInterval), u ≠ 0 → F (φ u) = ↑u} (t : ℝ) : (ofClamp F a ha hconv hanti hFa φ hφ hφanti hφ1 hright).toFun t = F (min t a)

theorem ProbabilityTheory.Copula.BivariateGenerator.ofClamp_invFun {F : ℝ → ℝ} {a : ℝ} {ha : 0 ≤ a} {hconv : ConvexOn ℝ (Set.Icc 0 a) F} {hanti : AntitoneOn F (Set.Icc 0 a)} {hFa : F a = 0} {φ : ↑unitInterval → ℝ} {hφ : ∀ (u : ↑unitInterval), u ≠ 0 → φ u ∈ Set.Icc 0 a} {hφanti : ∀ (u v : ↑unitInterval), u ≠ 0 → u ≤ v → φ v ≤ φ u} {hφ1 : φ 1 = 0} {hright : ∀ (u : ↑unitInterval), u ≠ 0 → F (φ u) = ↑u} (u : ↑unitInterval) : (ofClamp F a ha hconv hanti hFa φ hφ hφanti hφ1 hright).invFun u = φ u

theorem ProbabilityTheory.Copula.BivariateGenerator.ofClamp_toFun_of_le {F : ℝ → ℝ} {a : ℝ} {ha : 0 ≤ a} {hconv : ConvexOn ℝ (Set.Icc 0 a) F} {hanti : AntitoneOn F (Set.Icc 0 a)} {hFa : F a = 0} {φ : ↑unitInterval → ℝ} {hφ : ∀ (u : ↑unitInterval), u ≠ 0 → φ u ∈ Set.Icc 0 a} {hφanti : ∀ (u v : ↑unitInterval), u ≠ 0 → u ≤ v → φ v ≤ φ u} {hφ1 : φ 1 = 0} {hright : ∀ (u : ↑unitInterval), u ≠ 0 → F (φ u) = ↑u} {t : ℝ} (ht : a ≤ t) : (ofClamp F a ha hconv hanti hFa φ hφ hφanti hφ1 hright).toFun t = 0

A clamped generator is non-strict: its pseudo-inverse vanishes from a on.