multiset_prod_map_rpow — Mathlib

English

For any index set ι, multiset s, function f : ι → Real with f(i) ≥ 0, and r ∈ ℝ, (s.map (f ·^ r)).prod = (s.map f).prod^r.

Русский

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

LaTeX

$$(s.map (fun i => (f i) ^ r)).prod = (s.map f).prod ^ r$$

Lean4

/-- `rpow` version of `Multiset.prod_map_pow`. -/
theorem _root_.Real.multiset_prod_map_rpow {ι} (s : Multiset ι) (f : ι → ℝ) (hs : ∀ i ∈ s, (0 : ℝ) ≤ f i) (r : ℝ) :
    (s.map (f · ^ r)).prod = (s.map f).prod ^ r := by
  obtain ⟨l⟩ := s
  simpa using Real.list_prod_map_rpow' l f hs r

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