PiLp.iSup_edist_ne_top_aux
theorem PiLp.iSup_edist_ne_top_aux :
∀ {ι : Type u_5} [inst : Finite ι] {α : ι → Type u_6} [inst : (i : ι) → PseudoMetricSpace (α i)] (f g : PiLp ⊤ α),
⨆ i, edist (f i) (g i) ≠ ⊤
This theorem is an auxiliary lemma which is used in the proof of another, and is not intended for use outside of this file. It states that for any finite type `ι`, and any function `α : ι → Type u_6` that associates each element of `ι` with a pseudometric space, if `f` and `g` are two elements of the `PiLp ⊤ α` type (which represents sequences of functions from `ι` to `α` endowed with the `L^∞` distance), then the supremum of the extended distances (edist) between corresponding elements of `f` and `g` over all `i` in `ι` is not infinite.
More concisely: For any finite type `ι` and function `α : ι → Type u_6` that assigns each `ι` element a pseudometric space, the supremum of the extended distances between corresponding elements of any two sequences `f` and `g` in `PiLp ⊤ α` is finite.
|
PiLp.norm_equiv_symm_const'
theorem PiLp.norm_equiv_symm_const' :
∀ {p : ENNReal} {ι : Type u_2} [inst : Fact (1 ≤ p)] [inst : Fintype ι] {β : Type u_5}
[inst_1 : SeminormedAddCommGroup β] [inst_2 : Nonempty ι] (b : β),
‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖ = ↑↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖
This theorem states that for any extended non-negative real number `p` (greater or equal to 1), any type `ι` which is a `Fintype` (has finitely many elements) and non-empty, and any type `β` which is a seminormed add commutative group, the norm of the inverse of the canonical equivalence (from `WithLp p (ι → β)` to `(ι → β)`) applied to a constant function with value `b` from `ι` to `β` is equal to the cardinality of `ι` raised to the power of `1/p` times the norm of `b`. This equivalence relates the "Lp" space of functions and the original space of function values. The theorem does not hold when `p` equals infinity and when `ι` is empty, as the left-hand side would simplify to zero, while the right-hand side would simplify to the norm of `b`.
More concisely: For any `Fintype ι` with at least one element, `p >= 1` real number, and seminormed add commutative group `β`, the norm of the inverse of the canonical equivalence from `WithLp p (ι → β)` to `(ι → β)` of a constant function with value `b` equals `|ι|^{1/p} * ||b||_β`, where `|ι|` denotes the cardinality of `ι`.
|
PiLp.antilipschitzWith_equiv_aux
theorem PiLp.antilipschitzWith_equiv_aux :
∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [inst : Fact (1 ≤ p)]
[inst_1 : (i : ι) → PseudoEMetricSpace (β i)] [inst_2 : Fintype ι],
AntilipschitzWith (↑(Fintype.card ι) ^ (1 / p).toReal) ⇑(WithLp.equiv p ((i : ι) → β i))
This theorem states that for any extended nonnegative real number `p`, index type `ι`, and a function `β` mapping each `ι` to a type that has the structure of a pseudo-emetric space, given that the fact `1 ≤ p` holds and `ι` is finite, the function `WithLp.equiv p ((i : ι) → β i)` is `AntilipschitzWith` the nonnegative real number `(Fintype.card ι) ^ (1 / p).toReal`.
In other words, for any two points `x` and `y` in the domain of `WithLp.equiv p ((i : ι) → β i)`, the extended metric distance between `x` and `y` is less than or equal to `(Fintype.card ι) ^ (1 / p).toReal` times the extended metric distance between `WithLp.equiv p ((i : ι) → β i) x` and `WithLp.equiv p ((i : ι) → β i) y`. Here, `Fintype.card ι` denotes the number of elements in the type `ι`.
More concisely: For any finite index type `ι` and function `β:` `ι` → MetricSpace `A` with `p` being a positive real number, `WithLp.equiv p (β)` is an Antilipschitz function with constant `(Fintype.card ι) ^ (1/p)`.
|
PiLp.nndist_equiv_symm_single_same
theorem PiLp.nndist_equiv_symm_single_same :
∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [inst : Fact (1 ≤ p)] [inst_1 : Fintype ι]
[inst_2 : (i : ι) → SeminormedAddCommGroup (β i)] [inst_3 : DecidableEq ι] (i : ι) (b₁ b₂ : β i),
nndist ((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₁))
((WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b₂)) =
nndist b₁ b₂
This theorem asserts that for every extended nonnegative real number `p` such that `1 ≤ p`, every finite type `ι`, and every function `β : ι → Type u_4` where each `β i` is a seminormed additive commutative group with decidable equality, if we have elements `b₁` and `b₂` of some `β i`, then the nonnegative distance (or `nndist`) between the values of the function obtained by applying the canonical equivalence from `WithLp p ((i : ι) → β i)` to `Pi.single i b₁` and `Pi.single i b₂` (after taking the inverse of the equivalence), is the same as the nonnegative distance between `b₁` and `b₂` themselves. In other words, this equivalence preserves the nonnegative distance between the singleton functions at a given index `i`.
More concisely: For every extended nonnegative real number `p` with `1 ≤ p`, every finite type `ι`, and every function `β : ι → SeminormedAddCommGroup` such that each `β i` has decidable equality, the nonnegative distance between the elements `b₁` and `b₂` in `β i` is equal to the nonnegative distance between the functions `Pi.single i b₁` and `Pi.single i b₂` in the Lp space `WithLp p ((i : ι) → β i)`.
|
PiLp.nnnorm_eq_sum
theorem PiLp.nnnorm_eq_sum :
∀ {ι : Type u_2} [inst : Fintype ι] {p : ENNReal} [inst_1 : Fact (1 ≤ p)] {β : ι → Type u_5},
p ≠ ⊤ →
∀ [inst_2 : (i : ι) → SeminormedAddCommGroup (β i)] (f : PiLp p β),
‖f‖₊ = (Finset.univ.sum fun i => ‖f i‖₊ ^ p.toReal) ^ (1 / p.toReal)
The theorem `PiLp.nnnorm_eq_sum` states that for any given indexed type `ι` that is finite, a nonnegative real number `p` (extended by adding infinity) that is greater than or equal to 1, and any type `β` that is a function of the index `ι`, whenever `p` is not infinity, for a function `f` of type `PiLp p β` (a copy of a Pi type), the nonnegative norm of `f` is equal to the p-th root of the sum, across all indices in the universal finite set of `ι`, of the p-th power of the nonnegative norm of `f` evaluated at the index. The sum operation here is defined in the context of an additive commutative monoid.
In other words, this theorem characterizes the `L^p` norm of a function in terms of the `p`-norms of its components.
More concisely: For any finite indexed type `ι`, nonnegative real number `p ≥ 1` (extending it with infinity), and a function `f` of type `PiLp p β`, the `L^p` norm of `f` equals the `p`-th root of the sum, across all indices in `ι`, of the `p`-th power of the nonnegative norm of `f` evaluated at each index.
|
PiLp.lipschitzWith_equiv_aux
theorem PiLp.lipschitzWith_equiv_aux :
∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [inst : Fact (1 ≤ p)]
[inst_1 : (i : ι) → PseudoEMetricSpace (β i)] [inst_2 : Fintype ι],
LipschitzWith 1 ⇑(WithLp.equiv p ((i : ι) → β i))
The theorem `PiLp.lipschitzWith_equiv_aux` states that for every extended nonnegative real number `p`, every indexed type `ι`, and for each index `i` of type `ι`, a pseudo-emetric space `β i` (where the `β` is a function from the index set `ι` to some type `u_4`), assuming that `p` is at least 1 and the index set `ι` is a finite set (Fintype), the function `WithLp.equiv p ((i : ι) → β i))` is Lipschitz continuous with constant 1. In other words, the distance between the images of any two points under this function is at most the distance between the points themselves in their original pseudo-emetric space.
More concisely: For every finite indexed set `ι` and real number `p ≥ 1`, the function `WithLp.equiv p (β : ∀ i : ι, β i)` from the pseudo-metric space `(ι, d)` to the product pseudo-metric space `(Π i : ι, β i)` is Lipschitz continuous with constant 1.
|
PiLp.nnnorm_equiv_symm_single
theorem PiLp.nnnorm_equiv_symm_single :
∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [inst : Fintype ι]
[inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] [inst_2 : DecidableEq ι] [hp : Fact (1 ≤ p)] (i : ι) (b : β i),
‖(WithLp.equiv p ((i : ι) → β i)).symm (Pi.single i b)‖₊ = ‖b‖₊
This theorem states that for any extended nonnegative real number `p`, given a type `ι`, a function `β` mapping elements of `ι` to some other type, and assuming that `ι` has finite number of elements, elements of `β i` form a seminormed additively commutative group, there exists a decidable equality on `ι`, and `p` is greater than or equal to 1. For any element `i` of type `ι` and any element `b` of type `β i`, the nonnegative norm of the inverse of the canonical equivalence between the space of functions `WithLp p ((i : ι) → β i)` and `((i : ι) → β i)`, applied to the function supported at `i`, with value `b` there, and `0` elsewhere, is equal to the nonnegative norm of `b`. Essentially, the norm of a function that is non-zero at a single point `i` and zero elsewhere, under this equivalence, is just the norm of the value at `i`.
More concisely: For any finite type `ι`, function `β : ι →* X`, and extended nonnegative real number `p ≥ 1`, the inverse of the canonical equivalence between the `Lp[0]` space of functions `ι → β` and `β` under pointwise operations preserves the `Lp[0]` norm, i.e., for all `i ∈ ι` and `b ∈ β i`, the `Lp[0]` norm of the function supported at `i` with value `b` and zero elsewhere equals the `Lp[0]` norm of `b`.
|
PiLp.edist_self
theorem PiLp.edist_self :
∀ (p : ENNReal) {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → PseudoEMetricSpace (β i)]
(f : PiLp p β), edist f f = 0
This theorem states that for any positive extended nonnegative real number `p`, any finite index type `ι`, and any function `β` mapping from `ι` to a set of pseudo metric spaces, the distance from any function `f` of type `PiLp p β` to itself is always zero, irrespective of the value of `p`. This result holds true even when `p` is less than 1. The purpose of this theorem is to establish the zero-self-distance property, which is a fundamental property of metric spaces, for the `PiLp p β` space under the `edist` (extended distance) function.
More concisely: For any positive extended real number `p` and finite index type `ι`, the self-distance of any function `f` in `PiLp p β` under the extended distance `edist` is zero.
|
PiLp.nnnorm_eq_ciSup
theorem PiLp.nnnorm_eq_ciSup :
∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)]
(f : PiLp ⊤ β), ‖f‖₊ = ⨆ i, ‖f i‖₊
The theorem `PiLp.nnnorm_eq_ciSup` states that for any type `ι`, any function `β : ι → Type`, given that `ι` is a finite type and that for each `i : ι`, `β i` forms a seminormed additive commutative group, then for any function `f` from the Pi type with the `L^∞` distance (`PiLp ⊤ β`), the non-negative norm of `f` (`‖f‖₊`) is equal to the supremum (the least upper bound) over all `i`, of the non-negative norm of `f i` (`‖f i‖₊`).
More concisely: For any finite type `ι` and a function `β : ι → Type` such that each `β i` forms a seminormed additive commutative group, the `L^∞` norm of a function `f` from the Pi type `PiLp ⊤ β` equals the supremum of the `L^∞` norms of `f i` over all `i` in `ι`.
|
PiLp.edist_eq_sum
theorem PiLp.edist_eq_sum :
∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → EDist (β i)] {p : ENNReal},
0 < p.toReal →
∀ (f g : PiLp p β), edist f g = (Finset.univ.sum fun i => edist (f i) (g i) ^ p.toReal) ^ (1 / p.toReal)
The theorem `PiLp.edist_eq_sum` states that for any type `ι`, any function `β` from `ι` to some other type, given we have a finite number of `ι` and each `ι` has a defined 'extended' distance (`EDist`), and a nonnegative real number `p` that is greater than 0. Then for any two functions `f` and `g` of type `PiLp p β` (a type synonym defined to hold the `L^p` distance on a Pi type), the 'extended' distance between `f` and `g` is equal to the p-th root of the sum over all elements in the universal set (`Finset.univ`) of the p-th power of the 'extended' distance between `f i` and `g i`. In mathematical terms, given `0 < p`, we have `edist(f, g) = \left(\sum_{i \in \text{univ}} (edist(f(i), g(i)))^p\right)^{1/p}`.
More concisely: For any type `ι`, function `β`, finite `ι`, nonnegative real `p > 0`, and functions `f` and `g` of type `PiLp p β`, the extended distance `edist(f, g)` is equal to the `p`-th root of the sum over all `i ∈ Finset.univ` of the `p`-th power of the extended distance between `f i` and `g i`.
|
PiLp.norm_eq_of_L2
theorem PiLp.norm_eq_of_L2 :
∀ {ι : Type u_2} [inst : Fintype ι] {β : ι → Type u_5} [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)]
(x : PiLp 2 β), ‖x‖ = (Finset.univ.sum fun i => ‖x i‖ ^ 2).sqrt
This theorem states that for any finite type `ι`, any type `β` that is a function from `ι` to a seminormed commutative additive group, and any `x` which is a function from `ι` to `β` (i.e., `x` is a vector in `PiLp 2 β`), the norm of `x` is equal to the square root of the sum of the squares of the norms of the elements of `x`. This is essentially a generalization of the Pythagorean theorem: the norm of `x` is calculated in the same way as the Euclidean distance in `R^n`.
More concisely: For any finite type `ι`, given a function `β` from `ι` to a seminormed commutative additive group, and a function `x : ι → β`, the norm of `x` equals the square root of the sum of the squares of the element-wise norms of `x`.
|
PiLp.nnnorm_equiv_symm_const'
theorem PiLp.nnnorm_equiv_symm_const' :
∀ {p : ENNReal} {ι : Type u_2} [inst : Fact (1 ≤ p)] [inst_1 : Fintype ι] {β : Type u_5}
[inst_2 : SeminormedAddCommGroup β] [inst_3 : Nonempty ι] (b : β),
‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊
The theorem `PiLp.nnnorm_equiv_symm_const'` states that for any extended nonnegative real number `p` that is greater or equal to 1, any type `ι` with a `Fintype` instance, any `SeminormedAddCommGroup` `β`, and any non-empty `ι`, the nonnegative norm of the inverse function of the equivalence between `WithLp p (ι → β)` and `ι → β` applied to the constant function on `ι` with value `b`, equals the cardinality of `ι` raised to the power of the reciprocal of `p`, all multiplied by the nonnegative norm of `b`.
In mathematical terms, if you take a constant function on a finite type with some value, transform it using the inverse of the canonical equivalence between the space of functions `WithLp p (ι → β)` and `ι → β`, and then compute its nonnegative norm, you will get the nonnegative norm of the original value times the cardinality of the finite set raised to the power of the reciprocal of `p`. The theorem, however, requires the assumption that `ι` is nonempty and `p` is not infinity, as without these conditions, the theorem does not hold.
More concisely: For any finite type `ι` with a `Fintype` instance, `SeminormedAddCommGroup` `β`, nonempty `ι`, and `p >= 1` extended nonnegative real number, the nonnegative norm of the constant function's inverse under the `WithLp p (ι → β)` equivalence is the cardinality of `ι` raised to the power of `1/p` times the nonnegative norm of the constant value.
|
PiLp.nnnorm_equiv_symm_const
theorem PiLp.nnnorm_equiv_symm_const :
∀ {p : ENNReal} {ι : Type u_2} [inst : Fact (1 ≤ p)] [inst_1 : Fintype ι] {β : Type u_5}
[inst_2 : SeminormedAddCommGroup β],
p ≠ ⊤ →
∀ (b : β), ‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊
This theorem states that for any extended nonnegative real number `p` that is not infinity, any type `ι` that is a finite type, and any type `β` that forms a seminormalized additive commutative group, the nonnegative norm of the inverse function under the canonical equivalence between `WithLp p (ι → β)` and `ι → β` applied to the constant function with value `b`, is equal to the cardinality of `ι` raised to the power of the reciprocal of `p` times the nonnegative norm of `b`. This holds when `p` is greater than or equal to 1. However, when `p` is infinity, this theorem does not hold without the additional assumption that `ι` is nonempty because the left-hand side simplifies to `0`, while the right-hand side simplifies to the nonnegative norm of `b`.
More concisely: For finite types `ι`, nonnegative real number `p ≥ 1`, and additive commutative semigroup `β`, the nonnegative `Lp` norm of the constant function's inverse under the canonical equivalence between `WithLp p (ι → β)` and `ι → β` equals `|ι|^{1/p} * ∥b∥_β`, where `|ι|` is the cardinality of `ι` and `∥b∥_β` is the nonnegative norm of `b` in `β`.
|
PiLp.nnnorm_eq_of_L2
theorem PiLp.nnnorm_eq_of_L2 :
∀ {ι : Type u_2} [inst : Fintype ι] {β : ι → Type u_5} [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)]
(x : PiLp 2 β), ‖x‖₊ = NNReal.sqrt (Finset.univ.sum fun i => ‖x i‖₊ ^ 2)
This theorem states that for any type `ι` which is a finite type, and any function `β : ι → Type` such that for each `i : ι` the type `β i` forms a seminormed additively commutative group, the non-negative norm of a function `x` of type `PiLp 2 β` (which is a family of types equipped with a pseudo-metric space structure, where each type is a copy of a certain Pi type endowed with an `L^2` distance) is equal to the square root of the sum over all elements in `ι` of the square of the non-negative norm of `x i`. In mathematical notation, this would be represented as ‖x‖₊ = √(∑_{i ∈ ι} ‖x i‖₊²).
More concisely: For any finite type `ι` and function `β : ι → Type` where each `β i` forms a seminormed additively commutative group, the `L^2` norm of a function `x : PiLp 2 β` equals the square root of the sum of the squares of the non-negative norms of `x i` over all `i ∈ ι`.
|
PiLp.norm_equiv_symm_const
theorem PiLp.norm_equiv_symm_const :
∀ {p : ENNReal} {ι : Type u_2} [inst : Fact (1 ≤ p)] [inst : Fintype ι] {β : Type u_5}
[inst_1 : SeminormedAddCommGroup β],
p ≠ ⊤ →
∀ (b : β), ‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖ = ↑↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖
This theorem, `PiLp.norm_equiv_symm_const`, states that for any extended non-negative real number `p` that is not infinity, any type `ι` that is finite, and any `b` of type `β` where `β` is a semi-normed add commutative group, the norm of the reverse equivalence of `WithLp.equiv p (ι → β)` applied to the constant function with value `b` is equal to the cardinality of `ι` to the power of the reciprocal of `p` multiplied by the norm of `b`. However, when `p` equals infinity, this theorem does not hold without the additional assumption that `ι` is nonempty because the left-hand side simplifies to `0`, while the right-hand side simplifies to the norm of `b`. This is addressed in another theorem, `PiLp.norm_equiv_symm_const'`.
More concisely: For finite type `ι` and semi-normed add commutative group `β`, the norm of the reverse equivalence of `WithLp.equiv` applied to the constant function with value `b` equals the cardinality of `ι` raised to the power of `1/p` multiplied by the norm of `b`, except when `p` is infinity, in which case an additional nonempty assumption on `ι` is required.
|
PiLp.edist_comm
theorem PiLp.edist_comm :
∀ (p : ENNReal) {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → PseudoEMetricSpace (β i)]
(f g : PiLp p β), edist f g = edist g f
The theorem `PiLp.edist_comm` states that for any extended nonnegative real number `p`, any finite type `ι`, any type-valued function `β` over `ι` where each `β i` forms a pseudo-emetric space, and any two members `f` and `g` of the L^p space `PiLp p β`, the extended metric distance from `f` to `g` is equal to the extended metric distance from `g` to `f`. This symmetry property of the distance holds irrespective of the value of `p` and doesn't require `p` to be greater than or equal to one. This theorem is kept separate from `pi_Lp.pseudo_emetric_space` as it is applicable also when `p` is less than one.
More concisely: For any extended nonnegative real number `p`, any finite type `ι`, and any type-valued function `β` over `ι` turning each `β i` into a pseudo-metric space, the extended metric distances between any two members of the L^p space `PiLp p β` are commutative.
|