← Mathematical handbook

Total positivity of functions, copula CDFs and densities

IsTP2CDF concerns the CDF. HasMTP2Density requires a nonnegative Lebesgue density version satisfying the lattice inequality. They are distinct notions.

def ProbabilityTheory.IsTP2 {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α → β → ℝ) : Prop

Total positivity of order two of a bivariate function.

Equations

• ProbabilityTheory.IsTP2 f = ∀ (a b : α) (c d : β), a ≤ b → c ≤ d → f a d * f b c ≤ f a c * f b d

def ProbabilityTheory.IsMTP2 {α : Type u_1} [Lattice α] (f : α → ℝ) : Prop

Multivariate total positivity of order two, also called log-supermodularity. Nonnegativity is supplied separately when using this for a density.

Equations

• ProbabilityTheory.IsMTP2 f = ∀ (x y : α), f x * f y ≤ f (x ⊓ y) * f (x ⊔ y)

theorem ProbabilityTheory.IsTP2.swap {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f : α → β → ℝ} (h : IsTP2 f) : IsTP2 fun (b : β) (a : α) => f a b

theorem ProbabilityTheory.IsTP2.mul {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {f g : α → β → ℝ} (hf : IsTP2 f) (hg : IsTP2 g) (hnf : ∀ (a : α) (b : β), 0 ≤ f a b) (hng : ∀ (a : α) (b : β), 0 ≤ g a b) : IsTP2 fun (a : α) (b : β) => f a b * g a b

theorem ProbabilityTheory.IsMTP2.mul {α : Type u_1} [Lattice α] {f g : α → ℝ} (hf : IsMTP2 f) (hg : IsMTP2 g) (hnf : ∀ (x : α), 0 ≤ f x) (hng : ∀ (x : α), 0 ≤ g x) : IsMTP2 fun (x : α) => f x * g x

theorem ProbabilityTheory.IsMTP2.comp {α : Type u_1} {β : Type u_2} [Lattice α] [Lattice β] {f : β → ℝ} (hf : IsMTP2 f) (g : LatticeHom α β) : IsMTP2 (f ∘ ⇑g)

Composing with a lattice homomorphism preserves MTP2.

theorem ProbabilityTheory.isMTP2_const {α : Type u_1} [Lattice α] (c : ℝ) : IsMTP2 fun (x : α) => c

theorem ProbabilityTheory.isMTP2_prod {ι : Type u_1} {α : Type u_2} [Fintype ι] [LinearOrder α] (f : ι → α → ℝ) : IsMTP2 fun (x : ι → α) => ∏ i : ι, f i (x i)

Products of one-coordinate factors are MTP2, with equality in the lattice inequality.

theorem ProbabilityTheory.Copula.isMTP2_fin_two_iff {α : Type u_1} [LinearOrder α] (f : (Fin 2 → α) → ℝ) : IsMTP2 f ↔ IsTP2 fun (u v : α) => f ![u, v]

The lattice and ordered-rectangle formulations agree in dimension two.

def ProbabilityTheory.Copula.IsTP2CDF (C : Copula 2) : Prop

TP2 of the copula's distribution function.

Equations

• C.IsTP2CDF = ProbabilityTheory.IsTP2 fun (u v : ↑unitInterval) => C.cdf ![u, v]

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

A copula has an MTP2 density if some nonnegative measurable density version with respect to uniform cube volume satisfies the lattice inequality.

Equations

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

theorem ProbabilityTheory.Copula.IsTP2CDF.isLTD {C : Copula 2} (h : C.IsTP2CDF) : C.IsLTD

theorem ProbabilityTheory.Copula.IsTP2CDF.isPQD {C : Copula 2} (h : C.IsTP2CDF) : C.IsPQD

theorem ProbabilityTheory.Copula.isTP2CDF_independence : (independence 2).IsTP2CDF

theorem ProbabilityTheory.Copula.hasMTP2Density_independence (d : ℕ) : (independence d).HasMTP2Density