feat(analysis/mean_inequalities): AM and GM are equal on a constant t…

…uple (#12179)

The converse is also true, but I have not gotten around to proving it.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/analysis/mean_inequalities.lean

@@ -125,6 +125,43 @@ begin
       { rw [exp_log hz] } } }
 end
 
+theorem geom_mean_weighted_of_constant (w z : ι → ℝ) (x : ℝ) (hw : ∀ i ∈ s, 0 ≤ w i)
+  (hw' : ∑ i in s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) (hx : ∀ i ∈ s, w i ≠ 0 → z i = x) :
+  (∏ i in s, (z i) ^ (w i)) = x :=
+calc (∏ i in s, (z i) ^ (w i)) = ∏ i in s, x ^ w i :
+  begin
+    refine prod_congr rfl (λ i hi, _),
+    cases eq_or_ne (w i) 0 with h₀ h₀,
+    { rw [h₀, rpow_zero, rpow_zero] },
+    { rw hx i hi h₀ }
+  end
+... = x :
+  begin
+    rw [← rpow_sum_of_nonneg _ hw, hw', rpow_one],
+    have : (∑ i in s, w i) ≠ 0,
+    { rw hw', exact one_ne_zero },
+    obtain ⟨i, his, hi⟩ := exists_ne_zero_of_sum_ne_zero this,
+    rw ← hx i his hi,
+    exact hz i his
+  end
+
+theorem arith_mean_weighted_of_constant (w z : ι → ℝ) (x : ℝ)
+  (hw' : ∑ i in s, w i = 1) (hx : ∀ i ∈ s, w i ≠ 0 → z i = x) :
+  ∑ i in s, w i * z i = x :=
+calc ∑ i in s, w i * z i = ∑ i in s, w i * x :
+  begin
+    refine sum_congr rfl (λ i hi, _),
+    cases eq_or_ne (w i) 0 with hwi hwi,
+    { rw [hwi, zero_mul, zero_mul] },
+    { rw hx i hi hwi },
+  end
+... = x : by rw [←sum_mul, hw', one_mul]
+
+theorem geom_mean_eq_arith_mean_weighted_of_constant (w z : ι → ℝ) (x : ℝ) (hw : ∀ i ∈ s, 0 ≤ w i)
+  (hw' : ∑ i in s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) (hx : ∀ i ∈ s, w i ≠ 0 → z i = x) :
+  (∏ i in s, (z i) ^ (w i)) = ∑ i in s, w i * z i :=
+by rw [geom_mean_weighted_of_constant, arith_mean_weighted_of_constant]; assumption
+
 end real
 
 namespace nnreal

src/analysis/special_functions/pow.lean

@@ -20,8 +20,8 @@ We also prove basic properties of these functions.
 
 noncomputable theory
 
-open_locale classical real topological_space nnreal ennreal filter
-open filter
+open_locale classical real topological_space nnreal ennreal filter big_operators
+open filter finset set
 
 namespace complex
 
@@ -113,7 +113,7 @@ by simpa using cpow_neg x 1
 
 lemma cpow_nat_inv_pow (x : ℂ) {n : ℕ} (hn : 0 < n) : (x ^ (n⁻¹ : ℂ)) ^ n = x :=
 begin
-  suffices : im (log x * n⁻¹) ∈ set.Ioc (-π) π,
+  suffices : im (log x * n⁻¹) ∈ Ioc (-π) π,
   { rw [← cpow_nat_cast, ← cpow_mul _ this.1 this.2, inv_mul_cancel, cpow_one],
     exact_mod_cast hn.ne' },
   rw [mul_comm, ← of_real_nat_cast, ← of_real_inv, of_real_mul_im, ← div_eq_inv_mul],
@@ -407,10 +407,10 @@ namespace real
 
 variables {x y z : ℝ}
 
-lemma rpow_add {x : ℝ} (hx : 0 < x) (y z : ℝ) : x ^ (y + z) = x ^ y * x ^ z :=
+lemma rpow_add (hx : 0 < x) (y z : ℝ) : x ^ (y + z) = x ^ y * x ^ z :=
 by simp only [rpow_def_of_pos hx, mul_add, exp_add]
 
-lemma rpow_add' {x : ℝ} (hx : 0 ≤ x) {y z : ℝ} (h : y + z ≠ 0) : x ^ (y + z) = x ^ y * x ^ z :=
+lemma rpow_add' (hx : 0 ≤ x) (h : y + z ≠ 0) : x ^ (y + z) = x ^ y * x ^ z :=
 begin
   rcases hx.eq_or_lt with rfl|pos,
   { rw [zero_rpow h, zero_eq_mul],
@@ -419,6 +419,14 @@ begin
   { exact rpow_add pos _ _ }
 end
 
+lemma rpow_add_of_nonneg (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) :
+  x ^ (y + z) = x ^ y * x ^ z :=
+begin
+  rcases hy.eq_or_lt with rfl|hy,
+  { rw [zero_add, rpow_zero, one_mul] },
+  exact rpow_add' hx (ne_of_gt $ add_pos_of_pos_of_nonneg hy hz)
+end
+
 /-- For `0 ≤ x`, the only problematic case in the equality `x ^ y * x ^ z = x ^ (y + z)` is for
 `x = 0` and `y + z = 0`, where the right hand side is `1` while the left hand side can vanish.
 The inequality is always true, though, and given in this lemma. -/
@@ -434,6 +442,20 @@ begin
   { simp [rpow_add pos] }
 end
 
+lemma rpow_sum_of_pos {ι : Type*} {a : ℝ} (ha : 0 < a) (f : ι → ℝ) (s : finset ι) :
+  a ^ (∑ x in s, f x) = ∏ x in s, a ^ f x :=
+@add_monoid_hom.map_sum ℝ ι (additive ℝ) _ _ ⟨λ x : ℝ, (a ^ x : ℝ), rpow_zero a, rpow_add ha⟩ f s
+
+lemma rpow_sum_of_nonneg {ι : Type*} {a : ℝ} (ha : 0 ≤ a) {s : finset ι} {f : ι → ℝ}
+  (h : ∀ x ∈ s, 0 ≤ f x) :
+  a ^ (∑ x in s, f x) = ∏ x in s, a ^ f x :=
+begin
+  induction s using finset.cons_induction with i s hi ihs,
+  { rw [sum_empty, finset.prod_empty, rpow_zero] },
+  { rw forall_mem_cons at h,
+    rw [sum_cons, prod_cons, ← ihs h.2, rpow_add_of_nonneg ha h.1 (sum_nonneg h.2)] }
+end
+
 lemma rpow_mul {x : ℝ} (hx : 0 ≤ x) (y z : ℝ) : x ^ (y * z) = (x ^ y) ^ z :=
 by rw [← complex.of_real_inj, complex.of_real_cpow (rpow_nonneg_of_nonneg hx _),
     complex.of_real_cpow hx, complex.of_real_mul, complex.cpow_mul, complex.of_real_cpow hx];
@@ -635,7 +657,7 @@ begin
 end
 
 lemma rpow_left_inj_on {x : ℝ} (hx : x ≠ 0) :
-  set.inj_on (λ y : ℝ, y^x) {y : ℝ | 0 ≤ y} :=
+  inj_on (λ y : ℝ, y^x) {y : ℝ | 0 ≤ y} :=
 begin
   rintros y hy z hz (hyz : y ^ x = z ^ x),
   rw [←rpow_one y, ←rpow_one z, ←_root_.mul_inv_cancel hx, rpow_mul hy, rpow_mul hz, hyz]
@@ -745,7 +767,7 @@ begin
   have C : tendsto (λ p : ℝ × ℝ, p.1 ^ p.2) (𝓝[{0}] 0 ×ᶠ 𝓝 y) (pure 0),
   { rw [nhds_within_singleton, tendsto_pure, pure_prod, eventually_map],
     exact (lt_mem_nhds hp).mono (λ y hy, zero_rpow hy.ne') },
-  simpa only [← sup_prod, ← nhds_within_union, set.compl_union_self, nhds_within_univ, nhds_prod_eq,
+  simpa only [← sup_prod, ← nhds_within_union, compl_union_self, nhds_within_univ, nhds_prod_eq,
     continuous_at, zero_rpow hp.ne'] using B.sup (C.mono_right (pure_le_nhds _))
 end
 

src/data/finset/basic.lean

@@ -499,6 +499,10 @@ def cons (a : α) (s : finset α) (h : a ∉ s) : finset α := ⟨a ::ₘ s.1, n
 @[simp] lemma mem_cons_self (a : α) (s : finset α) {h} : a ∈ cons a s h := mem_cons_self _ _
 @[simp] lemma cons_val (h : a ∉ s) : (cons a s h).1 = a ::ₘ s.1 := rfl
 
+lemma forall_mem_cons (h : a ∉ s) (p : α → Prop) :
+  (∀ x, x ∈ cons a s h → p x) ↔ p a ∧ ∀ x, x ∈ s → p x :=
+by simp only [mem_cons, or_imp_distrib, forall_and_distrib, forall_eq]
+
 @[simp] lemma mk_cons {s : multiset α} (h : (a ::ₘ s).nodup) :
   (⟨a ::ₘ s, h⟩ : finset α) = cons a ⟨s, (nodup_cons.1 h).2⟩ (nodup_cons.1 h).1 := rfl
 
@@ -1390,6 +1394,9 @@ variable {p}
 
 @[simp] theorem mem_filter {s : finset α} {a : α} : a ∈ s.filter p ↔ a ∈ s ∧ p a := mem_filter
 
+lemma mem_of_mem_filter {s : finset α} (x : α) (h : x ∈ s.filter p) : x ∈ s :=
+mem_of_mem_filter h
+
 theorem filter_ssubset {s : finset α} : s.filter p ⊂ s ↔ ∃ x ∈ s, ¬ p x :=
 ⟨λ h, let ⟨x, hs, hp⟩ := set.exists_of_ssubset h in ⟨x, hs, mt (λ hp, mem_filter.2 ⟨hs, hp⟩) hp⟩,
   λ ⟨x, hs, hp⟩, ⟨s.filter_subset _, λ h, hp (mem_filter.1 (h hs)).2⟩⟩
@@ -1425,6 +1432,9 @@ begin
   rwa filter_eq_nil at hs'
 end
 
+lemma filter_nonempty_iff {s : finset α} : (s.filter p).nonempty ↔ ∃ a ∈ s, p a :=
+by simp only [nonempty_iff_ne_empty, ne.def, filter_eq_empty_iff, not_not, not_forall]
+
 lemma filter_congr {s : finset α} (H : ∀ x ∈ s, p x ↔ q x) : filter p s = filter q s :=
 eq_of_veq $ filter_congr H