Documentation

Frourio.Analysis.ZeroSpacing

Zero Spacing Optimization #

This file proves that the golden ratio maximizes the spacing between zeros of the Frourio symbol among all metallic ratios.

Main Definitions #

Main Theorems #

Implementation Notes #

The proof uses calculus to show that the function p ↦ log((p + √(p² + 4))/2) achieves its minimum at p = 1, which corresponds to the golden ratio.

source
def Frourio.MetallicLogFunction :
ℝ → ℝ

The logarithm of the metallic ratio as a function of p

Equations
Instances For
    source
    def Frourio.ZeroSpacingFunction :
    ℝ → ℝ

    Zero spacing as a function of the metallic parameter

    Equations
    Instances For
      source
      def Frourio.termL :
      Lean.ParserDescr
      Equations
      Instances For
        source
        def Frourio.termZ :
        Lean.ParserDescr
        Equations
        Instances For
          source
          theorem Frourio.metallic_characteristic_eq (p : ℝ) :
          (φ_ p) ^ 2 = (p * φ_ p) + 1

          Metallic ratios satisfy the characteristic equation

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

          Metallic ratios are positive for positive p

          source
          theorem Frourio.metallic_ratio_deriv (p : ℝ) :
          deriv (fun (x : ℝ) => φ_ x) p = (1 + p / √(p ^ 2 + 4)) / 2

          The derivative of the metallic ratio

          source
          theorem Frourio.metallic_log_deriv (p : ℝ) (hp : 0 < p) :
          deriv L p = (1 + p / √(p ^ 2 + 4)) / (2 * φ_ p)

          The derivative of the metallic log function

          source
          theorem Frourio.metallic_log_second_deriv (p : ℝ) (hp : 0 < p) :
          deriv (deriv L) p = 4 / ((p ^ 2 + 4) * √(p ^ 2 + 4) * (φ_ p) ^ 2) - (1 + p / √(p ^ 2 + 4)) ^ 2 / (2 * (φ_ p) ^ 2)

          The second derivative of the metallic log function

          source
          theorem Frourio.metallic_log_critical_point :
          deriv L 1 = 0

          Critical point analysis: L'(1) = 0

          source
          theorem Frourio.metallic_log_second_deriv_positive :
          0 < deriv (deriv L) 1

          Second derivative test: L''(1) > 0

          source
          theorem Frourio.metallic_log_minimum (p : ℝ) :
          p > 0 → L 1 ≤ L p

          The metallic log function achieves its global minimum at p = 1

          source
          theorem Frourio.golden_maximizes_zero_spacing_detailed (p : ℝ) :
          p > 0 → Z p ≤ Z 1

          Golden ratio maximizes zero spacing among metallic ratios

          source
          theorem Frourio.golden_unique_maximum (p : ℝ) :
          p > 0 → p ≠ 1 → Z p < Z 1

          Uniqueness of the maximum

          source
          theorem Frourio.zero_spacing_small_p (p : ℝ) (hp : 0 < p) (hp_small : p < 1) :
          ∃ ε > 0, |Z p - Real.pi / Real.log 2| < ε

          Asymptotic behavior for small p

          source
          theorem Frourio.zero_spacing_large_p :
          ∃ C > 0, ∀ p ≥ 2, Z p ≤ C / p

          Asymptotic behavior for large p

          source
          theorem Frourio.zero_spacing_continuous :
          Continuous Z

          Continuity of the zero spacing function

          source
          theorem Frourio.zero_spacing_differentiable (p : ℝ) (hp : 0 < p) :
          DifferentiableAt ℝ Z p

          Differentiability of the zero spacing function

          source
          theorem Frourio.zero_spacing_deriv_at_one :
          deriv Z 1 = 0

          The derivative of zero spacing at p = 1

          source
          theorem Frourio.zero_spacing_concave (p : ℝ) (hp : 0 < p) :
          deriv (deriv Z) p < 0

          Convexity properties

          source
          theorem Frourio.zero_spacing_operator_norm_relation (p : ℝ) :
          0 < p → ∀ (x✝ : ℝ), True

          Connection to operator norms