Help with cancelling a square and square root under integral

Stream: new members

[Strategist _]

I'm currently trying to prove that a d-dimensional gaussian is normalized. My goal at the moment is

∫ (x : Fin d → ℝ), ((4 * π * t) ^ (d / 2))⁻¹ * rexp (-√(inner x x) ^ 2 / (4 * t)) = 1

and I'm trying to use "simp_rw [sq_sqrt]" to cancel the square root and square, but I just got "simp made no progress". Can anyone explain why this is happening and how to fix it?

[Yury G. Kudryashov]

It needs to know that the argument is nonnegative

[Yury G. Kudryashov]

Also, this is not a #mwe

[Strategist _]

Whoops. I didn't know the mwe requirement. Pretty new to this. Thanks! Here's my mwe

import Mathlib
import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.Data.Real.Basic
import Mathlib.MeasureTheory.Integral.Lebesgue
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Fin.Basic

open Real
open Finset
open MeasureTheory

variable {d : ℕ}

noncomputable def heat_kernel (t : ℝ) (x : EuclideanSpace ℝ (Fin d)) : ℝ :=
  if t > 0 then
    ((4 * π * t)^(d / 2))⁻¹ * exp (-‖x‖^2 / (4 * t))
  else
    0

theorem heat_kernal_normalized : ∀ (t : ℝ), 0 < t → ∫ (x : Fin d → ℝ), heat_kernel t x = 1 := by
  intro t
  intro h1
  unfold heat_kernel
  simp_rw [if_pos h1]
  simp_rw [norm_eq_sqrt_real_inner]
  simp_rw [sq_sqrt]

[Strategist _]

I tried including inner_self_nonneg after the sq_sqrt as well, but that didn't fix it

[Yury G. Kudryashov]

Try simp

[Strategist _]

Like, replacing the simp_rw with simp? That just gives

∫ (x : Fin d → ℝ), ((4 * π * t) ^ (d / 2))⁻¹ * rexp (-√(∑ x_1 : Fin d, x x_1 * x x_1) ^ 2 / (4 * t)) = 1

[Strategist _]

It turns the norm into a sum, but doesn't cancel the square or square root

[Strategist _]

Oh huh wait using real_inner_self_nonneg did fix it. I guess inner x x doesn't qualify as an RCLike.re (inner x x)?

[Strategist _]

Thank you for your help!

[Notification Bot]

This topic was moved here from #general > Help with cancelling a square and square root under integral by Yury G. Kudryashov.

[Yury G. Kudryashov]

simp_rw [a, b] is simp only [a]; simp only [b]. So, if you need 2 lemmas in one simp call, then you should use simp only or simp.