Theorem: MellinOfPsi (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
⊢ (fun s => ‖𝓜 (fun x => ↑(Ψ x)) s‖) =O[𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}] fun s => 1 / ‖s‖
Tactic:
let f := fun (x : ℝ) ↦ ‖deriv Ψ x‖
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‖
⊢ (fun s => ‖𝓜 (fun x => ↑(Ψ x)) s‖) =O[𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}] fun s => 1 / ‖s‖

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‖
⊢ (fun s => ‖𝓜 (fun x => ↑(Ψ x)) s‖) =O[𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}] fun s => 1 / ‖s‖
Tactic:
have cont : ContinuousOn f (Icc (1 / 2) 2) :=
  (Continuous.comp (by continuity) <| diffΨ.continuous_deriv (by norm_num)).continuousOn
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)
⊢ (fun s => ‖𝓜 (fun x => ↑(Ψ x)) s‖) =O[𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}] fun s => 1 / ‖s‖

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)
⊢ (fun s => ‖𝓜 (fun x => ↑(Ψ x)) s‖) =O[𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}] fun s => 1 / ‖s‖
Tactic:
obtain ⟨a, _, max⟩ := isCompact_Icc.exists_isMaxOn (f := f) (by norm_num) cont
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
⊢ (fun s => ‖𝓜 (fun x => ↑(Ψ x)) s‖) =O[𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}] fun s => 1 / ‖s‖

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]
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‖‖

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)
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‖‖

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
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‖‖

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]
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‖‖

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]
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‖‖

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]
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))

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
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)

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
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)

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 _
  _ ≤ _ := ?_
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)

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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
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

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]
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

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Ψ
State after:
no goals

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
State after:
no goals

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)
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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) ?_
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 ^ σ₂

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 ⊢
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)

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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 ^ σ₂

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
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 ^ σ₂

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
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 ^ σ₂

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]
State after:
no goals

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])]
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 ^ σ₂

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]
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 ^ σ₂

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)
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 ^ σ₂

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
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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
State after:
no goals