audit-session037-axioms.txt

Raw #print axioms transcript

logDeriv_riemannZeta_sub_nearZeros_le_tight : ZeroCountProp →
  ZeroCountProp2 →
    NoLowZeros →
      ∀ {t : ℝ},
        10 ≤ t →
          ∀ {s : ℂ},
            -5 / 2 ≤ s.re →
              s.re ≤ 3 →
                s.im = t →
                  riemannZeta s ≠ 0 →
                    ‖logDeriv riemannZeta s - ∑ ρ ∈ nearZerosSub t, ↑(Zeta23.zeroMult ↑ρ) / (s - ↑ρ)‖ ≤
                      10.5 * Real.log (|t| + 2) + 48
'NguyenRH1.logDeriv_riemannZeta_sub_nearZeros_le_tight' depends on axioms: [propext, Classical.choice, Quot.sound]
def NguyenRH1.ZeroCountProp : Prop :=
∀ (t : ℝ), 2 ≤ t → ∑ ρ ∈ ⋯.toFinset, ↑(Zeta23.zeroMult ρ) ≤ C0hat (t + 1)
def NguyenRH1.ZeroCountProp2 : Prop :=
∀ (t : ℝ),
  10 ≤ t → ∑ ρ ∈ ⋯.toFinset, ↑(Zeta23.zeroMult ρ) ≤ 0.6 * Real.log (t + 2) + 0.886 * Real.log (Real.log (t + 2)) + 2.7
def NguyenRH1.NoLowZeros : Prop :=
∀ (ρ : ℂ), Zeta23.IsNontrivialZero ρ → 14 ≤ |ρ.im|
def NguyenRH1.C0hat : ℝ → ℝ :=
fun t => 0.433 * Real.log (t + 2) + 0.886 * Real.log (Real.log (t + 2)) + 2.9
def NguyenRH1.nearZerosSub : ℝ → Finset { ρ // Zeta23.IsNontrivialZero ρ } :=
fun t => {ρ ∈ ⋯.toFinset | |(↑ρ).im - t| < 1}
def Zeta23.zeroMult : ℂ → ℕ :=
fun ρ => (analyticOrderAt riemannZeta ρ).toNat
def NguyenRH1.zeroAbsWindow : ℝ → Set ℂ :=
fun t => {ρ | Zeta23.IsNontrivialZero ρ ∧ |ρ.im - t| ≤ 1}