FormalConjectures/ErdosProblems/416.lean

GitHub source file

7 declarations, 6 contain sorry, 0 declared as axioms

1. abbrev Erdos416.V Let V(x) count the number of n≤x such that ϕ(m)=n is solvable line 34 source

   Source documentation

   Let V(x) count the number of n≤x such that ϕ(m)=n is solvable.

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

   Statement uses: Real

   Proof uses: Finset.card, Nat, Finset.filter, Exists, Eq, Nat.totient, Classical.propDecidable, Finset.Icc, OfNat.ofNat, Nat.floor

   11 instances, coercions and auxiliary constants left out.

   noncomputable abbrev V (x : ℝ) : ℝ :=
   …

2. theorem Erdos416.erdos_416.parts.i Let V(x) count the number of n≤x such that ϕ(m)=n is solvable sorry line 42 source

   Source documentation

   Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. Does V(2x)/V(x)→2 ?

   depends on sorry what this means

   Statement uses: Filter.Tendsto, Real, HDiv.hDiv, Erdos416.V, HMul.hMul, OfNat.ofNat, Nat, Filter.atTop, nhds

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

   28 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_416.parts.i :
       Filter.Tendsto (fun x => (V (2 * x) / V (x))) Filter.atTop (𝓝 2) := by
   …

   Mentions: Erdos416.V

3. theorem Erdos416.erdos_416.parts.ii Let V(x) count the number of n≤x such that ϕ(m)=n is solvable sorry line 51 source

   Source documentation

   Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. Is there an asymptotic formula for V(x)?

   depends on sorry what this means

   Statement uses: Real, sorryAx, Bool.false, Filter.Tendsto, HDiv.hDiv, Erdos416.V, Filter.atTop, nhds, OfNat.ofNat

   Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat

   19 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_416.parts.ii :
       let f : ℝ → ℝ := answer(sorry)
   …

4. theorem Erdos416.erdos_416.variants.Pillai Let V(x) count the number of n≤x such that ϕ(m)=n is solvable sorry line 62 source

   Source documentation

   Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. Pillai proved V(x)=o(x). Ref: S. Sivasankaranarayana Pillai, On some functions connected with $\phi(n)$

   depends on sorry what this means

   Statement uses: Asymptotics.IsLittleO, Real, Filter.atTop, Erdos416.V, id

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

   5 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_416.variants.Pillai : V =o[atTop] id := by
   …

   Mentions: Erdos416.V

5. theorem Erdos416.erdos_416.variants.Erdos Let V(x) count the number of n≤x such that ϕ(m)=n is solvable sorry line 71 source

   Source documentation

   Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. Erdős proved V(x)=x(logx)^(−1+o(1)). Ref: Erdős, P., On the normal number of prime factors of $p-1$ and some related problems concerning Euler's $\varphi$-function.

   depends on sorry what this means

   Statement uses: Exists, Real, And, Asymptotics.IsLittleO, Filter.atTop, OfNat.ofNat, Filter.Eventually, Eq, Erdos416.V, HMul.hMul, HPow.hPow, Real.log, HAdd.hAdd, Neg.neg

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

   25 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_416.variants.Erdos : ∃ f : ℝ → ℝ, f =o[atTop] (1 : ℝ → ℝ) ∧
       ∀ᶠ x in Filter.atTop, V x = x * x.log ^ (-1 + f x) := by
   …

   Mentions: Erdos416.V

6. theorem Erdos416.erdos_416.variants.Maier_Pomerance Let V(x) count the number of n≤x such that ϕ(m)=n is solvable sorry line 83 source

   Source documentation

   Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. V(x)=x/logx * e^((C+o(1))(log log log x)^2), for some explicit constant C>0. Ref:Maier, Helmut and Pomerance, Carl, On the number of distinct values of Euler's $\phi$-function.

   depends on sorry what this means

   Statement uses: Real, sorryAx, Bool.false, And, LT.lt, OfNat.ofNat, Exists, Asymptotics.IsLittleO, Filter.atTop, Filter.Eventually, Eq, Erdos416.V, HMul.hMul, HDiv.hDiv, Real.log, Real.exp, HAdd.hAdd, HPow.hPow, Nat

   Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   40 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_416.variants.Maier_Pomerance :
       let C : ℝ := answer(sorry)
   …

7. theorem Erdos416.erdos_416.variants.Ford Let V(x) count the number of n≤x such that ϕ(m)=n is solvable sorry line 97 source

   Source documentation

   Let V(x) count the number of n≤x such that ϕ(m)=n is solvable. V(x) ≍ x/log x*e^(C_1*(log log log x − log log log log x)^2+C_2 log log log x − C_3 log log log log x) Ref: Ford, Kevin, The distribution of totients.

   depends on sorry what this means

   Statement uses: Erdos416.erdos_416.variants.Ford.match_1, Prod, Real, sorryAx, Bool.false, And, LT.lt, OfNat.ofNat, HMul.hMul, HDiv.hDiv, Real.log, Real.exp, HSub.hSub, HAdd.hAdd, HPow.hPow, Nat, Asymptotics.IsTheta, Filter.atTop, Erdos416.V

   Proof uses: Lean.Name, 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 erdos_416.variants.Ford :
       let (C₁, C₂, C₃) : ℝ × ℝ × ℝ := answer(sorry)
   …