internlm/Lean-Github huggingface dataset:
Theorem: MellinOfPsi
Proof state before:
case h.h₂.calc_3.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
f : ℝ → ℝ := fun x => ‖deriv Ψ x‖
cont : ContinuousOn f (Icc (1 / 2) 2)
a : ℝ
left✝ : a ∈ Icc (1 / 2) 2
max : IsMaxOn f (Icc (1 / 2) 2) a
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
s_ne_zero : s ≠ 0
x : ℝ
hx : x ∈ Icc (1 / 2) 2
f_bound : f x ≤ f a
⊢ ‖(fun x => f x * ‖↑x ^ s‖) x‖ ≤ f a * 2 ^ σ₂
Tactic:
have pow_bound : ‖(x : ℂ) ^ s‖ ≤ 2 ^ σ₂ := by
  rw [Complex.norm_eq_abs, abs_cpow_eq_rpow_re_of_pos (by linarith [mem_Icc.mp hx])]
  have xpos : 0 ≤ x := by linarith [(mem_Icc.mp hx).1]
  have h := rpow_le_rpow xpos (mem_Icc.mp hx).2 (by linarith : 0 ≤ s.re)
  exact le_trans h <| rpow_le_rpow_of_exponent_le (by norm_num) hs.2
Proof state after:
case h.h₂.calc_3.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
f : ℝ → ℝ := fun x => ‖deriv Ψ x‖
cont : ContinuousOn f (Icc (1 / 2) 2)
a : ℝ
left✝ : a ∈ Icc (1 / 2) 2
max : IsMaxOn f (Icc (1 / 2) 2) a
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
s_ne_zero : s ≠ 0
x : ℝ
hx : x ∈ Icc (1 / 2) 2
f_bound : f x ≤ f a
pow_bound : ‖↑x ^ s‖ ≤ 2 ^ σ₂
⊢ ‖(fun x => f x * ‖↑x ^ s‖) x‖ ≤ f a * 2 ^ σ₂
Theorem: MellinOfPsi
Proof state before:
case h.h₂.calc_3.refine_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
f : ℝ → ℝ := fun x => ‖deriv Ψ x‖
cont : ContinuousOn f (Icc (1 / 2) 2)
a : ℝ
left✝ : a ∈ Icc (1 / 2) 2
max : IsMaxOn f (Icc (1 / 2) 2) a
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
s_ne_zero : s ≠ 0
x : ℝ
hx : x ∈ Icc (1 / 2) 2
f_bound : f x ≤ f a
pow_bound : ‖↑x ^ s‖ ≤ 2 ^ σ₂
⊢ ‖(fun x => f x * ‖↑x ^ s‖) x‖ ≤ f a * 2 ^ σ₂
Tactic:
convert mul_le_mul f_bound pow_bound (norm_nonneg _) ?_ using 1 <;> simp [f]
Proof state after:
no goals
Theorem: MellinOfPsi
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
f : ℝ → ℝ := fun x => ‖deriv Ψ x‖
cont : ContinuousOn f (Icc (1 / 2) 2)
a : ℝ
left✝ : a ∈ Icc (1 / 2) 2
max : IsMaxOn f (Icc (1 / 2) 2) a
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
s_ne_zero : s ≠ 0
x : ℝ
hx : x ∈ Icc (1 / 2) 2
f_bound : f x ≤ f a
⊢ ‖↑x ^ s‖ ≤ 2 ^ σ₂
Tactic:
rw [Complex.norm_eq_abs, abs_cpow_eq_rpow_re_of_pos (by linarith [mem_Icc.mp hx])]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
f : ℝ → ℝ := fun x => ‖deriv Ψ x‖
cont : ContinuousOn f (Icc (1 / 2) 2)
a : ℝ
left✝ : a ∈ Icc (1 / 2) 2
max : IsMaxOn f (Icc (1 / 2) 2) a
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
s_ne_zero : s ≠ 0
x : ℝ
hx : x ∈ Icc (1 / 2) 2
f_bound : f x ≤ f a
⊢ x ^ s.re ≤ 2 ^ σ₂
Theorem: MellinOfPsi
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
f : ℝ → ℝ := fun x => ‖deriv Ψ x‖
cont : ContinuousOn f (Icc (1 / 2) 2)
a : ℝ
left✝ : a ∈ Icc (1 / 2) 2
max : IsMaxOn f (Icc (1 / 2) 2) a
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
s_ne_zero : s ≠ 0
x : ℝ
hx : x ∈ Icc (1 / 2) 2
f_bound : f x ≤ f a
⊢ x ^ s.re ≤ 2 ^ σ₂
Tactic:
have xpos : 0 ≤ x := by linarith [(mem_Icc.mp hx).1]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
f : ℝ → ℝ := fun x => ‖deriv Ψ x‖
cont : ContinuousOn f (Icc (1 / 2) 2)
a : ℝ
left✝ : a ∈ Icc (1 / 2) 2
max : IsMaxOn f (Icc (1 / 2) 2) a
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
s_ne_zero : s ≠ 0
x : ℝ
hx : x ∈ Icc (1 / 2) 2
f_bound : f x ≤ f a
xpos : 0 ≤ x
⊢ x ^ s.re ≤ 2 ^ σ₂
Theorem: MellinOfPsi
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
f : ℝ → ℝ := fun x => ‖deriv Ψ x‖
cont : ContinuousOn f (Icc (1 / 2) 2)
a : ℝ
left✝ : a ∈ Icc (1 / 2) 2
max : IsMaxOn f (Icc (1 / 2) 2) a
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
s_ne_zero : s ≠ 0
x : ℝ
hx : x ∈ Icc (1 / 2) 2
f_bound : f x ≤ f a
xpos : 0 ≤ x
⊢ x ^ s.re ≤ 2 ^ σ₂
Tactic:
have h := rpow_le_rpow xpos (mem_Icc.mp hx).2 (by linarith : 0 ≤ s.re)
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
f : ℝ → ℝ := fun x => ‖deriv Ψ x‖
cont : ContinuousOn f (Icc (1 / 2) 2)
a : ℝ
left✝ : a ∈ Icc (1 / 2) 2
max : IsMaxOn f (Icc (1 / 2) 2) a
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
s_ne_zero : s ≠ 0
x : ℝ
hx : x ∈ Icc (1 / 2) 2
f_bound : f x ≤ f a
xpos : 0 ≤ x
h : x ^ s.re ≤ 2 ^ s.re
⊢ x ^ s.re ≤ 2 ^ σ₂
Theorem: MellinOfPsi
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
f : ℝ → ℝ := fun x => ‖deriv Ψ x‖
cont : ContinuousOn f (Icc (1 / 2) 2)
a : ℝ
left✝ : a ∈ Icc (1 / 2) 2
max : IsMaxOn f (Icc (1 / 2) 2) a
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
s_ne_zero : s ≠ 0
x : ℝ
hx : x ∈ Icc (1 / 2) 2
f_bound : f x ≤ f a
xpos : 0 ≤ x
h : x ^ s.re ≤ 2 ^ s.re
⊢ x ^ s.re ≤ 2 ^ σ₂
Tactic:
exact le_trans h <| rpow_le_rpow_of_exponent_le (by norm_num) hs.2
Proof state after:
no goals
Theorem: MellinOfPsi
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
f : ℝ → ℝ := fun x => ‖deriv Ψ x‖
cont : ContinuousOn f (Icc (1 / 2) 2)
a : ℝ
left✝ : a ∈ Icc (1 / 2) 2
max : IsMaxOn f (Icc (1 / 2) 2) a
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
s_ne_zero : s ≠ 0
x : ℝ
hx : x ∈ Icc (1 / 2) 2
f_bound : f x ≤ f a
⊢ 0 < x
Tactic:
linarith [mem_Icc.mp hx]
Proof state after:
no goals
Theorem: MellinOfPsi
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
f : ℝ → ℝ := fun x => ‖deriv Ψ x‖
cont : ContinuousOn f (Icc (1 / 2) 2)
a : ℝ
left✝ : a ∈ Icc (1 / 2) 2
max : IsMaxOn f (Icc (1 / 2) 2) a
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
s_ne_zero : s ≠ 0
x : ℝ
hx : x ∈ Icc (1 / 2) 2
f_bound : f x ≤ f a
⊢ 0 ≤ x
Tactic:
linarith [(mem_Icc.mp hx).1]
Proof state after:
no goals
Theorem: MellinOfPsi
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
f : ℝ → ℝ := fun x => ‖deriv Ψ x‖
cont : ContinuousOn f (Icc (1 / 2) 2)
a : ℝ
left✝ : a ∈ Icc (1 / 2) 2
max : IsMaxOn f (Icc (1 / 2) 2) a
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
s_ne_zero : s ≠ 0
x : ℝ
hx : x ∈ Icc (1 / 2) 2
f_bound : f x ≤ f a
xpos : 0 ≤ x
⊢ 0 ≤ s.re
Tactic:
linarith
Proof state after:
no goals
Theorem: MellinOfPsi
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
f : ℝ → ℝ := fun x => ‖deriv Ψ x‖
cont : ContinuousOn f (Icc (1 / 2) 2)
a : ℝ
left✝ : a ∈ Icc (1 / 2) 2
max : IsMaxOn f (Icc (1 / 2) 2) a
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
s_ne_zero : s ≠ 0
x : ℝ
hx : x ∈ Icc (1 / 2) 2
f_bound : f x ≤ f a
xpos : 0 ≤ x
h : x ^ s.re ≤ 2 ^ s.re
⊢ 1 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: DeltaSpikeMass
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ ∫ (x : ℝ) in Ioi 0, DeltaSpike Ψ ε x / x =
    ∫ (x : ℝ) in Ioi 0, (|1 / ε| * x ^ (1 / ε - 1)) • (fun z => Ψ z / z) (x ^ (1 / ε))
Tactic:
apply setIntegral_congr_ae measurableSet_Ioi
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ ∀ᵐ (x : ℝ), x ∈ Ioi 0 → DeltaSpike Ψ ε x / x = (|1 / ε| * x ^ (1 / ε - 1)) • (fun z => Ψ z / z) (x ^ (1 / ε))
Theorem: DeltaSpikeMass
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ ∀ᵐ (x : ℝ), x ∈ Ioi 0 → DeltaSpike Ψ ε x / x = (|1 / ε| * x ^ (1 / ε - 1)) • (fun z => Ψ z / z) (x ^ (1 / ε))
Tactic:
filter_upwards with x hx
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ DeltaSpike Ψ ε x / x = (|1 / ε| * x ^ (1 / ε - 1)) • (Ψ (x ^ (1 / ε)) / x ^ (1 / ε))
Theorem: DeltaSpikeMass
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ DeltaSpike Ψ ε x / x = (|1 / ε| * x ^ (1 / ε - 1)) • (Ψ (x ^ (1 / ε)) / x ^ (1 / ε))
Tactic:
simp only [mem_Ioi, smul_eq_mul, abs_of_pos (one_div_pos.mpr εpos)]
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ DeltaSpike Ψ ε x / x = 1 / ε * x ^ (1 / ε - 1) * (Ψ (x ^ (1 / ε)) / x ^ (1 / ε))
Theorem: DeltaSpikeMass
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ DeltaSpike Ψ ε x / x = 1 / ε * x ^ (1 / ε - 1) * (Ψ (x ^ (1 / ε)) / x ^ (1 / ε))
Tactic:
symm
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ 1 / ε * x ^ (1 / ε - 1) * (Ψ (x ^ (1 / ε)) / x ^ (1 / ε)) = DeltaSpike Ψ ε x / x
Theorem: DeltaSpikeMass
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ 1 / ε * x ^ (1 / ε - 1) * (Ψ (x ^ (1 / ε)) / x ^ (1 / ε)) = DeltaSpike Ψ ε x / x
Tactic:
calc
_ = (Ψ (x ^ (1 / ε)) / x ^ (1 / ε)) * x ^ (1 / ε - 1) * (1 / ε) := by ring
_ = _ := by rw [rpow_sub hx, rpow_one]
_ = (Ψ (x ^ (1 / ε)) / x ^ (1 / ε) * x ^ (1 / ε) / x) * (1/ ε) := by ring
_ = _ := by rw [div_mul_cancel₀ _ (ne_of_gt (rpow_pos_of_pos hx (1/ε)))]
_ = (Ψ (x ^ (1 / ε)) / ε / x) := by ring
Proof state after:
no goals
Theorem: DeltaSpikeMass
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ 1 / ε * x ^ (1 / ε - 1) * (Ψ (x ^ (1 / ε)) / x ^ (1 / ε)) = Ψ (x ^ (1 / ε)) / x ^ (1 / ε) * x ^ (1 / ε - 1) * (1 / ε)
Tactic:
ring
Proof state after:
no goals
Theorem: DeltaSpikeMass
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ Ψ (x ^ (1 / ε)) / x ^ (1 / ε) * x ^ (1 / ε - 1) * (1 / ε) = ?m.397146
Tactic:
rw [rpow_sub hx, rpow_one]
Proof state after:
no goals
Theorem: DeltaSpikeMass
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ Ψ (x ^ (1 / ε)) / x ^ (1 / ε) * (x ^ (1 / ε) / x) * (1 / ε) =
    Ψ (x ^ (1 / ε)) / x ^ (1 / ε) * x ^ (1 / ε) / x * (1 / ε)
Tactic:
ring
Proof state after:
no goals
Theorem: DeltaSpikeMass
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ Ψ (x ^ (1 / ε)) / x ^ (1 / ε) * x ^ (1 / ε) / x * (1 / ε) = ?m.397745
Tactic:
rw [div_mul_cancel₀ _ (ne_of_gt (rpow_pos_of_pos hx (1/ε)))]
Proof state after:
no goals
Theorem: DeltaSpikeMass
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
x : ℝ
hx : x ∈ Ioi 0
⊢ Ψ (x ^ (1 / ε)) / x * (1 / ε) = Ψ (x ^ (1 / ε)) / ε / x
Tactic:
ring
Proof state after:
no goals
Theorem: DeltaSpikeMass
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ ∫ (x : ℝ) in Ioi 0, (|1 / ε| * x ^ (1 / ε - 1)) • (fun z => Ψ z / z) (x ^ (1 / ε)) = 1
Tactic:
rw [integral_comp_rpow_Ioi (fun z ↦ (Ψ z) / z), ← mass_one]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ 1 / ε ≠ 0
Theorem: DeltaSpikeMass
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
mass_one : ∫ (x : ℝ) in Ioi 0, Ψ x / x = 1
ε : ℝ
εpos : 0 < ε
⊢ 1 / ε ≠ 0
Tactic:
simp only [ne_eq, div_eq_zero_iff, one_ne_zero, εpos.ne', or_self, not_false_eq_true]
Proof state after:
no goals
Theorem: DeltaSpikeSupport_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
⊢ (Function.support fun x => if x < 0 then 0 else DeltaSpike Ψ ε x) ⊆ Icc (2 ^ (-ε)) (2 ^ ε)
Tactic:
unfold DeltaSpike
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
⊢ (Function.support fun x => if x < 0 then 0 else Ψ (x ^ (1 / ε)) / ε) ⊆ Icc (2 ^ (-ε)) (2 ^ ε)
Theorem: DeltaSpikeSupport_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
⊢ (Function.support fun x => if x < 0 then 0 else Ψ (x ^ (1 / ε)) / ε) ⊆ Icc (2 ^ (-ε)) (2 ^ ε)
Tactic:
simp only [one_div, Function.support_subset_iff, ne_eq, ite_eq_left_iff, not_lt, div_eq_zero_iff,
  not_forall, exists_prop, mem_Icc, and_imp]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
⊢ ∀ (x : ℝ), 0 ≤ x → ¬(Ψ (x ^ ε⁻¹) = 0 ∨ ε = 0) → 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Theorem: DeltaSpikeSupport_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
⊢ ∀ (x : ℝ), 0 ≤ x → ¬(Ψ (x ^ ε⁻¹) = 0 ∨ ε = 0) → 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Tactic:
intro x hx h
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : ¬(Ψ (x ^ ε⁻¹) = 0 ∨ ε = 0)
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Theorem: DeltaSpikeSupport_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : ¬(Ψ (x ^ ε⁻¹) = 0 ∨ ε = 0)
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Tactic:
push_neg at h
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Theorem: DeltaSpikeSupport_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Tactic:
have := suppΨ <| Function.mem_support.mpr h.1
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : x ^ ε⁻¹ ∈ Icc (1 / 2) 2
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Theorem: DeltaSpikeSupport_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : x ^ ε⁻¹ ∈ Icc (1 / 2) 2
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Tactic:
simp only [one_div, mem_Icc] at this
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Theorem: DeltaSpikeSupport_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Tactic:
have hl := (le_rpow_inv_iff_of_pos (by norm_num) hx εpos).mp this.1
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
hl : 2⁻¹ ^ ε ≤ x
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Theorem: DeltaSpikeSupport_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
hl : 2⁻¹ ^ ε ≤ x
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Tactic:
rw [inv_rpow (by norm_num) ε, ← rpow_neg (by norm_num)] at hl
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
hl : 2 ^ (-ε) ≤ x
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Theorem: DeltaSpikeSupport_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
hl : 2 ^ (-ε) ≤ x
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
Tactic:
refine ⟨hl, (rpow_inv_le_iff_of_pos ?_ (by norm_num) εpos).mp this.2⟩
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
hl : 2 ^ (-ε) ≤ x
⊢ 0 ≤ x
Theorem: DeltaSpikeSupport_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
hl : 2 ^ (-ε) ≤ x
⊢ 0 ≤ x
Tactic:
linarith [(by apply rpow_nonneg (by norm_num) : 0 ≤ (2 : ℝ) ^ (-ε))]
Proof state after:
no goals
Theorem: DeltaSpikeSupport_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
⊢ 0 ≤ 2⁻¹
Tactic:
norm_num
Proof state after:
no goals
Theorem: DeltaSpikeSupport_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
hl : 2⁻¹ ^ ε ≤ x
⊢ 0 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: DeltaSpikeSupport_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
hl : (2 ^ ε)⁻¹ ≤ x
⊢ 0 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: DeltaSpikeSupport_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
hl : 2 ^ (-ε) ≤ x
⊢ 0 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: DeltaSpikeSupport_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
hl : 2 ^ (-ε) ≤ x
⊢ 0 ≤ 2 ^ (-ε)
Tactic:
apply rpow_nonneg (by norm_num)
Proof state after:
no goals
Theorem: DeltaSpikeSupport'
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε x : ℝ
εpos : 0 < ε
xnonneg : 0 ≤ x
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
⊢ DeltaSpike Ψ ε x ≠ 0 → x ∈ Icc (2 ^ (-ε)) (2 ^ ε)
Tactic:
intro h
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε x : ℝ
εpos : 0 < ε
xnonneg : 0 ≤ x
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
h : DeltaSpike Ψ ε x ≠ 0
⊢ x ∈ Icc (2 ^ (-ε)) (2 ^ ε)
Theorem: DeltaSpikeSupport'
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε x : ℝ
εpos : 0 < ε
xnonneg : 0 ≤ x
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
h : DeltaSpike Ψ ε x ≠ 0
⊢ x ∈ Icc (2 ^ (-ε)) (2 ^ ε)
Tactic:
have : (fun x ↦ if x < 0 then 0 else DeltaSpike Ψ ε x) x = DeltaSpike Ψ ε x := by simp [xnonneg]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε x : ℝ
εpos : 0 < ε
xnonneg : 0 ≤ x
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
h : DeltaSpike Ψ ε x ≠ 0
this : (fun x => if x < 0 then 0 else DeltaSpike Ψ ε x) x = DeltaSpike Ψ ε x
⊢ x ∈ Icc (2 ^ (-ε)) (2 ^ ε)
Theorem: DeltaSpikeSupport'
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε x : ℝ
εpos : 0 < ε
xnonneg : 0 ≤ x
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
h : DeltaSpike Ψ ε x ≠ 0
this : (fun x => if x < 0 then 0 else DeltaSpike Ψ ε x) x = DeltaSpike Ψ ε x
⊢ x ∈ Icc (2 ^ (-ε)) (2 ^ ε)
Tactic:
rw [← this] at h
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε x : ℝ
εpos : 0 < ε
xnonneg : 0 ≤ x
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
h : (fun x => if x < 0 then 0 else DeltaSpike Ψ ε x) x ≠ 0
this : (fun x => if x < 0 then 0 else DeltaSpike Ψ ε x) x = DeltaSpike Ψ ε x
⊢ x ∈ Icc (2 ^ (-ε)) (2 ^ ε)
Theorem: DeltaSpikeSupport'
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε x : ℝ
εpos : 0 < ε
xnonneg : 0 ≤ x
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
h : (fun x => if x < 0 then 0 else DeltaSpike Ψ ε x) x ≠ 0
this : (fun x => if x < 0 then 0 else DeltaSpike Ψ ε x) x = DeltaSpike Ψ ε x
⊢ x ∈ Icc (2 ^ (-ε)) (2 ^ ε)
Tactic:
exact (Function.support_subset_iff.mp <| DeltaSpikeSupport_aux εpos suppΨ) _ h
Proof state after:
no goals
Theorem: DeltaSpikeSupport'
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε x : ℝ
εpos : 0 < ε
xnonneg : 0 ≤ x
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
h : DeltaSpike Ψ ε x ≠ 0
⊢ (fun x => if x < 0 then 0 else DeltaSpike Ψ ε x) x = DeltaSpike Ψ ε x
Tactic:
simp [xnonneg]
Proof state after:
no goals
Theorem: DeltaSpikeSupport
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε x : ℝ
εpos : 0 < ε
xnonneg : 0 ≤ x
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
⊢ x ∉ Icc (2 ^ (-ε)) (2 ^ ε) → DeltaSpike Ψ ε x = 0
Tactic:
contrapose!
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε x : ℝ
εpos : 0 < ε
xnonneg : 0 ≤ x
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
⊢ DeltaSpike Ψ ε x ≠ 0 → x ∈ Icc (2 ^ (-ε)) (2 ^ ε)
Theorem: DeltaSpikeSupport
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε x : ℝ
εpos : 0 < ε
xnonneg : 0 ≤ x
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
⊢ DeltaSpike Ψ ε x ≠ 0 → x ∈ Icc (2 ^ (-ε)) (2 ^ ε)
Tactic:
exact DeltaSpikeSupport' εpos xnonneg suppΨ
Proof state after:
no goals
Theorem: DeltaSpikeContinuous
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
diffΨ : ContDiff ℝ 1 Ψ
⊢ Continuous fun x => DeltaSpike Ψ ε x
Tactic:
apply diffΨ.continuous.comp (g := Ψ) _ |>.div_const
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
diffΨ : ContDiff ℝ 1 Ψ
⊢ Continuous fun x => x ^ (1 / ε)
Theorem: DeltaSpikeContinuous
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
diffΨ : ContDiff ℝ 1 Ψ
⊢ Continuous fun x => x ^ (1 / ε)
Tactic:
exact continuous_id.rpow_const fun _ ↦ Or.inr <| div_nonneg (by norm_num) εpos.le
Proof state after:
no goals
Theorem: DeltaSpikeContinuous
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
diffΨ : ContDiff ℝ 1 Ψ
x✝ : ℝ
⊢ 0 ≤ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: MellinOfDeltaSpike
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
⊢ 𝓜 (fun x => ↑(DeltaSpike Ψ ε x)) s = 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
unfold MellinTransform DeltaSpike
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
⊢ ∫ (x : ℝ) in Ioi 0, (fun x => ↑(Ψ (x ^ (1 / ε)) / ε)) x * ↑x ^ (s - 1) =
    ∫ (x : ℝ) in Ioi 0, (fun x => ↑(Ψ x)) x * ↑x ^ (↑ε * s - 1)