internlm/Lean-Github huggingface dataset:
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ ↑(Λ n) * (1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I))) =
    ↑(Λ n) * ↑(Smooth1 ψ ε (↑n / X))
Tactic:
congr
Proof state after:
case neg.e_a
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 1 / (2 * ↑π) * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))
Tactic:
rw [(by rw [div_mul]; simp : 1 / (2 * π) = 1 / (2 * π * I) * I), mul_assoc]
Proof state after:
case neg.e_a
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I))) =
    ↑(Smooth1 ψ ε (↑n / X))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I) * (↑n / ↑X) ^ (-(2 + ↑t * I))) =
    ↑(Smooth1 ψ ε (↑n / X))
Tactic:
conv => lhs; rhs; rhs; rhs; intro t; rw [mul_comm]; norm_cast
Proof state after:
case neg.e_a
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), ↑(↑n / X) ^ (-(2 + ↑t * I)) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), ↑(↑n / X) ^ (-(2 + ↑t * I)) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))
Tactic:
have := MellinInversion 2 (f := fun x ↦ (Smooth1 ψ ε x : ℂ)) (x := n / X)
  (by simp [n_pos, X_pos]) ?_ ?_ ?_
Proof state after:
case neg.e_a.refine_4
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
this : MellinInverseTransform (𝓜 fun x => ↑(Smooth1 ψ ε x)) 2 (↑n / X) = (fun x => ↑(Smooth1 ψ ε x)) (↑n / X)
⊢ 1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), ↑(↑n / X) ^ (-(2 + ↑t * I)) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))

case neg.e_a.refine_1
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MellinConvergent (fun x => ↑(Smooth1 ψ ε x)) ↑2

case neg.e_a.refine_2
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ VerticalIntegrable (mellin fun x => ↑(Smooth1 ψ ε x)) 2 MeasureTheory.volume

case neg.e_a.refine_3
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ ContinuousAt (fun x => ↑(Smooth1 ψ ε x)) (↑n / X)
Theorem: SmoothedChebyshevDirichlet
Proof state before:
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
⊢ 0 < n
Tactic:
simpa only [n_zero, gt_iff_lt, false_or] using (Nat.eq_zero_or_pos n)
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
Proof state before:
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 1 / (2 * ↑π) = 1 / (2 * ↑π * I) * I
Tactic:
rw [div_mul]
Proof state after:
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 1 / (2 * ↑π) = 1 / (2 * ↑π * I / I)
Theorem: SmoothedChebyshevDirichlet
Proof state before:
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 1 / (2 * ↑π) = 1 / (2 * ↑π * I / I)
Tactic:
simp
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
Proof state before:
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 0 < ↑n / X
Tactic:
simp [n_pos, X_pos]
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a.refine_4
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
this : MellinInverseTransform (𝓜 fun x => ↑(Smooth1 ψ ε x)) 2 (↑n / X) = (fun x => ↑(Smooth1 ψ ε x)) (↑n / X)
⊢ 1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), ↑(↑n / X) ^ (-(2 + ↑t * I)) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))
Tactic:
beta_reduce at this
Proof state after:
case neg.e_a.refine_4
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
this : MellinInverseTransform (𝓜 fun x => ↑(Smooth1 ψ ε x)) 2 (↑n / X) = ↑(Smooth1 ψ ε (↑n / X))
⊢ 1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), ↑(↑n / X) ^ (-(2 + ↑t * I)) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a.refine_4
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
this : MellinInverseTransform (𝓜 fun x => ↑(Smooth1 ψ ε x)) 2 (↑n / X) = ↑(Smooth1 ψ ε (↑n / X))
⊢ 1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), ↑(↑n / X) ^ (-(2 + ↑t * I)) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))
Tactic:
dsimp [MellinInverseTransform, VerticalIntegral] at this
Proof state after:
case neg.e_a.refine_4
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
this :
  1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), ↑(↑n / X) ^ (-(2 + ↑t * I)) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))
⊢ 1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), ↑(↑n / X) ^ (-(2 + ↑t * I)) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a.refine_4
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
this :
  1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), ↑(↑n / X) ^ (-(2 + ↑t * I)) * 𝓜 (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))
⊢ 1 / (2 * ↑π * I) * (I * ∫ (t : ℝ), ↑(↑n / X) ^ (-(2 + ↑t * I)) * mellin (fun x => ↑(Smooth1 ψ ε x)) (2 + ↑t * I)) =
    ↑(Smooth1 ψ ε (↑n / X))
Tactic:
rw [← MellinTransform_eq, this]
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a.refine_1
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MellinConvergent (fun x => ↑(Smooth1 ψ ε x)) ↑2
Tactic:
dsimp [MellinConvergent]
Proof state after:
case neg.e_a.refine_1
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.IntegrableOn (fun t => ↑t ^ (2 - 1) * ↑(Smooth1 ψ ε t)) (Ioi 0) MeasureTheory.volume
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a.refine_1
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.IntegrableOn (fun t => ↑t ^ (2 - 1) * ↑(Smooth1 ψ ε t)) (Ioi 0) MeasureTheory.volume
Tactic:
norm_num
Proof state after:
case neg.e_a.refine_1
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.IntegrableOn (fun t => ↑t * ↑(Smooth1 ψ ε t)) (Ioi 0) MeasureTheory.volume
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a.refine_1
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.IntegrableOn (fun t => ↑t * ↑(Smooth1 ψ ε t)) (Ioi 0) MeasureTheory.volume
Tactic:
norm_cast
Proof state after:
case neg.e_a.refine_1
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.IntegrableOn (fun t => ↑(t * Smooth1 ψ ε t)) (Ioi 0) MeasureTheory.volume
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a.refine_1
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.IntegrableOn (fun t => ↑(t * Smooth1 ψ ε t)) (Ioi 0) MeasureTheory.volume
Tactic:
exact (integrable_x_mul_Smooth1 diffΨ ψpos suppΨ mass_one ε εpos).ofReal
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a.refine_2
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ VerticalIntegrable (mellin fun x => ↑(Smooth1 ψ ε x)) 2 MeasureTheory.volume
Tactic:
dsimp [VerticalIntegrable, mellin]
Proof state after:
case neg.e_a.refine_2
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.Integrable (fun y => ∫ (t : ℝ) in Ioi 0, ↑t ^ (2 + ↑y * I - 1) * ↑(Smooth1 ψ ε t)) MeasureTheory.volume
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a.refine_2
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.Integrable (fun y => ∫ (t : ℝ) in Ioi 0, ↑t ^ (2 + ↑y * I - 1) * ↑(Smooth1 ψ ε t)) MeasureTheory.volume
Tactic:
ring_nf
Proof state after:
case neg.e_a.refine_2
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.Integrable (fun y => ∫ (t : ℝ) in Ioi 0, ↑t ^ (1 + ↑y * I) * ↑(Smooth1 ψ ε t)) MeasureTheory.volume
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a.refine_2
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ MeasureTheory.Integrable (fun y => ∫ (t : ℝ) in Ioi 0, ↑t ^ (1 + ↑y * I) * ↑(Smooth1 ψ ε t)) MeasureTheory.volume
Tactic:
exact vertical_integrable_Smooth1 diffΨ ψpos suppΨ mass_one ε εpos
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a.refine_3
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ ContinuousAt (fun x => ↑(Smooth1 ψ ε x)) (↑n / X)
Tactic:
refine ContinuousAt.comp (g := ofReal) RCLike.continuous_ofReal.continuousAt ?_
Proof state after:
case neg.e_a.refine_3
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ ContinuousAt (fun x => Smooth1 ψ ε x) (↑n / X)
Theorem: SmoothedChebyshevDirichlet
Proof state before:
case neg.e_a.refine_3
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ ContinuousAt (fun x => Smooth1 ψ ε x) (↑n / X)
Tactic:
exact continuousAt_Smooth1 diffΨ ψpos suppΨ mass_one ε εpos (n / X) (by positivity)
Proof state after:
no goals
Theorem: SmoothedChebyshevDirichlet
Proof state before:
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
X_pos : 0 < X
ε : ℝ
εpos : 0 < ε
n : ℕ
n_zero : ¬n = 0
n_pos : 0 < n
⊢ 0 < ↑n / X
Tactic:
positivity
Proof state after:
no goals
Theorem: SmoothedChebyshevClose
Proof state before:
ψ : ℝ → ℝ
ε : ℝ
ε_pos : 0 < ε
suppΨ : support ψ ⊆ Icc (1 / 2) 2
Ψnonneg : ∀ x > 0, 0 ≤ ψ x
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
X : ℝ
⊢ (fun X => ‖SmoothedChebyshev ψ ε X - ↑(ChebyshevPsi X)‖) =O[atTop] fun X => ε * X * X.log
Tactic:
sorry
Proof state after:
no goals
Theorem: MediumPNT
Proof state before:
⊢ ∃ c, ∃ (_ : c > 0), (ChebyshevPsi - id) =O[atTop] fun x => x * rexp (-c * x.log ^ (1 / 18))
Tactic:
sorry
Proof state after:
no goals
Theorem: Asymptotics.isBigO_of_isBigOUniformly
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
i : ι
hi : i ∈ s
⊢ (fun x => f (i, x)) =O[l] g
Tactic:
obtain ⟨C, hC⟩ := h.bound
Proof state after:
case intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
⊢ (fun x => f (i, x)) =O[l] g
Theorem: Asymptotics.isBigO_of_isBigOUniformly
Proof state before:
case intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
⊢ (fun x => f (i, x)) =O[l] g
Tactic:
obtain ⟨t, htl, ht⟩ := hC.exists_mem
Proof state after:
case intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
⊢ (fun x => f (i, x)) =O[l] g
Theorem: Asymptotics.isBigO_of_isBigOUniformly
Proof state before:
case intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
⊢ (fun x => f (i, x)) =O[l] g
Tactic:
obtain ⟨u, hu, v, hv, huv⟩ := Filter.mem_prod_iff.mp htl
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ (fun x => f (i, x)) =O[l] g
Theorem: Asymptotics.isBigO_of_isBigOUniformly
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ (fun x => f (i, x)) =O[l] g
Tactic:
refine isBigO_iff.mpr ⟨C, Filter.eventually_iff_exists_mem.mpr ⟨v, hv, ?_⟩⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ ∀ y ∈ v, ‖f (i, y)‖ ≤ C * ‖g y‖
Theorem: Asymptotics.isBigO_of_isBigOUniformly
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ ∀ y ∈ v, ‖f (i, y)‖ ≤ C * ‖g y‖
Tactic:
exact fun y hy ↦ ht _ <| huv ⟨hu hi, hy⟩
Proof state after:
no goals
Theorem: Asymptotics.isBigO_rev_of_isBigOUniformly_rev
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : (g ∘ Prod.snd) =O[𝓟 s ×ˢ l] f
i : ι
hi : i ∈ s
⊢ g =O[l] fun x => f (i, x)
Tactic:
obtain ⟨C, hC⟩ := h.bound
Proof state after:
case intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : (g ∘ Prod.snd) =O[𝓟 s ×ˢ l] f
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖(g ∘ Prod.snd) x‖ ≤ C * ‖f x‖
⊢ g =O[l] fun x => f (i, x)
Theorem: Asymptotics.isBigO_rev_of_isBigOUniformly_rev
Proof state before:
case intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : (g ∘ Prod.snd) =O[𝓟 s ×ˢ l] f
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖(g ∘ Prod.snd) x‖ ≤ C * ‖f x‖
⊢ g =O[l] fun x => f (i, x)
Tactic:
obtain ⟨t, htl, ht⟩ := hC.exists_mem
Proof state after:
case intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : (g ∘ Prod.snd) =O[𝓟 s ×ˢ l] f
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖(g ∘ Prod.snd) x‖ ≤ C * ‖f x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖(g ∘ Prod.snd) y‖ ≤ C * ‖f y‖
⊢ g =O[l] fun x => f (i, x)
Theorem: Asymptotics.isBigO_rev_of_isBigOUniformly_rev
Proof state before:
case intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : (g ∘ Prod.snd) =O[𝓟 s ×ˢ l] f
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖(g ∘ Prod.snd) x‖ ≤ C * ‖f x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖(g ∘ Prod.snd) y‖ ≤ C * ‖f y‖
⊢ g =O[l] fun x => f (i, x)
Tactic:
obtain ⟨u, hu, v, hv, huv⟩ := Filter.mem_prod_iff.mp htl
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : (g ∘ Prod.snd) =O[𝓟 s ×ˢ l] f
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖(g ∘ Prod.snd) x‖ ≤ C * ‖f x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖(g ∘ Prod.snd) y‖ ≤ C * ‖f y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ g =O[l] fun x => f (i, x)
Theorem: Asymptotics.isBigO_rev_of_isBigOUniformly_rev
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : (g ∘ Prod.snd) =O[𝓟 s ×ˢ l] f
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖(g ∘ Prod.snd) x‖ ≤ C * ‖f x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖(g ∘ Prod.snd) y‖ ≤ C * ‖f y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ g =O[l] fun x => f (i, x)
Tactic:
refine isBigO_iff.mpr ⟨C, Filter.eventually_iff_exists_mem.mpr ⟨v, hv, ?_⟩⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : (g ∘ Prod.snd) =O[𝓟 s ×ˢ l] f
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖(g ∘ Prod.snd) x‖ ≤ C * ‖f x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖(g ∘ Prod.snd) y‖ ≤ C * ‖f y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ ∀ y ∈ v, ‖g y‖ ≤ C * ‖f (i, y)‖
Theorem: Asymptotics.isBigO_rev_of_isBigOUniformly_rev
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝¹ : Norm E
inst✝ : Norm F
f : ι × α → E
g : α → F
l : Filter α
h : (g ∘ Prod.snd) =O[𝓟 s ×ˢ l] f
i : ι
hi : i ∈ s
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖(g ∘ Prod.snd) x‖ ≤ C * ‖f x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖(g ∘ Prod.snd) y‖ ≤ C * ‖f y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ ∀ y ∈ v, ‖g y‖ ≤ C * ‖f (i, y)‖
Tactic:
exact fun y hy ↦ ht (i, y) <| huv ⟨hu hi, hy⟩
Proof state after:
no goals