English
Let a ≥ 0. If s is finite and f: s → ℝ with f(x) ≥ 0 for all x ∈ s, then a^(∑_{x∈s} f(x)) = ∏_{x∈s} a^(f(x)).
Русский
Пусть a ≥ 0. Пусть s — конечное множество, f: s → ℝ и f(x) ≥ 0 для всех x ∈ s. Тогда a^{∑_{x∈s} f(x)} = ∏_{x∈s} a^{f(x)}.
LaTeX
$$$\forall a\ge 0,\ \forall s\in Finset(ι),\ \forall f: ι \to \mathbb{R},\ (a^{\sum_{x\in s} f(x)}) = \prod_{x\in s} a^{f(x)}$$$
Lean4
theorem rpow_sum_of_nonneg {ι : Type*} {a : ℝ} (ha : 0 ≤ a) {s : Finset ι} {f : ι → ℝ} (h : ∀ x ∈ s, 0 ≤ f x) :
(a ^ ∑ x ∈ s, f x) = ∏ x ∈ s, a ^ f x := by
induction s using Finset.cons_induction with
| empty => rw [sum_empty, Finset.prod_empty, rpow_zero]
| cons i s hi ihs =>
rw [forall_mem_cons] at h
rw [sum_cons, prod_cons, ← ihs h.2, rpow_add_of_nonneg ha h.1 (sum_nonneg h.2)]
