FormalConjectures/Wikipedia/RamanujanTau.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

8 declarations, 4 contain sorry, 0 declared as axioms

Ramanujan τ-function

There are two conjectures related to the Ramanujan τ-function:

References:

Imports (1)
Imported by 1 file
  1. def RamanujanTau.Δ line 40 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: PowerSeries, Int

    Proof uses: HMul.hMul, Unit, PowerSeries.X, tprod, PNat, PowerSeries.WithPiTopology.instTopologicalSpace, HPow.hPow, Nat, HSub.hSub, OfNat.ofNat, SummationFilter.unconditional

    21 instances, coercions and auxiliary constants left out.

  2. def RamanujanTau.τ line 42 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Int

    Proof uses: LinearMap, RingHom.id, PowerSeries, Unit, PowerSeries.coeff, RamanujanTau.Δ

    8 instances, coercions and auxiliary constants left out.

  3. lemma RamanujanTau.multipliable sorry line 46 source

    depends on sorry what this means

    Statement uses: Multipliable, PowerSeries, Int, PNat, Unit, PowerSeries.WithPiTopology.instTopologicalSpace, HPow.hPow, Nat, HSub.hSub, OfNat.ofNat, PowerSeries.X, SummationFilter.unconditional

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  4. lemma RamanujanTau.τ_zero line 50 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Eq, Int, RamanujanTau.τ, OfNat.ofNat, Nat

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, LinearMap, RingHom.id, PowerSeries, Unit, PowerSeries.coeff, HMul.hMul, PowerSeries.X, tprod, PNat, PowerSeries.WithPiTopology.instTopologicalSpace, HPow.hPow, HSub.hSub, SummationFilter.unconditional, RingHom, PowerSeries.constantCoeff and 6 more

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  5. lemma RamanujanTau.τ_one line 53 source

    depends on sorry what this means

    Statement uses: Eq, Int, RamanujanTau.τ, OfNat.ofNat, Nat

    Proof uses: Finset, PNat, LE.le, RingHom, PowerSeries, Unit, PowerSeries.constantCoeff, tprod, PowerSeries.WithPiTopology.instTopologicalSpace, HPow.hPow, HSub.hSub, PowerSeries.X, SummationFilter.unconditional, Exists, Eq.mp, Filter.Tendsto, Function.comp, Finset.prod, SummationFilter.filter, nhds and 41 more

    75 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

  6. lemma RamanujanTau.τ_two sorry line 58 source

    depends on sorry what this means

    Statement uses: Eq, Int, RamanujanTau.τ, OfNat.ofNat, Nat, Neg.neg

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  7. theorem RamanujanTau.ramanujan_petersson The Ramanujan-Petersson conjecture: $|\tau(p)| \le 2 p^{11/2}$ for primes $p$ sorry line 64 source

    Source documentation

    The Ramanujan-Petersson conjecture: $|\tau(p)| \le 2 p^{11/2}$ for primes $p$.

    depends on sorry what this means

    Statement uses: Nat, Prime, LE.le, Real, abs, Int, RamanujanTau.τ, HMul.hMul, OfNat.ofNat, HPow.hPow, HDiv.hDiv

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem ramanujan_petersson : ∀ p : ℕ, Prime p → abs (τ p) ≤ 2 * (p : ℝ) ^ ((11 : ℝ) / 2) := by
…

    Mentions: RamanujanTau.τ

  8. theorem RamanujanTau.lehmer_ramanujan_tau Lehmer's conjecture: $\tau(n) \ne 0$ for all $n > 0$ sorry line 69 source

    Source documentation

    Lehmer's conjecture: $\tau(n) \ne 0$ for all $n > 0$.

    depends on sorry what this means

    Statement uses: Nat, GT.gt, OfNat.ofNat, Ne, Int, RamanujanTau.τ

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem lehmer_ramanujan_tau : ∀ n > 0, τ n ≠ 0 := by
…

    Mentions: RamanujanTau.τ