geom_mean_eq_arith_mean_weighted_of_constant

English

Equality for the weighted AM-GM with a constant target: the product equals the weighted sum when the relevant conditions hold.

Русский

Равенство в взвешенном AM-GM при константе: произведение равно взвешенной сумме при выполнении условий.

LaTeX

$$$\\prod_{i\\in s} z_i^{w_i} = \\sum_{i\\in s} w_i z_i$$$

Lean4

theorem geom_mean_eq_arith_mean_weighted_of_constant (w z : ι → ℝ) (x : ℝ) (hw : ∀ i ∈ s, 0 ≤ w i)
    (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) (hx : ∀ i ∈ s, w i ≠ 0 → z i = x) :
    ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i := by
  rw [geom_mean_weighted_of_constant, arith_mean_weighted_of_constant] <;> assumption

Похожие утверждения