Convex.average_mem
theorem Convex.average_mem :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E}
[inst_3 : MeasureTheory.IsFiniteMeasure μ] [inst_4 : NeZero μ],
Convex ℝ s → IsClosed s → (∀ᵐ (x : α) ∂μ, f x ∈ s) → MeasureTheory.Integrable f μ → ⨍ (x : α), f x ∂μ ∈ s
The theorem `Convex.average_mem` states the following mathematical fact: For any non-zero finite measure `μ` on a set `α`, a convex and closed set `s` in a normed additive group `E` equipped with a normed space structure over the real numbers ℝ and a complete space structure, and an integrable function `f` from `α` to `E` such that almost every point with respect to `μ` is mapped to `s`, the average value of `f`, represented by the integral of `f` with respect to `μ`, belongs to the set `s`. This theorem can be seen as an infinite-dimensional version of the result stating that the center of mass of a finite set of points in a convex set also belongs to the convex set.
More concisely: If `μ` is a non-zero finite measure on a set `α`, `s` is a convex and closed set in a complete normed additive group `E` over `ℝ`, and `f` is an integrable function from `α` to `E` such that almost every point in `α` with respect to `μ` maps to `s`, then the integral of `f` with respect to `μ` is an element of `s`.
|
StrictConvex.ae_eq_const_or_average_mem_interior
theorem StrictConvex.ae_eq_const_or_average_mem_interior :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E}
[inst_3 : MeasureTheory.IsFiniteMeasure μ],
StrictConvex ℝ s →
IsClosed s →
(∀ᵐ (x : α) ∂μ, f x ∈ s) →
MeasureTheory.Integrable f μ →
μ.ae.EventuallyEq f (Function.const α (⨍ (x : α), f x ∂μ)) ∨ ⨍ (x : α), f x ∂μ ∈ interior s
The theorem `StrictConvex.ae_eq_const_or_average_mem_interior` states that for any strictly convex closed set `s` in a complete normed vector space where the scalar field is the real numbers and for any integrable function `f` that maps from a given measurable space `α` to the vector space such that almost every value of `f` lies in `s`, either the function `f` is almost everywhere equal to its average value, or the average value of the function `f` lies in the interior of the set `s`. Here, the average value of the function is calculated using Lebesgue integration with respect to the measure `μ`.
In mathematical terms, if $s$ is a strictly convex and closed subset of a complete normed vector space over the field of real numbers, and $f: \alpha \rightarrow E$ is an integrable function such that almost all of its values lie in $s$, then either $f$ is almost everywhere constant and equal to its average value, or this average value lies in the interior of the set $s$.
More concisely: If $s$ is a strictly convex and closed subset of a complete normed vector space over the real numbers, and $f: \alpha \rightarrow s$ is an integrable function with almost all values in $s$, then either $f$ is almost everywhere constant and equal to its Lebesgue average, or the Lebesgue average lies in the interior of $s$.
|
ConcaveOn.set_average_mem_hypograph
theorem ConcaveOn.set_average_mem_hypograph :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E} {g : E → ℝ},
ConcaveOn ℝ s g →
ContinuousOn g s →
IsClosed s →
↑↑μ t ≠ 0 →
↑↑μ t ≠ ⊤ →
(∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s) →
MeasureTheory.IntegrableOn f t μ →
MeasureTheory.IntegrableOn (g ∘ f) t μ →
(⨍ (x : α) in t, f x ∂μ, ⨍ (x : α) in t, g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ p.2 ≤ g p.1}
**Jensen's Inequality Theorem** states: For a function `g` mapping from `E` to real numbers that is both concave and continuous on a convex and closed set `s`, and given `μ` as a finite non-zero measure on a set `α`, if there's a function `f` that almost everywhere maps points of another set `t` to `s`, then the average value of the composition of `g` and `f` over `t` is less than or equal to the value of `g` at the average value of `f` over `t`. This is on the condition that both `f` and the composition of `g` and `f` are integrable. Here, `f` is a function from `α` to `E`, and `g` is a function from `E` to real numbers.
More concisely: For a concave and continuous function `g` on a convex and closed set `s`, and a finite non-zero measure `μ` on a set `α`, if `f` is an integrable function from `α` to `s` such that `g ∘ f` is also integrable, then the integral of `g ∘ f` over `α` is less than or equal to `g` evaluated at the integral of `f` over `α`.
|
ConcaveOn.le_map_integral
theorem ConcaveOn.le_map_integral :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ}
[inst_3 : MeasureTheory.IsProbabilityMeasure μ],
ConcaveOn ℝ s g →
ContinuousOn g s →
IsClosed s →
(∀ᵐ (x : α) ∂μ, f x ∈ s) →
MeasureTheory.Integrable f μ →
MeasureTheory.Integrable (g ∘ f) μ → ∫ (x : α), g (f x) ∂μ ≤ g (∫ (x : α), f x ∂μ)
**Jensen's inequality theorem** states that if we have a function `g : E → ℝ` that is concave and continuous on a convex closed set `s`, a probability measure `μ` on `α`, and another function `f : α → E` that maps almost every point with respect to `μ` to `s`, then the expected value of the function `g` composed with `f`, is less than or equal to the value of `g` at the expected value of `f`. This holds provided both `f` and the composite function `g ∘ f` are integrable. In mathematical terms, if `g` is concave on `s` and `f(x)` belongs to `s` for almost all `x` with respect to measure `μ`, then `∫ g(f(x)) dμ ≤ g(∫ f(x) dμ)`. This theorem is a fundamental result in probability theory and mathematical optimization.
More concisely: If `g : E → ℝ` is a concave, continuous function on a convex, closed set `s`, and `f : α → E` maps almost every point in the measure space `(α, μ)` to `s` with both `f` and `g ∘ f` integrable, then `∫ g(f(x)) dμ ≤ g(∫ f(x) dμ)`.
|
StrictConvexOn.ae_eq_const_or_map_average_lt
theorem StrictConvexOn.ae_eq_const_or_map_average_lt :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ}
[inst_3 : MeasureTheory.IsFiniteMeasure μ],
StrictConvexOn ℝ s g →
ContinuousOn g s →
IsClosed s →
(∀ᵐ (x : α) ∂μ, f x ∈ s) →
MeasureTheory.Integrable f μ →
MeasureTheory.Integrable (g ∘ f) μ →
μ.ae.EventuallyEq f (Function.const α (⨍ (x : α), f x ∂μ)) ∨
g (⨍ (x : α), f x ∂μ) < ⨍ (x : α), g (f x) ∂μ
This theorem is a strict version of Jensen's inequality. It states that if we have an integrable function `f` from `α` to `E`, which takes values in a closed convex set `s`, and another function `g` from `E` to real numbers that is continuous and strictly convex on `s`, then one of the following two conditions must hold:
1) The function `f` is almost everywhere equal to its average value, meaning that for almost every `x` in `α`, `f(x)` equals the integral over `α` of `f`, with respect to measure `μ`.
2) The value of the function `g` at the average value of `f` is strictly less than the integral over `α` of the function `g` composed with `f`, with respect to measure `μ`.
Note here that `⨍ (x : α), f x ∂μ` represents the integral of `f` with respect to `μ` over `α`, and `⨍ (x : α), g (f x) ∂μ` represents the integral of the composition of `g` and `f`, again with respect to `μ` over `α`.
More concisely: If `f` is an integrable function from `α` to a closed convex set `s` with continuous and strictly convex function `g` on `s`, then either `f` is almost everywhere the average of its integral or `g(⨍x:α, f x ∂μ) < ⨍x:α, g(f x) ∂μ`.
|
Convex.integral_mem
theorem Convex.integral_mem :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E}
[inst_3 : MeasureTheory.IsProbabilityMeasure μ],
Convex ℝ s → IsClosed s → (∀ᵐ (x : α) ∂μ, f x ∈ s) → MeasureTheory.Integrable f μ → ∫ (x : α), f x ∂μ ∈ s
This theorem states that if we have a probability measure `μ` on a type `α`, a convex and closed set `s` in a normed additive commutative group `E` which is also a complete normed space over the reals, and an integrable function `f` that maps almost every point with respect to the measure `μ` to the set `s`, then the expected value of `f` (that is, the integral of `f` with respect to `μ`) belongs to the set `s`. This result can also be seen as an infinite-dimensional version of the fact that the sum of points in a convex set is still within the set.
More concisely: If `μ` is a probability measure on type `α`, `s` is a convex, closed, and complete normed subspace of a real normed additive commutative group `E`, and `f` is an integrable function almost everywhere mapping values in `α` to `s`, then the expected value of `f` with respect to `μ` lies within `s`.
|
ConvexOn.map_average_le
theorem ConvexOn.map_average_le :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ}
[inst_3 : MeasureTheory.IsFiniteMeasure μ] [inst_4 : NeZero μ],
ConvexOn ℝ s g →
ContinuousOn g s →
IsClosed s →
(∀ᵐ (x : α) ∂μ, f x ∈ s) →
MeasureTheory.Integrable f μ →
MeasureTheory.Integrable (g ∘ f) μ → g (⨍ (x : α), f x ∂μ) ≤ ⨍ (x : α), g (f x) ∂μ
**Jensen's Inequality**: Given a function `g` from `E` to `ℝ` that is convex and continuous on a convex closed set `s`, a finite non-zero measure `μ` on `α`, and a function `f` from `α` to `E` that sends almost every point with respect to `μ` to `s`, Jensen's Inequality states that the value of `g` at the average of `f` is less than or equal to the average of `g` composed with `f`, provided that both `f` and `g ∘ f` are integrable with respect to `μ`. A version of this theorem for finite sums is also available as `ConvexOn.map_centerMass_le`.
In mathematical notation: Let `g : E → ℝ` be a convex and continuous function on a convex closed set `s`, `μ` a finite non-zero measure on `α`, and `f : α → E` a function such that for almost every `x` in `α` under `μ`, `f(x)` is in `s`. If both `f` and `g ∘ f` are integrable under `μ`, then `g ( ∫ x, f(x) dμ ) ≤ ∫ x, g(f(x)) dμ`.
More concisely: Given a convex, continuous function `g` on a convex closed set `s`, a finite non-zero measure `μ`, and a function `f` mapping almost every `μ`-measure point in a set to `s`, if `f` and `g ∘ f` are integrable, then `g(∫x, f(x) dμ) ≤ ∫x, g(f(x)) dμ`.
|
ConcaveOn.le_map_average
theorem ConcaveOn.le_map_average :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ}
[inst_3 : MeasureTheory.IsFiniteMeasure μ] [inst_4 : NeZero μ],
ConcaveOn ℝ s g →
ContinuousOn g s →
IsClosed s →
(∀ᵐ (x : α) ∂μ, f x ∈ s) →
MeasureTheory.Integrable f μ →
MeasureTheory.Integrable (g ∘ f) μ → ⨍ (x : α), g (f x) ∂μ ≤ g (⨍ (x : α), f x ∂μ)
This theorem, known as Jensen's Inequality, states the following: Given a function `g : E → ℝ` that is concave and continuous on a convex closed set `s`, a finite non-zero measure `μ` on a set `α`, and a function `f : α → E` that maps almost every point (with respect to `μ`) to `s`, if both `f` and `g ∘ f` are integrable (namely, measurable and having finite integral), then the average value of `g ∘ f` is less than or equal to the value of `g` at the average value of `f`. This theorem also references a finite sum version of this lemma, `ConcaveOn.le_map_centerMass`.
More concisely: For a concave and continuous function `g` on a convex closed set `s`, a finite non-zero measure `μ` on a set `α`, and a measurable function `f : α → s` such that both `f` and `g ∘ f` are integrable, the integral of `g ∘ f` with respect to `μ` is less than or equal to `g` evaluated at the integral of `f` with respect to `μ`.
|
ConvexOn.average_mem_epigraph
theorem ConvexOn.average_mem_epigraph :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ}
[inst_3 : MeasureTheory.IsFiniteMeasure μ] [inst_4 : NeZero μ],
ConvexOn ℝ s g →
ContinuousOn g s →
IsClosed s →
(∀ᵐ (x : α) ∂μ, f x ∈ s) →
MeasureTheory.Integrable f μ →
MeasureTheory.Integrable (g ∘ f) μ →
(⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ g p.1 ≤ p.2}
The theorem `ConvexOn.average_mem_epigraph` states that for any measurable space `α`, a normed additively commutative group `E` which is a complete normed space over the field of real numbers, a measure `μ` on `α`, a set `s` in `E`, and functions `f` from `α` to `E` and `g` from `E` to real numbers (`ℝ`), given that `μ` is a finite measure and non-zero, if `g` is convex on `s` and continuous on `s`, `s` is a closed set, `f(x)` is in `s` for almost every `x` (with respect to the measure `μ`), and both `f` and `g` composed with `f` are integrable (with respect to the measure `μ`), then the `pairwise` integral of `f` and `g` composed with `f` over `μ` is an element of the epigraph of `g` restricted to `s`. The epigraph of a function is the set of points lying above its graph, i.e., it is the set of `pairs (x, y)` such that `y` is greater than or equal to the function value at `x`.
More concisely: If `μ` is a finite, non-zero measure on measurable space `α`, `E` is a complete normed space over `ℝ`, `s ⊆ E` is a closed set, `f: α → E`, `g: E → ℝ` are measurable functions with `g` convex and continuous on `s`, and `f(x) ∈ s` almost surely with respect to `μ` and `f`, `g ∘ f` and `f` are integrable with respect to `μ`, then `∫ x ∈ α (g (f x)) dμ ∈ Epigraph g (s)`.
|
ae_eq_const_or_norm_set_integral_lt_of_norm_le_const
theorem ae_eq_const_or_norm_set_integral_lt_of_norm_le_const :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {t : Set α} {f : α → E} {C : ℝ}
[inst_3 : StrictConvexSpace ℝ E],
↑↑μ t ≠ ⊤ →
(∀ᵐ (x : α) ∂μ.restrict t, ‖f x‖ ≤ C) →
(μ.restrict t).ae.EventuallyEq f (Function.const α (⨍ (x : α) in t, f x ∂μ)) ∨
‖∫ (x : α) in t, f x ∂μ‖ < (↑↑μ t).toReal * C
This theorem, named `ae_eq_const_or_norm_set_integral_lt_of_norm_le_const`, states that for a strictly convex normed space `E` and a function `f : α → E` such that the norm of `f(x)` is less than or equal to a constant `C` almost everywhere on a set `t` of finite measure, either this function is almost everywhere equal to its average value on `t`, or the norm of its integral over `t` is strictly less than the product of the measure of `t` and `C`.
Here, `α` is the type of the elements in the set `t`, `E` denotes a normed add commutative group which is also a normed space over real numbers and is complete, `μ` represents a measure on `α`, and `C` is a real number.
More concisely: For a strictly convex, complete, real-valued normed space E with measure μ over set α, if function f : α → E has almost everywhere norm ≤ C and its integral over t with finite measure is not equal to the average of f over t, then the norm of the integral is strictly less than the product of the measure of t and C.
|
Convex.set_average_mem_closure
theorem Convex.set_average_mem_closure :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E},
Convex ℝ s →
↑↑μ t ≠ 0 →
↑↑μ t ≠ ⊤ →
(∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s) →
MeasureTheory.IntegrableOn f t μ → ⨍ (x : α) in t, f x ∂μ ∈ closure s
This theorem states that if we have a non-zero finite measure `μ` on a type `α`, a convex set `s` in a normed additively commutative group `E` that is also a complete normed space over the real numbers, and a function `f` that is integrable on a set `t` with respect to measure `μ` and that sends almost every point with respect to measure `μ` restricted to `t` to `s`, then the average value of `f` with respect to `μ` over `t` belongs to the closure of `s`. This theorem provides a generalization of the fact that the "center of mass" of a finite sum of points in a convex set remains within the set.
More concisely: If `μ` is a non-zero finite measure on `α`, `s` is a convex, complete normed subspace of a normed additively commutative group `E` over the real numbers, `f` is an integrable function from `t` to `E` that maps almost every point in `t` to `s`, then the average value of `f` with respect to `μ` over `t` is in the closure of `s`.
|
ae_eq_const_or_norm_average_lt_of_norm_le_const
theorem ae_eq_const_or_norm_average_lt_of_norm_le_const :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {f : α → E} {C : ℝ} [inst_3 : StrictConvexSpace ℝ E],
(∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) →
μ.ae.EventuallyEq f (Function.const α (⨍ (x : α), f x ∂μ)) ∨ ‖⨍ (x : α), f x ∂μ‖ < C
The theorem `ae_eq_const_or_norm_average_lt_of_norm_le_const` states that for any type `α`, any strictly convex normed space `E`, any measurable space `m0`, any measure `μ` on `m0`, and any function `f` from `α` to `E`, if almost every element `x` in the domain of `f` satisfies the condition that the norm of `f(x)` is less than or equal to a constant `C`, then either the function `f` is almost everywhere equal to its average value, or the norm of the average value of `f` is strictly less than `C`. The notation `⨍ (x : α), f x ∂μ` represents the average value of `f` with respect to the measure `μ`.
More concisely: If a measurable function from a domain to a strictly convex normed space satisfies almost everywhere that the norm is less than or equal to a constant, then either the function is almost everywhere equal to its norm-bounded average or the average's norm strictly falls below the constant.
|
Convex.average_mem_interior_of_set
theorem Convex.average_mem_interior_of_set :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E}
[inst_3 : MeasureTheory.IsFiniteMeasure μ],
Convex ℝ s →
↑↑μ t ≠ 0 →
(∀ᵐ (x : α) ∂μ, f x ∈ s) →
MeasureTheory.Integrable f μ → ⨍ (x : α) in t, f x ∂μ ∈ interior s → ⨍ (x : α), f x ∂μ ∈ interior s
The theorem `Convex.average_mem_interior_of_set` states that given a measurable space `α`, a normed add commutative group `E` that is also a normed space over the real numbers and a complete space, a measure `μ` on `α`, a convex set `s` of `E`, another set `t` of `α`, and a function `f` mapping from `α` to `E`. If `μ` is a finite measure, `s` is convex, the measure of `t` is not zero, almost every `x` in `α` maps to `s` by `f`, and `f` is integrable with respect to `μ`, then if the average value of `f` over `t` belongs to the interior of `s`, it implies that the average of `f` over the entirety of `α` also belongs to the interior of `s`. In mathematical terms, this means that if $\int_t f(x) d\mu$ is in the interior of `s`, then $\int f(x) d\mu$ is also in the interior of `s`.
More concisely: If a measurable function from a measurable space with a finite measure, mapping from a convex set in a complete normed space into itself, has its average value over a non-empty set with positive measure belonging to the interior of the set, then its overall average value also lies in the interior of the set.
|
ConvexOn.set_average_mem_epigraph
theorem ConvexOn.set_average_mem_epigraph :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E} {g : E → ℝ},
ConvexOn ℝ s g →
ContinuousOn g s →
IsClosed s →
↑↑μ t ≠ 0 →
↑↑μ t ≠ ⊤ →
(∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s) →
MeasureTheory.IntegrableOn f t μ →
MeasureTheory.IntegrableOn (g ∘ f) t μ →
(⨍ (x : α) in t, f x ∂μ, ⨍ (x : α) in t, g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ g p.1 ≤ p.2}
Jensen's inequality states that if we have a function `g : E → ℝ` that is both convex and continuous on a convex closed set `s`, and a measure `μ` on `α` which is finite and non-zero, then if there is a function `f : α → E` that sends `μ`-almost every point of a set `t` to `s`, the value of `g` taken at the average value of `f` over `t` is less than or equal to the average value of `g ∘ f` over `t`. This is under the condition that both `f` and `g ∘ f` are integrable. In other words, the pair consisting of the average value of `f` and the average value of `g ∘ f` lies in the epigraph of `g` (the set of points `(x, y)` such that `y` is greater than or equal to `g(x)`) on the set `s`.
More concisely: If `g` is a convex, continuous function on a convex, closed set `s`, and `μ` is a finite, non-zero measure, then for any integrable functions `f : α → E` with `μ`-almost every image in `s`, we have `∫ g(f(x)) dμ ≤ ∫ f(x) dμ * g(∫ f(x) dμ)`.
|
Convex.set_average_mem
theorem Convex.set_average_mem :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E},
Convex ℝ s →
IsClosed s →
↑↑μ t ≠ 0 →
↑↑μ t ≠ ⊤ →
(∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s) → MeasureTheory.IntegrableOn f t μ → ⨍ (x : α) in t, f x ∂μ ∈ s
The theorem `Convex.set_average_mem` states that given a non-zero finite measure `μ` on a type `α`, a convex closed set `s` in a type `E`, and a function `f` that is integrable on a set `t` and maps almost every point (with respect to the measure `μ` restricted to `t`) to `s`, then the average value of `f` (that is, the integral of `f` with respect to `μ` over the set `t`) belongs to `s`. This theorem is a generalization to measurable spaces of the property that the center of mass of a finite set of points in a convex set is also in the convex set.
More concisely: Given a non-zero finite measure `μ`, a convex closed set `s` in a type `E`, and a integrable function `f` that maps almost every point in the `μ`-measure zero set `t` to `s`, the average value of `f` over `t` belongs to `s`.
|
ConvexOn.map_integral_le
theorem ConvexOn.map_integral_le :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ}
[inst_3 : MeasureTheory.IsProbabilityMeasure μ],
ConvexOn ℝ s g →
ContinuousOn g s →
IsClosed s →
(∀ᵐ (x : α) ∂μ, f x ∈ s) →
MeasureTheory.Integrable f μ →
MeasureTheory.Integrable (g ∘ f) μ → g (∫ (x : α), f x ∂μ) ≤ ∫ (x : α), g (f x) ∂μ
**Jensen's inequality**: Given a function `g : E → ℝ` that is both convex and continuous on a convex, closed set `s`, a probability measure `μ` on `α`, and a function `f : α → E` that sends almost every point (with respect to `μ`) to `s`, the inequality asserts that the value of `g` at the expected value of `f` is less than or equal to the expected value of `g ∘ f`. This statement assumes that both `f` and `g ∘ f` are integrable. This theorem also highlights the finite sum version of this lemma, `ConvexOn.map_centerMass_le`.
More concisely: For a convex and continuous function `g` on a convex, closed set `s`, and a probability measure `μ` on `α` with integrable functions `f : α → E` and `g ∘ f`, the expected value of `g ∘ f` is greater than or equal to the value of `g` at the expected value of `f` with respect to `μ`.
|
ConvexOn.map_set_average_le
theorem ConvexOn.map_set_average_le :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E} {g : E → ℝ},
ConvexOn ℝ s g →
ContinuousOn g s →
IsClosed s →
↑↑μ t ≠ 0 →
↑↑μ t ≠ ⊤ →
(∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s) →
MeasureTheory.IntegrableOn f t μ →
MeasureTheory.IntegrableOn (g ∘ f) t μ → g (⨍ (x : α) in t, f x ∂μ) ≤ ⨍ (x : α) in t, g (f x) ∂μ
**Jensen's inequality** states that if you have a convex function `g` mapping from `E` to real numbers which is also continuous on a convex closed set `s`, a finite non-zero measure `μ` on `α`, and another function `f` which maps almost every point of a set `t` to the set `s` with respect to the measure `μ`, then the value of function `g` at the average value of `f` over `t` is less than or equal to the average value of the function `g ∘ f` over `t`. This holds true provided that both `f` and `g ∘ f` are integrable.
In the context of this theorem, integrable refers to the property that the function is almost everywhere strongly measurable on a set, and the integral of its pointwise norm over the set is less than infinity. The measure `μ` is assumed to be neither zero nor infinite. The function `f` is such that for almost every point in `t`, it maps to `s`.
More concisely: For any convex, continuous function `g` on a convex, closed set `s`, and any integrable functions `f` and `g ∘ f` on a measure `μ` with finite, non-zero value, the average value of `g(∫(f dμ))` is less than or equal to `∫(g ∘ f dμ)` on the set where `f` maps to `s`.
|
ae_eq_const_or_exists_average_ne_compl
theorem ae_eq_const_or_exists_average_ne_compl :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {f : α → E} [inst_3 : MeasureTheory.IsFiniteMeasure μ],
MeasureTheory.Integrable f μ →
μ.ae.EventuallyEq f (Function.const α (⨍ (x : α), f x ∂μ)) ∨
∃ t, MeasurableSet t ∧ ↑↑μ t ≠ 0 ∧ ↑↑μ tᶜ ≠ 0 ∧ ⨍ (x : α) in t, f x ∂μ ≠ ⨍ (x : α) in tᶜ, f x ∂μ
The theorem states that for any integrable function `f` from type `α` to `E`, it is 'almost everywhere' equal to the constant function whose value is the integral over `α` of `f`, or there exists a measurable set `t` such that the measure of `t` is not zero, the measure of the complement of `t` is not zero, and the average values of `f` over `t` and over the complement of `t` are different. In other words, if an integrable function is not almost everywhere constant, then it distinguishes between at least two sets with non-zero measures.
More concisely: If an integrable function from type `α` to `E` is not almost everywhere constant, then there exist measurable sets `t` and `s` with non-zero measures such that the integrals of the function over `t` and `s` differ.
|
StrictConcaveOn.ae_eq_const_or_lt_map_average
theorem StrictConcaveOn.ae_eq_const_or_lt_map_average :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ}
[inst_3 : MeasureTheory.IsFiniteMeasure μ],
StrictConcaveOn ℝ s g →
ContinuousOn g s →
IsClosed s →
(∀ᵐ (x : α) ∂μ, f x ∈ s) →
MeasureTheory.Integrable f μ →
MeasureTheory.Integrable (g ∘ f) μ →
μ.ae.EventuallyEq f (Function.const α (⨍ (x : α), f x ∂μ)) ∨
⨍ (x : α), g (f x) ∂μ < g (⨍ (x : α), f x ∂μ)
This is a strict version of **Jensen's inequality**. It states that if there exists an integrable function `f : α → E` that takes values in a convex closed set `s`, and another function `g : E → ℝ` which is continuous and strictly concave on `s`, then the function `f` is almost everywhere equal to its average value, or the integral over `x` of `g(f(x))` with respect to the measure `μ` is less than `g` evaluated at the integral over `x` of `f(x)` with respect to the measure `μ`. This holds for all measurable spaces `α` with a finite measure, normed addend commutative groups `E` that also form a complete space under a normed space over real numbers.
The theorem states that for every element of the measure space almost everywhere, the value of function `f` lies in set `s`. The functions `f` and `g ∘ f` are both integrable with respect to the measure `μ`.
More concisely: If `f : α → E` is an integrable function with values in a convex closed set `s`, and `g : E → ℝ` is a continuous, strictly concave function on `s`, then the integral of `g(f(x))` is less than the integral of `f(x)` multiplied by `g`'s average value over `s` for almost all elements `x` in the measurable space `α` with finite measure.
|
ae_eq_const_or_norm_integral_lt_of_norm_le_const
theorem ae_eq_const_or_norm_integral_lt_of_norm_le_const :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {f : α → E} {C : ℝ} [inst_3 : StrictConvexSpace ℝ E]
[inst_4 : MeasureTheory.IsFiniteMeasure μ],
(∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C) →
μ.ae.EventuallyEq f (Function.const α (⨍ (x : α), f x ∂μ)) ∨ ‖∫ (x : α), f x ∂μ‖ < (↑↑μ Set.univ).toReal * C
This theorem states that for any normed additive commutative group `E` that is also a complete normed space over the real numbers (`ℝ`) and strictly convex, any measurable space `α`, any measure `μ` on `α` that is finite, and any function `f` from `α` to `E` with the norm of `f(x)` being less than or equal to a real number `C` almost everywhere with respect to `μ`, the function `f` is either almost everywhere equal to its average value or the norm of its integral is strictly less than the product of the measure of the universal set and `C`.
In other words, if we have a function `f` mapping from a measurable space to a strictly convex normed space such that the norm of the function's output is almost always less than or equal to a constant `C`, then the function is almost everywhere equal to its mean or the norm of the function's integral over the entire space is less than the total measure of the space multiplied by `C`.
More concisely: For any strictly convex, complete normed space `E` over `ℝ`, measurable space `α` with finite measure `μ`, and measurable function `f: α → E` such that $\int_\alpha ||f(x)|| d\mu < \mu(\alpha) \cdot C$, either $||f(x)|| = \frac{1}{\mu(\alpha)} \int_\alpha ||f(x)|| d\mu$ almost everywhere or $\int_\alpha ||f(x)|| d\mu < C\cdot\mu(\alpha)$.
|
ConcaveOn.le_map_set_average
theorem ConcaveOn.le_map_set_average :
∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E} {g : E → ℝ},
ConcaveOn ℝ s g →
ContinuousOn g s →
IsClosed s →
↑↑μ t ≠ 0 →
↑↑μ t ≠ ⊤ →
(∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s) →
MeasureTheory.IntegrableOn f t μ →
MeasureTheory.IntegrableOn (g ∘ f) t μ → ⨍ (x : α) in t, g (f x) ∂μ ≤ g (⨍ (x : α) in t, f x ∂μ)
**Jensen's Inequality**: Given a function `g : E → ℝ` that is concave and continuous on a convex closed set `s`, a finite non-zero measure `μ` on `α`, and a function `f : α → E` that sends almost every point of a set `t` under `μ` to `s`, if both `f` and `g ∘ f` are integrable, then the inequality `⨍ (x : α) in t, g (f x) ∂μ ≤ g (⨍ (x : α) in t, f x ∂μ)` holds. This states that the average value of `g ∘ f` over `t` is less than or equal to the value of `g` at the average value of `f` over `t`.
More concisely: If `g : E → ℝ` is a concave and continuous function on a convex closed set `s`, `μ` is a finite non-zero measure on `α`, `f : α → E` sends almost every point of `t` under `μ` to `s`, and both `f` and `g ∘ f` are integrable, then `∫(g ∘ f) dμ ≤ ∫(g �circ f) dμ`, where the integrals are taken over `t`.
|