list_prod_map_rpow' — Mathlib

English

For any index type ι and l: List ι, f: ι → Real with hl: ∀ i ∈ l, f(i) ≥ 0, and r ∈ ℝ, (l.map (f ·^ r)).prod = (l.map f).prod^r.

Русский

Для типа индексов ι, списка l: List ι, функции f: ι → Real при условии hl: ∀ i ∈ l, f(i) ≥ 0 и r ∈ ℝ, имеем (l.map (f i)^r).prod = (l.map f).prod^r.

LaTeX

$$∀ l f hl r, (List.map (fun i => (f i) ^ r) l).prod = (List.map f l).prod ^ r$$

Lean4

theorem _root_.Real.list_prod_map_rpow' {ι} (l : List ι) (f : ι → ℝ) (hl : ∀ i ∈ l, (0 : ℝ) ≤ f i) (r : ℝ) :
    (l.map (f · ^ r)).prod = (l.map f).prod ^ r :=
  by
  rw [← Real.list_prod_map_rpow (l.map f) _ r, List.map_map]
  · rfl
  simpa using hl

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