internlm/Lean-Github huggingface dataset:
Theorem: MellinOfPsi
Proof state before:
case intro.intro
𝕂 : 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
⊢ (fun s => ‖𝓜 (fun x => ↑(Ψ x)) s‖) =O[𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}] fun s => 1 / ‖s‖
Tactic:
rw [Asymptotics.isBigO_iff]
Proof state after:
case intro.intro
𝕂 : 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
⊢ ∃ c, ∀ᶠ (x : ℂ) in 𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}, ‖‖𝓜 (fun x => ↑(Ψ x)) x‖‖ ≤ c * ‖1 / ‖x‖‖
Theorem: MellinOfPsi
Proof state before:
case intro.intro
𝕂 : 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
⊢ ∃ c, ∀ᶠ (x : ℂ) in 𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}, ‖‖𝓜 (fun x => ↑(Ψ x)) x‖‖ ≤ c * ‖1 / ‖x‖‖
Tactic:
use f a * 2 ^ σ₂ * (3 / 2)
Proof state after:
case h
𝕂 : 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
⊢ ∀ᶠ (x : ℂ) in 𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}, ‖‖𝓜 (fun x => ↑(Ψ x)) x‖‖ ≤ f a * 2 ^ σ₂ * (3 / 2) * ‖1 / ‖x‖‖
Theorem: MellinOfPsi
Proof state before:
case h
𝕂 : 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
⊢ ∀ᶠ (x : ℂ) in 𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}, ‖‖𝓜 (fun x => ↑(Ψ x)) x‖‖ ≤ f a * 2 ^ σ₂ * (3 / 2) * ‖1 / ‖x‖‖
Tactic:
filter_upwards [mem_within_strip σ₁ σ₂] with s hs
Proof state after:
case h
𝕂 : 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 ≤ σ₂
⊢ ‖‖𝓜 (fun x => ↑(Ψ x)) s‖‖ ≤ f a * 2 ^ σ₂ * (3 / 2) * ‖1 / ‖s‖‖
Theorem: MellinOfPsi
Proof state before:
case h
𝕂 : 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 ≤ σ₂
⊢ ‖‖𝓜 (fun x => ↑(Ψ x)) s‖‖ ≤ f a * 2 ^ σ₂ * (3 / 2) * ‖1 / ‖s‖‖
Tactic:
have s_ne_zero: s ≠ 0 := fun h ↦ by linarith [zero_re ▸ h ▸ hs.1]
Proof state after:
case h
𝕂 : 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
⊢ ‖‖𝓜 (fun x => ↑(Ψ x)) s‖‖ ≤ f a * 2 ^ σ₂ * (3 / 2) * ‖1 / ‖s‖‖
Theorem: MellinOfPsi
Proof state before:
case h
𝕂 : 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
⊢ ‖‖𝓜 (fun x => ↑(Ψ x)) s‖‖ ≤ f a * 2 ^ σ₂ * (3 / 2) * ‖1 / ‖s‖‖
Tactic:
simp only [MellinTransform, f, MellinOfPsi_aux diffΨ suppΨ s_ne_zero, norm_norm, norm_mul]
Proof state after:
case h
𝕂 : 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
⊢ ‖-(1 / s)‖ * ‖∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s‖ ≤ ‖deriv Ψ a‖ * 2 ^ σ₂ * (3 / 2) * ‖1 / ‖s‖‖
Theorem: MellinOfPsi
Proof state before:
case h
𝕂 : 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
⊢ ‖-(1 / s)‖ * ‖∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s‖ ≤ ‖deriv Ψ a‖ * 2 ^ σ₂ * (3 / 2) * ‖1 / ‖s‖‖
Tactic:
conv => rhs; rw [mul_comm]
Proof state after:
case h
𝕂 : 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
⊢ ‖-(1 / s)‖ * ‖∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s‖ ≤ ‖1 / ‖s‖‖ * (‖deriv Ψ a‖ * 2 ^ σ₂ * (3 / 2))
Theorem: MellinOfPsi
Proof state before:
case h
𝕂 : 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
⊢ ‖-(1 / s)‖ * ‖∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s‖ ≤ ‖1 / ‖s‖‖ * (‖deriv Ψ a‖ * 2 ^ σ₂ * (3 / 2))
Tactic:
gcongr
Proof state after:
case h.h₁
𝕂 : 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
⊢ ‖-(1 / s)‖ ≤ ‖1 / ‖s‖‖

case h.h₂
𝕂 : 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 : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s‖ ≤ ‖deriv Ψ a‖ * 2 ^ σ₂ * (3 / 2)
Theorem: MellinOfPsi
Proof state before:
case h.h₁
𝕂 : 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
⊢ ‖-(1 / s)‖ ≤ ‖1 / ‖s‖‖

case h.h₂
𝕂 : 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 : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s‖ ≤ ‖deriv Ψ a‖ * 2 ^ σ₂ * (3 / 2)
Tactic:
simp
Proof state after:
case h.h₂
𝕂 : 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 : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s‖ ≤ ‖deriv Ψ a‖ * 2 ^ σ₂ * (3 / 2)
Theorem: MellinOfPsi
Proof state before:
case h.h₂
𝕂 : 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 : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s‖ ≤ ‖deriv Ψ a‖ * 2 ^ σ₂ * (3 / 2)
Tactic:
calc
  _ ≤ ∫ (x : ℝ) in Ioi 0, ‖(deriv Ψ x * (x : ℂ) ^ s)‖ := ?_
  _ = ∫ (x : ℝ) in Icc (1 / 2) 2, ‖(deriv Ψ x * (x : ℂ) ^ s)‖ := ?_
  _ ≤ ‖∫ (x : ℝ) in Icc (1 / 2) 2, ‖(deriv Ψ x * (x : ℂ) ^ s)‖‖ := le_abs_self _
  _ ≤ _ := ?_
Proof state after:
case h.h₂.calc_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 : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s‖ ≤ ∫ (x : ℝ) in Ioi 0, ‖↑(deriv Ψ x) * ↑x ^ s‖

case h.h₂.calc_2
𝕂 : 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 : ℝ) in Ioi 0, ‖↑(deriv Ψ x) * ↑x ^ s‖ = ∫ (x : ℝ) in Icc (1 / 2) 2, ‖↑(deriv Ψ x) * ↑x ^ s‖

case h.h₂.calc_3
𝕂 : 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 : ℝ) in Icc (1 / 2) 2, ‖↑(deriv Ψ x) * ↑x ^ s‖‖ ≤ ‖deriv Ψ a‖ * 2 ^ σ₂ * (3 / 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‖
⊢ Continuous Norm.norm
Tactic:
continuity
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‖
⊢ 1 ≤ 1
Tactic:
norm_num
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)
⊢ (Icc (1 / 2) 2).Nonempty
Tactic:
norm_num
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 ≤ σ₂
h : s = 0
⊢ False
Tactic:
linarith [zero_re ▸ h ▸ hs.1]
Proof state after:
no goals
Theorem: MellinOfPsi
Proof state before:
case h.h₂.calc_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 : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s‖ ≤ ∫ (x : ℝ) in Ioi 0, ‖↑(deriv Ψ x) * ↑x ^ s‖
Tactic:
simp_rw [norm_integral_le_integral_norm]
Proof state after:
no goals
Theorem: MellinOfPsi
Proof state before:
case h.h₂.calc_2
𝕂 : 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 : ℝ) in Ioi 0, ‖↑(deriv Ψ x) * ↑x ^ s‖ = ∫ (x : ℝ) in Icc (1 / 2) 2, ‖↑(deriv Ψ x) * ↑x ^ s‖
Tactic:
apply SetIntegral.integral_eq_integral_inter_of_support_subset_Icc
Proof state after:
case h.h₂.calc_2.h
𝕂 : 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
⊢ (Function.support fun x => ‖↑(deriv Ψ x) * ↑x ^ s‖) ⊆ Icc (1 / 2) 2

case h.h₂.calc_2.hs
𝕂 : 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
⊢ Icc (1 / 2) 2 ⊆ Ioi 0
Theorem: MellinOfPsi
Proof state before:
case h.h₂.calc_2.h
𝕂 : 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
⊢ (Function.support fun x => ‖↑(deriv Ψ x) * ↑x ^ s‖) ⊆ Icc (1 / 2) 2
Tactic:
simp only [Function.support_abs, Function.support_mul, Function.support_ofReal]
Proof state after:
case h.h₂.calc_2.h
𝕂 : 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
⊢ ((Function.support fun x => deriv Ψ x) ∩ Function.support fun x => ↑x ^ s) ⊆ Icc (1 / 2) 2
Theorem: MellinOfPsi
Proof state before:
case h.h₂.calc_2.h
𝕂 : 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
⊢ ((Function.support fun x => deriv Ψ x) ∩ Function.support fun x => ↑x ^ s) ⊆ Icc (1 / 2) 2
Tactic:
apply subset_trans (by apply inter_subset_left) <| Function.support_deriv_subset_Icc suppΨ
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
⊢ ((Function.support fun x => deriv Ψ x) ∩ Function.support fun x => ↑x ^ s) ⊆ Function.support (deriv Ψ)
Tactic:
apply inter_subset_left
Proof state after:
no goals
Theorem: MellinOfPsi
Proof state before:
case h.h₂.calc_2.hs
𝕂 : 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
⊢ Icc (1 / 2) 2 ⊆ Ioi 0
Tactic:
exact (Icc_subset_Ioi_iff (by norm_num)).mpr (by norm_num)
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
⊢ 1 / 2 ≤ 2
Tactic:
norm_num
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
⊢ 0 < 1 / 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: MellinOfPsi
Proof state before:
case h.h₂.calc_3
𝕂 : 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 : ℝ) in Icc (1 / 2) 2, ‖↑(deriv Ψ x) * ↑x ^ s‖‖ ≤ ‖deriv Ψ a‖ * 2 ^ σ₂ * (3 / 2)
Tactic:
have := intervalIntegral.norm_integral_le_of_norm_le_const' (C := f a * 2 ^ σ₂)
  (f := fun x ↦ f x * ‖(x : ℂ) ^ s‖) (a := (1 / 2 : ℝ)) ( b := 2) (by norm_num) ?_
Proof state after:
case h.h₂.calc_3.refine_2
𝕂 : 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
this : ‖∫ (x : ℝ) in 1 / 2 ..2, (fun x => f x * ‖↑x ^ s‖) x‖ ≤ f a * 2 ^ σ₂ * |2 - 1 / 2|
⊢ ‖∫ (x : ℝ) in Icc (1 / 2) 2, ‖↑(deriv Ψ x) * ↑x ^ s‖‖ ≤ ‖deriv Ψ a‖ * 2 ^ σ₂ * (3 / 2)

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 ∈ Icc (1 / 2) 2, ‖(fun x => f x * ‖↑x ^ s‖) x‖ ≤ f a * 2 ^ σ₂
Theorem: MellinOfPsi
Proof state before:
case h.h₂.calc_3.refine_2
𝕂 : 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
this : ‖∫ (x : ℝ) in 1 / 2 ..2, (fun x => f x * ‖↑x ^ s‖) x‖ ≤ f a * 2 ^ σ₂ * |2 - 1 / 2|
⊢ ‖∫ (x : ℝ) in Icc (1 / 2) 2, ‖↑(deriv Ψ x) * ↑x ^ s‖‖ ≤ ‖deriv Ψ a‖ * 2 ^ σ₂ * (3 / 2)
Tactic:
simp only [Real.norm_eq_abs, Complex.norm_eq_abs, abs_ofReal, map_mul] at this ⊢
Proof state after:
case h.h₂.calc_3.refine_2
𝕂 : 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
this : |∫ (x : ℝ) in 1 / 2 ..2, f x * Complex.abs (↑x ^ s)| ≤ f a * 2 ^ σ₂ * |2 - 1 / 2|
⊢ |∫ (x : ℝ) in Icc (1 / 2) 2, |deriv Ψ x| * Complex.abs (↑x ^ s)| ≤ |deriv Ψ a| * 2 ^ σ₂ * (3 / 2)
Theorem: MellinOfPsi
Proof state before:
case h.h₂.calc_3.refine_2
𝕂 : 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
this : |∫ (x : ℝ) in 1 / 2 ..2, f x * Complex.abs (↑x ^ s)| ≤ f a * 2 ^ σ₂ * |2 - 1 / 2|
⊢ |∫ (x : ℝ) in Icc (1 / 2) 2, |deriv Ψ x| * Complex.abs (↑x ^ s)| ≤ |deriv Ψ a| * 2 ^ σ₂ * (3 / 2)
Tactic:
rwa [(by norm_num: |(2 : ℝ) - 1 / 2| = 3 / 2),
    intervalIntegral.integral_of_le (by norm_num), ← integral_Icc_eq_integral_Ioc] at this
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
this : |∫ (x : ℝ) in 1 / 2 ..2, f x * Complex.abs (↑x ^ s)| ≤ f a * 2 ^ σ₂ * |2 - 1 / 2|
⊢ |2 - 1 / 2| = 3 / 2
Tactic:
norm_num
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
this : |∫ (x : ℝ) in 1 / 2 ..2, f x * Complex.abs (↑x ^ s)| ≤ f a * 2 ^ σ₂ * (3 / 2)
⊢ 1 / 2 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
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 ∈ Icc (1 / 2) 2, ‖(fun x => f x * ‖↑x ^ s‖) x‖ ≤ f a * 2 ^ σ₂
Tactic:
intro x hx
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
⊢ ‖(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
⊢ ‖(fun x => f x * ‖↑x ^ s‖) x‖ ≤ f a * 2 ^ σ₂
Tactic:
have f_bound := isMaxOn_iff.mp max x hx
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
⊢ ‖(fun x => f x * ‖↑x ^ s‖) x‖ ≤ f a * 2 ^ σ₂