theorem ne_zero_of_re_neg {s : ℂ} (hs : 0 > s.re) : s ≠ 0

theorem φ_grossBound (s t x : ℝ) (h : x ≥ -max s t) [PosReal s] [PosReal t] : ↑(φ s t x) ≤ Real.exp (Real.log 2 / min s t * x) * Real.exp (Real.log 2 / min s t * max s t)

noncomputable def smStep (μ x : ℝ) : ℝ

Equations

• smStep μ x = if x ≤ 0 then 0 else if x ≤ μ then x / μ else 1

theorem smStepContinuous (μ : ℝ) [PosReal μ] : Continuous (smStep μ)

theorem smStepLe1 (μ x : ℝ) [PosReal μ] : smStep μ x ≤ 1

theorem smStepNonneg (μ x : ℝ) [PosReal μ] : 0 ≤ smStep μ x

noncomputable def φReg (s t μ σ x : ℝ) : ℝ

Equations

• φReg s t μ σ x = Real.exp (-σ * x) * ((Set.Ici 0).indicator (fun (x : ℝ) => 1) x + ∑' (pq : ℕ × ℕ), ↑(Jₚ pq) * smStep μ (x - (↑pq.1 * s + ↑pq.2 * t)))

theorem φRegLe (s t μ σ x : ℝ) [PosReal s] [PosReal t] [PosReal μ] : φReg s t μ σ x ≤ Real.exp (-σ * x) * ↑(φ s t x)

theorem φReg_neg (s t μ σ x : ℝ) (h : x < 0) [PosReal s] [PosReal t] : φReg s t μ σ x = 0

theorem φRegBound (s t μ σ x : ℝ) [PosReal s] [PosReal t] [PosReal μ] : φReg s t μ σ x ≤ Real.exp ((Real.log 2 / min s t - σ) * x) * Real.exp (Real.log 2 / min s t * max s t)

theorem φRegNonneg (s t μ σ x : ℝ) [PosReal s] [PosReal t] [PosReal μ] : 0 ≤ φReg s t μ σ x

theorem JceiledContinuous (s t μ : ℝ) [PosReal s] [PosReal t] [PosReal μ] : Continuous fun (x : ℝ) => ∑' (pq : ℕ × ℕ), ↑(Jₚ pq) * smStep μ (x - (↑pq.1 * s + ↑pq.2 * t))

theorem φRegContinuousAt (s t μ σ x : ℝ) (hx : x ≠ 0) [PosReal s] [PosReal t] [PosReal μ] : ContinuousAt (φReg s t μ σ) x

theorem φRegMeasurable (s t μ σ : ℝ) [PosReal s] [PosReal t] [PosReal μ] : Measurable (φReg s t μ σ)

noncomputable def φRegFourierIntegrant (s t μ σ f x : ℝ) : ℂ

Equations

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

theorem φReg_Fourier1 (s t μ σ f : ℝ) : Real.fourierIntegral (fun (x : ℝ) => ↑(φReg s t μ σ x)) f = ∫ (x : ℝ), φRegFourierIntegrant s t μ σ f x

theorem φReg_FourierIntegrable (s t μ σ f : ℝ) (σBound : Real.log 2 / min s t < σ) [PosReal s] [PosReal t] [PosReal μ] : MeasureTheory.Integrable (φRegFourierIntegrant s t μ σ f) MeasureTheory.volume

noncomputable def φRegFourierIntegrantLeft (σ f x : ℝ) : ℂ

Equations

• φRegFourierIntegrantLeft σ f x = (Set.Ici 0).indicator (fun (x : ℝ) => Complex.exp (-(2 * ↑Real.pi * ↑f * Complex.I + ↑σ) * ↑x)) x

noncomputable def φRegFourierIntegrantRight (s t μ σ f x : ℝ) : ℂ

Equations

• φRegFourierIntegrantRight s t μ σ f x = ∑' (pq : ℕ × ℕ), ↑(Jₚ pq) * Complex.exp (-(2 * ↑Real.pi * ↑f * Complex.I + ↑σ) * ↑x) * ↑(smStep μ (x - (↑pq.1 * s + ↑pq.2 * t)))

theorem indicator_cast {α : Type u_1} {s : Set α} {f : α → ℝ} {x : α} : ↑(s.indicator f x) = s.indicator (fun (a : α) => ↑(f a)) x

theorem φRegFourierIntegrantRw1 (s t μ σ f x : ℝ) : φRegFourierIntegrant s t μ σ f x = φRegFourierIntegrantLeft σ f x + φRegFourierIntegrantRight s t μ σ f x

theorem integrable_exp_mul_complex_Ioi {a : ℝ} {c : ℂ} (hc : c.re < 0) : MeasureTheory.IntegrableOn (fun (x : ℝ) => Complex.exp (c * ↑x)) (Set.Ioi a) MeasureTheory.volume

theorem rexp_mul_n (x : ℝ) (n : ℕ) : Real.exp (x * ↑n) = Real.exp x ^ n

theorem φReg_Fourier2 (s t μ σ f : ℝ) (σBound : Real.log 2 / min s t < σ) [PosReal s] [PosReal t] [PosReal μ] : Real.fourierIntegral (fun (x : ℝ) => ↑(φReg s t μ σ x)) f = (2 * ↑Real.pi * ↑f * Complex.I + ↑σ)⁻¹ + ∫ (x : ℝ), φRegFourierIntegrantRight s t μ σ f x

noncomputable def φRegFourierIntegrantRightSummand (δ μ : ℝ) (l : ℂ) : ℂ

Equations

• φRegFourierIntegrantRightSummand δ μ l = ∫ (x : ℝ), Complex.exp (l * ↑x) * ↑(smStep μ (x - δ))

theorem φRegFourierIntegrantRightExchange (s t μ σ f : ℝ) (σBound : Real.log 2 / min s t < σ) [PosReal s] [PosReal t] [PosReal μ] : ∫ (x : ℝ), φRegFourierIntegrantRight s t μ σ f x = ∑' (pq : ℕ × ℕ), ↑(Jₚ pq) * φRegFourierIntegrantRightSummand (↑pq.1 * s + ↑pq.2 * t) μ (-(2 * ↑Real.pi * ↑f * Complex.I + ↑σ))

theorem φRegFourierIntegrantRightSummandEq (δ μ : ℝ) (l : ℂ) (hl : l.re < 0) [PosReal μ] : φRegFourierIntegrantRightSummand δ μ l = Complex.exp (l * ↑δ) * (1 - Complex.exp (l * ↑μ)) / (l ^ 2 * ↑μ)

noncomputable def φRegFourierResult (s t μ σ f : ℝ) : ℂ

Equations

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

theorem φReg_Fourier (s t μ σ : ℝ) (σBound : Real.log 2 / min s t < σ) [PosReal s] [PosReal t] [PosReal μ] : (Real.fourierIntegral fun (x : ℝ) => ↑(φReg s t μ σ x)) = φRegFourierResult s t μ σ