Theorems · Theorem · real analysis

Real.harm_mean_le_geom_mean

∀ {ι : Type u_1} (s : Finset ι),
  s.Nonempty →
    ∀ (w z : ι → ℝ),
      (∀ i ∈ s, 0 < w i) →
        0 < ∑ i ∈ s, w i →
          (∀ i ∈ s, 0 < z i) → (∑ i ∈ s, w i) / ∑ i ∈ s, w i / z i ≤ (∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹

HM-GM inequality: The harmonic mean is less than or equal to the geometric mean.

Defined in

Mathlib.Analysis.MeanInequalities

Cited by

0 results in Mathlib

Foundations

Depth 206 from the axioms · uses propext, Classical.choice, Quot.sound