awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
x : V
⊢ 0 ≤ φ x

Tactic:
positivity
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
⊢ ∀ (x : V), 0 ≤ φ x

Tactic:
exact fun x ↦ by positivity
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
⊢ 0 < HPow.hPow (β := ℕ) π 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
h'φ :
  π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 *
      (π / HPow.hPow (β := ℕ) π 2) ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 =
    1
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦ φ x) 1

Tactic:
rw [integral_const_mul, GaussianFourier.integral_rexp_neg_mul_sq_norm (by positivity)]

Premises used: MeasureTheory.integral_const_mul, GaussianFourier.integral_rexp_neg_mul_sq_norm
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
h'φ :
  π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 *
      (HPow.hPow (β := ℕ) π 1 / HPow.hPow (β := ℕ) π 2) ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 =
    1
⊢ π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 *
      (π / HPow.hPow (β := ℕ) π 2) ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 =
    1

Tactic:
nth_rewrite 2 [← pow_one π]

Premises used: Real.pi, pow_one
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
h'φ :
  π ^
      (HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 +
        HSub.hSub (α := ℝ) (↑1 : ℝ) (↑2 : ℝ) * HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2) =
    1
⊢ π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 *
      (HPow.hPow (β := ℕ) π 1 / HPow.hPow (β := ℕ) π 2) ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 =
    1

Tactic:
rw [← rpow_natCast, ← rpow_natCast, ← rpow_sub pi_pos, ← rpow_mul pi_nonneg,
        ← rpow_add pi_pos]

Premises used: Real.pi_nonneg, Real.pi_pos, Real.rpow_add, Real.rpow_sub, Real.rpow_mul, Real.rpow_natCast
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
h'φ : HPow.hPow (β := ℝ) π 0 = 1
⊢ π ^
      (HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 +
        HSub.hSub (α := ℝ) (↑1 : ℝ) (↑2 : ℝ) * HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2) =
    1

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
⊢ HPow.hPow (β := ℝ) π 0 = 1

Tactic:
rpow_zero _

Premises used: Real.rpow_zero
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
⊢ HPow.hPow (β := ℝ) π 0 = 1

Tactic:
exact rpow_zero _

Premises used: Real.rpow_zero
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
rw : Tendsto (β := ℝ) (fun (w : V) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) (cobounded V) atTop
⊢ Tendsto (β := ℝ) (fun (w : V) ↦ HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2) (cobounded V) atTop

Tactic:
rw [tendsto_const_mul_atTop_of_pos (by positivity)]

Premises used: Filter.tendsto_const_mul_atTop_of_pos
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
⊢ Tendsto (β := ℝ) (fun (w : V) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) (cobounded V) atTop

Tactic:
apply (tendsto_pow_atTop two_ne_zero).comp tendsto_norm_cobounded_atTop

Premises used: two_ne_zero, tendsto_norm_cobounded_atTop, Filter.Tendsto.comp, Filter.tendsto_pow_atTop
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
⊢ Tendsto (β := ℝ) (fun (w : V) ↦ HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2) (cobounded V) atTop

Tactic:
have A : Tendsto (fun (w : V) ↦ π ^ 2 * ‖w‖ ^ 2) (cobounded V) atTop := by
        rw [tendsto_const_mul_atTop_of_pos (by positivity)]
        apply (tendsto_pow_atTop two_ne_zero).comp tendsto_norm_cobounded_atTop
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A : Tendsto (β := ℝ) (fun (w : V) ↦ HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2) (cobounded V) atTop
⊢ Tendsto
    (fun (x : V) ↦
      π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 *
        ((fun (x : ℝ) ↦ x ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-1 * x)) ∘ fun (w : V) ↦
            HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
          x)
    (cobounded V) (𝓝 (π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 * 0))

Tactic:
have B := tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero (finrank ℝ V / 2) 1
        zero_lt_one |>.comp A |>.const_mul (π ^ (-finrank ℝ V / 2 : ℝ))
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A : Tendsto (β := ℝ) (fun (w : V) ↦ HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2) (cobounded V) atTop
B :
  Tendsto
    (fun (x : V) ↦
      π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 *
        ((fun (x : ℝ) ↦ x ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-1 * x)) ∘ fun (w : V) ↦
            HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
          x)
    (cobounded V) (𝓝 (π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 * 0))
⊢ Tendsto (β := ℝ)
    (fun (x : V) ↦
      π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 *
        ((fun (x : ℝ) ↦ x ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-1 * x)) ∘ fun (w : V) ↦
            HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
          x)
    (cobounded V) (𝓝 0)

Tactic:
rw [mul_zero] at B

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A : Tendsto (β := ℝ) (fun (w : V) ↦ HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2) (cobounded V) atTop
B :
  Tendsto (β := ℝ)
    (fun (x : V) ↦
      π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 *
        ((fun (x : ℝ) ↦ x ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-1 * x)) ∘ fun (w : V) ↦
            HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
          x)
    (cobounded V) (𝓝 0)
⊢ Tendsto (β := ℝ)
    (fun (x : V) ↦
      π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 *
        ((fun (x : ℝ) ↦ x ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-1 * x)) ∘ fun (w : V) ↦
            HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
          x)
    (cobounded V) (𝓝 0)

Tactic:
B
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A : Tendsto (β := ℝ) (fun (w : V) ↦ HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2) (cobounded V) atTop
B :
  Tendsto (β := ℝ)
    (fun (x : V) ↦
      π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 *
        ((fun (x : ℝ) ↦ x ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-1 * x)) ∘ fun (w : V) ↦
            HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
          x)
    (cobounded V) (𝓝 0)
h :
  ∀ (x : V),
    ‖x‖ ^ finrank ℝ V * φ x =
      π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 *
        ((fun (x : ℝ) ↦ x ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-1 * x)) ∘ fun (w : V) ↦
            HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
          x
⊢ Tendsto (β := ℝ) (fun (x : V) ↦ ‖x‖ ^ finrank ℝ V * φ x) (cobounded V) (𝓝 0)

Tactic:
convert! B using 2 with x
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A : Tendsto (β := ℝ) (fun (w : V) ↦ HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2) (cobounded V) atTop
B :
  Tendsto (β := ℝ)
    (fun (x : V) ↦
      π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 *
        ((fun (x : ℝ) ↦ x ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-1 * x)) ∘ fun (w : V) ↦
            HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
          x)
    (cobounded V) (𝓝 0)
x : V
h :
  HPow.hPow (β := ℝ) ‖x‖ (↑(finrank ℝ V) : ℝ) * π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 *
      rexp (-(HPow.hPow (β := ℝ) π (↑2 : ℝ) * HPow.hPow (β := ℝ) ‖x‖ (↑2 : ℝ))) =
    π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 *
        (HPow.hPow (β := ℝ) π (↑2 : ℝ) * HPow.hPow (β := ℝ) ‖x‖ (↑2 : ℝ)) ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 *
      rexp (-(HPow.hPow (β := ℝ) π (↑2 : ℝ) * HPow.hPow (β := ℝ) ‖x‖ (↑2 : ℝ)))
⊢ ‖x‖ ^ finrank ℝ V * φ x =
    π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 *
      ((fun (x : ℝ) ↦ x ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-1 * x)) ∘ fun (w : V) ↦
          HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
        x

Tactic:
simp only [neg_mul, one_mul, Function.comp_apply, ← mul_assoc, ← rpow_natCast, φ]

Premises used: mul_assoc, Function.comp_apply, neg_mul, one_mul, Real.rpow_natCast
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A : Tendsto (β := ℝ) (fun (w : V) ↦ HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2) (cobounded V) atTop
B :
  Tendsto (β := ℝ)
    (fun (x : V) ↦
      π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 *
        ((fun (x : ℝ) ↦ x ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-1 * x)) ∘ fun (w : V) ↦
            HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
          x)
    (cobounded V) (𝓝 0)
x : V
h :
  HPow.hPow (β := ℝ) ‖x‖ (↑(finrank ℝ V) : ℝ) * π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 =
    π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 *
      (HPow.hPow (β := ℝ) π (↑2 : ℝ) * HPow.hPow (β := ℝ) ‖x‖ (↑2 : ℝ)) ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2
⊢ HPow.hPow (β := ℝ) ‖x‖ (↑(finrank ℝ V) : ℝ) * π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 *
      rexp (-(HPow.hPow (β := ℝ) π (↑2 : ℝ) * HPow.hPow (β := ℝ) ‖x‖ (↑2 : ℝ))) =
    π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 *
        (HPow.hPow (β := ℝ) π (↑2 : ℝ) * HPow.hPow (β := ℝ) ‖x‖ (↑2 : ℝ)) ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 *
      rexp (-(HPow.hPow (β := ℝ) π (↑2 : ℝ) * HPow.hPow (β := ℝ) ‖x‖ (↑2 : ℝ)))

Tactic:
congr 1
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A : Tendsto (β := ℝ) (fun (w : V) ↦ HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2) (cobounded V) atTop
B :
  Tendsto (β := ℝ)
    (fun (x : V) ↦
      π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 *
        ((fun (x : ℝ) ↦ x ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-1 * x)) ∘ fun (w : V) ↦
            HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
          x)
    (cobounded V) (𝓝 0)
x : V
⊢ 0 ≤ HPow.hPow (β := ℝ) π (↑2 : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A : Tendsto (β := ℝ) (fun (w : V) ↦ HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2) (cobounded V) atTop
B :
  Tendsto (β := ℝ)
    (fun (x : V) ↦
      π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 *
        ((fun (x : ℝ) ↦ x ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-1 * x)) ∘ fun (w : V) ↦
            HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
          x)
    (cobounded V) (𝓝 0)
x : V
⊢ 0 ≤ HPow.hPow (β := ℝ) ‖x‖ (↑2 : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A : Tendsto (β := ℝ) (fun (w : V) ↦ HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2) (cobounded V) atTop
B :
  Tendsto (β := ℝ)
    (fun (x : V) ↦
      π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 *
        ((fun (x : ℝ) ↦ x ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-1 * x)) ∘ fun (w : V) ↦
            HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
          x)
    (cobounded V) (𝓝 0)
x : V
h :
  π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * HPow.hPow (β := ℝ) ‖x‖ (↑(finrank ℝ V) : ℝ) =
    π ^ (HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 + (↑2 : ℝ) * HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2) *
      ‖x‖ ^ ((↑2 : ℝ) * HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2)
⊢ HPow.hPow (β := ℝ) ‖x‖ (↑(finrank ℝ V) : ℝ) * π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 =
    π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 *
      (HPow.hPow (β := ℝ) π (↑2 : ℝ) * HPow.hPow (β := ℝ) ‖x‖ (↑2 : ℝ)) ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2

Tactic:
rw [mul_rpow (by positivity) (by positivity), ← rpow_mul pi_nonneg,
        ← rpow_mul (norm_nonneg _), ← mul_assoc, ← rpow_add pi_pos, mul_comm]

Premises used: Real.pi_nonneg, mul_assoc, Real.mul_rpow, Real.pi_pos, mul_comm, Real.rpow_add, Real.rpow_mul, norm_nonneg
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A : Tendsto (β := ℝ) (fun (w : V) ↦ HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2) (cobounded V) atTop
B :
  Tendsto (β := ℝ)
    (fun (x : V) ↦
      π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 *
        ((fun (x : ℝ) ↦ x ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-1 * x)) ∘ fun (w : V) ↦
            HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
          x)
    (cobounded V) (𝓝 0)
x : V
h :
  HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 =
    HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 + (↑2 : ℝ) * HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2
h₁ : (↑(finrank ℝ V) : ℝ) = (↑2 : ℝ) * HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2
⊢ π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * HPow.hPow (β := ℝ) ‖x‖ (↑(finrank ℝ V) : ℝ) =
    π ^ (HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 + (↑2 : ℝ) * HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2) *
      ‖x‖ ^ ((↑2 : ℝ) * HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2)

Tactic:
congr
-- Module: Mathlib.Analysis.Fourier.Inversion
Goal:
V : Type u_1
E : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MeasurableSpace V
inst_3 : BorelSpace V
inst_4 : FiniteDimensional ℝ V
inst_5 : NormedAddCommGroup E
inst_6 : NormedSpace ℂ E
f : V → E
inst_7 : CompleteSpace E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
v : V
h'f : ContinuousAt f v
φ : V → ℝ :=
  fun (w : V) ↦
    π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
A : Tendsto (β := ℝ) (fun (w : V) ↦ HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2) (cobounded V) atTop
B :
  Tendsto (β := ℝ)
    (fun (x : V) ↦
      π ^ HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 *
        ((fun (x : ℝ) ↦ x ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 * rexp (-1 * x)) ∘ fun (w : V) ↦
            HPow.hPow (β := ℕ) π 2 * HPow.hPow (β := ℕ) ‖w‖ 2)
          x)
    (cobounded V) (𝓝 0)
x : V
⊢ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 =
    HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 + (↑2 : ℝ) * HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2

Tactic:
ring