Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized
Dark green border: this is in Mathlib

Definition 4.1Conjecture


Prop

This definition states a proposition. It does not prove that proposition.

LaTeX Lean

Definition 4.2NormalizedConjecture


Prop

This definition states a proposition. It does not prove that proposition.

LaTeX Lean

Lemma 2.3abs_hardyWeight_le


∀ {a : ℝ},
  0 < a →
    a < Real.pi / 4 →
      ∀ (t : ℝ), |HardyZeta.hardyWeight t| ≤ HardyZeta.thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t)

LaTeX Lean

Lemma 2.4abs_hardyWeight_le_abs


∀ {a : ℝ},
  0 < a →
    a < Real.pi / 4 →
      ∀ (t : ℝ), |HardyZeta.hardyWeight t| ≤ HardyZeta.thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * |t|)

LaTeX Lean

Lemma 2.5abs_iterate_modifiedDifference_le


∀ (h x M : ℝ) (f : ℝ → ℝ) (k : ℕ),
  (∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M) → |(HardyZeta.modifiedDifference h)^[k] f x| ≤ 4 ^ k * M

LaTeX Lean

Lemma 2.6abs_modifiedDifference_le


∀ (h x M : ℝ) (f : ℝ → ℝ), |f (x + h)| ≤ M → |f (x - h)| ≤ M → |f x| ≤ M → |HardyZeta.modifiedDifference h f x| ≤ 4 * M

LaTeX Lean

Lemma 2.7boundary_compact_comparison


∀ {f : ℝ → ℝ},
  Continuous f →
    ∀ {T : ℝ},
      0 < T →
        (∀ t > T, 0 ≤ f t) →
          ∀ (k : ℕ),
            (∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0),
                MeasureTheory.IntegrableOn (fun t => f t * HardyZeta.normalizedHardyKernel k h t) (Set.Ioi 0)
                  MeasureTheory.volume) →
              Filter.Tendsto (fun h => ∫ (t : ℝ) in Set.Ioi 0, f t * HardyZeta.normalizedHardyKernel k h t)
                  (nhdsWithin 0 (Set.Ioi 0)) (nhds 0) →
                ∫ (t : ℝ) in Set.Icc (2 * T) (2 * T + 1), f t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t) ≤
                  ∫ (t : ℝ) in Set.Icc 0 T, |f t| * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t)

LaTeX Lean

Lemma 2.8compact_tail_le_total_add_initial


∀ {q : ℝ → ℝ},
  Continuous q →
    MeasureTheory.IntegrableOn q (Set.Ioi 0) MeasureTheory.volume →
      ∀ {T : ℝ},
        0 < T →
          (∀ t > T, 0 ≤ q t) →
            ∫ (t : ℝ) in Set.Icc (2 * T) (2 * T + 1), q t ≤
              (∫ (t : ℝ) in Set.Ioi 0, q t) + ∫ (t : ℝ) in Set.Icc 0 T, |q t|

LaTeX Lean

Lemma 2.9_simp_1_1


∀ {α : Type u_1} [inst : Preorder α] {a b x : α}, (x ∈ Set.Icc a b) = (a ≤ x ∧ x ≤ b)

LaTeX Lean

Lemma 2.10_simp_1_2


∀ {α : Type u_1} [inst : Preorder α] {b x : α}, (x ∈ Set.Ioi b) = (b < x)

LaTeX Lean

Lemma 2.11completedZeta_conj


∀ (s : ℂ), completedRiemannZeta ((starRingEnd ℂ) s) = (starRingEnd ℂ) (completedRiemannZeta s)

LaTeX Lean

Lemma 2.12completedZeta_criticalPoint_eq_zero_iff


∀ (t : ℝ), completedRiemannZeta (HardyZeta.criticalPoint t) = 0 ↔ riemannZeta (HardyZeta.criticalPoint t) = 0

LaTeX Lean

Lemma 2.13_simp_1_1


∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b : G₀}, (a / b = 0) = (a = 0 ∨ b = 0)

LaTeX Lean

Lemma 2.14completedZeta_eq_fourier


∀ (t : ℝ),
  completedRiemannZeta (HardyZeta.criticalPoint t) =
    FourierTransform.fourier HardyZeta.modifiedThetaLogKernel (t / (4 * Real.pi)) / 2 - 1 / HardyZeta.criticalPoint t -
      1 / (1 - HardyZeta.criticalPoint t)

LaTeX Lean

Lemma 2.15completedZeta_eq_fourier_corrected


∀ (t : ℝ),
  completedRiemannZeta (HardyZeta.criticalPoint t) =
    FourierTransform.fourier HardyZeta.correctedThetaLogKernel (t / (4 * Real.pi)) / 2

LaTeX Lean

Lemma 2.16completedZeta_eq_fourier_theta


∀ (t : ℝ),
  completedRiemannZeta (HardyZeta.criticalPoint t) =
    FourierTransform.fourier (fun u => HardyZeta.thetaLogKernel ↑u) (t / (4 * Real.pi)) / 2

LaTeX Lean

Lemma 2.17completedZeta_eq_thetaFourierIntegral


∀ (t : ℝ),
  completedRiemannZeta (HardyZeta.criticalPoint t) = (∫ (u : ℝ), HardyZeta.thetaFourierIntegrand (t / 2) ↑u) / 2

LaTeX Lean

Lemma 2.18_simp_1_1


∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 2] [NeZero 2], (2 = 0) = False

LaTeX Lean

Lemma 2.19_simp_1_2


∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 3] [NeZero 3], (3 = 0) = False

LaTeX Lean

Lemma 2.20_simp_1_3


∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 4] [NeZero 4], (4 = 0) = False

LaTeX Lean

Lemma 2.21_simp_1_4


∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [NoZeroDivisors M₀] {a b : M₀}, a ≠ 0 → b ≠ 0 → (a * b = 0) = False

LaTeX Lean

Lemma 2.22_simp_1_5


∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} [IsReduced M₀] (n : ℕ), a ≠ 0 → (a ^ n = 0) = False

LaTeX Lean

Lemma 2.23_simp_1_6


∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} (n : ℤ), a ≠ 0 → (a ^ n = 0) = False

LaTeX Lean

Lemma 2.24_simp_1_7


∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] (n : ℕ), (↑n + 1 = 0) = False

LaTeX Lean

Lemma 2.25completedZeta₀_conj


∀ (s : ℂ), completedRiemannZeta₀ ((starRingEnd ℂ) s) = (starRingEnd ℂ) (completedRiemannZeta₀ s)

LaTeX Lean

Lemma 2.26completedZeta₀_eq_fourier


∀ (t : ℝ),
  completedRiemannZeta₀ (HardyZeta.criticalPoint t) =
    FourierTransform.fourier HardyZeta.modifiedThetaLogKernel (t / (4 * Real.pi)) / 2

LaTeX Lean

Lemma 2.27conj_criticalPoint


∀ (t : ℝ), (starRingEnd ℂ) (HardyZeta.criticalPoint t) = 1 - HardyZeta.criticalPoint t

LaTeX Lean

Lemma 2.28constant_sign_on_Ioi


∀ {f : ℝ → ℝ},
  Continuous f → ∀ (T : ℝ), (∀ (t : ℝ), T < t → f t ≠ 0) → (∀ (t : ℝ), T < t → 0 < f t) ∨ ∀ (t : ℝ), T < t → f t < 0

LaTeX Lean

Lemma 2.29continuous_criticalPoint


Continuous HardyZeta.criticalPoint

LaTeX Lean

Lemma 2.30continuous_criticalXi


Continuous HardyZeta.criticalXi

LaTeX Lean

Lemma 2.31continuous_dslope_sin


Continuous (dslope Real.sin 0)

LaTeX Lean

Lemma 2.32continuous_dslope_sinh


Continuous (dslope Real.sinh 0)

LaTeX Lean

Lemma 2.33continuous_extendedDifferenceMultiplier


Continuous fun p => HardyZeta.extendedDifferenceMultiplier p.1 p.2

LaTeX Lean

Lemma 2.34continuous_hardyWeight


Continuous HardyZeta.hardyWeight

LaTeX Lean

Lemma 2.35continuous_hardyXi


Continuous HardyZeta.hardyXi

LaTeX Lean

Lemma 2.36continuous_normalizedHardyKernel


∀ (k : ℕ) (h : ℝ), Continuous (HardyZeta.normalizedHardyKernel k h)

LaTeX Lean

Definition 2.37correctedThetaLogKernel


ℝ → ℂ

LaTeX Lean

Lemma 2.38eq_1


∀ (u : ℝ), HardyZeta.correctedThetaLogKernel u = HardyZeta.modifiedThetaLogKernel u - HardyZeta.poleLogKernel u

LaTeX Lean

Lemma 2.39correctedThetaLogKernel_ae_eq


HardyZeta.correctedThetaLogKernel =ᵐ[MeasureTheory.volume] fun u => HardyZeta.thetaLogKernel ↑u

LaTeX Lean

Lemma 2.40correctedThetaLogKernel_eq


∀ {u : ℝ}, u ≠ 0 → HardyZeta.correctedThetaLogKernel u = HardyZeta.thetaLogKernel ↑u

LaTeX Lean

Lemma 2.41cos_im_lower


∀ {z : ℂ} {b : ℝ}, b < Real.pi / 2 → |z.im| ≤ b → 0 < Real.cos b ∧ Real.cos b ≤ Real.cos z.im

LaTeX Lean

Lemma 2.42cosh_le_exp_abs


∀ (x : ℝ), Real.cosh x ≤ Real.exp |x|

LaTeX Lean

Lemma 2.43cpow_four_mul_half


∀ {z : ℂ}, z ≠ 0 → (4 * z) ^ (1 / 2) = 2 * z ^ (1 / 2)

LaTeX Lean

Definition 2.44criticalPoint


ℝ → ℂ

LaTeX Lean

Lemma 2.45_proof_1


(1 + 1).AtLeastTwo

LaTeX Lean

Lemma 2.46eq_1


∀ (t : ℝ), HardyZeta.criticalPoint t = 1 / 2 + ↑t * Complex.I

LaTeX Lean

Lemma 2.47criticalPoint_im


∀ (t : ℝ), (HardyZeta.criticalPoint t).im = t

LaTeX Lean

Lemma 2.48criticalPoint_injective


Function.Injective HardyZeta.criticalPoint

LaTeX Lean

Lemma 2.49criticalPoint_ne_one


∀ (t : ℝ), HardyZeta.criticalPoint t ≠ 1

LaTeX Lean

Lemma 2.50criticalPoint_ne_zero


∀ (t : ℝ), HardyZeta.criticalPoint t ≠ 0

LaTeX Lean

Lemma 2.51criticalPoint_neg


∀ (t : ℝ), HardyZeta.criticalPoint (-t) = 1 - HardyZeta.criticalPoint t

LaTeX Lean

Lemma 2.52criticalPoint_re


∀ (t : ℝ), (HardyZeta.criticalPoint t).re = 1 / 2

LaTeX Lean

Definition 2.53criticalXi


ℝ → ℂ

LaTeX Lean

Lemma 2.54eq_1


∀ (t : ℝ), HardyZeta.criticalXi t = HardyZeta.xi (HardyZeta.criticalPoint t)

LaTeX Lean

Lemma 2.55criticalXi_conj


∀ (t : ℝ), (starRingEnd ℂ) (HardyZeta.criticalXi t) = HardyZeta.criticalXi t

LaTeX Lean

Lemma 2.56criticalXi_eq_zero_iff


∀ (t : ℝ), HardyZeta.criticalXi t = 0 ↔ riemannZeta (HardyZeta.criticalPoint t) = 0

LaTeX Lean

Lemma 2.57_simp_1_3


∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀}, (a * b = 0) = (a = 0 ∨ b = 0)

LaTeX Lean

Lemma 2.58_simp_1_4


∀ (t : ℝ), (HardyZeta.criticalPoint t = 0) = False

LaTeX Lean

Lemma 2.59_simp_1_5


∀ (t : ℝ), (HardyZeta.criticalPoint t = 1) = False

LaTeX Lean

Lemma 2.60_simp_1_6


∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, (a - b = 0) = (a = b)

LaTeX Lean

Lemma 2.61_simp_1_7


∀ (t : ℝ), (completedRiemannZeta (HardyZeta.criticalPoint t) = 0) = (riemannZeta (HardyZeta.criticalPoint t) = 0)

LaTeX Lean

Lemma 2.62criticalXi_im


∀ (t : ℝ), (HardyZeta.criticalXi t).im = 0

LaTeX Lean

Lemma 2.63criticalXi_neg


∀ (t : ℝ), HardyZeta.criticalXi (-t) = HardyZeta.criticalXi t

LaTeX Lean

Lemma 2.68difference_sample_bounds


∀ {x h a : ℝ} {k : ℕ}, |x| + ↑(k + 1) * |h| < a → |x + h| + ↑k * |h| < a ∧ |x - h| + ↑k * |h| < a ∧ |x| + ↑k * |h| < a

LaTeX Lean

Definition 2.64differenceMultiplier


ℝ → ℝ → ℝ

LaTeX Lean

Lemma 2.65eq_1


∀ (h t : ℝ), HardyZeta.differenceMultiplier h t = 2 * (Real.cosh (h * t) - Real.cos (h / 2))

LaTeX Lean

Lemma 2.66differenceMultiplier_eq_squares


∀ (h t : ℝ), HardyZeta.differenceMultiplier h t = 4 * (Real.sinh (h * t / 2) ^ 2 + Real.sin (h / 4) ^ 2)

LaTeX Lean

Lemma 2.67differenceMultiplier_nonneg


∀ (h t : ℝ), 0 ≤ HardyZeta.differenceMultiplier h t

LaTeX Lean

Lemma 2.69differentiableAt_psi


∀ {z : ℂ}, 0 < z.re → DifferentiableAt ℂ HardyZeta.psi z

LaTeX Lean

Lemma 2.70differentiableAt_thetaFourierIntegrand


∀ (t : ℝ) {z : ℂ}, |z.im| < Real.pi / 2 → DifferentiableAt ℂ (HardyZeta.thetaFourierIntegrand t) z

LaTeX Lean

Lemma 2.71differentiableAt_thetaLogKernel


∀ {z : ℂ}, |z.im| < Real.pi / 2 → DifferentiableAt ℂ HardyZeta.thetaLogKernel z

LaTeX Lean

Lemma 2.72eventual_sign_of_not_zerosAboveEveryHeight


¬HardyZeta.ZerosAboveEveryHeight →
  ∃ T, 0 < T ∧ ((∀ (t : ℝ), T < t → 0 < HardyZeta.hardyXi t) ∨ ∀ (t : ℝ), T < t → HardyZeta.hardyXi t < 0)

LaTeX Lean

Lemma 2.73eventually_difference_center_inside


∀ {a : ℝ}, 0 < a → ∀ (k : ℕ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), |a - (↑k + 1) * h| + ↑k * |h| < a

LaTeX Lean

Lemma 2.74eventually_thetaCuspPath_sector


∀ᶠ (u : ℝ) in nhdsWithin 0 (Set.Ioi 0),
  HardyZeta.thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖HardyZeta.thetaCuspPath u‖ ≤ (HardyZeta.thetaCuspPath u).re

LaTeX Lean

Lemma 2.75_simp_1_1


∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 2] [NeZero 2], (2 = 0) = False

LaTeX Lean

Lemma 2.76_simp_1_2


∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 3] [NeZero 3], (3 = 0) = False

LaTeX Lean

Lemma 2.77_simp_1_3


∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 4] [NeZero 4], (4 = 0) = False

LaTeX Lean

Lemma 2.78_simp_1_4


∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [NoZeroDivisors M₀] {a b : M₀}, a ≠ 0 → b ≠ 0 → (a * b = 0) = False

LaTeX Lean

Lemma 2.79_simp_1_5


∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} [IsReduced M₀] (n : ℕ), a ≠ 0 → (a ^ n = 0) = False

LaTeX Lean

Lemma 2.80_simp_1_6


∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} (n : ℤ), a ≠ 0 → (a ^ n = 0) = False

LaTeX Lean

Lemma 2.81_simp_1_7


∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] (n : ℕ), (↑n + 1 = 0) = False

LaTeX Lean

Definition 2.82extendedDifferenceMultiplier


ℝ → ℝ → ℝ

LaTeX Lean

Lemma 2.83_proof_1


(3 + 1).AtLeastTwo

LaTeX Lean

Lemma 2.84_proof_2


(1 + 1).AtLeastTwo

LaTeX Lean

Lemma 2.85eq_1


∀ (h t : ℝ),
  HardyZeta.extendedDifferenceMultiplier h t =
    4 * ((t / 2 * dslope Real.sinh 0 (h * t / 2)) ^ 2 + (1 / 4 * dslope Real.sin 0 (h / 4)) ^ 2)

LaTeX Lean

Lemma 2.86extendedDifferenceMultiplier_eq


∀ {h : ℝ}, h ≠ 0 → ∀ (t : ℝ), HardyZeta.extendedDifferenceMultiplier h t = HardyZeta.differenceMultiplier h t / h ^ 2

LaTeX Lean

Lemma 2.87_simp_1_1


∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 2] [NeZero 2], (2 = 0) = False

LaTeX Lean

Lemma 2.88_simp_1_2


∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 3] [NeZero 3], (3 = 0) = False

LaTeX Lean

Lemma 2.89_simp_1_3


∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 4] [NeZero 4], (4 = 0) = False

LaTeX Lean

Lemma 2.90_simp_1_4


∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [NoZeroDivisors M₀] {a b : M₀}, a ≠ 0 → b ≠ 0 → (a * b = 0) = False

LaTeX Lean

Lemma 2.91_simp_1_5


∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} [IsReduced M₀] (n : ℕ), a ≠ 0 → (a ^ n = 0) = False

LaTeX Lean

Lemma 2.92_simp_1_6


∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} (n : ℤ), a ≠ 0 → (a ^ n = 0) = False

LaTeX Lean

Lemma 2.93_simp_1_7


∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] (n : ℕ), (↑n + 1 = 0) = False

LaTeX Lean

Lemma 2.94extendedDifferenceMultiplier_zero


∀ (t : ℝ), HardyZeta.extendedDifferenceMultiplier 0 t = t ^ 2 + 1 / 4

LaTeX Lean

Lemma 2.95finite_zeros_in_bounded_interval


∀ (a b : ℝ), {t | t ∈ Set.Icc a b ∧ HardyZeta.hardyXi t = 0}.Finite

LaTeX Lean

Lemma 2.96fourier_exp_neg_abs


∀ {a : ℝ},
  0 < a →
    ∀ (w : ℝ),
      FourierTransform.fourier (fun u => ↑(Real.exp (-a * |u|))) w =
        1 / (↑a - 2 * ↑Real.pi * ↑w * Complex.I) + 1 / (↑a + 2 * ↑Real.pi * ↑w * Complex.I)

LaTeX Lean

Lemma 2.97fourier_poleLogKernel


∀ (t : ℝ),
  FourierTransform.fourier HardyZeta.poleLogKernel (t / (4 * Real.pi)) / 2 =
    1 / HardyZeta.criticalPoint t + 1 / (1 - HardyZeta.criticalPoint t)

LaTeX Lean

Lemma 2.98_simp_1_1


∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 2] [NeZero 2], (2 = 0) = False

LaTeX Lean

Lemma 2.99_simp_1_2


∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 3] [NeZero 3], (3 = 0) = False

LaTeX Lean

Lemma 2.100_simp_1_3


∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 4] [NeZero 4], (4 = 0) = False

LaTeX Lean

Lemma 2.101_simp_1_4


∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [NoZeroDivisors M₀] {a b : M₀}, a ≠ 0 → b ≠ 0 → (a * b = 0) = False

LaTeX Lean

Lemma 2.102_simp_1_5


∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} [IsReduced M₀] (n : ℕ), a ≠ 0 → (a ^ n = 0) = False

LaTeX Lean

Lemma 2.103_simp_1_6


∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} (n : ℤ), a ≠ 0 → (a ^ n = 0) = False

LaTeX Lean

Lemma 2.104_simp_1_7


∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] (n : ℕ), (↑n + 1 = 0) = False

LaTeX Lean

Lemma 2.105fourier_sub_of_integrable


∀ {f g : ℝ → ℂ},
  MeasureTheory.Integrable f MeasureTheory.volume →
    MeasureTheory.Integrable g MeasureTheory.volume →
      ∀ (w : ℝ),
        FourierTransform.fourier (fun u => f u - g u) w = FourierTransform.fourier f w - FourierTransform.fourier g w

LaTeX Lean

Lemma 2.106fourier_theta_eq_hardyWeight


∀ (w : ℝ),
  FourierTransform.fourier (fun u => HardyZeta.thetaLogKernel ↑u) w = -4 * ↑(HardyZeta.hardyWeight (4 * Real.pi * w))

LaTeX Lean

Lemma 2.107_simp_1_1


∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 2] [NeZero 2], (2 = 0) = False

LaTeX Lean

Lemma 2.108_simp_1_2


∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 3] [NeZero 3], (3 = 0) = False

LaTeX Lean

Lemma 2.109_simp_1_3


∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 4] [NeZero 4], (4 = 0) = False

LaTeX Lean

Lemma 2.110_simp_1_4


∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [NoZeroDivisors M₀] {a b : M₀}, a ≠ 0 → b ≠ 0 → (a * b = 0) = False

LaTeX Lean

Lemma 2.111_simp_1_5


∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} [IsReduced M₀] (n : ℕ), a ≠ 0 → (a ^ n = 0) = False

LaTeX Lean

Lemma 2.112_simp_1_6


∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} (n : ℤ), a ≠ 0 → (a ^ n = 0) = False

LaTeX Lean

Lemma 2.113_simp_1_7


∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] (n : ℕ), (↑n + 1 = 0) = False

LaTeX Lean

Lemma 2.114fourier_theta_horizontal


∀ (w : ℝ) {b : ℝ},
  |b| < Real.pi / 2 →
    FourierTransform.fourier (fun u => HardyZeta.thetaLogKernel (↑u + ↑b * Complex.I)) w =
      ↑(Real.exp (-2 * Real.pi * w * b)) * FourierTransform.fourier (fun u => HardyZeta.thetaLogKernel ↑u) w

LaTeX Lean

Lemma 2.115fourier_theta_horizontal_eq_integral


∀ (b w : ℝ),
  FourierTransform.fourier (fun u => HardyZeta.thetaLogKernel (↑u + ↑b * Complex.I)) w =
    ∫ (u : ℝ), Complex.exp (-Complex.I * ↑(2 * Real.pi * w) * ↑u) * HardyZeta.thetaLogKernel (↑u + ↑b * Complex.I)

LaTeX Lean

Lemma 2.116fourier_theta_horizontal_eq_weight


∀ (w : ℝ) {b : ℝ},
  |b| < Real.pi / 2 →
    FourierTransform.fourier (fun u => HardyZeta.thetaLogKernel (↑u + ↑b * Complex.I)) w =
      -4 * ↑(HardyZeta.hardyWeight (4 * Real.pi * w) * Real.exp (-b / 2 * (4 * Real.pi * w)))

LaTeX Lean

Lemma 2.117hardy


{s | s.re = 1 / 2 ∧ riemannZeta s = 0}.Infinite

LaTeX Lean

Definition 2.118hardyTransform


ℝ → ℝ

LaTeX Lean

Lemma 2.119eq_1


∀ (α : ℝ), HardyZeta.hardyTransform α = ∫ (t : ℝ) in Set.Ioi 0, HardyZeta.hardyWeight t * Real.cosh (α * t)

LaTeX Lean

Lemma 2.120hardyTransform_eq


∀ (x : ℝ),
  |x| < Real.pi / 4 →
    HardyZeta.hardyTransform x = Real.pi * Real.cos (x / 2) - Real.pi * (HardyZeta.thetaBoundaryRemainder x).re

LaTeX Lean

Definition 2.121hardyWeight


ℝ → ℝ

LaTeX Lean

Lemma 2.122_proof_1


(3 + 1).AtLeastTwo

LaTeX Lean

Lemma 2.123eq_1


∀ (t : ℝ), HardyZeta.hardyWeight t = HardyZeta.hardyXi t / (t ^ 2 + 1 / 4)

LaTeX Lean

Lemma 2.124hardyWeight_abs


∀ (t : ℝ), HardyZeta.hardyWeight |t| = HardyZeta.hardyWeight t

LaTeX Lean

Lemma 2.125hardyWeight_neg


∀ (t : ℝ), HardyZeta.hardyWeight (-t) = HardyZeta.hardyWeight t

LaTeX Lean

Definition 2.126hardyXi


ℝ → ℝ

LaTeX Lean

Lemma 2.127eq_1


∀ (t : ℝ), HardyZeta.hardyXi t = (HardyZeta.criticalXi t).re

LaTeX Lean

Lemma 2.128hardyXi_eq_zero_iff


∀ (t : ℝ), HardyZeta.hardyXi t = 0 ↔ riemannZeta (HardyZeta.criticalPoint t) = 0

LaTeX Lean

Lemma 2.129hardyXi_neg


∀ (t : ℝ), HardyZeta.hardyXi (-t) = HardyZeta.hardyXi t

LaTeX Lean

Lemma 2.130hasDerivAt_thetaCuspPath_zero


HasDerivAt HardyZeta.thetaCuspPath 2 0

LaTeX Lean

Lemma 2.131hasSum_psi


∀ {z : ℂ}, 0 < z.re → HasSum (fun n => Complex.exp (-↑Real.pi * (↑n + 1) ^ 2 * z)) (HardyZeta.psi z)

LaTeX Lean

Lemma 2.132hasSum_thetaTerm


∀ {z : ℂ}, 0 < z.re → HasSum (HardyZeta.thetaTerm z) (1 + HardyZeta.psi z)

LaTeX Lean

Lemma 2.133infinite_criticalZeros_of_zerosAboveEveryHeight


HardyZeta.ZerosAboveEveryHeight → HardyZeta.InfinitelyManyCriticalZeros

LaTeX Lean

Definition 2.1InfinitelyManyCriticalZeros


Prop

This definition states a proposition. It does not prove that proposition.

LaTeX Lean

Lemma 2.134initial_polynomial_bound


∀ {w : ℝ → ℝ},
  Continuous w →
    ∀ {T : ℝ},
      0 < T →
        ∀ (k : ℕ),
          ∫ (t : ℝ) in Set.Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ k ≤
            (∫ (t : ℝ) in Set.Icc 0 T, |w t|) * (T ^ 2 + 1 / 4) ^ k

LaTeX Lean

Lemma 2.140integrable_correctedThetaLogKernel


MeasureTheory.Integrable HardyZeta.correctedThetaLogKernel MeasureTheory.volume

LaTeX Lean

Lemma 2.141integrable_difference_kernel


∀ {μ : MeasureTheory.Measure ℝ} {g : ℝ → ℝ} (h x : ℝ),
  MeasureTheory.Integrable (fun t => g t * Real.cosh ((x + h) * t)) μ →
    MeasureTheory.Integrable (fun t => g t * Real.cosh ((x - h) * t)) μ →
      MeasureTheory.Integrable (fun t => g t * Real.cosh (x * t)) μ →
        MeasureTheory.Integrable (fun t => g t * HardyZeta.differenceMultiplier h t * Real.cosh (x * t)) μ

LaTeX Lean

Lemma 2.142integrable_exp_neg_abs


∀ {a : ℝ}, 0 < a → MeasureTheory.Integrable (fun u => ↑(Real.exp (-a * |u|))) MeasureTheory.volume

LaTeX Lean

Lemma 2.143_simp_1_1


∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  MeasureTheory.IntegrableOn f Set.univ μ = MeasureTheory.Integrable f μ

LaTeX Lean

Lemma 2.144integrable_fourier_theta_horizontal


∀ {b : ℝ},
  |b| < Real.pi / 2 →
    MeasureTheory.Integrable (FourierTransform.fourier fun u => HardyZeta.thetaLogKernel (↑u + ↑b * Complex.I))
      MeasureTheory.volume

LaTeX Lean

Lemma 2.145integrable_hardyWeight_exp


∀ {α : ℝ},
  |α| < Real.pi / 4 →
    MeasureTheory.Integrable (fun t => HardyZeta.hardyWeight t * Real.exp (α * t)) MeasureTheory.volume

LaTeX Lean

Lemma 2.146integrable_mellinLogKernel


∀ {f : ℝ → ℂ} {σ : ℝ},
  MellinConvergent f ↑σ → MeasureTheory.Integrable (fun u => Real.exp (-σ * u) • f (Real.exp (-u))) MeasureTheory.volume

LaTeX Lean

Lemma 2.147integrable_modifiedThetaLogKernel


MeasureTheory.Integrable HardyZeta.modifiedThetaLogKernel MeasureTheory.volume

LaTeX Lean

Lemma 2.148integrable_poleLogKernel


MeasureTheory.Integrable HardyZeta.poleLogKernel MeasureTheory.volume

LaTeX Lean

Lemma 2.149integrable_thetaFourierIntegrand_horizontal


∀ (t : ℝ) {b : ℝ},
  |b| < Real.pi / 2 →
    MeasureTheory.Integrable (fun u => HardyZeta.thetaFourierIntegrand t (↑u + ↑b * Complex.I)) MeasureTheory.volume

LaTeX Lean

Lemma 2.150integrable_thetaLogKernel


MeasureTheory.Integrable (fun u => HardyZeta.thetaLogKernel ↑u) MeasureTheory.volume

LaTeX Lean

Lemma 2.151integrable_thetaLogKernel_horizontal


∀ {b : ℝ},
  |b| < Real.pi / 2 →
    MeasureTheory.Integrable (fun u => HardyZeta.thetaLogKernel (↑u + ↑b * Complex.I)) MeasureTheory.volume

LaTeX Lean

Lemma 2.135integrableOn_hardyDifference


∀ (k : ℕ) (h x : ℝ),
  |x| + ↑k * |h| < Real.pi / 4 →
    MeasureTheory.IntegrableOn
      (fun t => HardyZeta.hardyWeight t * HardyZeta.differenceMultiplier h t ^ k * Real.cosh (x * t)) (Set.Ioi 0)
      MeasureTheory.volume

LaTeX Lean

Lemma 2.136integrableOn_hardyWeight_cosh


∀ {α : ℝ},
  |α| < Real.pi / 4 →
    MeasureTheory.IntegrableOn (fun t => HardyZeta.hardyWeight t * Real.cosh (α * t)) (Set.Ioi 0) MeasureTheory.volume

LaTeX Lean

Lemma 2.137integrableOn_normalizedHardyKernel


∀ (k : ℕ) (h : ℝ),
  |Real.pi / 4 - (↑k + 1) * h| + ↑k * |h| < Real.pi / 4 →
    MeasureTheory.IntegrableOn (fun t => HardyZeta.hardyWeight t * HardyZeta.normalizedHardyKernel k h t) (Set.Ioi 0)
      MeasureTheory.volume

LaTeX Lean

Lemma 2.138_simp_1_1


∀ {M : Type u_2} [inst : Monoid M] (a : M) (m n : ℕ), (a ^ m) ^ n = a ^ (m * n)

LaTeX Lean

Lemma 2.139_simp_1_2


∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ℕ), (a ^ n)⁻¹ = a⁻¹ ^ n

LaTeX Lean

Lemma 2.152integral_fourier_theta_horizontal


∀ {b : ℝ},
  |b| < Real.pi / 2 →
    ∫ (w : ℝ), FourierTransform.fourier (fun u => HardyZeta.thetaLogKernel (↑u + ↑b * Complex.I)) w =
      HardyZeta.thetaLogKernel (↑b * Complex.I)

LaTeX Lean

Lemma 2.153integral_hardyWeight_cosh


∀ {α : ℝ},
  |α| < Real.pi / 4 →
    ↑(∫ (t : ℝ) in Set.Ioi 0, HardyZeta.hardyWeight t * Real.cosh (α * t)) =
      ↑Real.pi * ↑(Real.cos (α / 2)) - ↑Real.pi * HardyZeta.thetaBoundaryRemainder α

LaTeX Lean

Lemma 2.154integral_hardyWeight_exp


∀ {α : ℝ},
  |α| < Real.pi / 4 →
    ∫ (t : ℝ), ↑(HardyZeta.hardyWeight t * Real.exp (α * t)) =
      -↑Real.pi * HardyZeta.thetaLogKernel (↑(-2 * α) * Complex.I)

LaTeX Lean

Lemma 2.155integral_hardyWeight_exp_eq_cosh


∀ {α : ℝ},
  |α| < Real.pi / 4 →
    ∫ (t : ℝ), HardyZeta.hardyWeight t * Real.exp (α * t) =
      2 * ∫ (t : ℝ) in Set.Ioi 0, HardyZeta.hardyWeight t * Real.cosh (α * t)

LaTeX Lean

Lemma 2.156integral_shifted_even_power


∀ {w : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} {a C : ℝ},
  (∀ (n : ℕ), MeasureTheory.Integrable (fun t => t ^ (2 * n) * w t) μ) →
    (∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ n) →
      ∀ (k : ℕ), ∫ (t : ℝ), (t ^ 2 + a) ^ k * w t ∂μ = C * (-a + a) ^ k

LaTeX Lean

Lemma 2.157integral_shifted_even_power_eq_zero


∀ {w : ℝ → ℝ} {μ : MeasureTheory.Measure ℝ} {a C : ℝ},
  (∀ (n : ℕ), MeasureTheory.Integrable (fun t => t ^ (2 * n) * w t) μ) →
    (∀ (n : ℕ), ∫ (t : ℝ), t ^ (2 * n) * w t ∂μ = C * (-a) ^ n) →
      ∀ {k : ℕ}, k ≠ 0 → ∫ (t : ℝ), (t ^ 2 + a) ^ k * w t ∂μ = 0

LaTeX Lean

Lemma 2.158iterate_hardyTransform_eq_integral


∀ (k : ℕ) (h x : ℝ),
  |x| + ↑k * |h| < Real.pi / 4 →
    (HardyZeta.modifiedDifference h)^[k] HardyZeta.hardyTransform x =
      ∫ (t : ℝ) in Set.Ioi 0, HardyZeta.hardyWeight t * HardyZeta.differenceMultiplier h t ^ k * Real.cosh (x * t)

LaTeX Lean

Lemma 2.159iterate_hardyTransform_eq_theta


∀ (k : ℕ) (h x : ℝ),
  |x| + ↑(k + 1) * |h| < Real.pi / 4 →
    (HardyZeta.modifiedDifference h)^[k + 1] HardyZeta.hardyTransform x =
      -Real.pi * (HardyZeta.modifiedDifference h)^[k + 1] (fun α => (HardyZeta.thetaBoundaryRemainder α).re) x

LaTeX Lean

Lemma 2.160iterate_modifiedDifference_congr_strip


∀ {f g : ℝ → ℝ} {a : ℝ},
  (∀ (x : ℝ), |x| < a → f x = g x) →
    ∀ (k : ℕ) (h x : ℝ),
      |x| + ↑k * |h| < a → (HardyZeta.modifiedDifference h)^[k] f x = (HardyZeta.modifiedDifference h)^[k] g x

LaTeX Lean

Lemma 2.161iterate_modifiedDifference_const_mul


∀ (h c : ℝ) (f : ℝ → ℝ) (k : ℕ),
  ((HardyZeta.modifiedDifference h)^[k] fun x => c * f x) = fun x => c * (HardyZeta.modifiedDifference h)^[k] f x

LaTeX Lean

Lemma 2.162iterate_modifiedDifference_cos_succ


∀ (h : ℝ) (k : ℕ), ((HardyZeta.modifiedDifference h)^[k + 1] fun x => Real.cos (x / 2)) = fun x => 0

LaTeX Lean

Lemma 2.163iterate_modifiedDifference_cosh


∀ (h t : ℝ) (k : ℕ),
  ((HardyZeta.modifiedDifference h)^[k] fun x => Real.cosh (x * t)) = fun x =>
    HardyZeta.differenceMultiplier h t ^ k * Real.cosh (x * t)

LaTeX Lean

Lemma 2.164iterate_modifiedDifference_sub


∀ (h : ℝ) (f g : ℝ → ℝ) (k : ℕ),
  ((HardyZeta.modifiedDifference h)^[k] fun x => f x - g x) = fun x =>
    (HardyZeta.modifiedDifference h)^[k] f x - (HardyZeta.modifiedDifference h)^[k] g x

LaTeX Lean

Lemma 2.165mellin_conj_of_real_kernel


∀ (f : ℝ → ℂ),
  (∀ (x : ℝ), (starRingEnd ℂ) (f x) = f x) → ∀ (s : ℂ), mellin f ((starRingEnd ℂ) s) = (starRingEnd ℂ) (mellin f s)

LaTeX Lean

Definition 2.166modifiedDifference


ℝ → (ℝ → ℝ) → ℝ → ℝ

LaTeX Lean

Lemma 2.167_proof_1


(1 + 1).AtLeastTwo

LaTeX Lean

Lemma 2.168eq_1


∀ (h : ℝ) (f : ℝ → ℝ) (x : ℝ), HardyZeta.modifiedDifference h f x = f (x + h) + f (x - h) - 2 * Real.cos (h / 2) * f x

LaTeX Lean

Lemma 2.169modifiedDifference_const_mul


∀ (h c : ℝ) (f : ℝ → ℝ),
  (HardyZeta.modifiedDifference h fun x => c * f x) = fun x => c * HardyZeta.modifiedDifference h f x

LaTeX Lean

Lemma 2.170modifiedDifference_cos


∀ (h x : ℝ), HardyZeta.modifiedDifference h (fun x => Real.cos (x / 2)) x = 0

LaTeX Lean

Lemma 2.171modifiedDifference_cosh


∀ (h t x : ℝ),
  HardyZeta.modifiedDifference h (fun x => Real.cosh (x * t)) x = HardyZeta.differenceMultiplier h t * Real.cosh (x * t)

LaTeX Lean

Lemma 2.172modifiedDifference_integral


∀ {μ : MeasureTheory.Measure ℝ} (h x : ℝ) (f : ℝ → ℝ → ℝ),
  MeasureTheory.Integrable (f (x + h)) μ →
    MeasureTheory.Integrable (f (x - h)) μ →
      MeasureTheory.Integrable (f x) μ →
        HardyZeta.modifiedDifference h (fun y => ∫ (t : ℝ), f y t ∂μ) x =
          ∫ (t : ℝ), HardyZeta.modifiedDifference h (fun y => f y t) x ∂μ

LaTeX Lean

Lemma 2.176modifiedTheta_conj


∀ (x : ℝ), (starRingEnd ℂ) ((HurwitzZeta.hurwitzEvenFEPair 0).f_modif x) = (HurwitzZeta.hurwitzEvenFEPair 0).f_modif x

LaTeX Lean

Lemma 2.177modifiedTheta_mellinConvergent


∀ (s : ℂ), MellinConvergent (HurwitzZeta.hurwitzEvenFEPair 0).f_modif s

LaTeX Lean

Definition 2.173modifiedThetaLogKernel


ℝ → ℂ

LaTeX Lean

Lemma 2.174_proof_1


(3 + 1).AtLeastTwo

LaTeX Lean

Lemma 2.175eq_1


∀ (u : ℝ),
  HardyZeta.modifiedThetaLogKernel u = Real.exp (-u / 4) • (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (Real.exp (-u))

LaTeX Lean

Lemma 2.178norm_completedZeta_critical_le


∀ {a : ℝ},
  0 < a →
    a < Real.pi / 4 →
      ∀ (t : ℝ),
        ‖completedRiemannZeta (HardyZeta.criticalPoint t)‖ ≤
          HardyZeta.thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)

LaTeX Lean

Lemma 2.179norm_psi_cusp_le


∀ {z : ℂ},
  0 < z.re →
    ‖1 / 2 + HardyZeta.psi (Complex.I + z)‖ ≤
      ‖z ^ (1 / 2)‖⁻¹ *
        (Real.exp (-Real.pi * (1 / (4 * z)).re) / (1 - Real.exp (-Real.pi * (1 / (4 * z)).re)) +
          Real.exp (-Real.pi * (1 / z).re) / (1 - Real.exp (-Real.pi * (1 / z).re)))

LaTeX Lean

Lemma 2.180norm_psi_cusp_le_exp


∀ {z : ℂ},
  0 < z.re →
    1 ≤ (1 / (4 * z)).re →
      ‖1 / 2 + HardyZeta.psi (Complex.I + z)‖ ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * (1 / (4 * z)).re)

LaTeX Lean

Lemma 2.181norm_psi_cusp_le_sector


∀ {z : ℂ} {c : ℝ},
  0 < c →
    z ≠ 0 →
      c * ‖z‖ ≤ z.re →
        ‖z‖ ≤ c / 4 →
          ‖1 / 2 + HardyZeta.psi (Complex.I + z)‖ ≤ 4 * ‖z ^ (1 / 2)‖⁻¹ * Real.exp (-Real.pi * c / (4 * ‖z‖))

LaTeX Lean

Lemma 2.182norm_psi_le


∀ {z : ℂ}, 0 < z.re → ‖HardyZeta.psi z‖ ≤ Real.exp (-Real.pi * z.re) / (1 - Real.exp (-Real.pi * z.re))

LaTeX Lean

Lemma 2.183norm_psi_le_inv_re


∀ {z : ℂ} {c : ℝ}, 0 < c → c ≤ z.re → ‖HardyZeta.psi z‖ ≤ 1 / (Real.pi * z.re * (1 - Real.exp (-Real.pi * c)))

LaTeX Lean

Lemma 2.184norm_psi_le_two_exp


∀ {z : ℂ}, 1 ≤ z.re → ‖HardyZeta.psi z‖ ≤ 2 * Real.exp (-Real.pi * z.re)

LaTeX Lean

Lemma 2.191norm_theta_verticalIntegral_le


∀ (t : ℝ) {b : ℝ},
  |b| < Real.pi / 2 →
    ∀ (T : ℝ),
      ‖∫ (y : ℝ) in 0..b, HardyZeta.thetaFourierIntegrand t (↑T + ↑y * Complex.I)‖ ≤
        |b| * (Real.exp (|t| * |b|) * HardyZeta.thetaStripConstant |b|) * Real.exp (-|T| / 4)

LaTeX Lean

Lemma 2.185norm_thetaBoundaryRemainder


∀ (α : ℝ), ‖HardyZeta.thetaBoundaryRemainder α‖ = ‖1 / 2 + HardyZeta.psi (Complex.exp (2 * Complex.I * ↑α))‖

LaTeX Lean

Lemma 2.186norm_thetaFourierIntegral_le


∀ (t : ℝ) {b : ℝ},
  |b| < Real.pi / 2 →
    ‖∫ (u : ℝ), HardyZeta.thetaFourierIntegrand t ↑u‖ ≤ Real.exp (t * b) * HardyZeta.thetaHorizontalMass b

LaTeX Lean

Lemma 2.187norm_thetaFourierIntegrand


∀ (t : ℝ) (z : ℂ), ‖HardyZeta.thetaFourierIntegrand t z‖ = Real.exp (t * z.im) * ‖HardyZeta.thetaLogKernel z‖

LaTeX Lean

Lemma 2.188norm_thetaFourierIntegrand_le


∀ (t : ℝ) {b T y : ℝ},
  b < Real.pi / 2 →
    |y| ≤ b →
      ‖HardyZeta.thetaFourierIntegrand t (↑T + ↑y * Complex.I)‖ ≤
        Real.exp (|t| * b) * HardyZeta.thetaStripConstant b * Real.exp (-|T| / 4)

LaTeX Lean

Lemma 2.189norm_thetaLogKernel_le


∀ {z : ℂ} {b : ℝ},
  b < Real.pi / 2 → |z.im| ≤ b → ‖HardyZeta.thetaLogKernel z‖ ≤ HardyZeta.thetaStripConstant b * Real.exp (-|z.re| / 4)

LaTeX Lean

Lemma 2.190norm_thetaLogKernel_le_of_re_nonneg


∀ {z : ℂ} {b : ℝ},
  b < Real.pi / 2 →
    |z.im| ≤ b → 0 ≤ z.re → ‖HardyZeta.thetaLogKernel z‖ ≤ HardyZeta.thetaStripConstant b * Real.exp (-z.re / 4)

LaTeX Lean

Lemma 2.192normalizedHardyIntegral_eq


∀ (k : ℕ) (h : ℝ),
  |Real.pi / 4 - (↑k + 1) * h| + ↑k * |h| < Real.pi / 4 →
    ∫ (t : ℝ) in Set.Ioi 0, HardyZeta.hardyWeight t * HardyZeta.normalizedHardyKernel k h t =
      h⁻¹ ^ (2 * k) * (HardyZeta.modifiedDifference h)^[k] HardyZeta.hardyTransform (Real.pi / 4 - (↑k + 1) * h)

LaTeX Lean

Lemma 2.193_simp_1_1


∀ {M : Type u_2} [inst : Monoid M] (a : M) (m n : ℕ), (a ^ m) ^ n = a ^ (m * n)

LaTeX Lean

Lemma 2.194_simp_1_2


∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ℕ), (a ^ n)⁻¹ = a⁻¹ ^ n

LaTeX Lean

Definition 2.195normalizedHardyKernel


ℕ → ℝ → ℝ → ℝ

LaTeX Lean

Lemma 2.196_proof_1


(3 + 1).AtLeastTwo

LaTeX Lean

Lemma 2.197eq_1


∀ (k : ℕ) (h t : ℝ),
  HardyZeta.normalizedHardyKernel k h t =
    (HardyZeta.differenceMultiplier h t / h ^ 2) ^ k * Real.cosh ((Real.pi / 4 - (↑k + 1) * h) * t)

LaTeX Lean

Lemma 2.198normalizedHardyKernel_nonneg


∀ (k : ℕ) (h t : ℝ), 0 ≤ HardyZeta.normalizedHardyKernel k h t

LaTeX Lean

Lemma 2.199not_eventually_positive_hardyWeight_mul


∀ (c : ℝ) {T : ℝ}, 0 < T → (∀ t > T, 0 < c * HardyZeta.hardyWeight t) → False

LaTeX Lean

Lemma 2.200_simp_1_1


∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {L : Type u_6} [inst : RCLike L] (r : L)
  (f : α → L), r * ∫ (a : α), f a ∂μ = ∫ (a : α), r * f a ∂μ

LaTeX Lean

Lemma 2.201not_geometric_domination


∀ {m R A B : ℝ}, 0 < m → 0 < A → A < B → ¬∀ (k : ℕ), m * B ^ k ≤ R * A ^ k

LaTeX Lean

Lemma 2.202not_positive_tail_of_compact_moments


∀ {w : ℝ → ℝ},
  Continuous w →
    ∀ {T : ℝ},
      0 < T →
        (∀ t > T, 0 < w t) →
          (∀ (k : ℕ),
              ∫ (t : ℝ) in Set.Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ (k + 1) ≤
                ∫ (t : ℝ) in Set.Icc 0 T, |w t| * (t ^ 2 + 1 / 4) ^ (k + 1)) →
            False

LaTeX Lean

Lemma 2.203_simp_1_1


∀ {G : Type u_1} [inst : Semigroup G] (a b c : G), a * (b * c) = a * b * c

LaTeX Lean

Lemma 2.204not_positive_tail_of_vanishing_differences


∀ {f : ℝ → ℝ},
  Continuous f →
    ∀ {T : ℝ},
      0 < T →
        (∀ t > T, 0 < f t) →
          (∀ (k : ℕ),
              ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0),
                MeasureTheory.IntegrableOn (fun t => f t * HardyZeta.normalizedHardyKernel (k + 1) h t) (Set.Ioi 0)
                  MeasureTheory.volume) →
            (∀ (k : ℕ),
                Filter.Tendsto (fun h => ∫ (t : ℝ) in Set.Ioi 0, f t * HardyZeta.normalizedHardyKernel (k + 1) h t)
                  (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) →
              False

LaTeX Lean

Lemma 2.205ofReal_hardyWeight


∀ (t : ℝ), ↑(HardyZeta.hardyWeight t) = -completedRiemannZeta (HardyZeta.criticalPoint t) / 2

LaTeX Lean

Lemma 2.206ofReal_hardyXi


∀ (t : ℝ), ↑(HardyZeta.hardyXi t) = HardyZeta.criticalXi t

LaTeX Lean

Definition 2.207poleLogKernel


ℝ → ℂ

LaTeX Lean

Lemma 2.208eq_1


∀ (u : ℝ), HardyZeta.poleLogKernel u = ↑(Real.exp (-|u| / 4))

LaTeX Lean

Lemma 2.209positive_tail_mass


∀ {w : ℝ → ℝ}, Continuous w → ∀ {T : ℝ}, 0 < T → (∀ t > T, 0 < w t) → 0 < ∫ (t : ℝ) in Set.Icc (2 * T) (2 * T + 1), w t

LaTeX Lean

Definition 2.210psi


ℂ → ℂ

LaTeX Lean

Lemma 2.211_proof_1


(1 + 1).AtLeastTwo

LaTeX Lean

Lemma 2.212eq_1


∀ (z : ℂ), HardyZeta.psi z = (jacobiTheta (Complex.I * z) - 1) / 2

LaTeX Lean

Lemma 2.213psi_cusp_identity


∀ {z : ℂ},
  0 < z.re →
    1 / 2 + HardyZeta.psi (Complex.I + z) = 1 / z ^ (1 / 2) * (HardyZeta.psi (1 / (4 * z)) - HardyZeta.psi (1 / z))

LaTeX Lean

Lemma 2.214psi_eq_tsum


∀ {z : ℂ}, 0 < z.re → HardyZeta.psi z = ∑' (n : ℕ), Complex.exp (-↑Real.pi * (↑n + 1) ^ 2 * z)

LaTeX Lean

Lemma 2.215psi_inversion


∀ (z : ℂ), 1 + 2 * HardyZeta.psi z = 1 / z ^ (1 / 2) * (1 + 2 * HardyZeta.psi (1 / z))

LaTeX Lean

Lemma 2.216psi_ofReal_eq_evenKernel


∀ (x : ℝ), HardyZeta.psi ↑x = (↑(HurwitzZeta.evenKernel 0 x) - 1) / 2

LaTeX Lean

Lemma 2.217psi_shift


∀ {z : ℂ}, 0 < z.re → HardyZeta.psi (Complex.I + z) = 2 * HardyZeta.psi (4 * z) - HardyZeta.psi z

LaTeX Lean

Lemma 2.218_proof_1_1


∀ ⦃a b : ℕ⦄, 2 * a + 1 = 2 * b + 1 → ¬a = b → False

LaTeX Lean

Lemma 2.219re_one_div_pos


∀ {z : ℂ}, 0 < z.re → 0 < (1 / z).re

LaTeX Lean

Lemma 2.220re_reciprocal_four_mul


∀ (z : ℂ), (1 / (4 * z)).re = z.re / (4 * ‖z‖ ^ 2)

LaTeX Lean

Lemma 2.221sector_disk_bounds


∀ {z w : ℂ} {c : ℝ},
  0 < c →
    c ≤ 1 →
      z ≠ 0 → c * ‖z‖ ≤ z.re → ‖w - z‖ ≤ c * ‖z‖ / 4 → ‖z‖ / 2 ≤ ‖w‖ ∧ ‖w‖ ≤ 2 * ‖z‖ ∧ c / 2 * ‖w‖ ≤ w.re ∧ 0 < w.re

LaTeX Lean

Lemma 2.222sector_reciprocal_lower


∀ {z : ℂ} {c : ℝ}, z ≠ 0 → c * ‖z‖ ≤ z.re → c / (4 * ‖z‖) ≤ (1 / (4 * z)).re

LaTeX Lean

Lemma 2.223tail_polynomial_bound


∀ {w : ℝ → ℝ},
  Continuous w →
    ∀ {T : ℝ},
      0 < T →
        (∀ t > T, 0 ≤ w t) →
          ∀ (k : ℕ),
            (∫ (t : ℝ) in Set.Icc (2 * T) (2 * T + 1), w t) * ((2 * T) ^ 2 + 1 / 4) ^ k ≤
              ∫ (t : ℝ) in Set.Icc (2 * T) (2 * T + 1), w t * (t ^ 2 + 1 / 4) ^ k

LaTeX Lean

Lemma 2.224tendsto_compact_normalizedHardyKernel


∀ {f : ℝ → ℝ},
  Continuous f →
    ∀ (k : ℕ) (l r : ℝ),
      Filter.Tendsto (fun h => ∫ (t : ℝ) in Set.Icc l r, f t * HardyZeta.normalizedHardyKernel k h t)
        (nhdsWithin 0 (Set.Ioi 0))
        (nhds (∫ (t : ℝ) in Set.Icc l r, f t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (Real.pi / 4 * t)))

LaTeX Lean

Lemma 2.225tendsto_differenceMultiplier_div_sq


∀ (t : ℝ),
  Filter.Tendsto (fun h => HardyZeta.differenceMultiplier h t / h ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds (t ^ 2 + 1 / 4))

LaTeX Lean

Lemma 2.226tendsto_integral_differenceKernel_Icc


∀ {g : ℝ → ℝ},
  Continuous g →
    ∀ (a c l r : ℝ) (k : ℕ),
      Filter.Tendsto
        (fun h =>
          ∫ (t : ℝ) in Set.Icc l r,
            g t * (HardyZeta.differenceMultiplier h t / h ^ 2) ^ k * Real.cosh ((a - c * h) * t))
        (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (t : ℝ) in Set.Icc l r, g t * (t ^ 2 + 1 / 4) ^ k * Real.cosh (a * t)))

LaTeX Lean

Lemma 2.227tendsto_normalizedHardyIntegral


∀ (k : ℕ),
  Filter.Tendsto
    (fun h => ∫ (t : ℝ) in Set.Ioi 0, HardyZeta.hardyWeight t * HardyZeta.normalizedHardyKernel (k + 1) h t)
    (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

LaTeX Lean

Lemma 2.228tendsto_scaled_boundary_value


∀ {f : ℝ → ℝ} {a : ℝ} (n : ℕ),
  Filter.Tendsto (fun u => u⁻¹ ^ n * f (a - u)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0) →
    ∀ {c : ℝ}, 0 < c → Filter.Tendsto (fun h => h⁻¹ ^ n * f (a - c * h)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

LaTeX Lean

Lemma 2.229_simp_1_1


∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 2] [NeZero 2], (2 = 0) = False

LaTeX Lean

Lemma 2.230_simp_1_2


∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 3] [NeZero 3], (3 = 0) = False

LaTeX Lean

Lemma 2.231_simp_1_3


∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 4] [NeZero 4], (4 = 0) = False

LaTeX Lean

Lemma 2.232_simp_1_4


∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [NoZeroDivisors M₀] {a b : M₀}, a ≠ 0 → b ≠ 0 → (a * b = 0) = False

LaTeX Lean

Lemma 2.233_simp_1_5


∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} [IsReduced M₀] (n : ℕ), a ≠ 0 → (a ^ n = 0) = False

LaTeX Lean

Lemma 2.234_simp_1_6


∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} (n : ℤ), a ≠ 0 → (a ^ n = 0) = False

LaTeX Lean

Lemma 2.235_simp_1_7


∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] (n : ℕ), (↑n + 1 = 0) = False

LaTeX Lean

Lemma 2.236tendsto_scaled_hardy_difference


∀ (k : ℕ),
  Filter.Tendsto
    (fun h =>
      h⁻¹ ^ (2 * (k + 1)) *
        (HardyZeta.modifiedDifference h)^[k + 1] HardyZeta.hardyTransform (Real.pi / 4 - (↑(k + 1) + 1) * h))
    (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

LaTeX Lean

Lemma 2.237tendsto_scaled_iterate_modifiedDifference


∀ {f : ℝ → ℝ} {a : ℝ} (n k : ℕ),
  Filter.Tendsto (fun u => u⁻¹ ^ n * f (a - u)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0) →
    ∀ {c : ℝ},
      ↑k < c →
        Filter.Tendsto (fun h => h⁻¹ ^ n * (HardyZeta.modifiedDifference h)^[k] f (a - c * h))
          (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

LaTeX Lean

Lemma 2.238tendsto_scaled_theta_difference


∀ (k : ℕ),
  Filter.Tendsto
    (fun h =>
      h⁻¹ ^ (2 * k) *
        (HardyZeta.modifiedDifference h)^[k] (fun α => (HardyZeta.thetaBoundaryRemainder α).re)
          (Real.pi / 4 - (↑k + 1) * h))
    (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

LaTeX Lean

Lemma 2.244tendsto_theta_argument_weighted


∀ (n : ℕ),
  Filter.Tendsto (fun u => u⁻¹ ^ n * ‖1 / 2 + HardyZeta.psi (Complex.exp (2 * Complex.I * ↑(Real.pi / 4 - u)))‖)
    (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

LaTeX Lean

Lemma 2.245tendsto_theta_verticalIntegral


∀ (t : ℝ) {b : ℝ},
  |b| < Real.pi / 2 →
    ∀ (ε : ℝ),
      |ε| = 1 →
        Filter.Tendsto (fun T => ∫ (y : ℝ) in 0..b, HardyZeta.thetaFourierIntegrand t (↑(ε * T) + ↑y * Complex.I))
          Filter.atTop (nhds 0)

LaTeX Lean

Lemma 2.239tendsto_thetaBoundaryRemainder_re_weighted


∀ (n : ℕ),
  Filter.Tendsto (fun u => u⁻¹ ^ n * (HardyZeta.thetaBoundaryRemainder (Real.pi / 4 - u)).re) (nhdsWithin 0 (Set.Ioi 0))
    (nhds 0)

LaTeX Lean

Lemma 2.240tendsto_thetaBoundaryRemainder_weighted


∀ (n : ℕ),
  Filter.Tendsto (fun u => u⁻¹ ^ n * ‖HardyZeta.thetaBoundaryRemainder (Real.pi / 4 - u)‖) (nhdsWithin 0 (Set.Ioi 0))
    (nhds 0)

LaTeX Lean

Lemma 2.241tendsto_thetaCuspPath


Filter.Tendsto HardyZeta.thetaCuspPath (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

LaTeX Lean

Lemma 2.242tendsto_thetaCuspPath_div


Filter.Tendsto (fun u => HardyZeta.thetaCuspPath u / ↑u) (nhdsWithin 0 (Set.Ioi 0)) (nhds 2)

LaTeX Lean

Lemma 2.243tendsto_thetaCuspPath_weighted


∀ (n : ℕ),
  Filter.Tendsto (fun u => u⁻¹ ^ n * ‖1 / 2 + HardyZeta.psi (Complex.I + HardyZeta.thetaCuspPath u)‖)
    (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

LaTeX Lean

Lemma 2.246tendsto_weighted_psi_cusp


∀ {ι : Type u_1} {l : Filter ι} {z : ι → ℂ} {c : ℝ},
  0 < c →
    ∀ (s : ℝ),
      Filter.Tendsto z l (nhds 0) →
        (∀ᶠ (t : ι) in l, z t ≠ 0) →
          (∀ᶠ (t : ι) in l, c * ‖z t‖ ≤ (z t).re) →
            Filter.Tendsto (fun t => ‖z t‖⁻¹ ^ s * ‖1 / 2 + HardyZeta.psi (Complex.I + z t)‖) l (nhds 0)

LaTeX Lean

Definition 2.247thetaBoundaryRemainder


ℝ → ℂ

LaTeX Lean

Lemma 2.248eq_1


∀ (α : ℝ),
  HardyZeta.thetaBoundaryRemainder α =
    Complex.exp (Complex.I * ↑α / 2) * (1 / 2 + HardyZeta.psi (Complex.exp (2 * Complex.I * ↑α)))

LaTeX Lean

Definition 2.249thetaCuspPath


ℝ → ℂ

LaTeX Lean

Lemma 2.250_proof_1


(1 + 1).AtLeastTwo

LaTeX Lean

Lemma 2.251eq_1


∀ (u : ℝ), HardyZeta.thetaCuspPath u = Complex.I * (Complex.exp (-2 * ↑u * Complex.I) - 1)

LaTeX Lean

Lemma 2.252thetaCuspPath_eq


∀ (u : ℝ), HardyZeta.thetaCuspPath u = Complex.exp (2 * Complex.I * ↑(Real.pi / 4 - u)) - Complex.I

LaTeX Lean

Lemma 2.253thetaCuspPath_zero


HardyZeta.thetaCuspPath 0 = 0

LaTeX Lean

Lemma 2.254thetaFourierIntegral_shift


∀ (t : ℝ) {b : ℝ},
  |b| < Real.pi / 2 →
    ∫ (u : ℝ), HardyZeta.thetaFourierIntegrand t ↑u = ∫ (u : ℝ), HardyZeta.thetaFourierIntegrand t (↑u + ↑b * Complex.I)

LaTeX Lean

Definition 2.255thetaFourierIntegrand


ℝ → ℂ → ℂ

LaTeX Lean

Lemma 2.256eq_1


∀ (t : ℝ) (z : ℂ), HardyZeta.thetaFourierIntegrand t z = Complex.exp (-Complex.I * ↑t * z) * HardyZeta.thetaLogKernel z

LaTeX Lean

Lemma 2.257thetaFourierIntegrand_horizontal


∀ (t u b : ℝ),
  HardyZeta.thetaFourierIntegrand t (↑u + ↑b * Complex.I) =
    ↑(Real.exp (t * b)) * (Complex.exp (-Complex.I * ↑t * ↑u) * HardyZeta.thetaLogKernel (↑u + ↑b * Complex.I))

LaTeX Lean

Definition 2.258thetaHorizontalMass


ℝ → ℝ

LaTeX Lean

Lemma 2.259eq_1


∀ (b : ℝ), HardyZeta.thetaHorizontalMass b = ∫ (u : ℝ), ‖HardyZeta.thetaLogKernel (↑u + ↑b * Complex.I)‖

LaTeX Lean

Lemma 2.260thetaHorizontalMass_nonneg


∀ (b : ℝ), 0 ≤ HardyZeta.thetaHorizontalMass b

LaTeX Lean

Definition 2.261thetaLogKernel


ℂ → ℂ

LaTeX Lean

Lemma 2.262_proof_1


(1 + 1).AtLeastTwo

LaTeX Lean

Lemma 2.263eq_1


∀ (z : ℂ),
  HardyZeta.thetaLogKernel z = 2 * Complex.exp (-z / 4) * HardyZeta.psi (Complex.exp (-z)) - Complex.exp (z / 4)

LaTeX Lean

Lemma 2.264thetaLogKernel_neg


∀ {z : ℂ}, |z.im| < Real.pi / 2 → HardyZeta.thetaLogKernel (-z) = HardyZeta.thetaLogKernel z

LaTeX Lean

Definition 2.265thetaStripConstant


ℝ → ℝ

LaTeX Lean

Lemma 2.266_proof_1


(1 + 1).AtLeastTwo

LaTeX Lean

Definition 2.267thetaTerm


ℂ → ℕ → ℂ

LaTeX Lean

Lemma 2.268eq_1


∀ (z : ℂ) (n : ℕ), HardyZeta.thetaTerm z n = Complex.exp (-↑Real.pi * ↑n ^ 2 * z)

LaTeX Lean

Lemma 2.269thetaTerm_even


∀ (z : ℂ) (n : ℕ), HardyZeta.thetaTerm z (2 * n) = HardyZeta.thetaTerm (4 * z) n

LaTeX Lean

Lemma 2.270thetaTerm_shift


∀ (z : ℂ) (n : ℕ), HardyZeta.thetaTerm (Complex.I + z) n = (-1) ^ n * HardyZeta.thetaTerm z n

LaTeX Lean

Lemma 2.271_simp_1_1


∀ {m n : ℕ}, Even (m ^ n) = (Even m ∧ n ≠ 0)

LaTeX Lean

Lemma 2.272weighted_norm_psi_cusp_le_sector


∀ {z : ℂ} {c : ℝ} (s : ℝ),
  0 < c →
    z ≠ 0 →
      c * ‖z‖ ≤ z.re →
        ‖z‖ ≤ c / 4 →
          ‖z‖⁻¹ ^ s * ‖1 / 2 + HardyZeta.psi (Complex.I + z)‖ ≤
            4 * ‖z‖⁻¹ ^ (s + 1 / 2) * Real.exp (-(Real.pi * c / 4) * ‖z‖⁻¹)

LaTeX Lean

Definition 2.273xi


ℂ → ℂ

LaTeX Lean

Lemma 2.274eq_1


∀ (s : ℂ), HardyZeta.xi s = 1 / 2 * s * (s - 1) * completedRiemannZeta s

LaTeX Lean

Lemma 2.275xi_conj


∀ (s : ℂ), HardyZeta.xi ((starRingEnd ℂ) s) = (starRingEnd ℂ) (HardyZeta.xi s)

LaTeX Lean

Lemma 2.276xi_one_sub


∀ (s : ℂ), HardyZeta.xi (1 - s) = HardyZeta.xi s

LaTeX Lean

Lemma 2.277zerosAboveEveryHeight


HardyZeta.ZerosAboveEveryHeight

LaTeX Lean

Definition 2.2ZerosAboveEveryHeight


Prop

This definition states a proposition. It does not prove that proposition.

LaTeX Lean

Lemma 2.278_simp_1_1


∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a : α}, (0 < -a) = (a < 0)

LaTeX Lean

Definition 3.1Conjecture


Prop

This definition states a proposition. It does not prove that proposition.

LaTeX Lean

Lemma 3.2_proof_1


NeZero (1 + 1)

LaTeX Lean

Theorem 5.2Four Exponentials: DEFERRED

Prove FourExponentials.Conjecture after a successful Sharp Five proof. This work order is not a mathematical implication.

LaTeX

Theorem 5.1Sharp Five Exponentials: OPEN

Hardy is complete. Prove SharpFiveExponentials.Conjecture next. No proof is present.

LaTeX