awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
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φ : ∀ (x : V), 0 ≤ φ x
⊢ Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
have h'φ : Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦ φ x) 1
Tactic: apply tendsto_integral_comp_smul_smul_of_integrable'
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
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φ : ∀ (x : V), 0 ≤ φ x
h'φ : Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦ φ x) 1
⊢ Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
have h : Tendsto (β := ℝ) (fun (x : V) ↦ ‖x‖ ^ finrank ℝ V * φ x) (cobounded V) (𝓝 0)
Tactic: apply tendsto_integral_comp_smul_smul_of_integrable'
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
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)
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦ φ x) 1
have h'φ : π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 *
    (π / HPow.hPow (β := ℕ) π 2) ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 =
  1
Tactic: rw [integral_const_mul, GaussianFourier.integral_rexp_neg_mul_sq_norm (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
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)
⊢ π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 *
      (π / HPow.hPow (β := ℕ) π 2) ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 =
    1
have h'φ : π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 *
    (HPow.hPow (β := ℕ) π 1 / HPow.hPow (β := ℕ) π 2) ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 =
  1
Tactic: nth_rewrite 2 [← pow_one π]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
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)
⊢ π ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 *
      (HPow.hPow (β := ℕ) π 1 / HPow.hPow (β := ℕ) π 2) ^ HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 =
    1
have h'φ : π ^
    (HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 +
      HSub.hSub (α := ℝ) (↑1 : ℝ) (↑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]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
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)
⊢ π ^
      (HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 +
        HSub.hSub (α := ℝ) (↑1 : ℝ) (↑2 : ℝ) * HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2) =
    1
have h'φ : HPow.hPow (β := ℝ) π 0 = 1
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
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
have rw : Tendsto (β := ℝ) (fun (w : V) ↦ HPow.hPow (β := ℕ) ‖w‖ 2) (cobounded V) atTop
Tactic: rw [tendsto_const_mul_atTop_of_pos (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (hypothesis)
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 (x : V) ↦ ‖x‖ ^ finrank ℝ V * φ x) (cobounded V) (𝓝 0)
have A : 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
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (hypothesis)
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) ↦ ‖x‖ ^ finrank ℝ V * φ x) (cobounded V) (𝓝 0)
have 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))
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 : ℝ))
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (hypothesis)
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) ↦ ‖x‖ ^ finrank ℝ V * φ x) (cobounded V) (𝓝 0)
have 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)
Tactic: rw [mul_zero] at B
Cleared hypotheses: B
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
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) ↦ ‖x‖ ^ finrank ℝ V * φ x) (cobounded V) (𝓝 0)
have 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
Tactic: convert! B using 2 with x
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
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
⊢ ‖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
have 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 : ℝ)))
Tactic: simp only [neg_mul, one_mul, Function.comp_apply, ← mul_assoc, ← rpow_natCast, φ]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
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
⊢ 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 : ℝ)))
have 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
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
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
⊢ 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
have 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)
Tactic: rw [mul_rpow (by positivity) (by positivity), ← rpow_mul pi_nonneg,
        ← rpow_mul (norm_nonneg _), ← mul_assoc, ← rpow_add pi_pos, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
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 * HPow.hPow (β := ℝ) ‖x‖ (↑(finrank ℝ V) : ℝ) =
    π ^ (HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 + (↑2 : ℝ) * HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2) *
      ‖x‖ ^ ((↑2 : ℝ) * HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2)
have h : HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2 =
  HDiv.hDiv (α := ℝ) (-(↑(finrank ℝ V) : ℝ)) 2 + (↑2 : ℝ) * HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (goal)
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
⊢ π ^ 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)
have h₁ : (↑(finrank ℝ V) : ℝ) = (↑2 : ℝ) * HDiv.hDiv (α := ℝ) (↑(finrank ℝ V) : ℝ) 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (hypothesis)
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 (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
            cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
          f w)
    atTop (𝓝 (f v))
have A : Tendsto
  (fun (c : ℝ) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
  atTop (𝓝 (f v))
Tactic: have A : Tendsto (fun (c : ℝ) ↦ ∫ w : V, (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
      atTop (𝓝 (f v)) := by
    apply tendsto_integral_comp_smul_smul_of_integrable'
    · exact fun x ↦ by positivity
    · rw [integral_const_mul, GaussianFourier.integral_rexp_neg_mul_sq_norm (by positivity)]
      nth_rewrite 2 [← pow_one π]
      rw [← rpow_natCast, ← rpow_natCast, ← rpow_sub pi_pos, ← rpow_mul pi_nonneg,
        ← rpow_add pi_pos]
      ring_nf
      exact rpow_zero _
    · 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
      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 : ℝ))
      rw [mul_zero] at B
      convert! B using 2 with x
      simp only [neg_mul, one_mul, Function.comp_apply, ← mul_assoc, ← rpow_natCast, φ]
      congr 1
      rw [mul_rpow (by positivity) (by positivity), ← rpow_mul pi_nonneg,
        ← rpow_mul (norm_nonneg _), ← mul_assoc, ← rpow_add pi_pos, mul_comm]
      congr <;> ring
    · exact hf
    · exact h'f
-- Lean 4 proof step from Mathlib.Analysis.Fourier.Inversion (hypothesis)
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 (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦ (c ^ finrank ℝ V * φ (c • (v - w))) • f w)
    atTop (𝓝 (f v))
⊢ Tendsto
    (fun (c : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
        (((↑π : ℂ) * (↑c : ℂ)) ^ HDiv.hDiv (α := ℂ) (↑(finrank ℝ V) : ℂ) 2 *
            cexp (-HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑c : ℂ) * HPow.hPow (β := ℕ) (↑‖v - w‖ : ℂ) 2)) •
          f w)
    atTop (𝓝 (f v))
have B : Tendsto
  (fun (c : ℝ) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (w : V) ↦
      ((c ^ (1 / 2)) ^ finrank ℝ V * φ (c ^ (1 / 2) • (v - w))) • f w)
  atTop (𝓝 (f v))
Tactic: have B : Tendsto
      (fun (c : ℝ) ↦
        ∫ w : V, ((c ^ (1 / 2 : ℝ)) ^ finrank ℝ V * φ ((c ^ (1 / 2 : ℝ)) • (v - w))) • f w)
      atTop (𝓝 (f v)) :=
    A.comp (tendsto_rpow_atTop (by simp))