rieszContentAux_le
theorem rieszContentAux_le :
∀ {X : Type u_1} [inst : TopologicalSpace X] (Λ : BoundedContinuousFunction X NNReal →ₗ[NNReal] NNReal)
{K : TopologicalSpace.Compacts X} {f : BoundedContinuousFunction X NNReal},
(∀ x ∈ K, 1 ≤ f x) → rieszContentAux Λ K ≤ Λ f
This theorem states that for any type `X` with a topological space structure, a positive linear functional `Λ` on the space of bounded continuous functions from `X` to the nonnegative real numbers, a compact subset `K` of `X`, and a bounded continuous function `f` from `X` to the nonnegative real numbers such that `f` is greater than or equal to 1 on `K`, the Riesz content of `K` (defined as the infimum of the image of `Λ` over all functions that are greater than or equal to 1 on `K`) is less than or equal to the value of `Λ` at `f`. In other words, any bounded continuous nonnegative function `f` that is greater than or equal to 1 on a compact subset `K` provides an upper bound on the Riesz content of `K`.
More concisely: For any compact subset K of a topological space X with a topology and a positive linear functional Λ on the bounded continuous functions from X to the nonnegative real numbers, if f is a bounded, continuous, nonnegative function on X that is greater than or equal to 1 on K, then the Riesz content of K is less than or equal to Λ(f).
|
rieszContentAux_mono
theorem rieszContentAux_mono :
∀ {X : Type u_1} [inst : TopologicalSpace X] (Λ : BoundedContinuousFunction X NNReal →ₗ[NNReal] NNReal)
{K₁ K₂ : TopologicalSpace.Compacts X}, K₁ ≤ K₂ → rieszContentAux Λ K₁ ≤ rieszContentAux Λ K₂
The theorem `rieszContentAux_mono` states that the Riesz content, associated with a positive linear functional Λ, is monotonic with respect to the inclusion of compact subsets in a given topological space X. More precisely, if `K₁` and `K₂` are compact subsets of X such that `K₁` is a subset of `K₂`, then the Riesz content of `K₁` with respect to Λ is less than or equal to the Riesz content of `K₂` with respect to Λ. In mathematical terms, if `K₁ ⊆ K₂`, then `λ(K₁) ≤ λ(K₂)`.
More concisely: If `K₁` is a compact subset of `X` that is included in `K₂`, then the Riesz content of `K₁` with respect to a positive linear functional `Λ` is less than or equal to the Riesz content of `K₂` with respect to `Λ` (i.e., `λ(K₁) ≤ λ(K₂)`).
|
exists_lt_rieszContentAux_add_pos
theorem exists_lt_rieszContentAux_add_pos :
∀ {X : Type u_1} [inst : TopologicalSpace X] (Λ : BoundedContinuousFunction X NNReal →ₗ[NNReal] NNReal)
(K : TopologicalSpace.Compacts X) {ε : NNReal}, 0 < ε → ∃ f, (∀ x ∈ K, 1 ≤ f x) ∧ Λ f < rieszContentAux Λ K + ε
This theorem states that the Riesz content can be approximated arbitrarily well by evaluating a positive linear functional on test functions in a topological space. More specifically, for any nonnegative real number `ε` that is greater than zero, there exists a bounded continuous nonnegative function `f` on the topological space `X` such that `f` is greater than or equal to `1` on a compact subset `K` of `X`, and the value of the positive linear functional `Λ` applied to `f` is less than the Riesz content of `Λ` on `K` increased by `ε`.
More concisely: For any nonnegative real number `ε` and compact subset `K` of a topological space `X`, there exists a bounded continuous nonnegative function `f` on `X` with `f ≥ 1` on `K`, such that the Riesz functional value `Λ(f)` is less than the Riesz content of `Λ` on `K` plus `ε`.
|
rieszContentAux_image_nonempty
theorem rieszContentAux_image_nonempty :
∀ {X : Type u_1} [inst : TopologicalSpace X] (Λ : BoundedContinuousFunction X NNReal →ₗ[NNReal] NNReal)
(K : TopologicalSpace.Compacts X), (⇑Λ '' {f | ∀ x ∈ K, 1 ≤ f x}).Nonempty
This theorem states that for any compact subset `K` of a topological space `X`, there exist some bounded continuous nonnegative real-valued functions `f` on `X`, such that the value of `f` is greater than or equal to 1 on `K`. Here, `Λ` is a linear map from the space of bounded continuous functions from `X` to nonnegative real numbers to the nonnegative real numbers. The theorem asserts that the image of the set of such functions `f` under the map `Λ` is nonempty.
More concisely: For any compact subset K of a topological space X, the image under a linear map Λ from the space of bounded continuous nonnegative real-valued functions on X to the nonnegative real numbers containing only functions with a minimum value of 1 on K is nonempty.
|
rieszContentAux_sup_le
theorem rieszContentAux_sup_le :
∀ {X : Type u_1} [inst : TopologicalSpace X] (Λ : BoundedContinuousFunction X NNReal →ₗ[NNReal] NNReal)
(K1 K2 : TopologicalSpace.Compacts X),
rieszContentAux Λ (K1 ⊔ K2) ≤ rieszContentAux Λ K1 + rieszContentAux Λ K2
The theorem named `rieszContentAux_sup_le` states that for any type `X` equipped with a topological space structure, given a positive linear functional `Λ` acting on bounded continuous functions from `X` to the nonnegative real numbers (`NNReal`), and any two compact sets `K1` and `K2` in `X`, the Riesz content `λ` associated to `Λ` satisfies finite subadditivity. Specifically, the Riesz content of the union of `K1` and `K2` is less than or equal to the sum of the Riesz content of `K1` and the Riesz content of `K2`. This can be written mathematically as `λ(K₁ ∪ K₂) ≤ λ(K₁) + λ(K₂)`. This property is a crucial aspect of measure theory and is fundamental to the integration of functions over topological spaces.
More concisely: For any positive linear functional acting on bounded continuous functions from a topological space `X` to nonnegative real numbers and any two compact sets `K1` and `K2` in `X`, the Riesz content of their union is less than or equal to the sum of their individual Riesz contents.
|