Documentation

Copula.Order.Supermodular

← Copula mathematical handbook

Supermodular order and orthant comparisons #

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

Supermodularity on a lattice.

Equations

ProbabilityTheory.IsSupermodular f = ∀ (x y : α), f x + f y ≤ f (x ⊓ y) + f (x ⊔ y)

Instances For

theorem ProbabilityTheory.isSupermodular_lowerIndicator {α : Type u_1} [Lattice α] [DecidableLE α] (u : α) :

IsSupermodular fun (x : α) => if x ≤ u then 1 else 0

theorem ProbabilityTheory.isSupermodular_upperIndicator {α : Type u_1} [Lattice α] [DecidableLE α] (u : α) :

IsSupermodular fun (x : α) => if u ≤ x then 1 else 0

def ProbabilityTheory.Copula.SupermodularLE {d : ℕ} (C D : Copula d) :

Comparison of expectations of all bounded measurable supermodular functions.

Equations

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

Instances For

theorem ProbabilityTheory.Copula.SupermodularLE.refl {d : ℕ} (C : Copula d) :

C.SupermodularLE C

theorem ProbabilityTheory.Copula.SupermodularLE.trans {d : ℕ} {C D E : Copula d} (h : C.SupermodularLE D) (k : D.SupermodularLE E) :

C.SupermodularLE E

theorem ProbabilityTheory.Copula.SupermodularLE.lowerOrthantLE {d : ℕ} {C D : Copula d} (h : C.SupermodularLE D) :

C.LowerOrthantLE D

theorem ProbabilityTheory.Copula.SupermodularLE.upperOrthantLE {d : ℕ} {C D : Copula d} (h : C.SupermodularLE D) :

C.UpperOrthantLE D

theorem ProbabilityTheory.Copula.SupermodularLE.concordanceLE {d : ℕ} {C D : Copula d} (h : C.SupermodularLE D) :

C.ConcordanceLE D

theorem ProbabilityTheory.Copula.SupermodularLE.antisymm {d : ℕ} {C D : Copula d} (h : C.SupermodularLE D) (k : D.SupermodularLE C) :

C = D