2 HardyZeta: checked declarations
Prop
This definition states a proposition. It does not prove that proposition.
Prop
This definition states a proposition. It does not prove that proposition.
∀ {a : ℝ},
0 < a →
a < Real.pi / 4 →
∀ (t : ℝ), |HardyZeta.hardyWeight t| ≤ HardyZeta.thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * t)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {a : ℝ},
0 < a →
a < Real.pi / 4 →
∀ (t : ℝ), |HardyZeta.hardyWeight t| ≤ HardyZeta.thetaHorizontalMass (-2 * a) / 4 * Real.exp (-a * |t|)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (h x M : ℝ) (f : ℝ → ℝ) (k : ℕ), (∀ (y : ℝ), |y - x| ≤ ↑k * |h| → |f y| ≤ M) → |(HardyZeta.modifiedDifference h)^[k] f x| ≤ 4 ^ k * M
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (h x M : ℝ) (f : ℝ → ℝ), |f (x + h)| ≤ M → |f (x - h)| ≤ M → |f x| ≤ M → |HardyZeta.modifiedDifference h f x| ≤ 4 * M
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {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)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {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|
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_1} [inst : Preorder α] {a b x : α}, (x ∈ Set.Icc a b) = (a ≤ x ∧ x ≤ b)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_1} [inst : Preorder α] {b x : α}, (x ∈ Set.Ioi b) = (b < x)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (s : ℂ), completedRiemannZeta ((starRingEnd ℂ) s) = (starRingEnd ℂ) (completedRiemannZeta s)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), completedRiemannZeta (HardyZeta.criticalPoint t) = 0 ↔ riemannZeta (HardyZeta.criticalPoint t) = 0
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b : G₀}, (a / b = 0) = (a = 0 ∨ b = 0)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ),
completedRiemannZeta (HardyZeta.criticalPoint t) =
FourierTransform.fourier HardyZeta.modifiedThetaLogKernel (t / (4 * Real.pi)) / 2 - 1 / HardyZeta.criticalPoint t -
1 / (1 - HardyZeta.criticalPoint t)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ),
completedRiemannZeta (HardyZeta.criticalPoint t) =
FourierTransform.fourier HardyZeta.correctedThetaLogKernel (t / (4 * Real.pi)) / 2
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ),
completedRiemannZeta (HardyZeta.criticalPoint t) =
FourierTransform.fourier (fun u => HardyZeta.thetaLogKernel ↑u) (t / (4 * Real.pi)) / 2
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), completedRiemannZeta (HardyZeta.criticalPoint t) = (∫ (u : ℝ), HardyZeta.thetaFourierIntegrand (t / 2) ↑u) / 2
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 2] [NeZero 2], (2 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 3] [NeZero 3], (3 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 4] [NeZero 4], (4 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [NoZeroDivisors M₀] {a b : M₀}, a ≠ 0 → b ≠ 0 → (a * b = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} [IsReduced M₀] (n : ℕ), a ≠ 0 → (a ^ n = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} (n : ℤ), a ≠ 0 → (a ^ n = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] (n : ℕ), (↑n + 1 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (s : ℂ), completedRiemannZeta₀ ((starRingEnd ℂ) s) = (starRingEnd ℂ) (completedRiemannZeta₀ s)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ),
completedRiemannZeta₀ (HardyZeta.criticalPoint t) =
FourierTransform.fourier HardyZeta.modifiedThetaLogKernel (t / (4 * Real.pi)) / 2
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), (starRingEnd ℂ) (HardyZeta.criticalPoint t) = 1 - HardyZeta.criticalPoint t
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {f : ℝ → ℝ},
Continuous f → ∀ (T : ℝ), (∀ (t : ℝ), T < t → f t ≠ 0) → (∀ (t : ℝ), T < t → 0 < f t) ∨ ∀ (t : ℝ), T < t → f t < 0
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
Continuous HardyZeta.criticalPoint
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
Continuous HardyZeta.criticalXi
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
Continuous (dslope Real.sin 0)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
Continuous (dslope Real.sinh 0)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
Continuous fun p => HardyZeta.extendedDifferenceMultiplier p.1 p.2
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
Continuous HardyZeta.hardyWeight
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
Continuous HardyZeta.hardyXi
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (k : ℕ) (h : ℝ), Continuous (HardyZeta.normalizedHardyKernel k h)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℝ → ℂ
∀ (u : ℝ), HardyZeta.correctedThetaLogKernel u = HardyZeta.modifiedThetaLogKernel u - HardyZeta.poleLogKernel u
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
HardyZeta.correctedThetaLogKernel =ᵐ[MeasureTheory.volume] fun u => HardyZeta.thetaLogKernel ↑u
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {u : ℝ}, u ≠ 0 → HardyZeta.correctedThetaLogKernel u = HardyZeta.thetaLogKernel ↑u
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {z : ℂ} {b : ℝ}, b < Real.pi / 2 → |z.im| ≤ b → 0 < Real.cos b ∧ Real.cos b ≤ Real.cos z.im
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (x : ℝ), Real.cosh x ≤ Real.exp |x|
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {z : ℂ}, z ≠ 0 → (4 * z) ^ (1 / 2) = 2 * z ^ (1 / 2)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℝ → ℂ
(1 + 1).AtLeastTwo
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), HardyZeta.criticalPoint t = 1 / 2 + ↑t * Complex.I
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), (HardyZeta.criticalPoint t).im = t
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
Function.Injective HardyZeta.criticalPoint
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), HardyZeta.criticalPoint t ≠ 1
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), HardyZeta.criticalPoint t ≠ 0
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), HardyZeta.criticalPoint (-t) = 1 - HardyZeta.criticalPoint t
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), (HardyZeta.criticalPoint t).re = 1 / 2
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℝ → ℂ
∀ (t : ℝ), HardyZeta.criticalXi t = HardyZeta.xi (HardyZeta.criticalPoint t)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), (starRingEnd ℂ) (HardyZeta.criticalXi t) = HardyZeta.criticalXi t
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), HardyZeta.criticalXi t = 0 ↔ riemannZeta (HardyZeta.criticalPoint t) = 0
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀}, (a * b = 0) = (a = 0 ∨ b = 0)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), (HardyZeta.criticalPoint t = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), (HardyZeta.criticalPoint t = 1) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, (a - b = 0) = (a = b)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), (completedRiemannZeta (HardyZeta.criticalPoint t) = 0) = (riemannZeta (HardyZeta.criticalPoint t) = 0)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), (HardyZeta.criticalXi t).im = 0
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), HardyZeta.criticalXi (-t) = HardyZeta.criticalXi t
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℝ → ℝ → ℝ
∀ (h t : ℝ), HardyZeta.differenceMultiplier h t = 2 * (Real.cosh (h * t) - Real.cos (h / 2))
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (h t : ℝ), HardyZeta.differenceMultiplier h t = 4 * (Real.sinh (h * t / 2) ^ 2 + Real.sin (h / 4) ^ 2)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (h t : ℝ), 0 ≤ HardyZeta.differenceMultiplier h t
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {x h a : ℝ} {k : ℕ}, |x| + ↑(k + 1) * |h| < a → |x + h| + ↑k * |h| < a ∧ |x - h| + ↑k * |h| < a ∧ |x| + ↑k * |h| < a
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {z : ℂ}, 0 < z.re → DifferentiableAt ℂ HardyZeta.psi z
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ) {z : ℂ}, |z.im| < Real.pi / 2 → DifferentiableAt ℂ (HardyZeta.thetaFourierIntegrand t) z
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {z : ℂ}, |z.im| < Real.pi / 2 → DifferentiableAt ℂ HardyZeta.thetaLogKernel z
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
¬HardyZeta.ZerosAboveEveryHeight → ∃ T, 0 < T ∧ ((∀ (t : ℝ), T < t → 0 < HardyZeta.hardyXi t) ∨ ∀ (t : ℝ), T < t → HardyZeta.hardyXi t < 0)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {a : ℝ}, 0 < a → ∀ (k : ℕ), ∀ᶠ (h : ℝ) in nhdsWithin 0 (Set.Ioi 0), |a - (↑k + 1) * h| + ↑k * |h| < a
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ᶠ (u : ℝ) in nhdsWithin 0 (Set.Ioi 0), HardyZeta.thetaCuspPath u ≠ 0 ∧ 1 / 3 * ‖HardyZeta.thetaCuspPath u‖ ≤ (HardyZeta.thetaCuspPath u).re
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 2] [NeZero 2], (2 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 3] [NeZero 3], (3 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 4] [NeZero 4], (4 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [NoZeroDivisors M₀] {a b : M₀}, a ≠ 0 → b ≠ 0 → (a * b = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} [IsReduced M₀] (n : ℕ), a ≠ 0 → (a ^ n = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} (n : ℤ), a ≠ 0 → (a ^ n = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] (n : ℕ), (↑n + 1 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℝ → ℝ → ℝ
(3 + 1).AtLeastTwo
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
(1 + 1).AtLeastTwo
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (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)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {h : ℝ}, h ≠ 0 → ∀ (t : ℝ), HardyZeta.extendedDifferenceMultiplier h t = HardyZeta.differenceMultiplier h t / h ^ 2
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 2] [NeZero 2], (2 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 3] [NeZero 3], (3 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 4] [NeZero 4], (4 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [NoZeroDivisors M₀] {a b : M₀}, a ≠ 0 → b ≠ 0 → (a * b = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} [IsReduced M₀] (n : ℕ), a ≠ 0 → (a ^ n = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} (n : ℤ), a ≠ 0 → (a ^ n = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] (n : ℕ), (↑n + 1 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), HardyZeta.extendedDifferenceMultiplier 0 t = t ^ 2 + 1 / 4
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (a b : ℝ), {t | t ∈ Set.Icc a b ∧ HardyZeta.hardyXi t = 0}.Finite
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {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)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ),
FourierTransform.fourier HardyZeta.poleLogKernel (t / (4 * Real.pi)) / 2 =
1 / HardyZeta.criticalPoint t + 1 / (1 - HardyZeta.criticalPoint t)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 2] [NeZero 2], (2 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 3] [NeZero 3], (3 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 4] [NeZero 4], (4 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [NoZeroDivisors M₀] {a b : M₀}, a ≠ 0 → b ≠ 0 → (a * b = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} [IsReduced M₀] (n : ℕ), a ≠ 0 → (a ^ n = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} (n : ℤ), a ≠ 0 → (a ^ n = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] (n : ℕ), (↑n + 1 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {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
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (w : ℝ), FourierTransform.fourier (fun u => HardyZeta.thetaLogKernel ↑u) w = -4 * ↑(HardyZeta.hardyWeight (4 * Real.pi * w))
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 2] [NeZero 2], (2 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 3] [NeZero 3], (3 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 4] [NeZero 4], (4 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [NoZeroDivisors M₀] {a b : M₀}, a ≠ 0 → b ≠ 0 → (a * b = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} [IsReduced M₀] (n : ℕ), a ≠ 0 → (a ^ n = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} (n : ℤ), a ≠ 0 → (a ^ n = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] (n : ℕ), (↑n + 1 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (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
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (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)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (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)))
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
{s | s.re = 1 / 2 ∧ riemannZeta s = 0}.Infinite
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℝ → ℝ
∀ (α : ℝ), HardyZeta.hardyTransform α = ∫ (t : ℝ) in Set.Ioi 0, HardyZeta.hardyWeight t * Real.cosh (α * t)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (x : ℝ),
|x| < Real.pi / 4 →
HardyZeta.hardyTransform x = Real.pi * Real.cos (x / 2) - Real.pi * (HardyZeta.thetaBoundaryRemainder x).re
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℝ → ℝ
(3 + 1).AtLeastTwo
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), HardyZeta.hardyWeight t = HardyZeta.hardyXi t / (t ^ 2 + 1 / 4)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), HardyZeta.hardyWeight |t| = HardyZeta.hardyWeight t
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), HardyZeta.hardyWeight (-t) = HardyZeta.hardyWeight t
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℝ → ℝ
∀ (t : ℝ), HardyZeta.hardyXi t = (HardyZeta.criticalXi t).re
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), HardyZeta.hardyXi t = 0 ↔ riemannZeta (HardyZeta.criticalPoint t) = 0
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), HardyZeta.hardyXi (-t) = HardyZeta.hardyXi t
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
HasDerivAt HardyZeta.thetaCuspPath 2 0
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {z : ℂ}, 0 < z.re → HasSum (fun n => Complex.exp (-↑Real.pi * (↑n + 1) ^ 2 * z)) (HardyZeta.psi z)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {z : ℂ}, 0 < z.re → HasSum (HardyZeta.thetaTerm z) (1 + HardyZeta.psi z)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
HardyZeta.ZerosAboveEveryHeight → HardyZeta.InfinitelyManyCriticalZeros
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {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
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (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
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : ℝ},
|α| < Real.pi / 4 →
MeasureTheory.IntegrableOn (fun t => HardyZeta.hardyWeight t * Real.cosh (α * t)) (Set.Ioi 0) MeasureTheory.volume
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (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
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {M : Type u_2} [inst : Monoid M] (a : M) (m n : ℕ), (a ^ m) ^ n = a ^ (m * n)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ℕ), (a ^ n)⁻¹ = a⁻¹ ^ n
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
MeasureTheory.Integrable HardyZeta.correctedThetaLogKernel MeasureTheory.volume
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {μ : 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)) μ
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {a : ℝ}, 0 < a → MeasureTheory.Integrable (fun u => ↑(Real.exp (-a * |u|))) MeasureTheory.volume
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {μ : MeasureTheory.Measure α}
[inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
MeasureTheory.IntegrableOn f Set.univ μ = MeasureTheory.Integrable f μ
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {b : ℝ},
|b| < Real.pi / 2 →
MeasureTheory.Integrable (FourierTransform.fourier fun u => HardyZeta.thetaLogKernel (↑u + ↑b * Complex.I))
MeasureTheory.volume
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : ℝ},
|α| < Real.pi / 4 →
MeasureTheory.Integrable (fun t => HardyZeta.hardyWeight t * Real.exp (α * t)) MeasureTheory.volume
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {f : ℝ → ℂ} {σ : ℝ},
MellinConvergent f ↑σ → MeasureTheory.Integrable (fun u => Real.exp (-σ * u) • f (Real.exp (-u))) MeasureTheory.volume
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
MeasureTheory.Integrable HardyZeta.modifiedThetaLogKernel MeasureTheory.volume
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
MeasureTheory.Integrable HardyZeta.poleLogKernel MeasureTheory.volume
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ) {b : ℝ},
|b| < Real.pi / 2 →
MeasureTheory.Integrable (fun u => HardyZeta.thetaFourierIntegrand t (↑u + ↑b * Complex.I)) MeasureTheory.volume
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
MeasureTheory.Integrable (fun u => HardyZeta.thetaLogKernel ↑u) MeasureTheory.volume
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {b : ℝ},
|b| < Real.pi / 2 →
MeasureTheory.Integrable (fun u => HardyZeta.thetaLogKernel (↑u + ↑b * Complex.I)) MeasureTheory.volume
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {b : ℝ},
|b| < Real.pi / 2 →
∫ (w : ℝ), FourierTransform.fourier (fun u => HardyZeta.thetaLogKernel (↑u + ↑b * Complex.I)) w =
HardyZeta.thetaLogKernel (↑b * Complex.I)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : ℝ},
|α| < Real.pi / 4 →
↑(∫ (t : ℝ) in Set.Ioi 0, HardyZeta.hardyWeight t * Real.cosh (α * t)) =
↑Real.pi * ↑(Real.cos (α / 2)) - ↑Real.pi * HardyZeta.thetaBoundaryRemainder α
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : ℝ},
|α| < Real.pi / 4 →
∫ (t : ℝ), ↑(HardyZeta.hardyWeight t * Real.exp (α * t)) =
-↑Real.pi * HardyZeta.thetaLogKernel (↑(-2 * α) * Complex.I)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : ℝ},
|α| < Real.pi / 4 →
∫ (t : ℝ), HardyZeta.hardyWeight t * Real.exp (α * t) =
2 * ∫ (t : ℝ) in Set.Ioi 0, HardyZeta.hardyWeight t * Real.cosh (α * t)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {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
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {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
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (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)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (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
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {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
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (h c : ℝ) (f : ℝ → ℝ) (k : ℕ), ((HardyZeta.modifiedDifference h)^[k] fun x => c * f x) = fun x => c * (HardyZeta.modifiedDifference h)^[k] f x
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (h : ℝ) (k : ℕ), ((HardyZeta.modifiedDifference h)^[k + 1] fun x => Real.cos (x / 2)) = fun x => 0
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (h t : ℝ) (k : ℕ),
((HardyZeta.modifiedDifference h)^[k] fun x => Real.cosh (x * t)) = fun x =>
HardyZeta.differenceMultiplier h t ^ k * Real.cosh (x * t)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (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
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (f : ℝ → ℂ), (∀ (x : ℝ), (starRingEnd ℂ) (f x) = f x) → ∀ (s : ℂ), mellin f ((starRingEnd ℂ) s) = (starRingEnd ℂ) (mellin f s)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℝ → (ℝ → ℝ) → ℝ → ℝ
(1 + 1).AtLeastTwo
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (h : ℝ) (f : ℝ → ℝ) (x : ℝ), HardyZeta.modifiedDifference h f x = f (x + h) + f (x - h) - 2 * Real.cos (h / 2) * f x
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (h c : ℝ) (f : ℝ → ℝ), (HardyZeta.modifiedDifference h fun x => c * f x) = fun x => c * HardyZeta.modifiedDifference h f x
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (h x : ℝ), HardyZeta.modifiedDifference h (fun x => Real.cos (x / 2)) x = 0
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (h t x : ℝ), HardyZeta.modifiedDifference h (fun x => Real.cosh (x * t)) x = HardyZeta.differenceMultiplier h t * Real.cosh (x * t)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {μ : 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 ∂μ
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℝ → ℂ
(3 + 1).AtLeastTwo
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (u : ℝ), HardyZeta.modifiedThetaLogKernel u = Real.exp (-u / 4) • (HurwitzZeta.hurwitzEvenFEPair 0).f_modif (Real.exp (-u))
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (x : ℝ), (starRingEnd ℂ) ((HurwitzZeta.hurwitzEvenFEPair 0).f_modif x) = (HurwitzZeta.hurwitzEvenFEPair 0).f_modif x
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (s : ℂ), MellinConvergent (HurwitzZeta.hurwitzEvenFEPair 0).f_modif s
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {a : ℝ},
0 < a →
a < Real.pi / 4 →
∀ (t : ℝ),
‖completedRiemannZeta (HardyZeta.criticalPoint t)‖ ≤
HardyZeta.thetaHorizontalMass (-2 * a) / 2 * Real.exp (-a * t)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {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)))
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {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)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {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‖))
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {z : ℂ}, 0 < z.re → ‖HardyZeta.psi z‖ ≤ Real.exp (-Real.pi * z.re) / (1 - Real.exp (-Real.pi * z.re))
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {z : ℂ} {c : ℝ}, 0 < c → c ≤ z.re → ‖HardyZeta.psi z‖ ≤ 1 / (Real.pi * z.re * (1 - Real.exp (-Real.pi * c)))
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {z : ℂ}, 1 ≤ z.re → ‖HardyZeta.psi z‖ ≤ 2 * Real.exp (-Real.pi * z.re)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (α : ℝ), ‖HardyZeta.thetaBoundaryRemainder α‖ = ‖1 / 2 + HardyZeta.psi (Complex.exp (2 * Complex.I * ↑α))‖
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ) {b : ℝ},
|b| < Real.pi / 2 →
‖∫ (u : ℝ), HardyZeta.thetaFourierIntegrand t ↑u‖ ≤ Real.exp (t * b) * HardyZeta.thetaHorizontalMass b
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ) (z : ℂ), ‖HardyZeta.thetaFourierIntegrand t z‖ = Real.exp (t * z.im) * ‖HardyZeta.thetaLogKernel z‖
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (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)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {z : ℂ} {b : ℝ},
b < Real.pi / 2 → |z.im| ≤ b → ‖HardyZeta.thetaLogKernel z‖ ≤ HardyZeta.thetaStripConstant b * Real.exp (-|z.re| / 4)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {z : ℂ} {b : ℝ},
b < Real.pi / 2 →
|z.im| ≤ b → 0 ≤ z.re → ‖HardyZeta.thetaLogKernel z‖ ≤ HardyZeta.thetaStripConstant b * Real.exp (-z.re / 4)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (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)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (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)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {M : Type u_2} [inst : Monoid M] (a : M) (m n : ℕ), (a ^ m) ^ n = a ^ (m * n)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ℕ), (a ^ n)⁻¹ = a⁻¹ ^ n
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℕ → ℝ → ℝ → ℝ
(3 + 1).AtLeastTwo
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (k : ℕ) (h t : ℝ),
HardyZeta.normalizedHardyKernel k h t =
(HardyZeta.differenceMultiplier h t / h ^ 2) ^ k * Real.cosh ((Real.pi / 4 - (↑k + 1) * h) * t)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (k : ℕ) (h t : ℝ), 0 ≤ HardyZeta.normalizedHardyKernel k h t
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (c : ℝ) {T : ℝ}, 0 < T → (∀ t > T, 0 < c * HardyZeta.hardyWeight t) → False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : 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 ∂μ
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {m R A B : ℝ}, 0 < m → 0 < A → A < B → ¬∀ (k : ℕ), m * B ^ k ≤ R * A ^ k
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {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
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {G : Type u_1} [inst : Semigroup G] (a b c : G), a * (b * c) = a * b * c
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {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
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), ↑(HardyZeta.hardyWeight t) = -completedRiemannZeta (HardyZeta.criticalPoint t) / 2
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), ↑(HardyZeta.hardyXi t) = HardyZeta.criticalXi t
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℝ → ℂ
∀ (u : ℝ), HardyZeta.poleLogKernel u = ↑(Real.exp (-|u| / 4))
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {w : ℝ → ℝ}, Continuous w → ∀ {T : ℝ}, 0 < T → (∀ t > T, 0 < w t) → 0 < ∫ (t : ℝ) in Set.Icc (2 * T) (2 * T + 1), w t
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℂ → ℂ
(1 + 1).AtLeastTwo
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (z : ℂ), HardyZeta.psi z = (jacobiTheta (Complex.I * z) - 1) / 2
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {z : ℂ},
0 < z.re →
1 / 2 + HardyZeta.psi (Complex.I + z) = 1 / z ^ (1 / 2) * (HardyZeta.psi (1 / (4 * z)) - HardyZeta.psi (1 / z))
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {z : ℂ}, 0 < z.re → HardyZeta.psi z = ∑' (n : ℕ), Complex.exp (-↑Real.pi * (↑n + 1) ^ 2 * z)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (z : ℂ), 1 + 2 * HardyZeta.psi z = 1 / z ^ (1 / 2) * (1 + 2 * HardyZeta.psi (1 / z))
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (x : ℝ), HardyZeta.psi ↑x = (↑(HurwitzZeta.evenKernel 0 x) - 1) / 2
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {z : ℂ}, 0 < z.re → HardyZeta.psi (Complex.I + z) = 2 * HardyZeta.psi (4 * z) - HardyZeta.psi z
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ ⦃a b : ℕ⦄, 2 * a + 1 = 2 * b + 1 → ¬a = b → False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {z : ℂ}, 0 < z.re → 0 < (1 / z).re
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (z : ℂ), (1 / (4 * z)).re = z.re / (4 * ‖z‖ ^ 2)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {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
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {z : ℂ} {c : ℝ}, z ≠ 0 → c * ‖z‖ ≤ z.re → c / (4 * ‖z‖) ≤ (1 / (4 * z)).re
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {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
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {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)))
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ), Filter.Tendsto (fun h => HardyZeta.differenceMultiplier h t / h ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds (t ^ 2 + 1 / 4))
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {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)))
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (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)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {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)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 2] [NeZero 2], (2 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 3] [NeZero 3], (3 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u_2} [inst : Zero α] [inst_1 : OfNat α 4] [NeZero 4], (4 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {M₀ : Type u_1} [inst : Mul M₀] [inst_1 : Zero M₀] [NoZeroDivisors M₀] {a b : M₀}, a ≠ 0 → b ≠ 0 → (a * b = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} [IsReduced M₀] (n : ℕ), a ≠ 0 → (a ^ n = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} (n : ℤ), a ≠ 0 → (a ^ n = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] (n : ℕ), (↑n + 1 = 0) = False
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (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)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {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)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (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)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (n : ℕ),
Filter.Tendsto (fun u => u⁻¹ ^ n * (HardyZeta.thetaBoundaryRemainder (Real.pi / 4 - u)).re) (nhdsWithin 0 (Set.Ioi 0))
(nhds 0)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (n : ℕ),
Filter.Tendsto (fun u => u⁻¹ ^ n * ‖HardyZeta.thetaBoundaryRemainder (Real.pi / 4 - u)‖) (nhdsWithin 0 (Set.Ioi 0))
(nhds 0)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
Filter.Tendsto HardyZeta.thetaCuspPath (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
Filter.Tendsto (fun u => HardyZeta.thetaCuspPath u / ↑u) (nhdsWithin 0 (Set.Ioi 0)) (nhds 2)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (n : ℕ),
Filter.Tendsto (fun u => u⁻¹ ^ n * ‖1 / 2 + HardyZeta.psi (Complex.I + HardyZeta.thetaCuspPath u)‖)
(nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (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)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (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)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {ι : 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)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℝ → ℂ
∀ (α : ℝ),
HardyZeta.thetaBoundaryRemainder α =
Complex.exp (Complex.I * ↑α / 2) * (1 / 2 + HardyZeta.psi (Complex.exp (2 * Complex.I * ↑α)))
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℝ → ℂ
(1 + 1).AtLeastTwo
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (u : ℝ), HardyZeta.thetaCuspPath u = Complex.I * (Complex.exp (-2 * ↑u * Complex.I) - 1)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (u : ℝ), HardyZeta.thetaCuspPath u = Complex.exp (2 * Complex.I * ↑(Real.pi / 4 - u)) - Complex.I
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
HardyZeta.thetaCuspPath 0 = 0
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (t : ℝ) {b : ℝ},
|b| < Real.pi / 2 →
∫ (u : ℝ), HardyZeta.thetaFourierIntegrand t ↑u = ∫ (u : ℝ), HardyZeta.thetaFourierIntegrand t (↑u + ↑b * Complex.I)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℝ → ℂ → ℂ
∀ (t : ℝ) (z : ℂ), HardyZeta.thetaFourierIntegrand t z = Complex.exp (-Complex.I * ↑t * z) * HardyZeta.thetaLogKernel z
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (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))
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℝ → ℝ
∀ (b : ℝ), HardyZeta.thetaHorizontalMass b = ∫ (u : ℝ), ‖HardyZeta.thetaLogKernel (↑u + ↑b * Complex.I)‖
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (b : ℝ), 0 ≤ HardyZeta.thetaHorizontalMass b
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℂ → ℂ
(1 + 1).AtLeastTwo
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (z : ℂ), HardyZeta.thetaLogKernel z = 2 * Complex.exp (-z / 4) * HardyZeta.psi (Complex.exp (-z)) - Complex.exp (z / 4)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {z : ℂ}, |z.im| < Real.pi / 2 → HardyZeta.thetaLogKernel (-z) = HardyZeta.thetaLogKernel z
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℝ → ℝ
(1 + 1).AtLeastTwo
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℂ → ℕ → ℂ
∀ (z : ℂ) (n : ℕ), HardyZeta.thetaTerm z n = Complex.exp (-↑Real.pi * ↑n ^ 2 * z)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (z : ℂ) (n : ℕ), HardyZeta.thetaTerm z (2 * n) = HardyZeta.thetaTerm (4 * z) n
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (z : ℂ) (n : ℕ), HardyZeta.thetaTerm (Complex.I + z) n = (-1) ^ n * HardyZeta.thetaTerm z n
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {m n : ℕ}, Even (m ^ n) = (Even m ∧ n ≠ 0)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {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‖⁻¹)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
ℂ → ℂ
∀ (s : ℂ), HardyZeta.xi s = 1 / 2 * s * (s - 1) * completedRiemannZeta s
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (s : ℂ), HardyZeta.xi ((starRingEnd ℂ) s) = (starRingEnd ℂ) (HardyZeta.xi s)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ (s : ℂ), HardyZeta.xi (1 - s) = HardyZeta.xi s
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
HardyZeta.ZerosAboveEveryHeight
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a : α}, (0 < -a) = (a < 0)
Lean checks the proof in the linked source. The axiom audit permits only the three standard logical axioms.