@[reducible, inline]

abbrev C₀Map (X : Type u_1) [TopologicalSpace X] : Type u_1

The space C₀(X, ℝ) of continuous real-valued functions on X vanishing at infinity.

def ContinuousFunctions.IsPositiveFunctional {X : Type u_1} [TopologicalSpace X] (u : C₀Map X →L[ℝ] ℝ) : Prop

A continuous linear functional u on C₀(X, ℝ) is positive iff it sends nonnegative functions to nonnegative real numbers.

theorem ContinuousFunctions.c0_eval_le_norm {X : Type u_1} [MetricSpace X] (f : C₀Map X) (x : X) : |f x| ≤ ‖f‖

Pointwise evaluation of a C₀ function is bounded by its sup norm.

theorem ContinuousFunctions.c0_norm_le_of_nonneg_le {X : Type u_1} [MetricSpace X] (f g : C₀Map X) (hg0 : ∀ (x : X), 0 ≤ g x) (hgf : ∀ (x : X), g x ≤ f x) : ‖g‖ ≤ ‖f‖

Monotonicity of the sup norm on nonnegative C₀ functions: if 0 ≤ g ≤ f pointwise then ‖g‖ ≤ ‖f‖.

noncomputable def ContinuousFunctions.c0min {X : Type u_1} [MetricSpace X] (f g : C₀Map X) : C₀Map X

The pointwise minimum of two C₀ functions, again in C₀(X, ℝ).

def ContinuousFunctions.posPartSet {X : Type u_1} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) (f : C₀Map X) : Set ℝ

For a functional u and f ∈ C₀(X, ℝ), the set of values u g ranging over g with 0 ≤ g ≤ f pointwise. The supremum of this set defines the positive part u⁺(f).

theorem ContinuousFunctions.posPartSet_nonempty {X : Type u_1} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) (f : C₀Map X) (hf : ∀ (x : X), 0 ≤ f x) : (posPartSet u f).Nonempty

For nonnegative f, the set posPartSet u f is nonempty, witnessed by the choice g = 0.

theorem ContinuousFunctions.posPartSet_bddAbove {X : Type u_1} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) (f : C₀Map X) (_hf : ∀ (x : X), 0 ≤ f x) : BddAbove (posPartSet u f)

The set posPartSet u f is bounded above by ‖u‖ * ‖f‖.

noncomputable def ContinuousFunctions.posPartSup {X : Type u_1} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) (f : C₀Map X) : ℝ

The positive part of u evaluated at f: defined as sup {u g | 0 ≤ g ≤ f}. This is the classical construction used to extract the positive component in the Jordan decomposition.

theorem ContinuousFunctions.posPartSup_nonneg {X : Type u_1} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) (f : C₀Map X) (hf : ∀ (x : X), 0 ≤ f x) : 0 ≤ posPartSup u f

For nonnegative f, the positive-part supremum is nonnegative.

theorem ContinuousFunctions.posPartSup_le_norm_mul {X : Type u_1} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) (f : C₀Map X) (hf : ∀ (x : X), 0 ≤ f x) : posPartSup u f ≤ ‖u‖ * ‖f‖

The positive-part supremum is bounded above by ‖u‖ * ‖f‖.

theorem ContinuousFunctions.posPartSup_zero {X : Type u_1} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) : posPartSup u 0 = 0

The positive-part supremum vanishes at the zero function.

theorem ContinuousFunctions.posPartSup_add {X : Type u_1} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) (f₁ f₂ : C₀Map X) (hf₁ : ∀ (x : X), 0 ≤ f₁ x) (hf₂ : ∀ (x : X), 0 ≤ f₂ x) : posPartSup u (f₁ + f₂) = posPartSup u f₁ + posPartSup u f₂

Additivity of the positive-part supremum on nonnegative functions: for f₁, f₂ ≥ 0 we have posPartSup u (f₁ + f₂) = posPartSup u f₁ + posPartSup u f₂.

theorem ContinuousFunctions.posPartSup_smul_pos {X : Type u_1} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) (f : C₀Map X) (hf : ∀ (x : X), 0 ≤ f x) (c : ℝ) (hc : 0 < c) : posPartSup u (c • f) = c * posPartSup u f

Homogeneity of posPartSup under multiplication by a positive scalar.

theorem ContinuousFunctions.posPartSup_smul_nonneg {X : Type u_1} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) (f : C₀Map X) (hf : ∀ (x : X), 0 ≤ f x) (c : ℝ) (hc : 0 ≤ c) : posPartSup u (c • f) = c * posPartSup u f

Homogeneity of posPartSup under multiplication by a nonnegative scalar.

theorem ContinuousFunctions.posPartSup_well_defined {X : Type u_1} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) (f h₁ h₂ : C₀Map X) (hh₁ : ∀ (x : X), 0 ≤ h₁ x) (hh₂ : ∀ (x : X), 0 ≤ h₂ x) (hf : f = h₁ - h₂) : posPartSup u (zeroAtInftyPosPart f) - posPartSup u (zeroAtInftyNegPart f) = posPartSup u h₁ - posPartSup u h₂

Well-definedness of the positive part on signed decompositions: if f = h₁ - h₂ with h₁, h₂ ≥ 0, then posPartSup u f⁺ - posPartSup u f⁻ = posPartSup u h₁ - posPartSup u h₂.

noncomputable def ContinuousFunctions.posPartFn {X : Type u_1} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) (f : C₀Map X) : ℝ

The positive-part functional extended to arbitrary (signed) C₀ functions via the decomposition f = f⁺ - f⁻.

theorem ContinuousFunctions.posPartFn_add {X : Type u_1} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) (f g : C₀Map X) : posPartFn u (f + g) = posPartFn u f + posPartFn u g

Additivity of posPartFn on arbitrary C₀ functions.

theorem ContinuousFunctions.posPartFn_smul_nonneg {X : Type u_1} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) (f : C₀Map X) (c : ℝ) (hc : 0 ≤ c) : posPartFn u (c • f) = c * posPartFn u f

Homogeneity of posPartFn under multiplication by a nonnegative scalar.

theorem ContinuousFunctions.posPartFn_smul_neg {X : Type u_1} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) (f : C₀Map X) (c : ℝ) (hc : c < 0) : posPartFn u (c • f) = c * posPartFn u f

Homogeneity of posPartFn under multiplication by a negative scalar (using the symmetry between positive and negative parts under negation).

theorem ContinuousFunctions.posPartFn_smul {X : Type u_1} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) (f : C₀Map X) (c : ℝ) : posPartFn u (c • f) = c * posPartFn u f

Full ℝ-linearity of posPartFn in the scalar argument.

theorem ContinuousFunctions.posPartFn_bound {X : Type u_1} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) (f : C₀Map X) : ‖posPartFn u f‖ ≤ ‖u‖ * ‖f‖

Operator-norm bound for the positive part functional: ‖posPartFn u f‖ ≤ ‖u‖ * ‖f‖.

noncomputable def ContinuousFunctions.posPartLinearMap {X : Type u_1} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) : C₀Map X →ₗ[ℝ] ℝ

The positive part of a continuous linear functional u packaged as a linear map.

noncomputable def ContinuousFunctions.posPartCLM {X : Type u_2} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) : C₀Map X →L[ℝ] ℝ

The positive part of a continuous linear functional u on C₀(X, ℝ), packaged as a CLM.

theorem ContinuousFunctions.posPartCLM_apply {X : Type u_1} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) (f : C₀Map X) : (posPartCLM u) f = posPartFn u f

The CLM posPartCLM u agrees with the function posPartFn u.

theorem ContinuousFunctions.posPartCLM_positive {X : Type u_2} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) : IsPositiveFunctional (posPartCLM u)

The positive part posPartCLM u is a positive linear functional on C₀(X, ℝ).

theorem ContinuousFunctions.posPartCLM_ge {X : Type u_2} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) (f : C₀Map X) (hf : ∀ (x : X), 0 ≤ f x) : u f ≤ (posPartCLM u) f

For nonnegative f, the value u f is dominated by the positive part posPartCLM u f.

theorem ContinuousFunctions.norm_posPartCLM_le {X : Type u_2} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) : ‖posPartCLM u‖ ≤ ‖u‖

The operator norm of the positive part is bounded by the operator norm of u.

theorem ContinuousFunctions.norm_negPart_le {X : Type u_2} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) : ‖posPartCLM u - u‖ ≤ ‖u‖

The operator norm of the negative part posPartCLM u - u is bounded by the operator norm of u.

theorem ContinuousFunctions.dual_jordan_decomposition {X : Type u_1} [MetricSpace X] (u : C₀Map X →L[ℝ] ℝ) : ∃ (u_pos : C₀Map X →L[ℝ] ℝ) (u_neg : C₀Map X →L[ℝ] ℝ), IsPositiveFunctional u_pos ∧ IsPositiveFunctional u_neg ∧ u = u_pos - u_neg ∧ ‖u_pos‖ ≤ ‖u‖ ∧ ‖u_neg‖ ≤ ‖u‖

Lemma 1.5 (Jordan decomposition for C₀ functionals): every continuous linear functional u : C₀(X, ℝ) →L[ℝ] ℝ decomposes as a difference u = u₊ - u₋ of two positive linear functionals whose operator norms are bounded by ‖u‖.