Theorem: continuousAt_Smooth1 (PrimeNumberTheoremAnd/MediumPNT.lean)

State before:
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
ε : ℝ
εpos : 0 < ε
y : ℝ
ypos : 0 < y
⊢ ContinuousAt (fun x => Smooth1 ψ ε x) y
Tactic:
apply Continuous.continuousAt
State after:
case h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
ε : ℝ
εpos : 0 < ε
y : ℝ
ypos : 0 < y
⊢ Continuous fun x => Smooth1 ψ ε x

State before:
case h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
ε : ℝ
εpos : 0 < ε
y : ℝ
ypos : 0 < y
⊢ Continuous fun x => Smooth1 ψ ε x
Tactic:
unfold Smooth1 DeltaSpike MellinConvolution
State after:
case h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
ε : ℝ
εpos : 0 < ε
y : ℝ
ypos : 0 < y
⊢ Continuous fun x =>
    ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * (fun x => ψ (x ^ (1 / ε)) / ε) (x / y) / ↑y

State before:
case h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
ε : ℝ
εpos : 0 < ε
y : ℝ
ypos : 0 < y
⊢ Continuous fun x =>
    ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * (fun x => ψ (x ^ (1 / ε)) / ε) (x / y) / ↑y
Tactic:
simp only [one_div, ite_mul, one_mul, zero_mul, RCLike.ofReal_real_eq_id, id_eq]
State after:
case h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
ε : ℝ
εpos : 0 < ε
y : ℝ
ypos : 0 < y
⊢ Continuous fun x => ∫ (y : ℝ) in Ioi 0, (if 0 < y ∧ y ≤ 1 then ψ ((x / y) ^ ε⁻¹) / ε else 0) / y

State before:
case h
ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 ψ
ψpos : ∀ (x : ℝ), 0 ≤ ψ x
suppΨ : support ψ ⊆ Icc (1 / 2) 2
mass_one : ∫ (x : ℝ) in Ioi 0, ψ x / x = 1
ε : ℝ
εpos : 0 < ε
y : ℝ
ypos : 0 < y
⊢ Continuous fun x => ∫ (y : ℝ) in Ioi 0, (if 0 < y ∧ y ≤ 1 then ψ ((x / y) ^ ε⁻¹) / ε else 0) / y
Tactic:
sorry
State after:
no goals