Theorems · Theorem · real analysis
NNReal.geom_mean_le_arith_mean3_weighted
∀ (w₁ w₂ w₃ p₁ p₂ p₃ : NNReal), w₁ + w₂ + w₃ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ * p₃ ^ ↑w₃ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃
- Defined in
- Mathlib.Analysis.MeanInequalities
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 199 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- NNRealstatement and proof · cited by 4,310
- mul_oneproof · cited by 3,885
- Finset.univproof · cited by 3,473
- add_zeroproof · cited by 2,707
- Finset.sum_congrproof · cited by 2,323
- mul_assocproof · cited by 1,667
- NNReal.toRealstatement and proof · cited by 1,260
- Matrix.vecConsproof · cited by 852
- Matrix.vecEmptyproof · cited by 832
- Finset.prod_congrproof · cited by 646
- Finset.univ_eq_emptyproof · cited by 51
Cited by1
Results whose statement or proof uses this declaration.
- Real.geom_mean_le_arith_mean3_weightedproof · cited by 0