feat: an equality condition for AM-GM inequality #19435
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -190,6 +190,75 @@ theorem geom_mean_eq_arith_mean_weighted_of_constant (w z : ι → ℝ) (x : ℝ | |
| ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i := by | ||
| rw [geom_mean_weighted_of_constant, arith_mean_weighted_of_constant] <;> assumption | ||
|
|
||
| /- **AM-GM inequality - equality condition**: This theorem provides the equality condition for the | ||
| *positive* weighted version of the AM-GM inequality for real-valued nonnegative functions. -/ | ||
| theorem geom_mean_eq_arith_mean_weighted_iff_aux_of_pos (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 < w i) | ||
| (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) : | ||
| ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i := by | ||
| by_cases A : ∃ i ∈ s, z i = 0 ∧ w i ≠ 0 | ||
| · rcases A with ⟨i, his, hzi, hwi⟩ | ||
| rw [prod_eq_zero his] | ||
| · constructor | ||
| · intro h; rw [← h]; intro j hj | ||
|
There was a problem hiding this comment. Generally we discourage chaining together multiple tactics on one line. |
||
| apply eq_zero_of_ne_zero_of_mul_left_eq_zero (ne_of_lt (hw j hj)).symm | ||
| apply (sum_eq_zero_iff_of_nonneg ?_).mp h.symm j hj | ||
| exact fun i hi => (mul_nonneg_iff_of_pos_left (hw i hi)).mpr (hz i hi) | ||
| · intro h | ||
| convert h i his | ||
| exact hzi.symm | ||
| · rw [hzi] | ||
| exact zero_rpow hwi | ||
| · simp only [not_exists, not_and] at A | ||
| have hz' := fun i h => lt_of_le_of_ne (hz i h) (fun a => (A i h a.symm) (ne_of_gt (hw i h))) | ||
| have := strictConvexOn_exp.map_sum_eq_iff hw hw' fun i _ => Set.mem_univ <| log (z i) | ||
| simp only [exp_sum, (· ∘ ·), smul_eq_mul, mul_comm (w _) (log _)] at this | ||
|
There was a problem hiding this comment. What does There was a problem hiding this comment. While reading the I'll delete it in my theorem. What about the original There was a problem hiding this comment. I think it's a hangover from an old version. If it's not needed please delete it (here and in the earlier proof). Always use as few simp lemmas as you can. There was a problem hiding this comment.
I think it's equivalent to |
||
| convert this using 1 | ||
| · apply Eq.congr <;> [apply prod_congr rfl; apply sum_congr rfl] | ||
| <;> intro i hi <;> simp [exp_mul, exp_log (hz' i hi)] | ||
|
Comment on lines
+216
to
+217
There was a problem hiding this comment. More line breaks, and putting the |
||
| · constructor <;> intro h j hj | ||
| · rw [← arith_mean_weighted_of_constant s w _ (log (z j)) hw' fun i _ => congrFun rfl] | ||
| apply sum_congr rfl | ||
| intro x hx | ||
| simp only [mul_comm, h j hj, h x hx] | ||
| · rw [← arith_mean_weighted_of_constant s w _ (z j) hw' fun i _ => congrFun rfl] | ||
| apply sum_congr rfl | ||
| intro x hx | ||
| simp only [log_injOn_pos (hz' j hj) (hz' x hx), h j hj, h x hx] | ||
|
|
||
| /- **AM-GM inequality - equality condition**: This theorem provides the equality condition for the | ||
| weighted version of the AM-GM inequality for real-valued nonnegative functions. -/ | ||
| theorem geom_mean_eq_arith_mean_weighted_iff (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) | ||
| (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) : | ||
| ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, w j ≠ 0 → z j = ∑ i ∈ s, w i * z i := by | ||
| have h (i) (_ : i ∈ s) : w i * z i ≠ 0 → w i ≠ 0 := by aesop | ||
| have h' (i) (_ : i ∈ s) : z i ^ w i ≠ 1 → w i ≠ 0 := by aesop | ||
|
Comment on lines
+233
to
+234
There was a problem hiding this comment. These |
||
| rw [← sum_filter_of_ne h, ← prod_filter_of_ne h', geom_mean_eq_arith_mean_weighted_iff_aux_of_pos] | ||
| · simp | ||
| · simp (config := { contextual := true }) [(hw _ _).gt_iff_ne] | ||
|
There was a problem hiding this comment. There was a Zulip thread recently about a new cleaner syntax for this, something like |
||
| · rwa [sum_filter_ne_zero] | ||
| · simp_all only [ne_eq, mul_eq_zero, not_or, not_false_eq_true, and_imp, implies_true, mem_filter] | ||
|
|
||
| /- **AM-GM inequality - strict inequality condition**: This theorem provides the strict inequality | ||
| condition for the *positive* weighted version of the AM-GM inequality for real-valued nonnegative | ||
| functions. -/ | ||
| theorem geom_mean_lt_arith_mean_weighted_iff_of_pos (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 < w i) | ||
| (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) : | ||
| ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i ↔ ∃ j ∈ s, ∃ k ∈ s, z j ≠ z k:= by | ||
| constructor | ||
| · intro h | ||
| by_contra! h_contra | ||
| rw [(geom_mean_eq_arith_mean_weighted_iff_aux_of_pos s w z hw hw' hz).mpr ?_] at h | ||
| · exact (lt_self_iff_false _).mp h | ||
| · intro j hjs | ||
| rw [← arith_mean_weighted_of_constant s w (fun _ => z j) (z j) hw' fun _ _ => congrFun rfl] | ||
| apply sum_congr rfl (fun x a => congrArg (HMul.hMul (w x)) (h_contra j hjs x a)) | ||
| · rintro ⟨j, hjs, k, hks, hzjk⟩ | ||
| have := geom_mean_le_arith_mean_weighted s w z (fun i a => le_of_lt (hw i a)) hw' hz | ||
| by_contra! h | ||
| apply le_antisymm this at h | ||
| apply (geom_mean_eq_arith_mean_weighted_iff_aux_of_pos s w z hw hw' hz).mp at h | ||
| simp only [h j hjs, h k hks, ne_eq, not_true_eq_false] at hzjk | ||
|
|
||
| end Real | ||
|
|
||
| namespace NNReal | ||
|
|
||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In this theorem,
wandzcan be inferred from the other arguments – you can't prove that∀ i ∈ s, 0 < w iwithout knowing whatwis – so the usual library convention would be to make them implicit. That is, replace the round brackets with curly ones,{w z : ι → ℝ}. (Same applies to the other theorems here too.)On another matter: is this first theorem only useful as a stepping-stone to the theorems later on in the file (as the
auxin the name suggests)? If it is no longer useful once those theorems are proved (i.e. if the later theorems trivially imply it) then you can mark it asprivate, so it doesn't appear in the reference manual and can't be used outside this file.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for the review.
I found two simililar theorem in Jasen.lean,
StrictConvexOn.map_sum_eq_iffandStrictConvexOn.map_sum_eq_iff'(here), and I followed the same style to write the two theorems here. I'm not sure if I should make the 'aux' one private or rename it properly. (I also tried to name it something likegeom_mean_eq_arith_mean_weighted_iff', but the linter didn't accept the apostrophe)There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Aha! The linter shouldn't complain about the apostrophe as long as there is a doc-string. In your case you clearly meant to make a doc-string (the text preceding the theorem); but doc-strings need to start with
/--(two dashes), not/-(one dash) which is just an ordinary comment. So this needs to be fixed anyway; and it will have the side-effect of stopping the linter complaining.I had overlooked this until now, so it's lucky that you made the remark about linters.