Indicator functions

The indicator function δ(· | s) of a set, which is 0 on s and +∞ off it. It is the device by which every statement about convex sets becomes an instance of a statement about convex functions, and it is used that way throughout the library.

Main results

• convexFn_indicatorFn — δ(· | s) is convex iff s is convex.
• dom_indicatorFn, proper_indicatorFn — the effective domain is s, and δ(· | s) is proper exactly when s is non-empty.
• indicatorFn_add, indicatorFn_finsetSum — adding indicators intersects the sets.
• epi_indicatorFn — the epigraph is the half-cylinder s ×ˢ Ici 0.

References

• R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970, §4.

noncomputable def Tdaf.ConvexAnalysis.indicatorFn {E : Type u_1} (s : Set E) : E → EReal

The indicator function δ(· | s) of a set s: 0 on s, ⊤ off it.

Equations

• Tdaf.ConvexAnalysis.indicatorFn s = Tdaf.ConvexAnalysis.restrict s fun (x : E) => 0

@[simp]

theorem Tdaf.ConvexAnalysis.indicatorFn_of_mem {E : Type u_1} {s : Set E} {x : E} (hx : x ∈ s) : indicatorFn s x = 0

@[simp]

theorem Tdaf.ConvexAnalysis.indicatorFn_of_notMem {E : Type u_1} {s : Set E} {x : E} (hx : x ∉ s) : indicatorFn s x = ⊤

theorem Tdaf.ConvexAnalysis.indicatorFn_ne_bot {E : Type u_1} (s : Set E) (x : E) : indicatorFn s x ≠ ⊥

@[simp]

theorem Tdaf.ConvexAnalysis.dom_indicatorFn {E : Type u_1} (s : Set E) : dom (indicatorFn s) = s

@[simp]

theorem Tdaf.ConvexAnalysis.proper_indicatorFn {E : Type u_1} {s : Set E} : Proper (indicatorFn s) ↔ s.Nonempty

δ(· | s) is proper exactly when s is non-empty. In particular a constrained problem h + δ(· | C) has a proper constraint term without C being closed.

@[simp]

theorem Tdaf.ConvexAnalysis.indicatorFn_add {E : Type u_1} (s t : Set E) : indicatorFn s + indicatorFn t = indicatorFn (s ∩ t)

Adding indicators intersects the sets. 0 + 0 = 0, and ⊤ absorbs everything an indicator can be, so there is no side condition. This is why the intersection forms of results about convex sets are the indicator instances of statements about sums.

theorem Tdaf.ConvexAnalysis.indicatorFn_finsetSum {E : Type u_1} {ι : Type u_2} (C : ι → Set E) (s : Finset ι) : ∑ i ∈ s, indicatorFn (C i) = indicatorFn (⋂ i ∈ s, C i)

The m-ary indicatorFn_add: δ(· | C₁) + ⋯ + δ(· | Cₘ) = δ(· | C₁ ∩ ⋯ ∩ Cₘ), with no side condition. Over the empty Finset both sides are the zero function, since ⋂ i ∈ ∅, C i is univ.

theorem Tdaf.ConvexAnalysis.epi_indicatorFn {E : Type u_1} (s : Set E) : epi (indicatorFn s) = s ×ˢ Set.Ici 0

The epigraph of an indicator function is a half-cylinder with cross-section s.

@[simp]

theorem Tdaf.ConvexAnalysis.convexFn_indicatorFn {E : Type u_1} [AddCommGroup E] [Module ℝ E] {s : Set E} : ConvexFn (indicatorFn s) ↔ Convex ℝ s

δ(· | s) is a convex function exactly when s is a convex set.

@[simp]

theorem Tdaf.ConvexAnalysis.indicatorFn_vadd {E : Type u_1} [AddCommGroup E] (a : E) (s : Set E) (x : E) : indicatorFn (a +ᵥ s) x = indicatorFn s (x - a)

Translating the set translates the indicator: δ(x | a + s) = δ(x - a | s).

theorem Tdaf.ConvexAnalysis.restrict_eq_add_indicatorFn {E : Type u_1} {s : Set E} {f : E → EReal} (hf : ∀ (x : E), f x ≠ ⊥) : restrict s f = f + indicatorFn s

Adding an indicator function restricts the effective domain.