Mahlers_Inequality
Provedanalysisinequalitiesproofwiki
The geometric mean of the termwise sum of two finite sequences of positive reals is at least the sum of their geometric means (Mahler's inequality).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Mahlers_Inequality (n : ℕ) (hn : 0 < n) (a b : Fin n → ℝ) (ha : ∀ i, 0 < a i) (hb : ∀ i, 0 < b i) : (∏ i : Fin n, (a i + b i)) ≥ (∏ i : Fin n, a i) + (∏ i : Fin n, b i) := by sorry
Source