feat(analysis/mean_inequalities): Minkowski inequality for infinite sums (#10984)

A few versions of the Minkowski inequality for `tsum` and `has_sum`.

Author: hrmacbeth

src/analysis/mean_inequalities.lean

@@ -377,6 +377,51 @@ begin
     ((is_greatest_Lp s g hpq).2 ⟨φ, hφ, rfl⟩)
 end
 
+/-- Minkowski inequality: the `L_p` seminorm of the infinite sum of two vectors is less than or
+equal to the infinite sum of the `L_p`-seminorms of the summands, if these infinite sums both
+exist. A version for `nnreal`-valued functions. For an alternative version, convenient if the
+infinite sums are already expressed as `p`-th powers, see `Lp_add_le_has_sum_of_nonneg`. -/
+theorem Lp_add_le_tsum {f g : ι → ℝ≥0} {p : ℝ} (hp : 1 ≤ p) (hf : summable (λ i, (f i) ^ p))
+  (hg : summable (λ i, (g i) ^ p)) :
+  summable (λ i, (f i + g i) ^ p) ∧
+  (∑' i, (f i + g i) ^ p) ^ (1 / p) ≤ (∑' i, (f i) ^ p) ^ (1 / p) + (∑' i, (g i) ^ p) ^ (1 / p) :=
+begin
+  have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp,
+  have H₁ : ∀ s : finset ι, ∑ i in s, (f i + g i) ^ p
+    ≤ ((∑' i, (f i)^p) ^ (1/p) + (∑' i, (g i)^p) ^ (1/p)) ^ p,
+  { intros s,
+    rw ← nnreal.rpow_one_div_le_iff pos,
+    refine le_trans (Lp_add_le s f g hp) (add_le_add _ _);
+    rw nnreal.rpow_le_rpow_iff (one_div_pos.mpr pos);
+    refine sum_le_tsum _ (λ _ _, zero_le _) _,
+    exacts [hf, hg] },
+  have bdd : bdd_above (set.range (λ s, ∑ i in s, (f i + g i) ^ p)),
+  { refine ⟨((∑' i, (f i)^p) ^ (1/p) + (∑' i, (g i)^p) ^ (1/p)) ^ p, _⟩,
+    rintros a ⟨s, rfl⟩,
+    exact H₁ s },
+  have H₂ : summable _ := (has_sum_of_is_lub _ (is_lub_csupr bdd)).summable,
+  refine ⟨H₂, _⟩,
+  rw nnreal.rpow_one_div_le_iff pos,
+  refine tsum_le_of_sum_le H₂ H₁,
+end
+
+/-- Minkowski inequality: the `L_p` seminorm of the infinite sum of two vectors is less than or
+equal to the infinite sum of the `L_p`-seminorms of the summands, if these infinite sums both
+exist. A version for `nnreal`-valued functions. For an alternative version, convenient if the
+infinite sums are not already expressed as `p`-th powers, see `Lp_add_le_tsum_of_nonneg`.  -/
+theorem Lp_add_le_has_sum {f g : ι → ℝ≥0} {A B : ℝ≥0} {p : ℝ} (hp : 1 ≤ p)
+  (hf : has_sum (λ i, (f i) ^ p) (A ^ p)) (hg : has_sum (λ i, (g i) ^ p) (B ^ p)) :
+  ∃ C, C ≤ A + B ∧ has_sum (λ i, (f i + g i) ^ p) (C ^ p) :=
+begin
+  have hp' : p ≠ 0 := (lt_of_lt_of_le zero_lt_one hp).ne',
+  obtain ⟨H₁, H₂⟩ := Lp_add_le_tsum hp hf.summable hg.summable,
+  have hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p) := by rw [hf.tsum_eq, rpow_inv_rpow_self hp'],
+  have hB : B = (∑' (i : ι), g i ^ p) ^ (1 / p) := by rw [hg.tsum_eq, rpow_inv_rpow_self hp'],
+  refine ⟨(∑' i, (f i + g i) ^ p) ^ (1 / p), _, _⟩,
+  { simpa [hA, hB] using H₂ },
+  { simpa only [rpow_self_rpow_inv hp'] using H₁.has_sum }
+end
+
 end nnreal
 
 namespace real
@@ -441,14 +486,49 @@ by convert rpow_sum_le_const_mul_sum_rpow s f hp using 2; apply sum_congr rfl; i
   simp only [abs_of_nonneg, hf i hi]
 
 /-- Minkowski inequality: the `L_p` seminorm of the sum of two vectors is less than or equal
-to the sum of the `L_p`-seminorms of the summands. A version for `real`-valued nonnegative
+to the sum of the `L_p`-seminorms of the summands. A version for `ℝ`-valued nonnegative
 functions. -/
 theorem Lp_add_le_of_nonneg (hp : 1 ≤ p) (hf : ∀ i ∈ s, 0 ≤ f i) (hg : ∀ i ∈ s, 0 ≤ g i) :
   (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤
     (∑ i in s, (f i) ^ p) ^ (1 / p) + (∑ i in s, (g i) ^ p) ^ (1 / p) :=
 by convert Lp_add_le s f g hp using 2 ; [skip, congr' 1, congr' 1];
   apply sum_congr rfl; intros i hi; simp only [abs_of_nonneg, hf i hi, hg i hi, add_nonneg]
 
+/-- Minkowski inequality: the `L_p` seminorm of the infinite sum of two vectors is less than or
+equal to the infinite sum of the `L_p`-seminorms of the summands, if these infinite sums both
+exist. A version for `ℝ`-valued functions. For an alternative version, convenient if the infinite
+sums are already expressed as `p`-th powers, see `Lp_add_le_has_sum_of_nonneg`. -/
+theorem Lp_add_le_tsum_of_nonneg (hp : 1 ≤ p) (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i)
+  (hf_sum : summable (λ i, (f i) ^ p)) (hg_sum : summable (λ i, (g i) ^ p)) :
+  summable (λ i, (f i + g i) ^ p) ∧
+  (∑' i, (f i + g i) ^ p) ^ (1 / p) ≤ (∑' i, (f i) ^ p) ^ (1 / p) + (∑' i, (g i) ^ p) ^ (1 / p) :=
+begin
+  lift f to (ι → ℝ≥0) using hf,
+  lift g to (ι → ℝ≥0) using hg,
+  norm_cast at *,
+  exact nnreal.Lp_add_le_tsum hp hf_sum hg_sum,
+end
+
+/-- Minkowski inequality: the `L_p` seminorm of the infinite sum of two vectors is less than or
+equal to the infinite sum of the `L_p`-seminorms of the summands, if these infinite sums both
+exist. A version for `ℝ`-valued functions. For an alternative version, convenient if the infinite
+sums are not already expressed as `p`-th powers, see `Lp_add_le_tsum_of_nonneg`. -/
+theorem Lp_add_le_has_sum_of_nonneg (hp : 1 ≤ p) (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i) {A B : ℝ}
+  (hA : 0 ≤ A) (hB : 0 ≤ B) (hfA : has_sum (λ i, (f i) ^ p) (A ^ p))
+  (hgB : has_sum (λ i, (g i) ^ p) (B ^ p)) :
+  ∃ C, 0 ≤ C ∧ C ≤ A + B ∧ has_sum (λ i, (f i + g i) ^ p) (C ^ p) :=
+begin
+  lift f to (ι → ℝ≥0) using hf,
+  lift g to (ι → ℝ≥0) using hg,
+  lift A to ℝ≥0 using hA,
+  lift B to ℝ≥0 using hB,
+  norm_cast at hfA hgB,
+  obtain ⟨C, hC₁, hC₂⟩ := nnreal.Lp_add_le_has_sum hp hfA hgB,
+  use C,
+  norm_cast,
+  exact ⟨zero_le _, hC₁, hC₂⟩,
+end
+
 end real
 
 namespace ennreal

src/analysis/special_functions/pow.lean

@@ -889,6 +889,12 @@ lemma rpow_sub' (x : ℝ≥0) {y z : ℝ} (h : y - z ≠ 0) :
   x ^ (y - z) = x ^ y / x ^ z :=
 nnreal.eq $ real.rpow_sub' x.2 h
 
+lemma rpow_inv_rpow_self {y : ℝ} (hy : y ≠ 0) (x : ℝ≥0) : (x ^ y) ^ (1 / y) = x :=
+by field_simp [← rpow_mul]
+
+lemma rpow_self_rpow_inv {y : ℝ} (hy : y ≠ 0) (x : ℝ≥0) : (x ^ (1 / y)) ^ y = x :=
+by field_simp [← rpow_mul]
+
 lemma inv_rpow (x : ℝ≥0) (y : ℝ) : (x⁻¹) ^ y = (x ^ y)⁻¹ :=
 nnreal.eq $ real.inv_rpow x.2 y
 
@@ -921,11 +927,10 @@ lemma rpow_le_rpow_iff {x y : ℝ≥0} {z : ℝ} (hz : 0 < z) : x ^ z ≤ y ^ z
 real.rpow_le_rpow_iff x.2 y.2 hz
 
 lemma le_rpow_one_div_iff {x y : ℝ≥0} {z : ℝ} (hz : 0 < z) :  x ≤ y ^ (1 / z) ↔ x ^ z ≤ y :=
-begin
-  nth_rewrite 0 ←rpow_one x,
-  nth_rewrite 0 ←@_root_.mul_inv_cancel _ _ z  hz.ne',
-  rw [rpow_mul, ←one_div, @rpow_le_rpow_iff _ _ (1/z) (by simp [hz])],
-end
+by rw [← rpow_le_rpow_iff hz, rpow_self_rpow_inv hz.ne']
+
+lemma rpow_one_div_le_iff {x y : ℝ≥0} {z : ℝ} (hz : 0 < z) :  x ^ (1 / z) ≤ y ↔ x ≤ y ^ z :=
+by rw [← rpow_le_rpow_iff hz, rpow_self_rpow_inv hz.ne']
 
 lemma rpow_lt_rpow_of_exponent_lt {x : ℝ≥0} {y z : ℝ} (hx : 1 < x) (hyz : y < z) : x^y < x^z :=
 real.rpow_lt_rpow_of_exponent_lt hx hyz
@@ -976,6 +981,24 @@ begin
   exact nnreal.rpow_le_rpow_of_exponent_ge h hx h_one_le,
 end
 
+lemma rpow_left_injective {x : ℝ} (hx : x ≠ 0) : function.injective (λ y : ℝ≥0, y^x) :=
+λ y z hyz, by simpa only [rpow_inv_rpow_self hx] using congr_arg (λ y, y ^ (1 / x)) hyz
+
+lemma rpow_eq_rpow_iff {x y : ℝ≥0} {z : ℝ} (hz : z ≠ 0) : x ^ z = y ^ z ↔ x = y :=
+(rpow_left_injective hz).eq_iff
+
+lemma rpow_left_surjective {x : ℝ} (hx : x ≠ 0) : function.surjective (λ y : ℝ≥0, y^x) :=
+λ y, ⟨y ^ x⁻¹, by simp_rw [←rpow_mul, _root_.inv_mul_cancel hx, rpow_one]⟩
+
+lemma rpow_left_bijective {x : ℝ} (hx : x ≠ 0) : function.bijective (λ y : ℝ≥0, y^x) :=
+⟨rpow_left_injective hx, rpow_left_surjective hx⟩
+
+lemma eq_rpow_one_div_iff {x y : ℝ≥0} {z : ℝ} (hz : z ≠ 0) :  x = y ^ (1 / z) ↔ x ^ z = y :=
+by rw [← rpow_eq_rpow_iff hz, rpow_self_rpow_inv hz]
+
+lemma rpow_one_div_eq_iff {x y : ℝ≥0} {z : ℝ} (hz : z ≠ 0) :  x ^ (1 / z) = y ↔ x = y ^ z :=
+by rw [← rpow_eq_rpow_iff hz, rpow_self_rpow_inv hz]
+
 lemma pow_nat_rpow_nat_inv (x : ℝ≥0) {n : ℕ} (hn : 0 < n) :
   (x ^ n) ^ (n⁻¹ : ℝ) = x :=
 by { rw [← nnreal.coe_eq, coe_rpow, nnreal.coe_pow], exact real.pow_nat_rpow_nat_inv x.2 hn }