Documentation

Frourio.Analysis.Zeros

Zero Lattice Structure of Frourio Symbols #

This file analyzes the zeros of the Frourio symbol and establishes the lattice structure of these zeros in the complex plane.

Main Definitions #

Main Theorems #

Implementation Notes #

The zeros of the Frourio symbol φ^(-s) - φ^(s-1) = 0 form a lattice in the complex plane. This analysis is crucial for understanding the spectral properties of the Frourio operator.

source
def Frourio.MellinZeros (φ : ℝ) :
Set ℂ

The set of zeros of the Frourio symbol for parameter φ

Equations
Instances For
    source
    def Frourio.ZeroSpacing (φ : ℝ) :
    ℝ

    Zero spacing function

    Equations
    Instances For
      source
      def Frourio.MetallicRatio (p : ℝ) :
      ℝ

      Metallic ratio with parameter p

      Equations
      Instances For
        source
        def Frourio.termφ__ :
        Lean.ParserDescr
        Equations
        Instances For
          source
          theorem Frourio.golden_is_metallic :
          goldenRatio = φ_ 1

          The golden ratio is the metallic ratio with p = 1

          source
          theorem Frourio.metallic_gt_one (p : ℝ) (hp : 0 < p) :
          1 < φ_ p

          Metallic ratios are greater than 1 for positive p

          source
          theorem Frourio.zeros_characterization (φ : ℝ) (hφ : 1 < φ) (s : ℂ) :
          s ∈ MellinZeros φ ↔ ∃ (k : ℤ), s = 1 / 2 + Complex.I * ↑Real.pi * ↑k / ↑(Real.log φ)

          Complete characterization of zeros

          source
          theorem Frourio.zero_lattice_structure (φ : ℝ) (hφ : 1 < φ) :
          MellinZeros φ = {x : ℂ | ∃ (k : ℤ), 1 / 2 + Complex.I * ↑Real.pi * ↑k / ↑(Real.log φ) = x}

          Zeros form a vertical lattice

          source
          theorem Frourio.zero_spacing_formula (φ : ℝ) (hφ : 1 < φ) :
          ZeroSpacing φ = Real.pi / Real.log φ

          Zero spacing equals π / log φ

          source
          theorem Frourio.golden_maximizes_spacing (p : ℝ) :
          p > 0 → ZeroSpacing (φ_ p) ≤ ZeroSpacing goldenRatio

          Golden ratio maximizes zero spacing among metallic ratios

          source
          theorem Frourio.zeros_on_critical_line (φ : ℝ) (hφ : 1 < φ) (s : ℂ) :
          s ∈ MellinZeros φ → s.re = 1 / 2

          Distribution of zeros on vertical lines

          source
          theorem Frourio.zero_density (φ : ℝ) (hφ : 1 < φ) (T : ℝ) :
          ∃ (n : ℕ), n = ⌊2 * T * Real.log φ / Real.pi⌋.natAbs + 1

          Density of zeros

          source
          theorem Frourio.zeros_off_real_axis (φ : ℝ) (hφ : 1 < φ) (s : ℝ) :
          ↑s ∈ MellinZeros φ ↔ s = 1 / 2 ∧ φ = 2

          Zeros avoid the real axis except at special points

          source
          theorem Frourio.asymptotic_spacing (φ : ℝ) (hφ : φ > 1) :
          ZeroSpacing φ = Real.pi / Real.log φ

          Asymptotic spacing for large φ

          source
          theorem Frourio.zeros_analogy_rh (φ : ℝ) (hφ : 1 < φ) (s : ℂ) :
          s ∈ MellinZeros φ → s.re = 1 / 2

          Connection to the Riemann zeta function zeros (analogy)

          source
          theorem Frourio.zero_functional_equation (φ : ℝ) (hφ : 1 < φ) (s : ℂ) :
          s ∈ MellinZeros φ ↔ 1 - s ∈ MellinZeros φ

          Functional equation relating zeros

          source
          theorem Frourio.zeros_determine_symbol (φ : ℝ) (hφ : 1 < φ) :
          frourioSymbol φ = fun (s : ℂ) => ↑φ ^ (-s) - ↑φ ^ (s - 1)

          Zeros determine the operator completely