7.3. Lemma 3.4 without the digamma identity (22)🔗

The report evaluates \lim_{\sigma\uparrow1}J_\sigma with the digamma log-moment identity (22) (Lemma 4.1.28). The formalization does not use (22): it computes the expectation of the endpoint phase against the limiting density p of (21) by exchanging the u-integral with a Frullani-type integral in a parameter t, which produces the Laplace kernel of the Wallis product already used for (33).

Definition7.3.1

uses 0

Used by 2

Reverse dependency previews

Preview

Lemma 7.3.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

For t > 0 and u \in \mathbb{R} put K(u,t) = \dfrac{(1 - e^{-t})\cos(ut) - te^{-t}}{t^2}, the real part of the complex Frullani kernel ((1 - e^{-t})e^{-zt} - te^{-t})/t^2 at z = -iu.

Lean code for Definition7.3.1●1 definition

defdefined in CohnElkies/LowerBound/LimitingDensity.lean

complete

def CohnElkies.wallisPhaseKernel (a u t : ℝ) : ℝ

def CohnElkies.wallisPhaseKernel (a u t : ℝ) :
  ℝ

The regularized Frullani phase kernel `((1 - e^{-t}) e^{-at} cos (ut) - t e^{-t}) / t²`,
the real part of `Frullani.shiftedCexpKernel` at `z = a - iu`.  The case `a = 0` is the kernel
whose `t`-integral produces the endpoint phase; report (22).

Lemma7.3.2

Statement uses 2

Statement dependency previews

Preview

Definition 7.2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

With K from Definition 7.3.1 and \Lambda from Definition 7.2.1, \int_0^\infty K(u,t)\,dt = 1 + \Lambda(2u) for every u.

Lean code for Lemma7.3.2●1 theorem

theoremdefined in CohnElkies/LowerBound/LimitingDensity.lean

complete

theorem CohnElkies.integral_wallisPhaseKernel_zero (u : ℝ) :
  ∫ (t : ℝ) in Set.Ioi 0, CohnElkies.wallisPhaseKernel 0 u t =
    1 + CohnElkies.lowerEndpointPhase (2 * u)

theorem CohnElkies.integral_wallisPhaseKernel_zero
  (u : ℝ) :
  ∫ (t : ℝ) in Set.Ioi 0,
      CohnElkies.wallisPhaseKernel 0 u t =
    1 +
      CohnElkies.lowerEndpointPhase
        (2 * u)

Report (22) at `a = 0`: the Frullani kernel integrates to `1 + φ(2u)`.

Proof for Lemma 7.3.2

uses 0

The t-integral of K(u,t) is evaluated through the antiderivative 1 + z\log z - (z+1)\log(z+1) of the complex Frullani kernel at z = a - iu (CohnElkies.integral_wallisPhaseKernel, CohnElkies.wallisComplexLogPhase), letting a \downarrow 0 by dominated convergence (CohnElkies.tendsto_integral_wallisPhaseKernel); the real part at z = -iu is 1 + \Lambda(2u) (CohnElkies.wallisComplexLogPhase_neg_I_mul).

Lemma7.3.3

Statement uses 2

Statement dependency previews

Preview

Lemma 4.1.27

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 2

Reverse dependency previews

Preview

Lemma 4.1.29

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

With p the density of Lemma 4.1.27 and K from Definition 7.3.1, for every t > 0, \int_{\mathbb{R}}p(u)K(u,t)\,du = \dfrac{e^{-t}(1 - e^{-t})}{t(1 + e^{-t})}, the Laplace kernel of the Wallis product.

Lean code for Lemma7.3.3●1 theorem

theoremdefined in CohnElkies/LowerBound/LimitingDensity.lean

complete

theorem CohnElkies.integral_poissonLogistic_mul_wallisPhaseKernel {t : ℝ}
  (ht : 0 < t) :
  ∫ (u : ℝ),
      CohnElkies.poissonLogisticDensity u *
        CohnElkies.wallisPhaseKernel 0 u t =
    Real.Wallis.laplaceKernel t

theorem CohnElkies.integral_poissonLogistic_mul_wallisPhaseKernel
  {t : ℝ} (ht : 0 < t) :
  ∫ (u : ℝ),
      CohnElkies.poissonLogisticDensity
          u *
        CohnElkies.wallisPhaseKernel 0 u
          t =
    Real.Wallis.laplaceKernel t

Averaging the Frullani kernel against `p` produces the Wallis Laplace kernel; report (22).

Proof for Lemma 7.3.3

uses 1

The u-integral of p(u)K(u,t) reduces, through the cosine transform of p in Lemma 4.1.27, \int p(u)\cos(tu)\,du = t/\sinh t, to ((1-e^{-t})\,t/\sinh t - te^{-t})/t^2, which is the Laplace kernel.

Lemma7.3.4

Statement uses 2

Statement dependency previews

Preview

Lemma 4.1.27

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

With p from Lemma 4.1.27 and \Lambda from Definition 7.2.1, \int_{\mathbb{R}}p(u)\bigl(1 + \Lambda(2u)\bigr)\,du = \log\dfrac{\pi}{2} and \int_{\mathbb{R}}p(u)\Lambda(2u)\,du = \log\dfrac{\pi}{2} - 1.

Lean code for Lemma7.3.4●2 theorems

theoremdefined in CohnElkies/LowerBound/LimitingDensity.lean

complete

theorem CohnElkies.integral_poissonLogistic_one_add_lowerEndpointPhase :
  ∫ (u : ℝ),
      CohnElkies.poissonLogisticDensity u *
        (1 + CohnElkies.lowerEndpointPhase (2 * u)) =
    Real.log (Real.pi / 2)

theorem CohnElkies.integral_poissonLogistic_one_add_lowerEndpointPhase :
  ∫ (u : ℝ),
      CohnElkies.poissonLogisticDensity
          u *
        (1 +
          CohnElkies.lowerEndpointPhase
            (2 * u)) =
    Real.log (Real.pi / 2)

theoremdefined in CohnElkies/LowerBound/LimitingDensity.lean

complete

theorem CohnElkies.integral_poissonLogistic_lowerEndpointPhase :
  ∫ (u : ℝ),
      CohnElkies.poissonLogisticDensity u *
        CohnElkies.lowerEndpointPhase (2 * u) =
    Real.log (Real.pi / 2) - 1

theorem CohnElkies.integral_poissonLogistic_lowerEndpointPhase :
  ∫ (u : ℝ),
      CohnElkies.poissonLogisticDensity
          u *
        CohnElkies.lowerEndpointPhase
          (2 * u) =
    Real.log (Real.pi / 2) - 1

Proof for Lemma 7.3.4

Proof uses 3

Proof dependency previews

Preview

Lemma 5.1.2

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

Fubini (the double integral converges absolutely, CohnElkies.poissonLogistic_wallisPhase_integrable) exchanges the two integrals of Lemma 7.3.2 and Lemma 7.3.3, and \int_0^\infty e^{-t}(1-e^{-t})/(t(1+e^{-t}))\,dt = \log(\pi/2) is the Wallis product, Lemma 5.1.2 (Real.Wallis.integral_laplaceKernel). Subtracting \int p = 1 gives the last identity.