Revision #1933 → #2930 · back to history
8ff90d2dbeec| Field | From #1933 | To #2930 |
|---|---|---|
| mathlib.decl | Real.inner_mul_le_norm_mul_norm | — |
| mathlib.module | Mathlib.Analysis.MeanInequalities | — |
| note | The harmonic mean appears informally in the HM-GM inequality discussion but is not given a top-level definition. | No top-level definition of the harmonic mean of a finite family exists in `Mathlib/`; it only appears implicitly inside inequality lemmas. |
| provenance | ai | ai-moderated |
| status | partial | not_formalized |
ba5f6d125832aaf06532787f