list_prod_map_rpow — Mathlib

English

For l: List Real with hl: all elements nonnegative, and r ∈ ℝ, (l.map (·^r)).prod = (l.prod)^r.

Русский

Для списка вещественных l с условием hl: все элементы неотрицательны и для r ∈ ℝ, (l.map (·^r)).prod = (l.prod)^r.

LaTeX

$$∀ l hl r, (l.map (fun x => x ^ r)).prod = (l.prod) ^ r$$

Lean4

/-- `rpow` version of `List.prod_map_pow` for `Real`. -/
theorem _root_.Real.list_prod_map_rpow (l : List ℝ) (hl : ∀ x ∈ l, (0 : ℝ) ≤ x) (r : ℝ) :
    (l.map (· ^ r)).prod = l.prod ^ r := by
  lift l to List ℝ≥0 using hl
  have := congr_arg ((↑) : ℝ≥0 → ℝ) (NNReal.list_prod_map_rpow l r)
  push_cast at this
  rw [List.map_map] at this ⊢
  exact mod_cast this

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