Theorem: Smooth1Properties_below (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
⊢ ∃ c, 0 < c ∧ ∀ (x : ℝ), 0 < x → x ≤ 1 - c * ε → Smooth1 Ψ ε x = 1
Tactic:
set c := Real.log 2
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ ∃ c, 0 < c ∧ ∀ (x : ℝ), 0 < x → x ≤ 1 - c * ε → Smooth1 Ψ ε x = 1

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ ∃ c, 0 < c ∧ ∀ (x : ℝ), 0 < x → x ≤ 1 - c * ε → Smooth1 Ψ ε x = 1
Tactic:
use c
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ 0 < c ∧ ∀ (x : ℝ), 0 < x → x ≤ 1 - c * ε → Smooth1 Ψ ε x = 1

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ 0 < c ∧ ∀ (x : ℝ), 0 < x → x ≤ 1 - c * ε → Smooth1 Ψ ε x = 1
Tactic:
constructor
State after:
case h.left
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ 0 < c

case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ ∀ (x : ℝ), 0 < x → x ≤ 1 - c * ε → Smooth1 Ψ ε x = 1

State before:
case h.left
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ 0 < c

case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ ∀ (x : ℝ), 0 < x → x ≤ 1 - c * ε → Smooth1 Ψ ε x = 1
Tactic:
exact log_pos (by norm_num)
State after:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ ∀ (x : ℝ), 0 < x → x ≤ 1 - c * ε → Smooth1 Ψ ε x = 1

State before:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ ∀ (x : ℝ), 0 < x → x ≤ 1 - c * ε → Smooth1 Ψ ε x = 1
Tactic:
intro x xpos hx
State after:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
⊢ Smooth1 Ψ ε x = 1

State before:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
⊢ Smooth1 Ψ ε x = 1
Tactic:
have hx2 := Smooth1Properties_below_aux hx εpos
State after:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ Smooth1 Ψ ε x = 1

State before:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ Smooth1 Ψ ε x = 1
Tactic:
rewrite [← DeltaSpikeMass mass_one εpos]
State after:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ Smooth1 Ψ ε x = ∫ (x : ℝ) in Ioi 0, DeltaSpike (fun x => Ψ x) ε x / x

State before:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ Smooth1 Ψ ε x = ∫ (x : ℝ) in Ioi 0, DeltaSpike (fun x => Ψ x) ε x / x
Tactic:
unfold Smooth1 MellinConvolution
State after:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * DeltaSpike Ψ ε (x / y) / ↑y =
    ∫ (x : ℝ) in Ioi 0, DeltaSpike (fun x => Ψ x) ε x / x

State before:
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * DeltaSpike Ψ ε (x / y) / ↑y =
    ∫ (x : ℝ) in Ioi 0, DeltaSpike (fun x => Ψ x) ε x / x
Tactic:
calc
  _ = ∫ (y : ℝ) in Ioi 0, indicator (Ioc 0 1) (fun y ↦ DeltaSpike Ψ ε (x / y) / ↑y) y := ?_
  _ = ∫ (y : ℝ) in Ioi 0, DeltaSpike Ψ ε (x / y) / y := ?_
  _ = _ := integral_comp_div_I0i_haar (fun y ↦ DeltaSpike Ψ ε y) xpos
State after:
case h.right.calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * DeltaSpike Ψ ε (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) y

case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ ∫ (y : ℝ) in Ioi 0, (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) y =
    ∫ (y : ℝ) in Ioi 0, DeltaSpike Ψ ε (x / y) / y

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
⊢ 1 < 2
Tactic:
norm_num
State after:
no goals

State before:
case h.right.calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ ∫ (y : ℝ) in Ioi 0, (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * DeltaSpike Ψ ε (x / y) / ↑y =
    ∫ (y : ℝ) in Ioi 0, (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) y
Tactic:
rw [setIntegral_congr (by simp)]
State after:
case h.right.calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ EqOn (fun y => (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * DeltaSpike Ψ ε (x / y) / ↑y)
    (fun x_1 => (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) x_1) (Ioi 0)

State before:
case h.right.calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ EqOn (fun y => (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * DeltaSpike Ψ ε (x / y) / ↑y)
    (fun x_1 => (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) x_1) (Ioi 0)
Tactic:
intro y hy
State after:
case h.right.calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * DeltaSpike Ψ ε (x / y) / ↑y) y =
    (fun x_1 => (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) x_1) y

State before:
case h.right.calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) y * DeltaSpike Ψ ε (x / y) / ↑y) y =
    (fun x_1 => (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) x_1) y
Tactic:
by_cases h : y ≤ 1 <;> simp [indicator, mem_Ioi.mp hy, h]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ MeasurableSet (Ioi 0)
Tactic:
simp
State after:
no goals

State before:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ ∫ (y : ℝ) in Ioi 0, (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) y =
    ∫ (y : ℝ) in Ioi 0, DeltaSpike Ψ ε (x / y) / y
Tactic:
rw [setIntegral_congr (by simp)]
State after:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ EqOn (fun y => (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) y)
    (fun x_1 => DeltaSpike Ψ ε (x / x_1) / x_1) (Ioi 0)

State before:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
⊢ EqOn (fun y => (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) y)
    (fun x_1 => DeltaSpike Ψ ε (x / x_1) / x_1) (Ioi 0)
Tactic:
intro y hy
State after:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) y) y =
    (fun x_1 => DeltaSpike Ψ ε (x / x_1) / x_1) y

State before:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => (Ioc 0 1).indicator (fun y => DeltaSpike Ψ ε (x / y) / y) y) y =
    (fun x_1 => DeltaSpike Ψ ε (x / x_1) / x_1) y
Tactic:
simp only [indicator_apply_eq_self, mem_Ioc, not_and, not_le, div_eq_zero_iff]
State after:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
⊢ (0 < y → 1 < y) → DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0

State before:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
⊢ (0 < y → 1 < y) → DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0
Tactic:
intro hy2
State after:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 0 < y → 1 < y
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0

State before:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 0 < y → 1 < y
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0
Tactic:
replace hy2 := hy2 <| mem_Ioi.mp hy
State after:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0

State before:
case h.right.calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0
Tactic:
by_cases h : y = 0
State after:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : y = 0
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0

State before:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : y = 0
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0
Tactic:
right
State after:
case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : y = 0
⊢ y = 0

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0

State before:
case pos.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : y = 0
⊢ y = 0

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0
Tactic:
exact h
State after:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0

State before:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ DeltaSpike Ψ ε (x / y) = 0 ∨ y = 0
Tactic:
left
State after:
case neg.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ DeltaSpike Ψ ε (x / y) = 0

State before:
case neg.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ DeltaSpike Ψ ε (x / y) = 0
Tactic:
apply DeltaSpikeSupport εpos ?_ suppΨ
State after:
case neg.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ x / y ∉ Icc (2 ^ (-ε)) (2 ^ ε)

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ 0 ≤ x / y

State before:
case neg.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ x / y ∉ Icc (2 ^ (-ε)) (2 ^ ε)
Tactic:
simp only [mem_Icc, not_and, not_le]
State after:
case neg.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ 2 ^ (-ε) ≤ x / y → 2 ^ ε < x / y

State before:
case neg.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ 2 ^ (-ε) ≤ x / y → 2 ^ ε < x / y
Tactic:
intro
State after:
case neg.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
a✝ : 2 ^ (-ε) ≤ x / y
⊢ 2 ^ ε < x / y

State before:
case neg.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
a✝ : 2 ^ (-ε) ≤ x / y
⊢ 2 ^ ε < x / y
Tactic:
linarith [(by apply (div_lt_iff (by linarith)).mpr; nlinarith : x / y < 2 ^ (-ε))]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
a✝ : 2 ^ (-ε) ≤ x / y
⊢ x / y < 2 ^ (-ε)
Tactic:
apply (div_lt_iff (by linarith)).mpr
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
a✝ : 2 ^ (-ε) ≤ x / y
⊢ x < 2 ^ (-ε) * y

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
a✝ : 2 ^ (-ε) ≤ x / y
⊢ x < 2 ^ (-ε) * y
Tactic:
nlinarith
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
a✝ : 2 ^ (-ε) ≤ x / y
⊢ 0 < y
Tactic:
linarith
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ 0 ≤ x / y
Tactic:
rw [le_div_iff (by linarith), zero_mul]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ 0 ≤ x

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ 0 ≤ x
Tactic:
exact xpos.le
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
c : ℝ := Real.log 2
x : ℝ
xpos : 0 < x
hx : x ≤ 1 - c * ε
hx2 : x < 2 ^ (-ε)
y : ℝ
hy : y ∈ Ioi 0
hy2 : 1 < y
h : ¬y = 0
⊢ 0 < y
Tactic:
linarith
State after:
no goals