Bounded Laplace and ordered Dirichlet boundary convergence

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremNewman's Tauberian theorem#

Let f : ℝ → ℂ be measurable and bounded on [0, ∞), and let G be holomorphic on an open set Ω containing the closed half-plane 0 ≤ re z, agreeing with the Laplace transform ∫ t in Ici 0, f t * exp (-z t) on the open half-plane 0 < re z. Then ∫ t in 0..T, f t converges to G 0 as T → ∞.

TauCeti.LSeries.newmanLaplace_tendsto_integral {f : ℝ → ℂ} {G : ℂ → ℂ} {M : ℝ} {Ω : Set ℂ}
  (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ici 0)))
  (hbound : ∀ t ∈ Set.Ici 0, ‖f t‖ ≤ M) (hΩ : IsOpen Ω) (hcover : {z | 0 ≤ z.re} ⊆ Ω)
  (hG : DifferentiableOn ℂ G Ω)
  (hLaplace : ∀ (z : ℂ), 0 < z.re → G z = ∫ (t : ℝ) in Set.Ici 0, f t * Complex.exp (-z * ↑t)) :
  Filter.Tendsto (fun T => ∫ (t : ℝ) in 0..T, f t) Filter.atTop (nhds (G 0))
Lean

Formalized in Tau Ceti as TauCeti.LSeries.newmanLaplace_tendsto_integral.

Other forms

Newman's Tauberian theorem, with a pointwise continuation hypothesis. Formalized in Tau Ceti as TauCeti.LSeries.newmanLaplace_tendsto_integral_of_analyticAt.

TauCeti.LSeries.newmanLaplace_tendsto_integral_of_analyticAt {f : ℝ → ℂ} {G : ℂ → ℂ} {M : ℝ}
  (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ici 0)))
  (hbound : ∀ t ∈ Set.Ici 0, ‖f t‖ ≤ M) (hG : ∀ (z : ℂ), z.re = 0 → AnalyticAt ℂ G z)
  (hLaplace : ∀ (z : ℂ), 0 < z.re → G z = ∫ (t : ℝ) in Set.Ici 0, f t * Complex.exp (-z * ↑t)) :
  Filter.Tendsto (fun T => ∫ (t : ℝ) in 0..T, f t) Filter.atTop (nhds (G 0))
Sources
LeanTauCeti.LSeries.newmanLaplace_tendsto_integral · TauCeti.LSeries.newmanLaplace_tendsto_integral_of_analyticAt
Uses 2
Proof usesHolomorphy of the Laplace transform · Newman's estimate at a fixed radius

TheoremNewman's estimate at a fixed radius#

Let f be measurable and bounded by M on [0, ∞), and let G be holomorphic on an open set Ω containing the closed half-plane 0 ≤ re z and equal to the Laplace transform of f on 0 < re z. For every R > 0 and ε > 0, eventually in T, ‖G 0 - ∫ t in 0..T, f t‖ ≤ 2 M / R + ε.

TauCeti.LSeries.eventually_norm_sub_intervalIntegral_le {f : ℝ → ℂ} {G : ℂ → ℂ} {M R : ℝ}
  {Ω : Set ℂ}
  (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ici 0)))
  (hbound : ∀ t ∈ Set.Ici 0, ‖f t‖ ≤ M) (hΩ : IsOpen Ω) (hcover : {z | 0 ≤ z.re} ⊆ Ω)
  (hG : DifferentiableOn ℂ G Ω)
  (hLaplace : ∀ (z : ℂ), 0 < z.re → G z = ∫ (t : ℝ) in Set.Ici 0, f t * Complex.exp (-z * ↑t))
  (hR : 0 < R) {ε : ℝ} (hε : 0 < ε) :
  ∀ᶠ (T : ℝ) in Filter.atTop, ‖G 0 - ∫ (t : ℝ) in 0..T, f t‖ ≤ 2 * M / R + ε
Lean

Formalized in Tau Ceti as TauCeti.LSeries.eventually_norm_sub_intervalIntegral_le.

Sources
LeanTauCeti.LSeries.eventually_norm_sub_intervalIntegral_le
Uses 4 · Used by 1
Proof usesThe detour contribution in Newman's argument vanishes in the limit · The detour inside the continuation domain · Newman's contour identity · Newman's left detour
Used byNewman's Tauberian theorem

TheoremNewman's contour identity#

Let G be holomorphic on an open convex set U containing the right semicircle of radius R > 0 and the detour newmanDetour R δ with δ > 0, and let G_T z = ∫ t in 0..T, f t * exp (-z t). Against Newman's kernel k_T z = exp (T z) (1 + z² / R²) / z, the right semicircle integral of (G - G_T) k_T (counterclockwise from -R * I to R * I) plus the detour integral of G k_T (from R * I back to -R * I) equals 2πi (G 0 - ∫ t in 0..T, f t) plus the left semicircle integral of G_T k_T (counterclockwise from R * I to -R * I). All integrals include the velocity of their parametrization.

TauCeti.LSeries.integral_right_semicircle_add_integral_newmanDetour_mul_kernel {f : ℝ → ℂ}
  {G : ℂ → ℂ} {T R δ : ℝ} {U : Set ℂ} (hf : IntervalIntegrable f MeasureTheory.volume 0 T)
  (hR : 0 < R) (hδ : 0 < δ) (hU : IsOpen U) (hconv : Convex ℝ U) (hG : DifferentiableOn ℂ G U)
  (hcirc : ∀ θ ∈ Set.Icc (-Real.pi / 2) (Real.pi / 2), circleMap 0 R θ ∈ U)
  (hdet : ∀ s ∈ Set.Icc (-1) 1, TauCeti.LSeries.newmanDetour R δ s ∈ U) :
  (∫ (θ : ℝ) in -Real.pi / 2..Real.pi / 2,
        circleMap 0 R θ * Complex.I *
          ((G (circleMap 0 R θ) - ∫ (t : ℝ) in 0..T, f t * Complex.exp (-circleMap 0 R θ * ↑t)) *
                Complex.exp (↑T * circleMap 0 R θ) *
              (1 + circleMap 0 R θ ^ 2 / ↑R ^ 2) /
            circleMap 0 R θ)) +
      ∫ (s : ℝ) in -1..1,
        deriv (TauCeti.LSeries.newmanDetour R δ) s *
          (G (TauCeti.LSeries.newmanDetour R δ s) *
                Complex.exp (↑T * TauCeti.LSeries.newmanDetour R δ s) *
              (1 + TauCeti.LSeries.newmanDetour R δ s ^ 2 / ↑R ^ 2) /
            TauCeti.LSeries.newmanDetour R δ s) =
    2 * ↑Real.pi * Complex.I * (G 0 - ∫ (t : ℝ) in 0..T, f t) +
      ∫ (θ : ℝ) in Real.pi / 2..3 * Real.pi / 2,
        circleMap 0 R θ * Complex.I *
          ((∫ (t : ℝ) in 0..T, f t * Complex.exp (-circleMap 0 R θ * ↑t)) *
                Complex.exp (↑T * circleMap 0 R θ) *
              (1 + circleMap 0 R θ ^ 2 / ↑R ^ 2) /
            circleMap 0 R θ)
Lean

Formalized in Tau Ceti as TauCeti.LSeries.integral_right_semicircle_add_integral_newmanDetour_mul_kernel.

Sources
LeanTauCeti.LSeries.integral_right_semicircle_add_integral_newmanDetour_mul_kernel
Uses 4 · Used by 1
Statement usesNewman's left detour
Proof usesCauchy's formula for Newman's contour · Holomorphic functions have primitives on a star-shaped set · Truncated Laplace transforms are entire
Used byNewman's estimate at a fixed radius

TheoremHolomorphic functions have primitives on a star-shaped set#

If U is open and star-shaped about some point, then every function holomorphic on U has a primitive on U.

TauCeti.Contour.isExactOn_of_starConvex {U : Set ℂ} {f : ℂ → ℂ} {x : ℂ} (hU : IsOpen U)
  (hstar : StarConvex ℝ x U) (hf : DifferentiableOn ℂ f U) : Complex.IsExactOn f U
Lean

Formalized in Tau Ceti as TauCeti.Contour.isExactOn_of_starConvex.

Sources
LeanTauCeti.Contour.isExactOn_of_starConvex
Uses 3 · Used by 2
Proof usesThe converse of Cauchy's theorem · Generalized winding number (HW Def 2.1) · The homology Cauchy theorem (roadmap homologyCauchyTheorem, Layer 3)
Used byCauchy's formula for Newman's contour · Newman's contour identity

TheoremHolomorphy of the step correction#

For coefficients bounded from n = 1 on, the step correction is holomorphic on the half-plane -1 < re z: near z₀, the terms are bounded uniformly by a multiple of the summable n ^ (-1 - ε) for ε = (re z₀ + 1) / 2.

TauCeti.LSeries.differentiableOn_stepCorrection {a : ℕ → ℂ} {M : ℝ}
  (hbound : ∀ (n : ℕ), 1 ≤ n → ‖a n‖ ≤ M) :
  DifferentiableOn ℂ (TauCeti.LSeries.stepCorrection a) {z | -1 < z.re}
Lean

Formalized in Tau Ceti as TauCeti.LSeries.differentiableOn_stepCorrection.

Sources
LeanTauCeti.LSeries.differentiableOn_stepCorrection
Uses 2
Proof usesSubstitution x = exp t · Truncated Laplace transforms are entire

TheoremThe step correction at 0#

stepCorrection a 0 = ∑' n, a n (log (1 + 1 / n) - 1 / n).

TauCeti.LSeries.stepCorrection_zero (a : ℕ → ℂ) :
  TauCeti.LSeries.stepCorrection a 0 = ∑' (n : ℕ), a n * ↑(Real.log (1 + 1 / ↑n) - 1 / ↑n)
Lean

Formalized in Tau Ceti as TauCeti.LSeries.stepCorrection_zero.

Sources
LeanTauCeti.LSeries.stepCorrection_zero
Uses 1
Proof usesSubstitution x = exp t

DefinitionNewman's left detour#

The parabolic arc s ↦ -δ (1 - s²) - R s I, which on [-1, 1] runs from R * I to -R * I; for R, δ ≥ 0 it stays in the strip -δ ≤ re z ≤ 0, |im z| ≤ R.

TauCeti.LSeries.newmanDetour (R δ s : ℝ) : ℂ
Lean

Formalized in Tau Ceti as TauCeti.LSeries.newmanDetour.

Sources
LeanTauCeti.LSeries.newmanDetour
Used by 5
Used byCauchy's formula for Newman's contour · Newman's contour identity · Newman's estimate at a fixed radius · The detour contribution in Newman's argument vanishes in the limit · The detour inside the continuation domain

TheoremThe detour inside the continuation domain#

If Ω is open and contains the closed half-plane 0 ≤ re z, then for some δ > 0 the right semicircle of radius R and the detour newmanDetour R δ lie in a common open convex subset of Ω.

TauCeti.LSeries.exists_convex_newmanDetour_subset {R : ℝ} {Ω : Set ℂ} (hΩ : IsOpen Ω)
  (hcover : {z | 0 ≤ z.re} ⊆ Ω) (hR : 0 ≤ R) :
  ∃ δ > 0,
    ∃ U ⊆ Ω,
      IsOpen U ∧
        Convex ℝ U ∧
          (∀ θ ∈ Set.Icc (-Real.pi / 2) (Real.pi / 2), circleMap 0 R θ ∈ U) ∧
            ∀ s ∈ Set.Icc (-1) 1, TauCeti.LSeries.newmanDetour R δ s ∈ U
Lean

Formalized in Tau Ceti as TauCeti.LSeries.exists_convex_newmanDetour_subset.

Sources
LeanTauCeti.LSeries.exists_convex_newmanDetour_subset
Uses 1 · Used by 1
Statement usesNewman's left detour
Used byNewman's estimate at a fixed radius

TheoremThe detour contribution in Newman's argument vanishes in the limit#

If G is continuous on the detour newmanDetour R δ with R, δ > 0, then the detour integral of G against Newman's kernel exp (T z) (1 + z² / R²) / z tends to 0 as T → ∞.

TauCeti.LSeries.tendsto_integral_newmanDetour_mul_kernel {R δ : ℝ} {G : ℂ → ℂ} (hR : 0 < R)
  (hδ : 0 < δ) (hG : ContinuousOn G (TauCeti.LSeries.newmanDetour R δ '' Set.Icc (-1) 1)) :
  Filter.Tendsto
    (fun T =>
      ∫ (s : ℝ) in -1..1,
        deriv (TauCeti.LSeries.newmanDetour R δ) s *
          (G (TauCeti.LSeries.newmanDetour R δ s) *
                Complex.exp (↑T * TauCeti.LSeries.newmanDetour R δ s) *
              (1 + TauCeti.LSeries.newmanDetour R δ s ^ 2 / ↑R ^ 2) /
            TauCeti.LSeries.newmanDetour R δ s))
    Filter.atTop (nhds 0)
Lean

Formalized in Tau Ceti as TauCeti.LSeries.tendsto_integral_newmanDetour_mul_kernel.

Sources
LeanTauCeti.LSeries.tendsto_integral_newmanDetour_mul_kernel
Uses 1 · Used by 1
Statement usesNewman's left detour
Used byNewman's estimate at a fixed radius

TheoremTruncated Laplace transforms are entire#

If f is interval integrable on [a, b], then z ↦ ∫ t in a..b, f t * exp (-z t) is complex differentiable everywhere.

TauCeti.differentiable_intervalIntegral_mul_cexp_neg_mul {f : ℝ → ℂ} {a b : ℝ}
  (hf : IntervalIntegrable f MeasureTheory.volume a b) :
  Differentiable ℂ fun z => ∫ (t : ℝ) in a..b, f t * Complex.exp (-z * ↑t)
Lean

Formalized in Tau Ceti as TauCeti.differentiable_intervalIntegral_mul_cexp_neg_mul.

Sources
LeanTauCeti.differentiable_intervalIntegral_mul_cexp_neg_mul
Used by 4
Used byCauchy's formula for Newman's contour · Holomorphy of the Laplace transform · Holomorphy of the step correction · Newman's contour identity

TheoremHolomorphy of the Laplace transform#

If f is bounded on [0, ∞), its Laplace transform z ↦ ∫ t in Ici 0, f t * exp (-z t) is complex differentiable on the half-plane 0 < re z.

TauCeti.differentiableOn_integral_mul_cexp_neg_mul {f : ℝ → ℂ} {M : ℝ}
  (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ici 0)))
  (hbound : ∀ t ∈ Set.Ici 0, ‖f t‖ ≤ M) :
  DifferentiableOn ℂ (fun z => ∫ (t : ℝ) in Set.Ici 0, f t * Complex.exp (-z * ↑t)) {z | 0 < z.re}
Lean

Formalized in Tau Ceti as TauCeti.differentiableOn_integral_mul_cexp_neg_mul.

Sources
LeanTauCeti.differentiableOn_integral_mul_cexp_neg_mul
Uses 1 · Used by 1
Proof usesTruncated Laplace transforms are entire
Used byNewman's Tauberian theorem

TheoremSubstitution x = exp t#

For 0 < u and 0 < v, the integral of x ^ (-z - 1) over [u, v] is the truncated Laplace transform ∫ t in log u..log v, exp (-z t) of the constant function 1.

TauCeti.intervalIntegral_ofReal_cpow_neg_sub_one {u v : ℝ} (hu : 0 < u) (hv : 0 < v) (z : ℂ) :
  ∫ (x : ℝ) in u..v, ↑x ^ (-z - 1) = ∫ (t : ℝ) in Real.log u..Real.log v, Complex.exp (-z * ↑t)
Lean

Formalized in Tau Ceti as TauCeti.intervalIntegral_ofReal_cpow_neg_sub_one.

Sources
LeanTauCeti.intervalIntegral_ofReal_cpow_neg_sub_one
Used by 2
Used byHolomorphy of the step correction · The step correction at 0

TheoremAbelian theorem for Dirichlet series at s = 1#

If the ordered partial sums ∑ n ∈ Icc 1 N, a n / n tend to L and the Dirichlet series of a converges absolutely at every real σ > 1, then LSeries a σ → L as σ decreases to 1.

TauCeti.LSeries.tendsto_LSeries_nhdsGT_one {a : ℕ → ℂ} {L : ℂ}
  (hlim : Filter.Tendsto (fun N => ∑ n ∈ Finset.Icc 1 N, a n / ↑n) Filter.atTop (nhds L))
  (hsum : ∀ (σ : ℝ), 1 < σ → LSeriesSummable a ↑σ) :
  Filter.Tendsto (fun σ => LSeries a ↑σ) (nhdsWithin 1 (Set.Ioi 1)) (nhds L)
Lean

Formalized in Tau Ceti as TauCeti.LSeries.tendsto_LSeries_nhdsGT_one.

Sources
LeanTauCeti.LSeries.tendsto_LSeries_nhdsGT_one

TheoremCauchy's formula for Newman's contour#

Let g be holomorphic on an open convex set U containing the right semicircle of radius R > 0 and the detour newmanDetour R δ with δ > 0. Then the integral of g z / z over the right semicircle, counterclockwise from -R * I to R * I, plus its integral over the detour, back from R * I to -R * I through the left half-plane, is 2πi g 0. Both integrals include the velocity of their parametrization.

TauCeti.LSeries.integral_right_semicircle_add_integral_newmanDetour {R δ : ℝ} {U : Set ℂ}
  {g : ℂ → ℂ} (hR : 0 < R) (hδ : 0 < δ) (hU : IsOpen U) (hconv : Convex ℝ U)
  (hg : DifferentiableOn ℂ g U)
  (hcirc : ∀ θ ∈ Set.Icc (-Real.pi / 2) (Real.pi / 2), circleMap 0 R θ ∈ U)
  (hdet : ∀ s ∈ Set.Icc (-1) 1, TauCeti.LSeries.newmanDetour R δ s ∈ U) :
  (∫ (θ : ℝ) in -Real.pi / 2..Real.pi / 2,
        circleMap 0 R θ * Complex.I * (g (circleMap 0 R θ) / circleMap 0 R θ)) +
      ∫ (s : ℝ) in -1..1,
        deriv (TauCeti.LSeries.newmanDetour R δ) s *
          (g (TauCeti.LSeries.newmanDetour R δ s) / TauCeti.LSeries.newmanDetour R δ s) =
    2 * ↑Real.pi * Complex.I * g 0
Lean

Formalized in Tau Ceti as TauCeti.LSeries.integral_right_semicircle_add_integral_newmanDetour.

Other forms

Cauchy's formula for a truncated transform. Formalized in Tau Ceti as TauCeti.LSeries.circleIntegral_intervalIntegral_mul_kernel.

TauCeti.LSeries.circleIntegral_intervalIntegral_mul_kernel {f : ℝ → ℂ} {T : ℝ}
  (hf : IntervalIntegrable f MeasureTheory.volume 0 T) {R : ℝ} (hR : 0 < R) :
  ∮ (z : ℂ) in C(0, R),
      (∫ (t : ℝ) in 0..T, f t * Complex.exp (-z * ↑t)) * Complex.exp (↑T * z) *
          (1 + z ^ 2 / ↑R ^ 2) /
        z =
    2 * ↑Real.pi * Complex.I * ∫ (t : ℝ) in 0..T, f t
Sources
LeanTauCeti.LSeries.integral_right_semicircle_add_integral_newmanDetour · TauCeti.LSeries.circleIntegral_intervalIntegral_mul_kernel
Uses 3 · Used by 1
Statement usesNewman's left detour
Proof usesHolomorphic functions have primitives on a star-shaped set · Truncated Laplace transforms are entire
Used byNewman's contour identity

TheoremThe converse of Cauchy's theorem#

A continuous function on an open set U whose contour integral vanishes along every closed piecewise-C¹ curve in U has a primitive on U.

TauCeti.Contour.isExactOn_of_forall_closed_integral_eq_zero.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set ℂ} {f : ℂ → E} [CompleteSpace E] (hU : IsOpen U)
  (hf : ContinuousOn f U)
  (h :
    ∀ (γ : ℝ → ℂ) (a b : ℝ),
      TauCeti.IsPiecewiseC1On γ a b →
        Set.MapsTo γ (Set.uIcc a b) U → γ a = γ b → ∫ (t : ℝ) in a..b, deriv γ t • f (γ t) = 0) :
  Complex.IsExactOn f U
Lean

Formalized in Tau Ceti as TauCeti.Contour.isExactOn_of_forall_closed_integral_eq_zero.

Sources
LeanTauCeti.Contour.isExactOn_of_forall_closed_integral_eq_zero
Used by 5
Used byA crosscut of a simply connected domain has exactly two sides · The Riemann map of a Jordan domain extends to a homeomorphism of the closures · The Schwarz--Christoffel theorem for a bounded polygonal Jordan domain · Carathéodory's theorem for the inside of a Jordan curve · Holomorphic functions have primitives on a star-shaped set

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.