Documentation

Mathlib.Analysis.Complex.Hadamard

Hadamard three-lines Theorem #

In this file we present a proof of a special case of Hadamard's three-lines Theorem.

Main result #

Main definitions #

Note #

The proof follows from Phragmén-Lindelöf when both frontiers are not everywhere zero. We then use a limit argument to cover the case when either of the sides are 0.

The vertical strip in the complex plane containing all z ∈ ℂ such that z.re ∈ Ioo a b.

Equations
Instances For

    The vertical strip in the complex plane containing all z ∈ ℂ such that z.re ∈ Icc a b.

    Equations
    Instances For
      noncomputable def Complex.HadamardThreeLines.sSupNormIm {E : Type u_1} [NormedAddCommGroup E] (f : E) (x : ) :

      The supremum of the norm of f on imaginary lines. (Fixed real part) This is also known as the function M

      Equations
      Instances For
        noncomputable def Complex.HadamardThreeLines.invInterpStrip {E : Type u_1} [NormedAddCommGroup E] (f : E) (z : ) (ε : ) :

        The inverse of the interpolation of sSupNormIm on the two boundaries. In other words, this is the inverse of the right side of the target inequality: |f(z)| ≤ |M(0) ^ (1-z)| * |M(1) ^ z|.

        Shifting this by a positive epsilon allows us to prove the case when either of the boundaries is zero.

        Equations
        Instances For
          noncomputable def Complex.HadamardThreeLines.F {E : Type u_1} [NormedAddCommGroup E] (f : E) [NormedSpace E] (ε : ) (z : ) :
          E

          A function useful for the proofs steps. We will aim to show that it is bounded by 1.

          Equations
          Instances For

            sSup of norm is nonneg applied to the image of f on the vertical line re z = x

            theorem Complex.HadamardThreeLines.sSupNormIm_eps_pos {E : Type u_1} [NormedAddCommGroup E] (f : E) {ε : } (hε : ε > 0) (x : ) :

            sSup of norm translated by ε > 0 is positive applied to the image of f on the vertical line re z = x

            Useful rewrite for the absolute value of invInterpStrip

            If f is bounded on the unit vertical strip, then f is bounded by sSupNormIm there.

            Alternative version of norm_le_sSupNormIm with a strict inequality and a positive ε.

            When the function f is bounded above on a vertical strip, then so is F.

            Proof that F is bounded by one one the edges.

            noncomputable def Complex.HadamardThreeLines.interpStrip {E : Type u_1} [NormedAddCommGroup E] (f : E) (z : ) :

            The interpolation of sSupNormIm on the two boundaries. In other words, this is the right side of the target inequality: |f(z)| ≤ |M(0) ^ (1-z)| * |M(1) ^ z|.

            Note that if (sSupNormIm f 0) = 0 ∨ (sSupNormIm f 1) = 0 then the power is not continuous since 0 ^ 0 = 1. Hence the use of ite.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Hadamard three-line theorem on re ⁻¹' [0,1]: If f is a bounded function, continuous on the closed strip re ⁻¹' [0,1] and differentiable on open strip re ⁻¹' (0,1), then for M(x) := sup ((norm ∘ f) '' (re ⁻¹' {x})) we have that for all z in the closed strip re ⁻¹' [0,1] the inequality ‖f(z)‖ ≤ M(0) ^ (1 - z.re) * M(1) ^ z.re holds.

              Hadamard three-line theorem on re ⁻¹' [0,1] (Variant in simpler terms): Let f be a bounded function, continuous on the closed strip re ⁻¹' [0,1] and differentiable on open strip re ⁻¹' (0,1). If, for all z.re = 0, ‖f z‖ ≤ a for some a ∈ ℝ and, similarly, for all z.re = 1, ‖f z‖ ≤ b for some b ∈ ℝ then for all z in the closed strip re ⁻¹' [0,1] the inequality ‖f(z)‖ ≤ a ^ (1 - z.re) * b ^ z.re holds.