Source indexedtheorem · leanprover/lean4:v4.32.0

laplaceIntegralCpowTrunc_eq_laplaceInvLineTrunc

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:2382 to 2400

Source documentation

The truncated multiplication-form inverse Laplace integral is the truncated vector-valued inverse Laplace line integral at log x.

Exact Lean statement

theorem laplaceIntegralCpowTrunc_eq_laplaceInvLineTrunc
    (sigma : ℝ) (f : ℝ → ℂ) {x : ℝ} (hx : 0 < x) (T : ℝ) :
    laplaceIntegralCpowTrunc f sigma x T =
      laplaceInvLineTrunc sigma (laplaceTransformBilateral f) (Real.log x) T

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem laplaceIntegralCpowTrunc_eq_laplaceInvLineTrunc    (sigma : ℝ) (f : ℝ → ℂ) {x : ℝ} (hx : 0 < x) (T : ℝ) :    laplaceIntegralCpowTrunc f sigma x T =      laplaceInvLineTrunc sigma (laplaceTransformBilateral f) (Real.log x) T := by  unfold laplaceIntegralCpowTrunc laplaceInvLineTrunc  simp_rw [laplaceIntegral_eq_laplaceTransformBilateral, smul_eq_mul]  rw [RCLike.real_smul_eq_coe_mul]  congr 1  · push_cast    field_simp [Real.pi_ne_zero]    rfl  · apply intervalIntegral.integral_congr    intro t _ht    change laplaceTransformBilateral f ((sigma : ℂ) + (t : ℂ) * I) *        (x : ℂ) ^ ((sigma : ℂ) + (t : ℂ) * I) =      Complex.exp (((sigma : ℂ) + (t : ℂ) * I) * (Real.log x : ℂ)) *        laplaceTransformBilateral f ((sigma : ℂ) + (t : ℂ) * I)    rw [← Complex.exp_mul_log_of_pos_eq_cpow hx ((sigma : ℂ) + (t : ℂ) * I)]    ring