theorem Frourio.norm_ofReal_exp_neg_mul_sq (a t : ℝ) : ‖↑(Real.exp (-(a * t ^ 2)))‖ = Real.exp (-(a * t ^ 2))

theorem Frourio.norm_cexp_neg_mul_sq (a t : ℝ) : ‖Complex.exp (-(↑a * ↑t ^ 2))‖ = Real.exp (-(a * t ^ 2))

theorem Frourio.exp_sq_eq (x : ℝ) : Real.exp x * Real.exp x = Real.exp (x + x)

theorem Frourio.exp_sq_pow_two (x : ℝ) : Real.exp x ^ 2 = Real.exp (2 * x)

theorem Frourio.memLp_two_iff_integrable_sq_complex (f : ℝ → ℂ) (hmeas : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) : MeasureTheory.MemLp f 2 MeasureTheory.volume ↔ MeasureTheory.Integrable (fun (t : ℝ) => ‖f t‖ ^ 2) MeasureTheory.volume

theorem Frourio.gaussian_memLp (a : ℝ) (ha : 0 < a) : MeasureTheory.MemLp (fun (t : ℝ) => Real.exp (-a * t ^ 2)) 2 MeasureTheory.volume

theorem Frourio.gaussian_memLpC_cexp (a : ℝ) (ha : 0 < a) : MeasureTheory.MemLp (fun (t : ℝ) => Complex.exp (-(↑a * ↑t ^ 2))) 2 MeasureTheory.volume

theorem Frourio.cexp_neg_mul_sq_ofReal (a t : ℝ) : Complex.exp (-(↑a * ↑t ^ 2)) = ↑(Real.exp (-(a * t ^ 2)))

theorem Frourio.gaussian_memLpC (a : ℝ) (ha : 0 < a) : MeasureTheory.MemLp (fun (t : ℝ) => ↑(Real.exp (-a * t ^ 2))) 2 MeasureTheory.volume

theorem Frourio.gaussian_integral_scaled (δ : ℝ) (hδ : 0 < δ) : ∫ (t : ℝ), Real.exp (-(2 * Real.pi) * t ^ 2 / δ ^ 2) = δ / √2

補題B: ガウスの L² ノルム計算に用いる積分評価。 ∫ ℝ exp(-2π t² / δ²) dt = δ / √2（δ>0）。

theorem Frourio.gaussian_l2_norm_sq_real (δ : ℝ) (hδ : 0 < δ) : ∫ (t : ℝ), Real.exp (-Real.pi * t ^ 2 / δ ^ 2) ^ 2 = δ / √2

実ガウス exp(-π t² / δ²) の L² ノルムの二乗は δ/√2（δ>0）。

theorem Frourio.gaussian_l2_norm_sq_complex (δ : ℝ) (hδ : 0 < δ) : ∫ (t : ℝ), ‖↑(Real.exp (-Real.pi * t ^ 2 / δ ^ 2))‖ ^ 2 = δ / √2

複素数値に持ち上げた実ガウスの L² ノルム二乗も同じ値。

正規化ガウス関数の構成

theorem Frourio.cexp_pi_delta_sq_eq (δ x : ℝ) : Complex.exp (-(↑Real.pi / ↑δ ^ 2 * ↑x ^ 2)) = ↑(Real.exp (-(Real.pi / δ ^ 2) * x ^ 2))

Helper lemma for complex exponential equality

theorem Frourio.gaussian_memLp_pi_delta_sq (δ : ℝ) (hδ : 0 < δ) : MeasureTheory.MemLp (fun (t : ℝ) => Complex.exp (-(↑Real.pi / ↑δ ^ 2 * ↑t ^ 2))) 2 MeasureTheory.volume

Helper lemma: Complex Gaussian exp(-(π/δ²) * t²) in L²

theorem Frourio.lintegral_norm_sq_eq_integral_norm_sq (f : ℝ → ℂ) (hmeas : MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume) (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) : ((∫⁻ (t : ℝ), ‖f t‖ₑ ^ 2) ^ (1 / 2)).toReal = √(∫ (t : ℝ), ‖f t‖ ^ 2)

Helper lemma: Convert L² norm from Lebesgue integral to regular integral form

theorem Frourio.build_normalized_gaussian (δ : ℝ) (hδ : 0 < δ) : ∃ (w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)), ‖w‖ = 1 ∧ ∀ᵐ (t : ℝ), ↑↑w t = ↑(2 ^ (1 / 4) / √δ) * ↑(Real.exp (-Real.pi * t ^ 2 / δ ^ 2))

正規化ガウス関数を L² 空間の要素として構成する。 δ > 0 に対して、exp(-π t²/δ²) を正規化して L² ノルム 1 の関数を得る。

theorem Frourio.normalized_gaussian_pointwise_bound (δ : ℝ) (hδ : 0 < δ) : ∃ (w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)), ‖w‖ = 1 ∧ ∀ᵐ (t : ℝ), ‖↑↑w t‖ ≤ 2 ^ (1 / 4) / √δ * Real.exp (-Real.pi * t ^ 2 / δ ^ 2)

補題2-3（包絡評価）: δ > 0 に対し，build_normalized_gaussian で得た 正規化ガウス w は a.e. で ‖w t‖ ≤ (2)^(1/4)/√δ · exp(-π t²/δ²) を満たす。

theorem Frourio.integral_const_mul_gaussian (c δ : ℝ) : ∫ (t : ℝ), c * Real.exp (-Real.pi * t ^ 2 / δ ^ 2) = c * ∫ (t : ℝ), Real.exp (-Real.pi * t ^ 2 / δ ^ 2)

Helper lemma for integral_const_mul application

theorem Frourio.gaussian_tail_integral_factor_out (R δ : ℝ) : ∫ (t : ℝ), Real.exp (-Real.pi * R ^ 2 / δ ^ 2) * Real.exp (-Real.pi * t ^ 2 / δ ^ 2) = Real.exp (-Real.pi * R ^ 2 / δ ^ 2) * ∫ (t : ℝ), Real.exp (-Real.pi * t ^ 2 / δ ^ 2)

Helper lemma for factoring out constant from integral

theorem Frourio.measurableSet_abs_gt (R : ℝ) : MeasurableSet {t : ℝ | R < |t|}

Helper lemma: The set {t : ℝ | R < |t|} is measurable

theorem Frourio.integrable_gaussian_product (δ : ℝ) (hδ : 0 < δ) (R : ℝ) : MeasureTheory.Integrable (fun (t : ℝ) => Real.exp (-Real.pi * R ^ 2 / δ ^ 2) * Real.exp (-Real.pi * t ^ 2 / δ ^ 2)) MeasureTheory.volume

theorem Frourio.tail_bound_calc_helper (δ R : ℝ) (hL : ∫ (t : ℝ) in {t : ℝ | R < |t|}, Real.exp (-2 * Real.pi * t ^ 2 / δ ^ 2) = ∫ (t : ℝ), {t : ℝ | R < |t|}.indicator (fun (t : ℝ) => Real.exp (-2 * Real.pi * t ^ 2 / δ ^ 2)) t) (h_int_le : ∫ (t : ℝ), {t : ℝ | R < |t|}.indicator (fun (t : ℝ) => Real.exp (-2 * Real.pi * t ^ 2 / δ ^ 2)) t ≤ ∫ (t : ℝ), Real.exp (-Real.pi * R ^ 2 / δ ^ 2) * Real.exp (-Real.pi * t ^ 2 / δ ^ 2)) : ∫ (t : ℝ) in {t : ℝ | R < |t|}, Real.exp (-2 * Real.pi * t ^ 2 / δ ^ 2) ≤ ∫ (t : ℝ), Real.exp (-Real.pi * R ^ 2 / δ ^ 2) * Real.exp (-Real.pi * t ^ 2 / δ ^ 2)

Helper lemma for the tail bound calculation

theorem Frourio.gaussian_exp_square_split (a t : ℝ) : Real.exp (-2 * a * t ^ 2) = Real.exp (-a * t ^ 2) * Real.exp (-a * t ^ 2)

theorem Frourio.gaussian_tail_exp_monotonicity (δ R t : ℝ) (hδ : 0 < δ) (hR_pos : 0 ≤ R) (hR : R ≤ |t|) : -Real.pi * t ^ 2 / δ ^ 2 ≤ -Real.pi * R ^ 2 / δ ^ 2

theorem Frourio.gaussian_tail_pointwise_bound (δ R t : ℝ) (hδ : 0 < δ) (hR : 0 < R) (hmem : R < |t|) : Real.exp (-2 * Real.pi * t ^ 2 / δ ^ 2) ≤ Real.exp (-Real.pi * R ^ 2 / δ ^ 2) * Real.exp (-Real.pi * t ^ 2 / δ ^ 2)

theorem Frourio.gaussian_product_nonneg (δ R t : ℝ) : 0 ≤ Real.exp (-Real.pi * R ^ 2 / δ ^ 2) * Real.exp (-Real.pi * t ^ 2 / δ ^ 2)

theorem Frourio.integral_mono_of_pointwise_le_indicator {f g : ℝ → ℝ} {S : Set ℝ} (hf_nonneg : ∀ (t : ℝ), 0 ≤ S.indicator f t) (hg_int : MeasureTheory.Integrable g MeasureTheory.volume) (hle : ∀ (t : ℝ), S.indicator f t ≤ g t) : ∫ (t : ℝ), S.indicator f t ≤ ∫ (t : ℝ), g t

theorem Frourio.gaussian_integral_value (δ : ℝ) (hδ : 0 < δ) : ∫ (t : ℝ), Real.exp (-Real.pi * t ^ 2 / δ ^ 2) = δ

theorem Frourio.gaussian_tail_l2_bound (δ : ℝ) (hδ : 0 < δ) (R : ℝ) (hR : 0 < R) : ∫ (t : ℝ) in {t : ℝ | R < |t|}, Real.exp (-2 * Real.pi * t ^ 2 / δ ^ 2) ≤ 2 * Real.exp (-Real.pi * R ^ 2 / δ ^ 2) / √(Real.pi / δ ^ 2)

Gaussian tail bound: The L² norm of a Gaussian outside radius R decays exponentially

theorem Frourio.gaussian_normalization_factor_squared (δ : ℝ) (hδ : 0 < δ) : (2 ^ (1 / 4) / √δ) ^ 2 = √2 / δ

theorem Frourio.exp_squared_formula (t δ : ℝ) : Real.exp (-Real.pi * t ^ 2 / δ ^ 2) ^ 2 = Real.exp (-2 * Real.pi * t ^ 2 / δ ^ 2)

theorem Frourio.integrable_indicator_gaussian (δ : ℝ) (hδ : 0 < δ) (R A : ℝ) : MeasureTheory.Integrable (fun (t : ℝ) => {t : ℝ | R < |t|}.indicator (fun (t : ℝ) => A ^ 2 * Real.exp (-2 * Real.pi * t ^ 2 / δ ^ 2)) t) MeasureTheory.volume

theorem Frourio.integral_indicator_const_mul (S : Set ℝ) (c : ℝ) (f : ℝ → ℝ) : ∫ (t : ℝ), S.indicator (fun (t : ℝ) => c * f t) t = c * ∫ (t : ℝ), S.indicator f t

theorem Frourio.two_le_four_pi : 2 ≤ 4 * Real.pi

π is greater than 1/2, so 4π > 2

theorem Frourio.pi_lt_four : Real.pi < 4

π is less than 4 - re-export from Mathlib

theorem Frourio.normalized_gaussian_tail_vanishes (δ : ℝ) (hδ : 0 < δ) (R : ℝ) (hR : 0 < R) : ∃ (w : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)), ‖w‖ = 1 ∧ ∫ (t : ℝ) in {t : ℝ | R < |t|}, ‖↑↑w t‖ ^ 2 ≤ 4 * Real.exp (-Real.pi * R ^ 2 / δ ^ 2)

For normalized Gaussian with width δ, the L² mass outside radius R vanishes as δ → 0

theorem Frourio.sqrt_two_pi_lt_three : √(2 * Real.pi) < 3

theorem Frourio.sqrt_div_sqrt_pi : √(2 * Real.pi) / √Real.pi = √2

theorem Frourio.rpow_half_eq_quarter_sq (x : ℝ) (hx : 0 ≤ x) : x ^ (1 / 2) = x ^ (1 / 4) * x ^ (1 / 4)

theorem Frourio.nat_split_sqrt (n : ℕ) (hn : 0 < ↑n) : ↑n = ↑n ^ (1 / 2) * ↑n ^ (1 / 2)

theorem Frourio.gaussian_const_squared (n : ℕ) (hn : 0 < ↑n + 1) : (2 ^ (1 / 4) * √(↑n + 1)) ^ 2 = 2 ^ (1 / 2) * (↑n + 1)

theorem Frourio.pi_quarter_div_squared (n : ℕ) : ((↑n + 1) / Real.pi ^ (1 / 4)) ^ 2 = (↑n + 1) * (↑n + 1) / Real.pi ^ (1 / 2)

theorem Frourio.gaussian_norm_const_le_alt_const_for_large_n (n : ℕ) (hn : 2 ≤ n) : 2 ^ (1 / 4) / √(1 / (↑n + 1)) ≤ (1 / (↑n + 1) * Real.pi ^ (1 / 4))⁻¹

大きな n に対する正規化定数の比較補題。 δ n = 1/(n+1) のとき，n ≥ 2 なら 2^(1/4)/√(δ n) ≤ (δ n · π^(1/4))⁻¹ が成り立つ。