Revision #3422 → #3995 · back to history
9030978461c3| Field | From #3422 | To #3995 |
|---|---|---|
| anchor.section | List of possible averages | Definitions |
| note | Mathlib has no top-level `geomMean` definition, but the geometric mean of positive weighted terms appears inside AM–GM inequality lemmas such as `Real.geom_mean_le_arith_mean_weighted` in `Mathlib.Analysis.MeanInequalities`. | Mathlib has no top-level `geomMean` definition, but the geometric mean of positive weighted terms appears inside AM–GM inequality lemmas such as `Real.geom_mean_le_arith_mean_weighted` in `Mathlib.Analysis.MeanInequalities`. Section corrected from 'List of possible averages' to 'Definitions' to match the snippet's actual location. |
| provenance | ai | ai-moderated |
d14cb812549caaf06532787f| Field | From #3422 | To #3995 |
|---|---|---|
| kind | definition | proposition |
| note | `Finset.expect_const` proves the arithmetic average of a constant function is that constant; the general statement quantifies over the unformalized class of all averages. | `Finset.expect_const` proves the arithmetic average of a constant function is that constant; the general statement quantifies over the unformalized class of all averages. Kind corrected from 'definition' to 'proposition'. |
| provenance | ai | ai-moderated |