Theorem: MellinOfPsi_aux (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
⊢ ∫ (x : ℝ) in Ioi 0, ↑(Ψ x) * ↑x ^ (s - 1) = -(1 / s) * ∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s
Tactic:
let g {s : ℂ} := fun (x : ℝ)  ↦ x ^ s / s
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
⊢ ∫ (x : ℝ) in Ioi 0, ↑(Ψ x) * ↑x ^ (s - 1) = -(1 / s) * ∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s

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, ↑(Ψ x) * ↑x ^ (s - 1) = -(1 / s) * ∫ (x : ℝ) in Ioi 0, ↑(deriv Ψ x) * ↑x ^ s
Tactic:
calc
  _ =  ∫ (x : ℝ) in Ioi 0, ↑(Ψ x) * deriv (@g s) x := ?_
  _ = -∫ (x : ℝ) in Ioi 0, deriv (fun x ↦ ↑(Ψ x)) x * @g s x := ?_
  _ = -∫ (x : ℝ) in Ioi 0, deriv Ψ x * @g s x := ?_
  _ = -∫ (x : ℝ) in Ioi 0, deriv Ψ x * x ^ s / s := by simp only [mul_div, g]
  _ = _ := ?_
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 : ℝ) in Ioi 0, ↑(Ψ x) * ↑x ^ (s - 1) = ∫ (x : ℝ) in Ioi 0, ↑(Ψ x) * deriv g x

case calc_2
𝕂 : 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) * deriv g x = -∫ (x : ℝ) in Ioi 0, deriv (fun x => ↑(Ψ x)) x * g x

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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