WithLp.prod_lipschitzWith_equiv_aux
theorem WithLp.prod_lipschitzWith_equiv_aux :
∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
[inst_1 : PseudoEMetricSpace β], LipschitzWith 1 ⇑(WithLp.equiv p (α × β))
This theorem states that for any extended nonnegative real number `p`, any types `α` and `β`, given that `p` is greater than or equal to 1 and both `α` and `β` have a PseudoEMetricSpace instance, the function obtained by applying (or "lifting") the canonical equivalence between `WithLp p (α × β)` and `(α × β)` is Lipschitz continuous with a Lipschitz constant of `1`. In mathematical terms, for all `x, y` in `α × β`, the distance between the images of `x` and `y` under this function is less than or equal to the distance between `x` and `y` itself.
More concisely: For any extended nonnegative real number `p` greater than or equal to 1, the function lifting the canonical equivalence between `WithLp p (α × β)` and `(α × β)` is Lipschitz continuous with a Lipschitz constant of 1.
|
WithLp.prod_edist_eq_add
theorem WithLp.prod_edist_eq_add :
∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [inst : EDist α] [inst_1 : EDist β],
0 < p.toReal →
∀ (f g : WithLp p (α × β)),
edist f g = (edist f.1 g.1 ^ p.toReal + edist f.2 g.2 ^ p.toReal) ^ (1 / p.toReal)
This theorem, `WithLp.prod_edist_eq_add`, states that for any extended nonnegative real number `p` greater than 0, and for any types `α` and `β` equipped with an `edist` (extended distance) function, the extended distance between two `WithLp` elements `f` and `g` of the product type `(α × β)` is equal to the pth root of the sum of the `p` power of the extended distance between the first elements of `f` and `g` and the `p` power of the extended distance between the second elements of `f` and `g`. In mathematical terms, for `f = (f1, f2)` and `g = (g1, g2)`, the theorem proves that `edist f g = (edist f1 g1 ^ p.toReal + edist f2 g2 ^ p.toReal) ^ (1/p.toReal)`. This is analogous to the Minkowski inequality in Lp spaces for real numbers.
More concisely: For any extended real number `p > 0` and types `α` and `β` with an `edist` function, the extended distance between `WithLp` elements `(f1, f2)` and `(g1, g2)` of the product type `α × β` is equal to `(edist (f1, f2) (g1, g2) ^ p.toReal) ^ (1/p.toReal)`, where `edist (f1, f2) (g1, g2)` is the sum of `p`-th powers of the extended distances between their respective components.
|
WithLp.prod_edist_eq_sup
theorem WithLp.prod_edist_eq_sup :
∀ {α : Type u_2} {β : Type u_3} [inst : EDist α] [inst_1 : EDist β] (f g : WithLp ⊤ (α × β)),
edist f g = edist f.1 g.1 ⊔ edist f.2 g.2
The theorem `WithLp.prod_edist_eq_sup` states that for any two values `f` and `g` of type `WithLp ⊤ (α × β)`, where `α` and `β` are types equipped with an `edist` (extended distance) function, the extended distance between `f` and `g` is equal to the supremum of the extended distances between the first elements of `f` and `g` and the second elements of `f` and `g`. Essentially, this means that the distance between two pairs is the greatest distance between their corresponding elements.
More concisely: For any `WithLp` functions `f` and `g` of type `α × β`, the extended distance `∥f - g∥∞` is equal to the supremum of the extended distances `∥f.1 - g.1∥∞` and `∥f.2 - g.2∥∞`.
|
WithLp.prod_sup_edist_ne_top_aux
theorem WithLp.prod_sup_edist_ne_top_aux :
∀ {α : Type u_2} {β : Type u_3} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
(f g : WithLp ⊤ (α × β)), edist f.1 g.1 ⊔ edist f.2 g.2 ≠ ⊤
This theorem, `WithLp.prod_sup_edist_ne_top_aux`, is an auxiliary lemma used in the proof of another theorem `WithLp.prodPseudoMetricAux`. It asserts that for any types `α` and `β` that are pseudometric spaces, and for any two elements `f` and `g` of the type `WithLp ⊤ (α × β)`, the supremum (or least upper bound) of the extended distances between the first elements of `f` and `g` and between the second elements of `f` and `g` is not infinite. This theorem is not intended for use outside this particular context.
More concisely: For any pseudometric spaces `α` and `β`, the supremum of the extended distances between corresponding components of two elements in `WithLp ⊤ (α × β)` is not infinite.
|
WithLp.prod_edist_self
theorem WithLp.prod_edist_self :
∀ (p : ENNReal) {α : Type u_2} {β : Type u_3} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
(f : WithLp p (α × β)), edist f f = 0
The theorem `WithLp.prod_edist_self` asserts that the distance from a point to itself, within the context of the extended nonnegative real numbers associated with L`p` norm, is always zero. This holds regardless of the value of `p` and does not require the condition that `p` is greater than or equal to 1. This theorem retains its independence from `WithLp.instProdPseudoEMetricSpace` so it can be applied even when `p` is less than 1. The theorem is applicable to any two types `α` and `β` both with a `PseudoEMetricSpace` instance and any function `f` of a type that is associated with the L`p` norm of `p` and the Cartesian product of the types `α` and `β`.
More concisely: The theorem `WithLp.prod_edist_self` asserts that the Lp distance of a point to itself in the Cartesian product of two pseudo-metric spaces is zero, for any value of p.
|
WithLp.prod_edist_comm
theorem WithLp.prod_edist_comm :
∀ (p : ENNReal) {α : Type u_2} {β : Type u_3} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
(f g : WithLp p (α × β)), edist f g = edist g f
This theorem states that the distance in the L`p` space is symmetric, meaning that the distance between two points `f` and `g` is the same regardless of the order in which they are considered. This property is valid for any `p` value within the extended nonnegative real numbers and does not require `p` to be greater than or equal to 1. The symmetry property is applicable even to spaces where `p < 1`. The theorem holds for any types `α` and `β` that have a `PseudoEMetricSpace` structure, where `WithLp p (α × β)` is a type synonym for the given `α` and `β`, associated with the L`p` norm.
More concisely: The L`p` distance between two points in a `PseudoEMetricSpace` is commutative, i.e., `d(f, g) = d(g, f)` for any `p`-norm.
|
WithLp.prod_antilipschitzWith_equiv_aux
theorem WithLp.prod_antilipschitzWith_equiv_aux :
∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
[inst_1 : PseudoEMetricSpace β], AntilipschitzWith (2 ^ (1 / p).toReal) ⇑(WithLp.equiv p (α × β))
The theorem `WithLp.prod_antilipschitzWith_equiv_aux` states that for every extended nonnegative real number `p` such that `1 ≤ p`, and for every pair of types `α` and `β` that have pseudometric space structures, the canonical equivalence function between `WithLp p (α × β)` and `α × β` (which is given by `WithLp.equiv p (α × β)`) is Antilipschitz with constant `2^(1/p)`.
In more mathematical terms, an Antilipschitz condition ensures that the distances between points in the original space and their images under a map do not shrink too much. In this context, for any two points `x` and `y` in the space `WithLp p (α × β)`, the edistance between `x` and `y` is less than or equal to `2^(1/p)` times the edistance between their images under the equivalence function.
More concisely: For every extended nonnegative real number `p` with `1 ≤ p`, the canonical equivalence function between `WithLp p (α × β)` and `α × β` is an Antilipschitz function with constant `2^(1/p)`.
|
WithLp.prod_norm_eq_add
theorem WithLp.prod_norm_eq_add :
∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [inst : Norm α] [inst_1 : Norm β],
0 < p.toReal → ∀ (f : WithLp p (α × β)), ‖f‖ = (‖f.1‖ ^ p.toReal + ‖f.2‖ ^ p.toReal) ^ (1 / p.toReal)
The theorem `WithLp.prod_norm_eq_add` states that for all extended nonnegative real numbers `p` greater than zero and for any function `f` with L^p norm in the product space of two types `α` and `β` (which have a norm structure), the norm of `f` is equal to the p-th root of the sum of the p-th powers of the norms of the first and second components of `f`. This is a statement about the calculation of L^p norms in product spaces.
More concisely: For any function `f` in the product space of types `α` and `β` with L^p norm, where `p > 0`, the L^p norm of `f` equals the p-th root of the sum of the p-th powers of the L^p norms of its first and second components.
|
WithLp.prod_nnnorm_eq_sup
theorem WithLp.prod_nnnorm_eq_sup :
∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β]
(f : WithLp ⊤ (α × β)), ‖f‖₊ = ‖f.1‖₊ ⊔ ‖f.2‖₊
This theorem states that for any types `α` and `β` that are both semi-normed additive commutative groups, and for any function `f` of type `WithLp ⊤ (α × β)`, the semi-norm of `f` (denoted as `‖f‖₊`) is equal to the supremum (`⊔`, the least upper bound) of the semi-norms of the first (`f.1`) and second (`f.2`) components of `f`. In simpler words, the semi-norm of a function on a product of two semi-normed additive groups is the maximum of the semi-norms of its components.
More concisely: For any function `f` of type `WithLp ⊤ (α × β)`, where `α` and `β` are semi-normed additive commutative groups, the semi-norm `‖f‖₊` is equal to the supremum of the semi-norms of `f.1` and `f.2`.
|