|
| 1 | +/- |
| 2 | +Copyright (c) 2020 Sébastien Gouëzel. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Sébastien Gouëzel |
| 5 | +-/ |
| 6 | +import analysis.mean_inequalities |
| 7 | + |
| 8 | +/-! |
| 9 | +# `L^p` distance on finite products of metric spaces |
| 10 | +Given finitely many metric spaces, one can put the max distance on their product, but there is also |
| 11 | +a whole family of natural distances, indexed by a real parameter `p ∈ [1, ∞)`, that also induce |
| 12 | +the product topology. We define them in this file. The distance on `Π i, α i` is given by |
| 13 | +$$ |
| 14 | +d(x, y) = \left(\sum d(x_i, y_i)^p\right)^{1/p}. |
| 15 | +$$ |
| 16 | +
|
| 17 | +We give instances of this construction for emetric spaces, metric spaces, normed groups and normed |
| 18 | +spaces. |
| 19 | +
|
| 20 | +To avoid conflicting instances, all these are defined on a copy of the original Pi type, named |
| 21 | +`pi_Lp p hp α`, where `hp : 1 ≤ p`. This assumption is included in the definition of the type |
| 22 | +to make sure that it is always available to typeclass inference to construct the instances. |
| 23 | +
|
| 24 | +We ensure that the topology and uniform structure on `pi_Lp p hp α` are (defeq to) the product |
| 25 | +topology and product uniformity, to be able to use freely continuity statements for the coordinate |
| 26 | +functions, for instance. |
| 27 | +
|
| 28 | +## Implementation notes |
| 29 | +
|
| 30 | +We only deal with the `L^p` distance on a product of finitely many metric spaces, which may be |
| 31 | +distinct. A closely related construction is the `L^p` norm on the space of |
| 32 | +functions from a measure space to a normed space, where the norm is |
| 33 | +$$ |
| 34 | +\left(\int ∥f (x)∥^p dμ\right)^{1/p}. |
| 35 | +$$ |
| 36 | +However, the topology induced by this construction is not the product topology, this only |
| 37 | +defines a seminorm (as almost everywhere zero functions have zero `L^p` norm), and some functions |
| 38 | +have infinite `L^p` norm. All these subtleties are not present in the case of finitely many |
| 39 | +metric spaces (which corresponds to the basis which is a finite space with the counting measure), |
| 40 | +hence it is worth devoting a file to this specific case which is particularly well behaved. |
| 41 | +The general case is not yet formalized in mathlib. |
| 42 | +
|
| 43 | +To prove that the topology (and the uniform structure) on a finite product with the `L^p` distance |
| 44 | +are the same as those coming from the `L^∞` distance, we could argue that the `L^p` and `L^∞` norms |
| 45 | +are equivalent on `ℝ^n` for abstract (norm equivalence) reasons. Instead, we give a more explicit |
| 46 | +(easy) proof which provides a comparison between these two norms with explicit constants. |
| 47 | +-/ |
| 48 | + |
| 49 | +open real set filter |
| 50 | +open_locale big_operators uniformity topological_space |
| 51 | + |
| 52 | +noncomputable theory |
| 53 | + |
| 54 | +variables {ι : Type*} |
| 55 | + |
| 56 | +/-- A copy of a Pi type, on which we will put the `L^p` distance. Since the Pi type itself is |
| 57 | +already endowed with the `L^∞` distance, we need the type synonym to avoid confusing typeclass |
| 58 | +resolution. Also, we let it depend on `p`, to get a whole family of type on which we can put |
| 59 | +different distances, and we provide the assumption `hp` in the definition, to make it available |
| 60 | +to typeclass resolution when it looks for a distance on `pi_Lp p hp α`. -/ |
| 61 | +@[nolint unused_arguments] |
| 62 | +def pi_Lp {ι : Type*} (p : ℝ) (hp : 1 ≤ p) (α : ι → Type*) : Type* := Π (i : ι), α i |
| 63 | + |
| 64 | +instance {ι : Type*} (p : ℝ) (hp : 1 ≤ p) (α : ι → Type*) [∀ i, inhabited (α i)] : |
| 65 | + inhabited (pi_Lp p hp α) := |
| 66 | +⟨λ i, default (α i)⟩ |
| 67 | + |
| 68 | +namespace pi_Lp |
| 69 | + |
| 70 | +variables (p : ℝ) (hp : 1 ≤ p) (α : ι → Type*) |
| 71 | + |
| 72 | +/-- Canonical bijection between `pi_Lp p hp α` and the original Pi type. We introduce it to be able |
| 73 | +to compare the `L^p` and `L^∞` distances through it. -/ |
| 74 | +protected def equiv : pi_Lp p hp α ≃ Π (i : ι), α i := |
| 75 | +equiv.refl _ |
| 76 | + |
| 77 | +section |
| 78 | +/-! |
| 79 | +### The uniformity on finite `L^p` products is the product uniformity |
| 80 | +
|
| 81 | +In this section, we put the `L^p` edistance on `pi_Lp p hp α`, and we check that the uniformity |
| 82 | +coming from this edistance coincides with the product uniformity, by showing that the canonical |
| 83 | +map to the Pi type (with the `L^∞` distance) is a uniform embedding, as it is both Lipschitz and |
| 84 | +antiLipschitz. |
| 85 | +
|
| 86 | +We only register this emetric space structure as a temporary instance, as the true instance (to be |
| 87 | +registered later) will have as uniformity exactly the product uniformity, instead of the one coming |
| 88 | +from the edistance (which is equal to it, but not defeq). |
| 89 | +-/ |
| 90 | + |
| 91 | +variables [∀ i, emetric_space (α i)] [fintype ι] |
| 92 | + |
| 93 | +/-- Endowing the space `pi_Lp p hp α` with the `L^p` edistance. This definition is not satisfactory, |
| 94 | +as it does not register the fact that the topology and the uniform structure coincide with the |
| 95 | +product one. Therefore, we do not register it as an instance. Using this as a temporary emetric |
| 96 | +space instance, we will show that the uniform structure is equal (but not defeq) to the product one, |
| 97 | +and then register an instance in which we replace the uniform structure by the product one using |
| 98 | +this emetric space and `emetric_space.replace_uniformity`. -/ |
| 99 | +def emetric_aux : emetric_space (pi_Lp p hp α) := |
| 100 | +have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp, |
| 101 | +{ edist := λ f g, (∑ (i : ι), (edist (f i) (g i)) ^ p) ^ (1/p), |
| 102 | + edist_self := λ f, by simp [edist, ennreal.zero_rpow_of_pos pos, |
| 103 | + ennreal.zero_rpow_of_pos (inv_pos.2 pos)], |
| 104 | + edist_comm := λ f g, by simp [edist, edist_comm], |
| 105 | + edist_triangle := λ f g h, calc |
| 106 | + (∑ (i : ι), edist (f i) (h i) ^ p) ^ (1 / p) ≤ |
| 107 | + (∑ (i : ι), (edist (f i) (g i) + edist (g i) (h i)) ^ p) ^ (1 / p) : |
| 108 | + begin |
| 109 | + apply ennreal.rpow_le_rpow _ (div_nonneg zero_le_one pos), |
| 110 | + refine finset.sum_le_sum (λ i hi, _), |
| 111 | + exact ennreal.rpow_le_rpow (edist_triangle _ _ _) (le_trans zero_le_one hp) |
| 112 | + end |
| 113 | + ... ≤ |
| 114 | + (∑ (i : ι), edist (f i) (g i) ^ p) ^ (1 / p) + (∑ (i : ι), edist (g i) (h i) ^ p) ^ (1 / p) : |
| 115 | + ennreal.Lp_add_le _ _ _ hp, |
| 116 | + eq_of_edist_eq_zero := λ f g hfg, |
| 117 | + begin |
| 118 | + simp [edist, ennreal.rpow_eq_zero_iff, pos, asymm pos, finset.sum_eq_zero_iff_of_nonneg] at hfg, |
| 119 | + exact funext hfg |
| 120 | + end } |
| 121 | + |
| 122 | +local attribute [instance] pi_Lp.emetric_aux |
| 123 | + |
| 124 | +lemma lipschitz_with_equiv : lipschitz_with 1 (pi_Lp.equiv p hp α) := |
| 125 | +begin |
| 126 | + have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp, |
| 127 | + have cancel : p * (1/p) = 1 := mul_div_cancel' 1 (ne_of_gt pos), |
| 128 | + assume x y, |
| 129 | + simp only [edist, forall_prop_of_true, one_mul, finset.mem_univ, finset.sup_le_iff, |
| 130 | + ennreal.coe_one], |
| 131 | + assume i, |
| 132 | + calc |
| 133 | + edist (x i) (y i) = (edist (x i) (y i) ^ p) ^ (1/p) : |
| 134 | + by simp [← ennreal.rpow_mul, cancel, -one_div_eq_inv] |
| 135 | + ... ≤ (∑ (i : ι), edist (x i) (y i) ^ p) ^ (1 / p) : |
| 136 | + begin |
| 137 | + apply ennreal.rpow_le_rpow _ (div_nonneg zero_le_one pos), |
| 138 | + exact finset.single_le_sum (λ i hi, (bot_le : (0 : ennreal) ≤ _)) (finset.mem_univ i) |
| 139 | + end |
| 140 | +end |
| 141 | + |
| 142 | +lemma antilipschitz_with_equiv : |
| 143 | + antilipschitz_with ((fintype.card ι : nnreal) ^ (1/p)) (pi_Lp.equiv p hp α) := |
| 144 | +begin |
| 145 | + have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp, |
| 146 | + have cancel : p * (1/p) = 1 := mul_div_cancel' 1 (ne_of_gt pos), |
| 147 | + assume x y, |
| 148 | + simp [edist, -one_div_eq_inv], |
| 149 | + calc (∑ (i : ι), edist (x i) (y i) ^ p) ^ (1 / p) ≤ |
| 150 | + (∑ (i : ι), edist (pi_Lp.equiv p hp α x) (pi_Lp.equiv p hp α y) ^ p) ^ (1 / p) : |
| 151 | + begin |
| 152 | + apply ennreal.rpow_le_rpow _ (div_nonneg zero_le_one pos), |
| 153 | + apply finset.sum_le_sum (λ i hi, _), |
| 154 | + apply ennreal.rpow_le_rpow _ (le_of_lt pos), |
| 155 | + exact finset.le_sup (finset.mem_univ i) |
| 156 | + end |
| 157 | + ... = (((fintype.card ι : nnreal)) ^ (1/p) : nnreal) * |
| 158 | + edist (pi_Lp.equiv p hp α x) (pi_Lp.equiv p hp α y) : |
| 159 | + begin |
| 160 | + simp only [nsmul_eq_mul, finset.card_univ, ennreal.rpow_one, finset.sum_const, |
| 161 | + ennreal.mul_rpow_of_nonneg _ _ (div_nonneg zero_le_one pos), ←ennreal.rpow_mul, cancel], |
| 162 | + have : (fintype.card ι : ennreal) = (fintype.card ι : nnreal) := |
| 163 | + (ennreal.coe_nat (fintype.card ι)).symm, |
| 164 | + rw [this, ennreal.coe_rpow_of_nonneg _ (div_nonneg zero_le_one pos)] |
| 165 | + end |
| 166 | +end |
| 167 | + |
| 168 | +lemma aux_uniformity_eq : |
| 169 | + 𝓤 (pi_Lp p hp α) = @uniformity _ (Pi.uniform_space _) := |
| 170 | +begin |
| 171 | + have A : uniform_embedding (pi_Lp.equiv p hp α) := |
| 172 | + (antilipschitz_with_equiv p hp α).uniform_embedding |
| 173 | + (lipschitz_with_equiv p hp α).uniform_continuous, |
| 174 | + have : (λ (x : pi_Lp p hp α × pi_Lp p hp α), |
| 175 | + ((pi_Lp.equiv p hp α) x.fst, (pi_Lp.equiv p hp α) x.snd)) = id, |
| 176 | + by ext i; refl, |
| 177 | + rw [← A.comap_uniformity, this, comap_id] |
| 178 | +end |
| 179 | + |
| 180 | +end |
| 181 | + |
| 182 | +/-! ### Instances on finite `L^p` products -/ |
| 183 | + |
| 184 | +instance uniform_space [∀ i, uniform_space (α i)] : uniform_space (pi_Lp p hp α) := |
| 185 | +Pi.uniform_space _ |
| 186 | + |
| 187 | +variable [fintype ι] |
| 188 | + |
| 189 | +/-- emetric space instance on the product of finitely many emetric spaces, using the `L^p` |
| 190 | +edistance, and having as uniformity the product uniformity. -/ |
| 191 | +instance [∀ i, emetric_space (α i)] : emetric_space (pi_Lp p hp α) := |
| 192 | +(emetric_aux p hp α).replace_uniformity (aux_uniformity_eq p hp α).symm |
| 193 | + |
| 194 | +protected lemma edist {p : ℝ} {hp : 1 ≤ p} {α : ι → Type*} |
| 195 | + [∀ i, emetric_space (α i)] (x y : pi_Lp p hp α) : |
| 196 | + edist x y = (∑ (i : ι), (edist (x i) (y i)) ^ p) ^ (1/p) := rfl |
| 197 | + |
| 198 | +/-- metric space instance on the product of finitely many metric spaces, using the `L^p` distance, |
| 199 | +and having as uniformity the product uniformity. -/ |
| 200 | +instance [∀ i, metric_space (α i)] : metric_space (pi_Lp p hp α) := |
| 201 | +begin |
| 202 | + /- we construct the instance from the emetric space instance to avoid checking again that the |
| 203 | + uniformity is the same as the product uniformity, but we register nevertheless a nice formula |
| 204 | + for the distance -/ |
| 205 | + have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp, |
| 206 | + refine emetric_space.to_metric_space_of_dist |
| 207 | + (λf g, (∑ (i : ι), (dist (f i) (g i)) ^ p) ^ (1/p)) (λ f g, _) (λ f g, _), |
| 208 | + { simp [pi_Lp.edist, ennreal.rpow_eq_top_iff, asymm pos, pos, |
| 209 | + ennreal.sum_eq_top_iff, edist_ne_top] }, |
| 210 | + { have A : ∀ (i : ι), i ∈ (finset.univ : finset ι) → edist (f i) (g i) ^ p < ⊤ := |
| 211 | + λ i hi, by simp [lt_top_iff_ne_top, edist_ne_top, le_of_lt pos], |
| 212 | + simp [dist, -one_div_eq_inv, pi_Lp.edist, ← ennreal.to_real_rpow, |
| 213 | + ennreal.to_real_sum A, dist_edist] } |
| 214 | +end |
| 215 | + |
| 216 | +protected lemma dist {p : ℝ} {hp : 1 ≤ p} {α : ι → Type*} |
| 217 | + [∀ i, metric_space (α i)] (x y : pi_Lp p hp α) : |
| 218 | + dist x y = (∑ (i : ι), (dist (x i) (y i)) ^ p) ^ (1/p) := rfl |
| 219 | + |
| 220 | +/-- normed group instance on the product of finitely many normed groups, using the `L^p` norm. -/ |
| 221 | +instance normed_group [∀i, normed_group (α i)] : normed_group (pi_Lp p hp α) := |
| 222 | +{ norm := λf, (∑ (i : ι), norm (f i) ^ p) ^ (1/p), |
| 223 | + dist_eq := λ x y, by { simp [pi_Lp.dist, dist_eq_norm], refl }, |
| 224 | + .. pi.add_comm_group } |
| 225 | + |
| 226 | +lemma norm_eq {p : ℝ} {hp : 1 ≤ p} {α : ι → Type*} |
| 227 | + [∀i, normed_group (α i)] (f : pi_Lp p hp α) : |
| 228 | + ∥f∥ = (∑ (i : ι), ∥f i∥ ^ p) ^ (1/p) := rfl |
| 229 | + |
| 230 | +variables (𝕜 : Type*) [normed_field 𝕜] |
| 231 | + |
| 232 | +/-- The product of finitely many normed spaces is a normed space, with the `L^p` norm. -/ |
| 233 | +instance normed_space [∀i, normed_group (α i)] [∀i, normed_space 𝕜 (α i)] : |
| 234 | + normed_space 𝕜 (pi_Lp p hp α) := |
| 235 | +{ norm_smul_le := |
| 236 | + begin |
| 237 | + assume c f, |
| 238 | + have : p * (1 / p) = 1 := mul_div_cancel' 1 (ne_of_gt (lt_of_lt_of_le zero_lt_one hp)), |
| 239 | + simp only [pi_Lp.norm_eq, norm_smul, mul_rpow, norm_nonneg, ←finset.mul_sum, pi.smul_apply], |
| 240 | + rw [mul_rpow (rpow_nonneg_of_nonneg (norm_nonneg _) _), ← rpow_mul (norm_nonneg _), |
| 241 | + this, rpow_one], |
| 242 | + exact finset.sum_nonneg (λ i hi, rpow_nonneg_of_nonneg (norm_nonneg _) _) |
| 243 | + end, |
| 244 | + .. pi.semimodule ι α 𝕜 } |
| 245 | + |
| 246 | +/- Register simplification lemmas for the applications of `pi_Lp` elements, as the usual lemmas |
| 247 | +for Pi types will not trigger. -/ |
| 248 | +variables {𝕜 p hp α} |
| 249 | +[∀i, normed_group (α i)] [∀i, normed_space 𝕜 (α i)] (c : 𝕜) (x y : pi_Lp p hp α) (i : ι) |
| 250 | + |
| 251 | +@[simp] lemma add_apply : (x + y) i = x i + y i := rfl |
| 252 | +@[simp] lemma sub_apply : (x - y) i = x i - y i := rfl |
| 253 | +@[simp] lemma smul_apply : (c • x) i = c • x i := rfl |
| 254 | +@[simp] lemma neg_apply : (-x) i = - (x i) := rfl |
| 255 | + |
| 256 | +end pi_Lp |
0 commit comments