From cfdbbffdc19320d6bf6c85b9b9c45a40122313b7 Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Sun, 19 Apr 2026 21:42:34 +0800 Subject: [PATCH 1/2] refactor: golf Gaussian/GaussianIntegral --- .../Gaussian/GaussianIntegral.lean | 33 ++++++++----------- 1 file changed, 13 insertions(+), 20 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean b/Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean index 9337e217183da0..36369ef668f727 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean @@ -288,27 +288,20 @@ theorem integral_gaussian_complex {b : ℂ} (hb : 0 < re b) : -- The Gaussian integral on the half-line, `∫ x in Ioi 0, exp (-b * x^2)`, for complex `b`. theorem integral_gaussian_complex_Ioi {b : ℂ} (hb : 0 < re b) : ∫ x : ℝ in Ioi 0, cexp (-b * (x : ℂ) ^ 2) = (π / b) ^ (1 / 2 : ℂ) / 2 := by + let f : ℝ → ℂ := fun x => cexp (-b * (x : ℂ) ^ 2) have full_integral := integral_gaussian_complex hb - have : MeasurableSet (Ioi (0 : ℝ)) := measurableSet_Ioi - rw [← integral_add_compl this (integrable_cexp_neg_mul_sq hb), compl_Ioi] at full_integral - suffices ∫ x : ℝ in Iic 0, cexp (-b * (x : ℂ) ^ 2) = ∫ x : ℝ in Ioi 0, cexp (-b * (x : ℂ) ^ 2) by - rw [this, ← mul_two] at full_integral - rwa [eq_div_iff]; exact two_ne_zero - have : ∀ c : ℝ, ∫ x in (0 : ℝ)..c, cexp (-b * (x : ℂ) ^ 2) = - ∫ x in -c..0, cexp (-b * (x : ℂ) ^ 2) := by - intro c - have := intervalIntegral.integral_comp_sub_left (a := 0) (b := c) - (fun x => cexp (-b * (x : ℂ) ^ 2)) 0 - simpa [zero_sub, neg_sq, neg_zero] using this - have t1 := - intervalIntegral_tendsto_integral_Ioi 0 (integrable_cexp_neg_mul_sq hb).integrableOn tendsto_id - have t2 : - Tendsto (fun c : ℝ => ∫ x : ℝ in (0 : ℝ)..c, cexp (-b * (x : ℂ) ^ 2)) atTop - (𝓝 (∫ x : ℝ in Iic 0, cexp (-b * (x : ℂ) ^ 2))) := by - simp_rw [this] - refine intervalIntegral_tendsto_integral_Iic _ ?_ tendsto_neg_atTop_atBot - apply (integrable_cexp_neg_mul_sq hb).integrableOn - exact tendsto_nhds_unique t2 t1 + have h_eq : ∫ x : ℝ in Iic 0, f x = ∫ x : ℝ in Ioi 0, f x := by + calc + ∫ x : ℝ in Iic 0, f x = ∫ x : ℝ in Ioi 0, f (-x) := by + simpa [f] using (integral_comp_neg_Ioi (c := 0) (f := f)).symm + _ = ∫ x : ℝ in Ioi 0, f x := by + refine setIntegral_congr_fun measurableSet_Ioi ?_ + intro x hx + simp [f] + have hmeas : MeasurableSet (Ioi (0 : ℝ)) := measurableSet_Ioi + rw [← integral_add_compl hmeas (integrable_cexp_neg_mul_sq hb), compl_Ioi, h_eq, ← mul_two] + at full_integral + exact (eq_div_iff two_ne_zero).2 (by simpa [mul_comm] using full_integral) -- The Gaussian integral on the half-line, `∫ x in Ioi 0, exp (-b * x^2)`, for real `b`. theorem integral_gaussian_Ioi (b : ℝ) : From 773b4783fdded381c7c40d5c7e163a2d4942fca2 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sun, 19 Apr 2026 21:56:11 +0800 Subject: [PATCH 2/2] golf --- .../SpecialFunctions/Gaussian/GaussianIntegral.lean | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean b/Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean index 36369ef668f727..f6241a1ac70946 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean @@ -292,16 +292,12 @@ theorem integral_gaussian_complex_Ioi {b : ℂ} (hb : 0 < re b) : have full_integral := integral_gaussian_complex hb have h_eq : ∫ x : ℝ in Iic 0, f x = ∫ x : ℝ in Ioi 0, f x := by calc - ∫ x : ℝ in Iic 0, f x = ∫ x : ℝ in Ioi 0, f (-x) := by - simpa [f] using (integral_comp_neg_Ioi (c := 0) (f := f)).symm - _ = ∫ x : ℝ in Ioi 0, f x := by - refine setIntegral_congr_fun measurableSet_Ioi ?_ - intro x hx - simp [f] + _ = ∫ x : ℝ in Ioi 0, f (-x) := by simp + _ = _ := setIntegral_congr_fun measurableSet_Ioi fun x hx ↦ by simp [f] have hmeas : MeasurableSet (Ioi (0 : ℝ)) := measurableSet_Ioi rw [← integral_add_compl hmeas (integrable_cexp_neg_mul_sq hb), compl_Ioi, h_eq, ← mul_two] at full_integral - exact (eq_div_iff two_ne_zero).2 (by simpa [mul_comm] using full_integral) + exact (eq_div_iff two_ne_zero).2 (by simpa using full_integral) -- The Gaussian integral on the half-line, `∫ x in Ioi 0, exp (-b * x^2)`, for real `b`. theorem integral_gaussian_Ioi (b : ℝ) :