theorem Frourio.gaussian_shifted_norm_bound (a c : ℂ) (x : ℝ) : ‖Complex.exp (-a * (↑x + c) ^ 2)‖ ≤ Real.exp (-a.re * (x + c.re) ^ 2 + a.re * c.im ^ 2 + |2 * a.im * c.im * (x + c.re)|)

Bound for the norm of complex Gaussian with shifted argument

theorem Frourio.gaussian_shifted_bound_integrable (a : ℂ) (ha : 0 < a.re) (c : ℂ) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (-a.re * (x + c.re) ^ 2 + a.re * c.im ^ 2)) MeasureTheory.volume

Integrability of the shifted Gaussian bound function

theorem Frourio.gaussian_norm_real (a : ℂ) : 0 < a.re → ∀ (x : ℝ), ‖Complex.exp (-a * ↑x ^ 2)‖ = Real.exp (-a.re * x ^ 2)

Norm of complex Gaussian with real argument

theorem Frourio.young_inequality_for_products (a b c ε : ℝ) (hε : 0 < ε) : |2 * a * b * c| ≤ ε / 2 * c ^ 2 + 2 * (a * b) ^ 2 / ε

Young's inequality for products: For any real numbers a, b and ε > 0, we have |2 * a * b * c| ≤ ε/2 * c^2 + 2 * |a * b|^2 / ε

theorem Frourio.gaussian_shifted_integrable (a : ℂ) (ha : 0 < a.re) (c : ℂ) : MeasureTheory.Integrable (fun (x : ℝ) => Complex.exp (-a * (↑x + c) ^ 2)) MeasureTheory.volume

Integrability of the complex Gaussian with shifted argument

theorem Frourio.gaussian_integrable_real (a : ℂ) (ha : 0 < a.re) : MeasureTheory.Integrable (fun (x : ℝ) => Real.exp (-a.re * x ^ 2)) MeasureTheory.volume

Integrability of real Gaussian function

theorem Frourio.gaussian_integrable_complex (a : ℂ) (ha : 0 < a.re) : MeasureTheory.Integrable (fun (x : ℝ) => Complex.exp (-a * ↑x ^ 2)) MeasureTheory.volume

Integrability of complex Gaussian function

theorem Frourio.gaussian_rectangular_contour (a : ℂ) (_ha : 0 < a.re) (y R : ℝ) (_hR : 0 < R) : let f := fun (z : ℂ) => Complex.exp (-a * z ^ 2); (((∫ (x : ℝ) in -R..R, f ↑x) - ∫ (x : ℝ) in -R..R, f (↑x + ↑y * Complex.I)) + ∫ (t : ℝ) in 0 ..y, f (↑R + ↑t * Complex.I) * Complex.I) - ∫ (t : ℝ) in 0 ..y, f (-↑R + ↑t * Complex.I) * Complex.I = 0

Cauchy's theorem for rectangular contour with Gaussian

theorem Frourio.R_positive_from_bound (a : ℂ) (ha : 0 < a.re) (sign : ℝ) (hsign : sign ≠ 0) (b R : ℝ) (hb : b < 0) (hR : R ≥ 2 * √(-b * 4 / a.re) / |sign|) : 0 < R

Helper lemma: R is positive when it's bounded below by a specific expression

theorem Frourio.sq_exceeds_threshold (a_re : ℝ) (ha : 0 < a_re) (sign : ℝ) (hsign : sign ≠ 0) (b R : ℝ) (hb : b < 0) (hR : R ≥ 2 * √(-b * 4 / a_re) / |sign|) : (sign * R) ^ 2 > -4 * b / a_re

Helper lemma: For R large enough, (sign * R)^2 exceeds the threshold

theorem Frourio.gaussian_bound_rearrange (a_re : ℝ) (ha : 0 < a_re) (b x : ℝ) (hx : x ^ 2 > -4 * b / a_re) : -(a_re * x ^ 2 / 4) < b

Helper lemma: Rearranging inequality for Gaussian bound

theorem Frourio.gaussian_exp_decay (a : ℂ) (ha : 0 < a.re) (sign : ℝ) (hsign : sign ≠ 0) : Filter.Tendsto (fun (R : ℝ) => Real.exp (-(a.re * (sign * R) ^ 2 / 4))) Filter.atTop (nhds 0)

Helper lemma: exponential decay for Gaussian-like functions

theorem Frourio.sqrt_mul_of_nonneg {x y : ℝ} (hx : 0 ≤ x) : √(x * y) = √x * √y

Helper lemma: sqrt of product equals product of sqrts for non-negative reals

theorem Frourio.complex_norm_eq_sqrt (z : ℂ) : ‖z‖ = √(z.re ^ 2 + z.im ^ 2)

Helper lemma: Complex norm equals sqrt of sum of squares

theorem Frourio.neg_real_to_complex_eq_neg_mul (R : ℝ) : -↑R = ↑(-1) * ↑R

Helper lemma: negative real to complex conversion

theorem Frourio.complex_neg_R_plus_tc_eq (R t : ℝ) (c : ℂ) : -↑R + ↑t * c = ↑(-1) * ↑R + ↑t * c

Helper lemma: equality of complex expressions with negative R

theorem Frourio.gaussian_integrand_neg_R_eq (a c : ℂ) (R t : ℝ) : Complex.exp (-a * (-↑R + ↑t * c) ^ 2) * c = Complex.exp (-a * (↑(-1) * ↑R + ↑t * c) ^ 2) * c

Helper lemma: Gaussian integrand equality for negative R

theorem Frourio.gaussian_left_vertical_eq (a c : ℂ) (R : ℝ) : ∫ (t : ℝ) in 0 ..1, Complex.exp (-a * (-↑R + ↑t * c) ^ 2) * c = ∫ (t : ℝ) in 0 ..1, Complex.exp (-a * (↑(-1) * ↑R + ↑t * c) ^ 2) * c

Helper lemma: left vertical integral equals the general form

theorem Frourio.gaussian_horizontal_conv_shifted (a : ℂ) (ha : 0 < a.re) (c : ℂ) : let f := fun (z : ℂ) => Complex.exp (-a * z ^ 2); Filter.Tendsto (fun (R : ℝ) => ∫ (x : ℝ) in -R..R, f (↑x + c)) Filter.atTop (nhds (∫ (x : ℝ), f (↑x + c)))

Convergence of horizontal shifted integral to improper integral

theorem Frourio.gaussian_horizontal_conv_real (a : ℂ) (ha : 0 < a.re) : let f := fun (z : ℂ) => Complex.exp (-a * z ^ 2); Filter.Tendsto (fun (R : ℝ) => ∫ (x : ℝ) in -R..R, f ↑x) Filter.atTop (nhds (∫ (x : ℝ), f ↑x))

Convergence of horizontal real integral to improper integral

theorem Frourio.gaussian_vertical_norm_eq_aux (a : ℂ) (R t : ℝ) (right : Bool) (hz_mul : -a * ((if right = true then ↑R else -↑R) + ↑t * Complex.I) ^ 2 = -a * (↑((if right = true then 1 else -1) * R) + ↑t * Complex.I) ^ 2) : ‖Complex.exp (-a * ((if right = true then ↑R else -↑R) + ↑t * Complex.I) ^ 2)‖ = Real.exp (-a * (↑((if right = true then 1 else -1) * R) + ↑t * Complex.I) ^ 2).re

Helper lemma: Exponential bound for Gaussian on vertical lines

theorem Frourio.gaussian_vertical_norm_eq (a : ℂ) (R t : ℝ) (right : Bool) : ‖Complex.exp (-a * ((if right = true then ↑R else -↑R) + ↑t * Complex.I) ^ 2)‖ = Real.exp (-a * (↑((if right = true then 1 else -1) * R) + ↑t * Complex.I) ^ 2).re

theorem Frourio.gaussian_vertical_exponential_bound (a : ℂ) (ha : 0 < a.re) (y : ℝ) (right : Bool) : ∃ C > 0, ∀ R > 0, ∀ t ∈ Set.Icc 0 y, ‖Complex.exp (-a * ((if right = true then ↑R else -↑R) + ↑t * Complex.I) ^ 2)‖ ≤ C * Real.exp (-a.re * R ^ 2 + a.re * y ^ 2 + 2 * |a.im| * R * |y|)

theorem Frourio.gaussian_vertical_integral_norm_estimate (a : ℂ) (ha : 0 < a.re) (ha_im : a.im = 0) (y : ℝ) (hy : 0 ≤ y) (right : Bool) (C₁ : ℝ) (hC₁_pos : 0 < C₁) (hC₁_bound : ∀ R > 0, ∀ t ∈ Set.Icc 0 y, ‖Complex.exp (-a * ((if right = true then ↑R else -↑R) + ↑t * Complex.I) ^ 2)‖ ≤ C₁ * Real.exp (-a.re * R ^ 2 + a.re * y ^ 2)) (R : ℝ) : R > 1 → ‖∫ (t : ℝ) in 0 ..y, Complex.exp (-a * ((if right = true then ↑R else -↑R) + ↑t * Complex.I) ^ 2) * Complex.I‖ ≤ |y| * C₁ * Real.exp (-a.re * R ^ 2 + a.re * y ^ 2)

Helper lemma: Integral norm estimate using exponential bound

theorem Frourio.exp_comparison_large_R (a : ℂ) (ha : 0 < a.re) (y R : ℝ) (hR : R > 1) : Real.exp (-a.re * R ^ 2 + a.re * y ^ 2) ≤ Real.exp (2 * a.re * y ^ 2) * Real.exp (-a.re * R ^ 2 / 2)

Helper lemma: Exponential comparison for large R

theorem Frourio.gaussian_vertical_integral_bound (a : ℂ) (ha : 0 < a.re) (ha_im : a.im = 0) (y : ℝ) (hy : 0 ≤ y) (right : Bool) : ∃ C > 0, ∀ R > 1, ‖∫ (t : ℝ) in 0 ..y, Complex.exp (-a * ((if right = true then ↑R else -↑R) + ↑t * Complex.I) ^ 2) * Complex.I‖ ≤ C * Real.exp (-a.re * R ^ 2 / 2)

Helper lemma: Bound for the vertical integral of Gaussian

theorem Frourio.exp_neg_quadratic_tendsto_zero (c : ℝ) (hc : 0 < c) : Filter.Tendsto (fun (R : ℝ) => Real.exp (-c * R ^ 2 / 2)) Filter.atTop (nhds 0)

Helper lemma: Exponential decay exp(-cx²) → 0 as x → ∞ for c > 0

inductive Frourio.IntegralBoundType : Type

Type for different integral bound conditions

• at_one : IntegralBoundType
• interval : IntegralBoundType
• negative : IntegralBoundType

theorem Frourio.gaussian_vertical_integral_bounded_unified (a : ℂ) (ha : 0 < a.re) (y : ℝ) (right : Bool) (R : ℝ) (bound_type : IntegralBoundType) (h_cond : match bound_type with | IntegralBoundType.at_one => R = 1 | IntegralBoundType.interval => 0 ≤ R ∧ R ≤ 1 | IntegralBoundType.negative => R < 0 ∧ R ≤ 1) : ∃ M > 0, ‖∫ (t : ℝ) in 0 ..y, Complex.exp (-a * ((if right = true then ↑R else -↑R) + ↑t * Complex.I) ^ 2) * Complex.I‖ ≤ M

Unified helper lemma: Vertical integral bounds for various R conditions

theorem Frourio.gaussian_vertical_integral_bounded_with_C (a : ℂ) (_ha : 0 < a.re) (y : ℝ) (right : Bool) (R C : ℝ) (_hC_pos : 0 < C) (hC_bound : ∀ R' > 1, ‖∫ (t : ℝ) in 0 ..y, Complex.exp (-a * ((if right = true then ↑R' else -↑R') + ↑t * Complex.I) ^ 2) * Complex.I‖ ≤ C * Real.exp (-a.re * R' ^ 2 / 2)) (hR : R = 1) : ‖∫ (t : ℝ) in 0 ..y, Complex.exp (-a * ((if right = true then ↑R else -↑R) + ↑t * Complex.I) ^ 2) * Complex.I‖ ≤ C * Real.exp (-a.re * R ^ 2 / 2)

Unified helper lemma with C bound: For R = 1 with given C

theorem Frourio.gaussian_vertical_integral_at_one (a : ℂ) (ha : 0 < a.re) (y : ℝ) (right : Bool) (C : ℝ) (hC_pos : 0 < C) (hC_bound : ∀ R > 1, ‖∫ (t : ℝ) in 0 ..y, Complex.exp (-a * ((if right = true then ↑R else -↑R) + ↑t * Complex.I) ^ 2) * Complex.I‖ ≤ C * Real.exp (-a.re * R ^ 2 / 2)) : ‖∫ (t : ℝ) in 0 ..y, Complex.exp (-a * ((if right = true then 1 else -1) + ↑t * Complex.I) ^ 2) * Complex.I‖ ≤ C * Real.exp (-a.re / 2)

Helper lemma: Vertical integral bound at R = 1

inductive Frourio.SqLeOneCondition : Type

Type for different conditions on R that imply R² ≤ 1

• nonneg_le : SqLeOneCondition
• abs_le : SqLeOneCondition
• neg_le : SqLeOneCondition

theorem Frourio.sq_le_one_unified (R : ℝ) (cond : SqLeOneCondition) (h : match cond with | SqLeOneCondition.nonneg_le => 0 ≤ R ∧ R ≤ 1 | SqLeOneCondition.abs_le => |R| ≤ 1 | SqLeOneCondition.neg_le => R < 0 ∧ R ≤ 1 ∧ -1 ≤ R) : R ^ 2 ≤ 1

Unified lemma: Various conditions that imply R² ≤ 1

theorem Frourio.sq_le_one_of_le_one (R : ℝ) (hR : R ≤ 1) (hR_nonneg : 0 ≤ R) : R ^ 2 ≤ 1

Helper lemma: If R ≤ 1 and R ≥ 0, then R² ≤ 1

theorem Frourio.sq_le_one_of_abs_le_one (R : ℝ) (hR : |R| ≤ 1) : R ^ 2 ≤ 1

Helper lemma: If |R| ≤ 1, then R² ≤ 1

theorem Frourio.sq_le_one_of_neg_le_one (R : ℝ) (hR_neg : R < 0) (hR_le : R ≤ 1) (hR_ge : -1 ≤ R) : R ^ 2 ≤ 1

Helper lemma: If R < 0 and -1 ≤ R ≤ 1, then R² ≤ 1

theorem Frourio.gaussian_vertical_integral_bounded_on_interval (a : ℂ) (ha : 0 < a.re) (y : ℝ) (right : Bool) (R : ℝ) (hR_le : R ≤ 1) (hR_ge : 0 ≤ R) : ∃ M > 0, ‖∫ (t : ℝ) in 0 ..y, Complex.exp (-a * ((if right = true then ↑R else -↑R) + ↑t * Complex.I) ^ 2) * Complex.I‖ ≤ M

Helper lemma: The vertical integral is bounded for R ∈ [0,1]

theorem Frourio.gaussian_vertical_integral_bounded_negative (a : ℂ) (ha : 0 < a.re) (y : ℝ) (right : Bool) (R : ℝ) (hR_neg : R < 0) (hR_le : R ≤ 1) : ∃ M > 0, ‖∫ (t : ℝ) in 0 ..y, Complex.exp (-a * ((if right = true then ↑R else -↑R) + ↑t * Complex.I) ^ 2) * Complex.I‖ ≤ M

Helper lemma: The vertical integral is bounded for negative R with R ≤ 1

theorem Frourio.gaussian_vertical_integral_continuous (a : ℂ) (y : ℝ) (right : Bool) : ContinuousOn (fun (R : ℝ) => ‖∫ (t : ℝ) in 0 ..y, Complex.exp (-a * ((if right = true then ↑R else -↑R) + ↑t * Complex.I) ^ 2) * Complex.I‖) (Set.Icc 0 1)

Helper lemma: Gaussian vertical integral is continuous in R

theorem Frourio.continuous_on_compact_attains_max {α : Type u_1} [TopologicalSpace α] [CompactSpace α] {f : α → ℝ} (hf : Continuous f) (S : Set α) (hS_compact : IsCompact S) (hS_nonempty : S.Nonempty) : ∃ x₀ ∈ S, ∀ x ∈ S, f x ≤ f x₀

Helper lemma: Continuous function on compact set attains maximum

theorem Frourio.gaussian_vertical_integral_max_exists (a : ℂ) (y : ℝ) (right : Bool) : ∃ R_max ∈ Set.Icc 0 1, ∀ R ∈ Set.Icc 0 1, ‖∫ (t : ℝ) in 0 ..y, Complex.exp (-a * ((if right = true then ↑R else -↑R) + ↑t * Complex.I) ^ 2) * Complex.I‖ ≤ ‖∫ (t : ℝ) in 0 ..y, Complex.exp (-a * ((if right = true then ↑R_max else -↑R_max) + ↑t * Complex.I) ^ 2) * Complex.I‖

Helper lemma: Maximum of gaussian vertical integral on [0,1] exists

theorem Frourio.integral_bound_on_interval (a : ℂ) (y : ℝ) (right : Bool) (M : ℝ) (hM_is_max : ∃ R₀ ∈ Set.Icc 0 1, ‖∫ (t : ℝ) in 0 ..y, Complex.exp (-a * ((if right = true then ↑R₀ else -↑R₀) + ↑t * Complex.I) ^ 2) * Complex.I‖ = M ∧ ∀ R ∈ Set.Icc 0 1, ‖∫ (t : ℝ) in 0 ..y, Complex.exp (-a * ((if right = true then ↑R else -↑R) + ↑t * Complex.I) ^ 2) * Complex.I‖ ≤ M) (R : ℝ) : R ∈ Set.Icc 0 1 → ‖∫ (t : ℝ) in 0 ..y, Complex.exp (-a * ((if right = true then ↑R else -↑R) + ↑t * Complex.I) ^ 2) * Complex.I‖ ≤ M

Helper lemma: If M is the maximum of the integral on [0,1], it bounds all values

theorem Frourio.abs_le_one_of_in_interval (R : ℝ) (hR_lower : -1 ≤ R) (hR_upper : R ≤ 1) : |R| ≤ 1

Helper lemma: For R ∈ [0, 1] we have |R| ≤ 1, even when considering negative extensions

theorem Frourio.exp_ge_one_of_R_sq_le_one (a : ℂ) (ha : 0 < a.re) (R : ℝ) (h_R_sq : R ^ 2 ≤ 1) : 1 ≤ Real.exp (a.re / 2 - a.re * R ^ 2 / 2)

Helper lemma: For 0 ≤ R^2 ≤ 1 and a.re > 0, we have exp(a.re/2 - a.re*R^2/2) ≥ 1

theorem Frourio.small_bound_le_C_small_exp (a : ℂ) (ha : 0 < a.re) (R : ℝ) (h_R_sq : R ^ 2 ≤ 1) (M_small : ℝ) (hM_small_nonneg : 0 ≤ M_small) : M_small + 1 ≤ (M_small + 1) * Real.exp (a.re / 2) * Real.exp (-a.re * R ^ 2 / 2)

Helper lemma: Shows M_small + 1 ≤ C_small * exp(-a.re * R^2 / 2) when R^2 ≤ 1

theorem Frourio.gaussian_vertical_integral_bounded_all (a : ℂ) (ha : 0 < a.re) (ha_im : a.im = 0) (y : ℝ) (hy : 0 ≤ y) (right : Bool) : ∃ C > 0, ∀ (R : ℝ), ‖∫ (t : ℝ) in 0 ..y, Complex.exp (-a * ((if right = true then ↑R else -↑R) + ↑t * Complex.I) ^ 2) * Complex.I‖ ≤ C * Real.exp (-a.re * R ^ 2 / 2)

Helper lemma: The C from gaussian_vertical_integral_bound works for all R

theorem Frourio.gaussian_vertical_integral_vanish_aux (a : ℂ) (ha : 0 < a.re) (ha_im : a.im = 0) (y : ℝ) (hy : 0 ≤ y) (right : Bool) : Filter.Tendsto (fun (R : ℝ) => ∫ (t : ℝ) in 0 ..y, Complex.exp (-a * ((if right = true then ↑R else -↑R) + ↑t * Complex.I) ^ 2) * Complex.I) Filter.atTop (nhds 0)

Helper lemma: A single vertical integral of Gaussian vanishes as R → ∞ If right = true, it's the right vertical integral (at x = R). If right = false, it's the left vertical integral (at x = -R).

theorem Frourio.gaussian_vertical_integrals_vanish (a : ℂ) (ha : 0 < a.re) (ha_im : a.im = 0) (y : ℝ) (hy : 0 ≤ y) : let f := fun (z : ℂ) => Complex.exp (-a * z ^ 2); Filter.Tendsto (fun (R : ℝ) => (∫ (t : ℝ) in 0 ..y, f (↑R + ↑t * Complex.I) * Complex.I) - ∫ (t : ℝ) in 0 ..y, f (-↑R + ↑t * Complex.I) * Complex.I) Filter.atTop (nhds 0)

Vertical integrals of Gaussian vanish as R → ∞

theorem Frourio.gaussian_integral_diff_limit (a : ℂ) (y : ℝ) : let f := fun (z : ℂ) => Complex.exp (-a * z ^ 2); Filter.Tendsto (fun (R : ℝ) => ∫ (x : ℝ) in -R..R, f ↑x) Filter.atTop (nhds (∫ (x : ℝ), f ↑x)) → Filter.Tendsto (fun (R : ℝ) => ∫ (x : ℝ) in -R..R, f (↑x + ↑y * Complex.I)) Filter.atTop (nhds (∫ (x : ℝ), f (↑x + ↑y * Complex.I))) → (∀ R > 0, (∫ (x : ℝ) in -R..R, f ↑x) - ∫ (x : ℝ) in -R..R, f (↑x + ↑y * Complex.I) = -((∫ (t : ℝ) in 0 ..y, f (↑R + ↑t * Complex.I) * Complex.I) - ∫ (t : ℝ) in 0 ..y, f (-↑R + ↑t * Complex.I) * Complex.I)) → Filter.Tendsto (fun (R : ℝ) => (∫ (t : ℝ) in 0 ..y, f (↑R + ↑t * Complex.I) * Complex.I) - ∫ (t : ℝ) in 0 ..y, f (-↑R + ↑t * Complex.I) * Complex.I) Filter.atTop (nhds 0) → (∫ (x : ℝ), f ↑x) - ∫ (x : ℝ), f (↑x + ↑y * Complex.I) = 0

Limit of difference of integrals using rectangular contour

theorem Frourio.gaussian_contour_shift_general {a : ℂ} (ha : 0 < a.re) (ha_im : a.im = 0) (c : ℂ) (hc : c.re = 0) (hc_im : 0 ≤ c.im) : ∫ (x : ℝ), Complex.exp (-a * (↑x + c) ^ 2) = ∫ (x : ℝ), Complex.exp (-a * ↑x ^ 2)

Special case: Gaussian contour shift. The integral of a Gaussian function exp(-a(z+c)²) over a horizontal line equals the integral over the real axis.

theorem Frourio.pi_div_delta_sq_re_pos {δ : ℝ} (hδ : 0 < δ) : 0 < (↑Real.pi / ↑δ ^ 2).re

Helper lemma: Real part of π/δ² is positive when δ > 0

theorem Frourio.pi_div_delta_sq_im_zero (δ : ℝ) : (↑Real.pi / ↑δ ^ 2).im = 0

Helper lemma: Imaginary part of π/δ² is zero

theorem Frourio.i_delta_sq_xi_re_zero (δ ξ : ℝ) : (Complex.I * ↑(δ ^ 2) * ↑ξ).re = 0

Helper lemma: Real part of Iδ²ξ is zero

theorem Frourio.i_delta_sq_xi_im (δ ξ : ℝ) : (Complex.I * ↑(δ ^ 2) * ↑ξ).im = δ ^ 2 * ξ

Helper lemma: Imaginary part of Iδ²ξ equals δ²*ξ

theorem Frourio.gaussian_integrable_basic (a : ℂ) (ha : 0 < a.re) (c : ℂ) : MeasureTheory.Integrable (fun (x : ℝ) => Complex.exp (-a * (↑x + c) ^ 2)) MeasureTheory.volume

Helper lemma: Gaussian functions are integrable

def Frourio.neg_homeomorph : ℝ ≃ₜ ℝ

Standard negation homeomorphism on ℝ

Equations

• One or more equations did not get rendered due to their size.

theorem Frourio.neg_homeomorph_measure_preserving : MeasureTheory.MeasurePreserving neg_homeomorph.toFun MeasureTheory.volume MeasureTheory.volume

Helper lemma: The standard negation homeomorphism preserves Lebesgue measure

theorem Frourio.integral_gaussian_neg_substitution (a c : ℂ) : ∫ (x : ℝ), Complex.exp (-a * (↑x + c) ^ 2) = ∫ (x : ℝ), Complex.exp (-a * (↑(-x) + c) ^ 2)

theorem Frourio.gaussian_shift_transform (a_param c_param : ℂ) (h_subst_left : ∫ (a : ℝ), Complex.exp (-a_param * (↑a + c_param) ^ 2) = ∫ (u : ℝ), Complex.exp (-a_param * (↑(-u) + c_param) ^ 2)) (h_simplified : ∫ (u : ℝ), Complex.exp (-a_param * (↑(-u) + c_param) ^ 2) = ∫ (u : ℝ), Complex.exp (-a_param * (↑u - c_param) ^ 2)) (h_expand : ∫ (u : ℝ), Complex.exp (-a_param * (↑u - c_param) ^ 2) = ∫ (u : ℝ), Complex.exp (-a_param * (↑u ^ 2 - 2 * ↑u * c_param + c_param ^ 2))) (h_general : ∫ (u : ℝ), Complex.exp (-a_param * (↑u + -c_param) ^ 2) = ∫ (s : ℝ), Complex.exp (-a_param * ↑s ^ 2)) : ∫ (a : ℝ), Complex.exp (-a_param * (↑a + c_param) ^ 2) = ∫ (s : ℝ), Complex.exp (-a_param * ↑s ^ 2)

Helper lemma: Transform integral with shift to standard form

theorem Frourio.gaussian_parametric_to_original (δ ξ : ℝ) (a_param c_param : ℂ) (h_a_def : a_param = ↑Real.pi / ↑δ ^ 2) (h_c_def : c_param = Complex.I * ↑δ ^ 2 * ↑ξ) : ∫ (a : ℝ), Complex.exp (-a_param * (↑a + c_param) ^ 2) = ∫ (s : ℝ), Complex.exp (-a_param * ↑s ^ 2) ↔ ∫ (a : ℝ), Complex.exp (-↑Real.pi / ↑δ ^ 2 * (↑a + Complex.I * ↑δ ^ 2 * ↑ξ) ^ 2) = ∫ (s : ℝ), Complex.exp (-↑Real.pi / ↑δ ^ 2 * ↑s ^ 2)

Helper lemma: Connect parametric form to original form

theorem Frourio.gaussian_shift_neg_case (δ ξ : ℝ) (hδ : 0 < δ) (hξ : ξ < 0) : ∫ (a : ℝ), Complex.exp (-↑Real.pi / ↑δ ^ 2 * (↑a + Complex.I * ↑δ ^ 2 * ↑ξ) ^ 2) = ∫ (s : ℝ), Complex.exp (-↑Real.pi / ↑δ ^ 2 * ↑s ^ 2)

Helper lemma for handling the case when c.im < 0 in gaussian_contour_shift. This lemma directly provides the needed equality with the correct variable names.

theorem Frourio.gaussian_contour_shift_real {δ : ℝ} (hδ : 0 < δ) (ξ : ℝ) : ∫ (a : ℝ), Complex.exp (-↑Real.pi / ↑δ ^ 2 * (↑a + Complex.I * ↑δ ^ 2 * ↑ξ) ^ 2) = ∫ (s : ℝ), Complex.exp (-↑Real.pi / ↑δ ^ 2 * ↑s ^ 2)

Specific version for our use case with real parameters. This is the version needed for the Gaussian Fourier transform proof.