feat: an equality condition for AM-GM inequality

[hehepig166]

Add some theorems on the equality condition of the weighted AM-GM inequality for real-valued nonnegative functions, referring to geom_mean_arith_mean_weighted_eq_iff in Mathlib/Analysis/MeanInequalities.lean.

---

[github-actions]

PR summary 0de365a3b0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ geom_mean_eq_arith_mean_weighted_iff
+ geom_mean_eq_arith_mean_weighted_iff_aux_of_pos
+ geom_mean_lt_arith_mean_weighted_iff_of_pos

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[YaelDillies]

Thanks for the PR!

[YaelDillies]

The usual way to prove the equality case of an inequality is to first prove its strict inequality case. Could you please do that here? Thanks!

[hehepig166]

The usual way to prove the equality case of an inequality is to first prove its strict inequality case. Could you please do that here? Thanks!

Do you mean I should write a new theorem to handle the strict inequality case first, or just modify the current proof to include it as a step?

something like this?

theorem geom_mean_lt_arith_mean_weighted' (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 < w i)
    (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 < z i) (hzne : ∃ j ∈ s, ∃ k ∈ s, z j ≠ z k) :
    ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i := by
  sorry

[YaelDillies]

You should write a new theorem 😄

[hehepig166]

The strict inequality equivalent condition is done (maybe?).

I ended up splitting the equality case into two versions to make proving the strict inequality more convenient (yes, I used the equality condition to prove the strict inequality, which was quite easy to write).
As for the version where weights can be zero, I tried writing the strict inequality case, but the equivalent condition turned out to be too complex.

[acmepjz]

The usual way to prove the equality case of an inequality is to first prove its strict inequality case. Could you please do that here? Thanks!

But I think eq_iff case is enough. Since we already have le, so if it's not eq it must be lt.

[acmepjz]

Looks good, though I'm not familiar with elementary inequalities.

[loefflerd]

Here are a few more small tips. This is looking pretty good now, thanks for the nice contribution!

[loefflerd]

In this theorem, w and z can be inferred from the other arguments – you can't prove that ∀ i ∈ s, 0 < w i without knowing what w is – 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 aux in 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 as private, so it doesn't appear in the reference manual and can't be used outside this file.

[hehepig166]

Thanks for the review.
I found two simililar theorem in Jasen.lean, StrictConvexOn.map_sum_eq_iff and StrictConvexOn.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 like geom_mean_eq_arith_mean_weighted_iff' , but the linter didn't accept the apostrophe)

[loefflerd]

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.

[loefflerd]

Generally we discourage chaining together multiple tactics on one line.

[loefflerd]

What does simp only [(· ∘ ·)] do? I've never seen this syntax before.

[hehepig166]

While reading the geom_mean_le_arith_mean_weighted theorem earlier in the same file, I noticed this. Deleting it doesn't affect local compilation, but I kept it in case it was a historical issue. Perhaps the code is a bit outdated due to Lean version differences?

I'll delete it in my theorem. What about the original geom_mean_le_arith_mean_weighted theorem?

[loefflerd]

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.

[acmepjz]

What does simp only [(· ∘ ·)] do? I've never seen this syntax before.

I think it's equivalent to Function.comp or Function.comp_def. (· ∘ ·) is for cuteness 😂

[loefflerd]

More line breaks, and putting the <;> at the end of lines rather than the beginning, would be easier to read.

[loefflerd]

These haves seem to be duplicating existing lemmas in the library, eg the first is just left_ne_zero_of_mul.

[loefflerd]

There was a Zulip thread recently about a new cleaner syntax for this, something like simp +contextual [foo]