Core Definitions

Basic definitions used throughout the formalization: the hinge function (x - u)₊, the stop-loss transform, and the tail-sense sub-Gaussian condition with zero mean.

def psi (u x : ℝ) : ℝ

The hinge function (x - u)_+.

Equations

• psi u x = max (x - u) 0

def IsSimpleConvex (f : ℝ → ℝ) : Prop

A finite positive linear combination of hinge functions plus an affine term.

Equations

• IsSimpleConvex f = ∃ (a : ℝ) (b : ℝ) (s : Finset ℝ) (w : ℝ → ℝ), (∀ u ∈ s, 0 ≤ w u) ∧ ∀ (x : ℝ), f x = a * x + b + ∑ u ∈ s, w u * psi u x

def IsOneSubgaussian {Ω : Type u_1} [MeasurableSpace Ω] (P : MeasureTheory.Measure Ω) (X : Ω → ℝ) : Prop

Tail-sense one-sub-Gaussianity with zero mean.

Equations

• IsOneSubgaussian P X = (MeasureTheory.Integrable X P ∧ ∫ (ω : Ω), X ω ∂P = 0 ∧ ∀ (t : ℝ), 0 ≤ t → (P {ω : Ω | |X ω| > t}).toReal ≤ 2 * Real.exp (-t ^ 2 / 2))

def OneDimConvexDom.posPart (x : ℝ) : ℝ

Positive part.

Equations

• OneDimConvexDom.posPart x = max x 0

def OneDimConvexDom.hinge (u x : ℝ) : ℝ

Stop-loss hinge (x - u)_+, written with the threshold first.

Equations

• OneDimConvexDom.hinge u x = OneDimConvexDom.posPart (x - u)

@[simp]

theorem OneDimConvexDom.posPart_def (x : ℝ) : posPart x = max x 0

@[simp]

theorem OneDimConvexDom.hinge_def (u x : ℝ) : hinge u x = max (x - u) 0

theorem OneDimConvexDom.hinge_nonneg (u x : ℝ) : 0 ≤ hinge u x

theorem OneDimConvexDom.posPart_add_eq (x v : ℝ) : posPart (x + v) = x + v + posPart (-x - v)

theorem OneDimConvexDom.hinge_neg_threshold (x v : ℝ) : hinge (-v) x = x + v + hinge v (-x)

def OneDimConvexDom.stopLoss (mu : MeasureTheory.Measure ℝ) (u : ℝ) : ℝ

Stop-loss transform of a measure.

Equations

• OneDimConvexDom.stopLoss mu u = ∫ (x : ℝ), OneDimConvexDom.hinge u x ∂mu

def OneDimConvexDom.mean (mu : MeasureTheory.Measure ℝ) : ℝ

Mean of a real-valued law.

Equations

• OneDimConvexDom.mean mu = ∫ (x : ℝ), x ∂mu

def OneDimConvexDom.StopLossDom (mu nu : MeasureTheory.Measure ℝ) : Prop

One-dimensional stop-loss domination.

Equations

• OneDimConvexDom.StopLossDom mu nu = (OneDimConvexDom.mean mu = OneDimConvexDom.mean nu ∧ ∀ (u : ℝ), OneDimConvexDom.stopLoss mu u ≤ OneDimConvexDom.stopLoss nu u)