Uniform positivity of continuous functions

The continuous real-valued functions bounded below by a positive constant form a convex set. On a compact domain this set is open for the uniform topology. These facts apply, for example, to separating positive continuous functions in the proof of Pietsch domination.

A linear functional on C(X, ℝ) that is bounded above on the uniformly positive functions is nonpositive on them, since they form a cone, and hence nonpositive on every nonnegative function: adding a small positive constant to a nonnegative function makes it uniformly positive. This is the positivity of the functional produced by separating the uniformly positive functions from a cone.

Main results

• ContinuousMap.convex_uniformlyPositive: the uniformly positive functions form a convex set.
• ContinuousMap.isOpen_uniformlyPositive: on a compact space they form an open set.
• LinearMap.apply_nonpos_of_forall_uniformlyPositive_lt: a functional bounded above on the uniformly positive functions is nonpositive on the nonnegative functions.

theorem ContinuousMap.convex_uniformlyPositive {X : Type u_1} [TopologicalSpace X] : Convex ℝ {h : C(X, ℝ) | ∃ δ > 0, ∀ (x : X), δ ≤ h x}

The continuous real functions uniformly bounded below by a positive constant form a convex set.

theorem ContinuousMap.isOpen_uniformlyPositive {X : Type u_1} [TopologicalSpace X] [CompactSpace X] : IsOpen {h : C(X, ℝ) | ∃ δ > 0, ∀ (x : X), δ ≤ h x}

Uniform positivity is open in the uniform topology on continuous functions on a compact space.

theorem LinearMap.apply_nonpos_of_forall_uniformlyPositive_lt {X : Type u_1} [TopologicalSpace X] (L : C(X, ℝ) →ₗ[ℝ] ℝ) {u : ℝ} (hL : ∀ h ∈ {h : C(X, ℝ) | ∃ δ > 0, ∀ (x : X), δ ≤ h x}, L h < u) {h : C(X, ℝ)} (hh : 0 ≤ h) : L h ≤ 0

A linear functional on C(X, ℝ) that is bounded above on the functions bounded below by a positive constant is nonpositive on the nonnegative functions.