internlm/Lean-Github huggingface dataset:
Theorem: MellinOfPsi_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s✝ : ℂ
hs✝ : s✝ ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
s : ℂ
hs : s ≠ 0
x : ℝ
hx : x ∈ Ioi 0
⊢ deriv g x = ↑x ^ (s - 1)
Tactic:
have := HasDerivAt.cpow_const (c := s) (hasDerivAt_id (x : ℂ)) (Or.inl hx)
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s✝ : ℂ
hs✝ : s✝ ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
s : ℂ
hs : s ≠ 0
x : ℝ
hx : x ∈ Ioi 0
this : HasDerivAt (fun x => id x ^ s) (s * id ↑x ^ (s - 1) * 1) ↑x
⊢ deriv g x = ↑x ^ (s - 1)
Theorem: MellinOfPsi_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s✝ : ℂ
hs✝ : s✝ ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
s : ℂ
hs : s ≠ 0
x : ℝ
hx : x ∈ Ioi 0
this : HasDerivAt (fun x => id x ^ s) (s * id ↑x ^ (s - 1) * 1) ↑x
⊢ deriv g x = ↑x ^ (s - 1)
Tactic:
simp_rw [mul_one, id_eq] at this
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s✝ : ℂ
hs✝ : s✝ ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
s : ℂ
hs : s ≠ 0
x : ℝ
hx : x ∈ Ioi 0
this : HasDerivAt (fun x => x ^ s) (s * ↑x ^ (s - 1)) ↑x
⊢ deriv g x = ↑x ^ (s - 1)
Theorem: MellinOfPsi_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s✝ : ℂ
hs✝ : s✝ ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
s : ℂ
hs : s ≠ 0
x : ℝ
hx : x ∈ Ioi 0
this : HasDerivAt (fun x => x ^ s) (s * ↑x ^ (s - 1)) ↑x
⊢ deriv g x = ↑x ^ (s - 1)
Tactic:
rw [deriv_div_const, deriv.comp_ofReal (e := fun x ↦ x ^ s)]
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s✝ : ℂ
hs✝ : s✝ ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
s : ℂ
hs : s ≠ 0
x : ℝ
hx : x ∈ Ioi 0
this : HasDerivAt (fun x => x ^ s) (s * ↑x ^ (s - 1)) ↑x
⊢ deriv (fun x => x ^ s) ↑x / s = ↑x ^ (s - 1)

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s✝ : ℂ
hs✝ : s✝ ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
s : ℂ
hs : s ≠ 0
x : ℝ
hx : x ∈ Ioi 0
this : HasDerivAt (fun x => x ^ s) (s * ↑x ^ (s - 1)) ↑x
⊢ DifferentiableAt ℂ (fun x => x ^ s) ↑x
Theorem: MellinOfPsi_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s✝ : ℂ
hs✝ : s✝ ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
s : ℂ
hs : s ≠ 0
x : ℝ
hx : x ∈ Ioi 0
this : HasDerivAt (fun x => x ^ s) (s * ↑x ^ (s - 1)) ↑x
⊢ deriv (fun x => x ^ s) ↑x / s = ↑x ^ (s - 1)
Tactic:
rw [this.deriv, mul_div_right_comm, div_self hs, one_mul]
Proof state after:
no goals
Theorem: MellinOfPsi_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s✝ : ℂ
hs✝ : s✝ ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
s : ℂ
hs : s ≠ 0
x : ℝ
hx : x ∈ Ioi 0
this : HasDerivAt (fun x => x ^ s) (s * ↑x ^ (s - 1)) ↑x
⊢ DifferentiableAt ℂ (fun x => x ^ s) ↑x
Tactic:
apply hasDerivAt_deriv_iff.mp
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s✝ : ℂ
hs✝ : s✝ ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
s : ℂ
hs : s ≠ 0
x : ℝ
hx : x ∈ Ioi 0
this : HasDerivAt (fun x => x ^ s) (s * ↑x ^ (s - 1)) ↑x
⊢ HasDerivAt (fun x => x ^ s) (deriv (fun x => x ^ s) ↑x) ↑x
Theorem: MellinOfPsi_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s✝ : ℂ
hs✝ : s✝ ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
s : ℂ
hs : s ≠ 0
x : ℝ
hx : x ∈ Ioi 0
this : HasDerivAt (fun x => x ^ s) (s * ↑x ^ (s - 1)) ↑x
⊢ HasDerivAt (fun x => x ^ s) (deriv (fun x => x ^ s) ↑x) ↑x
Tactic:
simp only [this.deriv, this]
Proof state after:
no goals
Theorem: MellinOfPsi_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ -∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * g x = -∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s / s
Tactic:
simp only [mul_div, g]
Proof state after:
no goals
Theorem: MellinOfPsi_aux
Proof state before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ ∫ (x : ℝ) in Ioi 0, ↑(Ψ x) * ↑x ^ (s - 1) = ∫ (x : ℝ) in Ioi 0, ↑(Ψ x) * deriv g x
Tactic:
rw [setIntegral_congr (by simp)]
Proof state after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ EqOn (fun x => ↑(Ψ x) * ↑x ^ (s - 1)) (fun x => ↑(Ψ x) * deriv g x) (Ioi 0)
Theorem: MellinOfPsi_aux
Proof state before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ EqOn (fun x => ↑(Ψ x) * ↑x ^ (s - 1)) (fun x => ↑(Ψ x) * deriv g x) (Ioi 0)
Tactic:
intro _ hx
Proof state after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ (fun x => ↑(Ψ x) * ↑x ^ (s - 1)) x✝ = (fun x => ↑(Ψ x) * deriv g x) x✝
Theorem: MellinOfPsi_aux
Proof state before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
x✝ : ℝ
hx : x✝ ∈ Ioi 0
⊢ (fun x => ↑(Ψ x) * ↑x ^ (s - 1)) x✝ = (fun x => ↑(Ψ x) * deriv g x) x✝
Tactic:
simp only [gderiv hs hx]
Proof state after:
no goals
Theorem: MellinOfPsi_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ MeasurableSet (Ioi 0)
Tactic:
simp
Proof state after:
no goals
Theorem: MellinOfPsi_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ 0 < 1 / 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: MellinOfPsi_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ 1 / 2 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: MellinOfPsi_aux
Proof state before:
case calc_2.fSupp
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ (Function.support fun x => ↑(Ψ x)) ⊆ Icc (1 / 2) 2
Tactic:
simpa only [Function.support_subset_iff, ne_eq, ofReal_eq_zero]
Proof state after:
no goals
Theorem: MellinOfPsi_aux
Proof state before:
case calc_2.fDiff
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ DifferentiableOn ℝ (fun x => ↑(Ψ x)) (Ioi 0)
Tactic:
exact (Differentiable.ofReal_comp_iff.mpr (diffΨ.differentiable (by norm_num))).differentiableOn
Proof state after:
no goals
Theorem: MellinOfPsi_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ 1 ≤ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: MellinOfPsi_aux
Proof state before:
case calc_2.gDiff
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ DifferentiableOn ℝ g (Ioi 0)
Tactic:
refine DifferentiableOn.div_const ?_ s
Proof state after:
case calc_2.gDiff
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ DifferentiableOn ℝ (fun x => ↑x ^ s) (Ioi 0)
Theorem: MellinOfPsi_aux
Proof state before:
case calc_2.gDiff
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ DifferentiableOn ℝ (fun x => ↑x ^ s) (Ioi 0)
Tactic:
intro a ha
Proof state after:
case calc_2.gDiff
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
a : ℝ
ha : a ∈ Ioi 0
⊢ DifferentiableWithinAt ℝ (fun x => ↑x ^ s) (Ioi 0) a
Theorem: MellinOfPsi_aux
Proof state before:
case calc_2.gDiff
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
a : ℝ
ha : a ∈ Ioi 0
⊢ DifferentiableWithinAt ℝ (fun x => ↑x ^ s) (Ioi 0) a
Tactic:
refine DifferentiableAt.comp_ofReal (e := fun x ↦ x ^ s) ?_ |>.differentiableWithinAt
Proof state after:
case calc_2.gDiff
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
a : ℝ
ha : a ∈ Ioi 0
⊢ DifferentiableAt ℂ (fun x => x ^ s) ↑a
Theorem: MellinOfPsi_aux
Proof state before:
case calc_2.gDiff
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
a : ℝ
ha : a ∈ Ioi 0
⊢ DifferentiableAt ℂ (fun x => x ^ s) ↑a
Tactic:
apply differentiableAt_id'.cpow (differentiableAt_const s) <| by exact Or.inl ha
Proof state after:
no goals
Theorem: MellinOfPsi_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
a : ℝ
ha : a ∈ Ioi 0
⊢ ↑a ∈ slitPlane
Tactic:
exact Or.inl ha
Proof state after:
no goals
Theorem: MellinOfPsi_aux
Proof state before:
case calc_2.fderivCont
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ ContinuousOn (deriv fun x => ↑(Ψ x)) (Ioi 0)
Tactic:
simp only [deriv.ofReal_comp']
Proof state after:
case calc_2.fderivCont
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ ContinuousOn (fun x => ↑(deriv (fun x => Ψ x) x)) (Ioi 0)
Theorem: MellinOfPsi_aux
Proof state before:
case calc_2.fderivCont
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ ContinuousOn (fun x => ↑(deriv (fun x => Ψ x) x)) (Ioi 0)
Tactic:
exact continuous_ofReal.comp (diffΨ.continuous_deriv (by norm_num)) |>.continuousOn
Proof state after:
no goals
Theorem: MellinOfPsi_aux
Proof state before:
case calc_2.gderivCont
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ ContinuousOn (deriv g) (Ioi 0)
Tactic:
apply ContinuousOn.congr (f := fun (x : ℝ) ↦ (x : ℂ) ^ (s - 1)) ?_ fun x hx ↦ gderiv hs hx
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ ContinuousOn (fun x => ↑x ^ (s - 1)) (Ioi 0)
Theorem: MellinOfPsi_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ ContinuousOn (fun x => ↑x ^ (s - 1)) (Ioi 0)
Tactic:
exact Continuous.continuousOn (by continuity) |>.cpow continuousOn_const (by simp)
Proof state after:
no goals
Theorem: MellinOfPsi_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ Continuous fun x => ↑x
Tactic:
continuity
Proof state after:
no goals
Theorem: MellinOfPsi_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ ∀ a ∈ Ioi 0, ↑a ∈ slitPlane
Tactic:
simp
Proof state after:
no goals
Theorem: MellinOfPsi_aux
Proof state before:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ -∫ (x : ℝ) in Ioi 0, deriv (fun x => ↑(Ψ x)) x * g x = -∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * g x
Tactic:
congr
Proof state after:
case calc_3.e_a.e_f
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ (fun x => deriv (fun x => ↑(Ψ x)) x * g x) = fun x => ↑(deriv Ψ x) * g x
Theorem: MellinOfPsi_aux
Proof state before:
case calc_3.e_a.e_f
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ (fun x => deriv (fun x => ↑(Ψ x)) x * g x) = fun x => ↑(deriv Ψ x) * g x
Tactic:
funext
Proof state after:
case calc_3.e_a.e_f.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
x✝ : ℝ
⊢ deriv (fun x => ↑(Ψ x)) x✝ * g x✝ = ↑(deriv Ψ x✝) * g x✝
Theorem: MellinOfPsi_aux
Proof state before:
case calc_3.e_a.e_f.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
x✝ : ℝ
⊢ deriv (fun x => ↑(Ψ x)) x✝ * g x✝ = ↑(deriv Ψ x✝) * g x✝
Tactic:
congr
Proof state after:
case calc_3.e_a.e_f.h.e_a
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
x✝ : ℝ
⊢ deriv (fun x => ↑(Ψ x)) x✝ = ↑(deriv Ψ x✝)
Theorem: MellinOfPsi_aux
Proof state before:
case calc_3.e_a.e_f.h.e_a
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
x✝ : ℝ
⊢ deriv (fun x => ↑(Ψ x)) x✝ = ↑(deriv Ψ x✝)
Tactic:
apply (hasDerivAt_deriv_iff.mpr ?_).ofReal_comp.deriv
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
x✝ : ℝ
⊢ DifferentiableAt ℝ (fun y => Ψ y) x✝
Theorem: MellinOfPsi_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
x✝ : ℝ
⊢ DifferentiableAt ℝ (fun y => Ψ y) x✝
Tactic:
exact diffΨ.contDiffAt.differentiableAt (by norm_num)
Proof state after:
no goals
Theorem: MellinOfPsi_aux
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
x✝ : ℝ
⊢ 1 ≤ 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: MellinOfPsi_aux
Proof state before:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ -∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s / s = -(1 / s) * ∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s
Tactic:
simp only [neg_mul, neg_inj]
Proof state after:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ ∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s / s = 1 / s * ∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s
Theorem: MellinOfPsi_aux
Proof state before:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ ∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s / s = 1 / s * ∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s
Tactic:
conv => lhs; rhs; intro; rw [← mul_one_div, mul_comm]
Proof state after:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ ∫ (x : ℝ) in Ioi 0, 1 / s * (↑(deriv Ψ x) * ↑x ^ s) = 1 / s * ∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s
Theorem: MellinOfPsi_aux
Proof state before:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ ∫ (x : ℝ) in Ioi 0, 1 / s * (↑(deriv Ψ x) * ↑x ^ s) = 1 / s * ∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s
Tactic:
rw [integral_mul_left]
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 < σ₁
⊢ (fun s => ‖𝓜 (fun x => ↑(Ψ x)) s‖) =O[𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}] fun s => 1 / ‖s‖
Tactic:
let f := fun (x : ℝ) ↦ ‖deriv Ψ x‖
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‖
⊢ (fun s => ‖𝓜 (fun x => ↑(Ψ x)) s‖) =O[𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}] fun s => 1 / ‖s‖
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‖
⊢ (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
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)
⊢ (fun s => ‖𝓜 (fun x => ↑(Ψ x)) s‖) =O[𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}] fun s => 1 / ‖s‖
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)
⊢ (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
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
⊢ (fun s => ‖𝓜 (fun x => ↑(Ψ x)) s‖) =O[𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}] fun s => 1 / ‖s‖