Real.sqrt_prod

Stream: Is there code for X?

[Monica Omar]

Do we not have this?

import Mathlib

theorem Real.sqrt_prod {ι : Type*} (s : Finset ι)
    {x : ι → ℝ} (hx : ∀ i ∈ s, 0 ≤ x i) :
    (∏ i ∈ s, x i).sqrt = ∏ i ∈ s, (x i).sqrt := by
  classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s hnis h =>
    rw [Finset.prod_insert hnis, Real.sqrt_mul (hx _ (by grind))]
    grind

[Michael Rothgang]

This holds for any multiplicative function (i.e. f (a * b) = f a * f b)), right? (I haven't tried to search.)

[Aaron Liu]

sqrt is only multiplicative on the nonnegative reals

[Aaron Liu]

but yeah it's docs#map_prod

[Monica Omar]

so we don't have the special case for sqrt, right?

[Michael Rothgang]

Aaron Liu said:

sqrt is only multiplicative on the nonnegative reals

(I know; sqrt is more "multiplicative on a set". Which is perhaps not worth its own typeclass.)

[Ruben Van de Velde]

import Mathlib

theorem Real.sqrt_prod {ι : Type*} (s : Finset ι)
    {x : ι → ℝ} (hx : ∀ i ∈ s, 0 ≤ x i) :
    (∏ i ∈ s, x i).sqrt = ∏ i ∈ s, (x i).sqrt := by
  convert congr_arg NNReal.toReal <| map_prod NNReal.sqrtHom (Real.toNNReal ∘ x) s <;>
    simp +contextual [-map_prod, NNReal.sqrtHom, hx]

[Monica Omar]

cool, I've added this to #33637