Adding Equality Conditions to MeanInequalities in Mathlib4

Stream: mathlib4

[Zhu]

Hi!

I've been working on filling some TODO's of MeanInequalities in Mathlib4, specifically focusing on the equality conditions for various inequalities, such as AM-GM.

I'm wondering whether it would be more appropriate to create a new file for these additions or simply append them to the existing MeanInequalities file. Also, If I modify the existing file, should I update the Authors section in the headers?

here's my code for equality conditions for weighted version of AM-GM inequalitit.

/- **AM-GM inequality**: The geometric mean is less than or equal to the arithmetic mean. For the
weighted version with real-valued nonnegative functions, equality holds if and only if all values
are equal to the weighted arithmetic mean. -/

theorem geom_mean_arith_mean_weighted_eq_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, 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
        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
    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)]
    . 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]

[Ruben Van de Velde]

Oh cool, I think I attempted this at one point and didn't manage to prove it

[Ruben Van de Velde]

How long is the file?

[Zhu]

Ruben Van de Velde said:

How long is the file?

Actually, I've only written the case I shared above for now. And I'm currently working on filling in the code for other cases.

[Zhu]

The original file is about 900 lines long and contains many inequalities including AM-GM, HM-GM, Young's inequality, Hölder's inequality and others.

[Ruben Van de Velde]

If it goes over 1500 with your new results, I'd probably put them in a new file

[Zhu]

Thanks.
I think the equality condition proofs are about the same length as the inequality proofs in most cases.
For now, I plan to incrementally add them to the original file and commit. Once it grows large enough, I'll organize them into a separate file.