def CommutingRepetition.LaplaceUniq.U : Set ℂ

The open strip |Re z| < π.

Equations

• CommutingRepetition.LaplaceUniq.U = {z : ℂ | |z.re| < Real.pi}

theorem CommutingRepetition.LaplaceUniq.isOpen_U : IsOpen U

theorem CommutingRepetition.LaplaceUniq.convex_U : Convex ℝ U

theorem CommutingRepetition.LaplaceUniq.zero_mem_U : 0 ∈ U

noncomputable def CommutingRepetition.LaplaceUniq.G (g : ℝ → ℂ) (t : ℝ) : ℂ

G t = g t / (2 cosh(πt)).

Equations

• CommutingRepetition.LaplaceUniq.G g t = g t / (2 * ↑(Real.cosh (Real.pi * t)))

theorem CommutingRepetition.LaplaceUniq.continuous_G {g : ℝ → ℂ} (hg : Continuous g) : Continuous (G g)

theorem CommutingRepetition.LaplaceUniq.norm_G_le {g : ℝ → ℂ} {C : ℝ} (hC : ∀ (t : ℝ), ‖g t‖ ≤ C) (t : ℝ) : ‖G g t‖ ≤ C * Real.exp (-(Real.pi * |t|))

theorem CommutingRepetition.LaplaceUniq.abs_mul_exp_neg_le {ε : ℝ} (hε : 0 < ε) (t : ℝ) : |t| * Real.exp (-(ε * |t|)) ≤ 2 / ε * max 1 (2 / (ε / 2) ^ 2) * (1 + t ^ 2)⁻¹

|t| e^{-ε|t|} ≤ K_ε (1 + t²)⁻¹.

noncomputable def CommutingRepetition.LaplaceUniq.F (g : ℝ → ℂ) (z : ℂ) : ℂ

The Laplace transform F z = ∫ e^{-zt} G t dt.

Equations

• CommutingRepetition.LaplaceUniq.F g z = ∫ (t : ℝ), Complex.exp (-(z * ↑t)) * CommutingRepetition.LaplaceUniq.G g t

theorem CommutingRepetition.LaplaceUniq.integrable_F_integrand {g : ℝ → ℂ} (hg : Continuous g) {C : ℝ} (hC : ∀ (t : ℝ), ‖g t‖ ≤ C) {z : ℂ} (hz : |z.re| < Real.pi) : MeasureTheory.Integrable (fun (t : ℝ) => Complex.exp (-(z * ↑t)) * G g t) MeasureTheory.volume

Integrability of e^{-zt} G t for |Re z| < π.

theorem CommutingRepetition.LaplaceUniq.hasDerivAt_F {g : ℝ → ℂ} (hg : Continuous g) {C : ℝ} (hC : ∀ (t : ℝ), ‖g t‖ ≤ C) {z₀ : ℂ} (hz₀ : |z₀.re| < Real.pi) : HasDerivAt (F g) (∫ (t : ℝ), -↑t * Complex.exp (-(z₀ * ↑t)) * G g t) z₀

F is complex differentiable on the strip.

theorem CommutingRepetition.LaplaceUniq.differentiableOn_F {g : ℝ → ℂ} (hg : Continuous g) {C : ℝ} (hC : ∀ (t : ℝ), ‖g t‖ ≤ C) : DifferentiableOn ℂ (F g) U

theorem CommutingRepetition.LaplaceUniq.analyticOnNhd_F {g : ℝ → ℂ} (hg : Continuous g) {C : ℝ} (hC : ∀ (t : ℝ), ‖g t‖ ≤ C) : AnalyticOnNhd ℂ (F g) U

theorem CommutingRepetition.LaplaceUniq.F_real {g : ℝ → ℂ} (φ : ℝ) : F g ↑φ = ∫ (t : ℝ), ↑(StripCauchy.w φ t) * g t

F φ = ∫ w φ t · g t for real φ.

theorem CommutingRepetition.LaplaceUniq.F_eq_zero_of_real {g : ℝ → ℂ} (hg : Continuous g) {C : ℝ} (hC : ∀ (t : ℝ), ‖g t‖ ≤ C) (h : ∀ (φ : ℝ), |φ| < Real.pi → F g ↑φ = 0) {z : ℂ} (hz : z ∈ U) : F g z = 0

If F vanishes on the real segment (-π, π), it vanishes on the whole strip.

theorem CommutingRepetition.LaplaceUniq.fourier_G_eq {g : ℝ → ℂ} (hg : Continuous g) {C : ℝ} (hC : ∀ (t : ℝ), ‖g t‖ ≤ C) (w : ℝ) : FourierTransform.fourier (G g) w = F g (2 * ↑Real.pi * ↑w * Complex.I)

The Fourier transform of G is F on the imaginary axis.

theorem CommutingRepetition.LaplaceUniq.eq_zero_of_forall_integral_w_eq_zero {g : ℝ → ℂ} (hg : Continuous g) {C : ℝ} (hC : ∀ (t : ℝ), ‖g t‖ ≤ C) (h : ∀ (φ : ℝ), |φ| < Real.pi → ∫ (t : ℝ), ↑(StripCauchy.w φ t) * g t = 0) (t : ℝ) : g t = 0

Laplace uniqueness: if ∫ w φ t · g t dt = 0 for all |φ| < π, then g = 0.