Source indexedlemma · leanprover/lean4:v4.32.0

Kadiri.kadiri_laplace_line_local_quotient_integrable

PrimeNumberTheoremAnd.IEANTN.KadiriEq13 · PrimeNumberTheoremAnd/IEANTN/KadiriEq13.lean:173 to 191

Mathematical statement

Exact Lean statement

lemma kadiri_laplace_line_local_quotient_integrable {φ : ℝ → ℂ}
    (hφ : ContDiff ℝ 1 φ) (sigma x : ℝ) {R : ℝ} (hR : 0 < R) :
    IntervalIntegrable
      (fun u : ℝ =>
        if u = 0 then 0 else
          (1 / (Real.pi * u) : ℂ) •
            (exp (-((sigma : ℂ) * ((x - u : ℝ) : ℂ))) * φ (x - u) -
              exp (-((sigma : ℂ) * (x : ℂ))) * φ x))
      volume (-R) R

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma kadiri_laplace_line_local_quotient_integrable {φ : ℝ → ℂ}    (hφ : ContDiff ℝ 1 φ) (sigma x : ℝ) {R : ℝ} (hR : 0 < R) :    IntervalIntegrable      (fun u : ℝ =>        if u = 0 then 0 else          (1 / (Real.pi * u) : ℂ) •            (exp (-((sigma : ℂ) * ((x - u : ℝ) : ℂ))) * φ (x - u) -              exp (-((sigma : ℂ) * (x : ℂ))) * φ x))      volume (-R) R := by  let g : ℝ → ℂ := fun y => exp (-((sigma : ℂ) * (y : ℂ))) * φ y  have hg_cont : ContinuousOn g (Set.Icc (x - R) (x + R)) := by    dsimp [g]    exact (Complex.continuous_exp.comp (by continuity)).continuousOn.mul      hφ.continuous.continuousOn  have hg_diff : DifferentiableAt ℝ g x :=    (kadiri_laplace_line_weight_differentiable hφ sigma) x  simpa [g] using    intervalIntegrable_local_quotient_of_differentiableAt (E := ℂ)      (f := g) (x := x) hR hg_cont hg_diff