Theorem: MellinOfSmooth1a (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
let f' : ℝ → ℂ := fun x ↦ DeltaSpike Ψ ε x
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
let f : ℝ → ℂ := fun x ↦ DeltaSpike Ψ ε x / x
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
let g : ℝ → ℂ := fun x ↦ if 0 < x ∧ x ≤ 1 then 1 else 0
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
let F : ℝ × ℝ → ℂ := Function.uncurry fun x y ↦ f y * g (x / y) * (x : ℂ) ^ (s - 1)
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
let S := {⟨x, y⟩ : ℝ × ℝ | 0 < x  ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
let F' : ℝ × ℝ → ℂ := piecewise S (fun ⟨x, y⟩ ↦ f y * (x : ℂ) ^ (s - 1))
   (fun _ ↦ 0)
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
let Tx := Ioc 0 ((2 : ℝ) ^ ε)
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
let Ty := Icc ((2 : ℝ) ^ (-ε)) ((2 : ℝ) ^ ε)
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
have SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0 :=
  fun z hz ↦ ⟨hz.1, lt_of_lt_of_le (by apply rpow_pos_of_pos; norm_num) hz.2.2.1⟩
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
have SsubT: S ⊆ Tx ×ˢ Ty := by simp_rw [Seq, inter_subset_left]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
have Smeas : MeasurableSet S := by
  rw [Seq]; apply MeasurableSet.inter ?_ <| measurableSet_le measurable_fst measurable_snd
  simp [measurableSet_prod, Tx, Ty]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
have : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s := by
  rw [mul_comm, ← MellinConvolutionTransform f' g s (by convert int_F using 1; field_simp [F, f, f'])]
  dsimp [MellinTransform]; rw [setIntegral_congr (by simp)]
  intro x hx; simp_rw [MellinConvolutionSymmetric _ _ <| mem_Ioi.mp hx]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
this : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
this : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)
Tactic:
convert this using 1
State after:
case h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
this : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 𝓜 (MellinConvolution g f') s

case h.e'_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
this : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s
⊢ 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s) = 𝓜 g s * 𝓜 f' s

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
⊢ S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
Tactic:
ext ⟨x, y⟩
State after:
case h.mk
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
x y : ℝ
⊢ (x, y) ∈ S ↔ (x, y) ∈ Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}

State before:
case h.mk
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
x y : ℝ
⊢ (x, y) ∈ S ↔ (x, y) ∈ Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
Tactic:
constructor
State after:
case h.mk.mp
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
x y : ℝ
⊢ (x, y) ∈ S → (x, y) ∈ Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}

case h.mk.mpr
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
x y : ℝ
⊢ (x, y) ∈ Tx ×ˢ Ty ∩ {(x, y) | x ≤ y} → (x, y) ∈ S

State before:
case h.mk.mp
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
x y : ℝ
⊢ (x, y) ∈ S → (x, y) ∈ Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
Tactic:
exact fun h ↦ ⟨⟨⟨h.1, le_trans h.2.1 h.2.2.2⟩, ⟨h.2.2.1, h.2.2.2⟩⟩, h.2.1⟩
State after:
no goals

State before:
case h.mk.mpr
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
x y : ℝ
⊢ (x, y) ∈ Tx ×ˢ Ty ∩ {(x, y) | x ≤ y} → (x, y) ∈ S
Tactic:
exact fun h ↦  ⟨h.1.1.1, ⟨h.2, h.1.2.1, h.1.2.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 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
z : ℝ × ℝ
hz : z ∈ S
⊢ 0 < 2 ^ (-ε)
Tactic:
apply rpow_pos_of_pos
State after:
case hx
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
z : ℝ × ℝ
hz : z ∈ S
⊢ 0 < 2

State before:
case hx
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
z : ℝ × ℝ
hz : z ∈ S
⊢ 0 < 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 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
⊢ S ⊆ Tx ×ˢ Ty
Tactic:
simp_rw [Seq, inter_subset_left]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
⊢ MeasurableSet S
Tactic:
rw [Seq]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
⊢ MeasurableSet (Tx ×ˢ Ty ∩ {(x, y) | x ≤ y})

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
⊢ MeasurableSet (Tx ×ˢ Ty ∩ {(x, y) | x ≤ y})
Tactic:
apply MeasurableSet.inter ?_ <| measurableSet_le measurable_fst measurable_snd
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
⊢ MeasurableSet (Tx ×ˢ Ty)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
⊢ MeasurableSet (Tx ×ˢ Ty)
Tactic:
simp [measurableSet_prod, Tx, Ty]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
Tactic:
apply IntegrableOn.congr_fun (f := F') ?_ ?_ (by simp [measurableSet_prod])
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ IntegrableOn F' (Ioi 0 ×ˢ Ioi 0) volume

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ EqOn F' F (Ioi 0 ×ˢ Ioi 0)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ IntegrableOn F' (Ioi 0 ×ˢ Ioi 0) volume

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ EqOn F' F (Ioi 0 ×ˢ Ioi 0)
Tactic:
swap
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ EqOn F' F (Ioi 0 ×ˢ Ioi 0)

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ IntegrableOn F' (Ioi 0 ×ˢ Ioi 0) volume

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ MeasurableSet (Ioi 0 ×ˢ Ioi 0)
Tactic:
simp [measurableSet_prod]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ EqOn F' F (Ioi 0 ×ˢ Ioi 0)
Tactic:
simp only [F, F', f, g, mul_ite, mul_one, mul_zero, Function.uncurry_apply_pair]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ EqOn (S.piecewise (fun x => ↑(DeltaSpike Ψ ε x.2) / ↑x.2 * ↑x.1 ^ (s - 1)) fun x => 0)
    (Function.uncurry fun x y => (if 0 < x / y ∧ x / y ≤ 1 then ↑(DeltaSpike Ψ ε y) / ↑y else 0) * ↑x ^ (s - 1))
    (Ioi 0 ×ˢ Ioi 0)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ EqOn (S.piecewise (fun x => ↑(DeltaSpike Ψ ε x.2) / ↑x.2 * ↑x.1 ^ (s - 1)) fun x => 0)
    (Function.uncurry fun x y => (if 0 < x / y ∧ x / y ≤ 1 then ↑(DeltaSpike Ψ ε y) / ↑y else 0) * ↑x ^ (s - 1))
    (Ioi 0 ×ˢ Ioi 0)
Tactic:
intro ⟨x, y⟩ hz
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hz : (x, y) ∈ Ioi 0 ×ˢ Ioi 0
⊢ S.piecewise (fun x => ↑(DeltaSpike Ψ ε x.2) / ↑x.2 * ↑x.1 ^ (s - 1)) (fun x => 0) (x, y) =
    Function.uncurry (fun x y => (if 0 < x / y ∧ x / y ≤ 1 then ↑(DeltaSpike Ψ ε y) / ↑y else 0) * ↑x ^ (s - 1)) (x, y)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hz : (x, y) ∈ Ioi 0 ×ˢ Ioi 0
⊢ S.piecewise (fun x => ↑(DeltaSpike Ψ ε x.2) / ↑x.2 * ↑x.1 ^ (s - 1)) (fun x => 0) (x, y) =
    Function.uncurry (fun x y => (if 0 < x / y ∧ x / y ≤ 1 then ↑(DeltaSpike Ψ ε y) / ↑y else 0) * ↑x ^ (s - 1)) (x, y)
Tactic:
by_cases hS : ⟨x, y⟩ ∈ S <;> simp only [hS, piecewise, hz]
<;> simp only [mem_prod, mem_Ioi, mem_setOf_eq, not_and, not_le, S] at hz hS
State after:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hS : 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε
hz : 0 < x ∧ 0 < y
⊢ (if True then ↑(DeltaSpike Ψ ε y) / ↑y * ↑x ^ (s - 1) else 0) =
    Function.uncurry (fun x y => (if 0 < x / y ∧ x / y ≤ 1 then ↑(DeltaSpike Ψ ε y) / ↑y else 0) * ↑x ^ (s - 1)) (x, y)

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hz : 0 < x ∧ 0 < y
hS : 0 < x → x ≤ y → 2 ^ (-ε) ≤ y → 2 ^ ε < y
⊢ (if False then ↑(DeltaSpike Ψ ε y) / ↑y * ↑x ^ (s - 1) else 0) =
    Function.uncurry (fun x y => (if 0 < x / y ∧ x / y ≤ 1 then ↑(DeltaSpike Ψ ε y) / ↑y else 0) * ↑x ^ (s - 1)) (x, y)

State before:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hS : 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε
hz : 0 < x ∧ 0 < y
⊢ (if True then ↑(DeltaSpike Ψ ε y) / ↑y * ↑x ^ (s - 1) else 0) =
    Function.uncurry (fun x y => (if 0 < x / y ∧ x / y ≤ 1 then ↑(DeltaSpike Ψ ε y) / ↑y else 0) * ↑x ^ (s - 1)) (x, y)
Tactic:
simp [hS, div_pos hz.1 hz.2, (div_le_one hz.2).mpr hS.2.1]
State after:
no goals

State before:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hz : 0 < x ∧ 0 < y
hS : 0 < x → x ≤ y → 2 ^ (-ε) ≤ y → 2 ^ ε < y
⊢ (if False then ↑(DeltaSpike Ψ ε y) / ↑y * ↑x ^ (s - 1) else 0) =
    Function.uncurry (fun x y => (if 0 < x / y ∧ x / y ≤ 1 then ↑(DeltaSpike Ψ ε y) / ↑y else 0) * ↑x ^ (s - 1)) (x, y)
Tactic:
by_cases hxy : x / y ≤ 1
State after:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hz : 0 < x ∧ 0 < y
hS : 0 < x → x ≤ y → 2 ^ (-ε) ≤ y → 2 ^ ε < y
hxy : x / y ≤ 1
⊢ (if False then ↑(DeltaSpike Ψ ε y) / ↑y * ↑x ^ (s - 1) else 0) =
    Function.uncurry (fun x y => (if 0 < x / y ∧ x / y ≤ 1 then ↑(DeltaSpike Ψ ε y) / ↑y else 0) * ↑x ^ (s - 1)) (x, y)

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hz : 0 < x ∧ 0 < y
hS : 0 < x → x ≤ y → 2 ^ (-ε) ≤ y → 2 ^ ε < y
hxy : ¬x / y ≤ 1
⊢ (if False then ↑(DeltaSpike Ψ ε y) / ↑y * ↑x ^ (s - 1) else 0) =
    Function.uncurry (fun x y => (if 0 < x / y ∧ x / y ≤ 1 then ↑(DeltaSpike Ψ ε y) / ↑y else 0) * ↑x ^ (s - 1)) (x, y)

State before:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hz : 0 < x ∧ 0 < y
hS : 0 < x → x ≤ y → 2 ^ (-ε) ≤ y → 2 ^ ε < y
hxy : x / y ≤ 1
⊢ (if False then ↑(DeltaSpike Ψ ε y) / ↑y * ↑x ^ (s - 1) else 0) =
    Function.uncurry (fun x y => (if 0 < x / y ∧ x / y ≤ 1 then ↑(DeltaSpike Ψ ε y) / ↑y else 0) * ↑x ^ (s - 1)) (x, y)

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hz : 0 < x ∧ 0 < y
hS : 0 < x → x ≤ y → 2 ^ (-ε) ≤ y → 2 ^ ε < y
hxy : ¬x / y ≤ 1
⊢ (if False then ↑(DeltaSpike Ψ ε y) / ↑y * ↑x ^ (s - 1) else 0) =
    Function.uncurry (fun x y => (if 0 < x / y ∧ x / y ≤ 1 then ↑(DeltaSpike Ψ ε y) / ↑y else 0) * ↑x ^ (s - 1)) (x, y)
Tactic:
swap
State after:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hz : 0 < x ∧ 0 < y
hS : 0 < x → x ≤ y → 2 ^ (-ε) ≤ y → 2 ^ ε < y
hxy : ¬x / y ≤ 1
⊢ (if False then ↑(DeltaSpike Ψ ε y) / ↑y * ↑x ^ (s - 1) else 0) =
    Function.uncurry (fun x y => (if 0 < x / y ∧ x / y ≤ 1 then ↑(DeltaSpike Ψ ε y) / ↑y else 0) * ↑x ^ (s - 1)) (x, y)

case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hz : 0 < x ∧ 0 < y
hS : 0 < x → x ≤ y → 2 ^ (-ε) ≤ y → 2 ^ ε < y
hxy : x / y ≤ 1
⊢ (if False then ↑(DeltaSpike Ψ ε y) / ↑y * ↑x ^ (s - 1) else 0) =
    Function.uncurry (fun x y => (if 0 < x / y ∧ x / y ≤ 1 then ↑(DeltaSpike Ψ ε y) / ↑y else 0) * ↑x ^ (s - 1)) (x, y)

State before:
case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hz : 0 < x ∧ 0 < y
hS : 0 < x → x ≤ y → 2 ^ (-ε) ≤ y → 2 ^ ε < y
hxy : ¬x / y ≤ 1
⊢ (if False then ↑(DeltaSpike Ψ ε y) / ↑y * ↑x ^ (s - 1) else 0) =
    Function.uncurry (fun x y => (if 0 < x / y ∧ x / y ≤ 1 then ↑(DeltaSpike Ψ ε y) / ↑y else 0) * ↑x ^ (s - 1)) (x, y)

case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hz : 0 < x ∧ 0 < y
hS : 0 < x → x ≤ y → 2 ^ (-ε) ≤ y → 2 ^ ε < y
hxy : x / y ≤ 1
⊢ (if False then ↑(DeltaSpike Ψ ε y) / ↑y * ↑x ^ (s - 1) else 0) =
    Function.uncurry (fun x y => (if 0 < x / y ∧ x / y ≤ 1 then ↑(DeltaSpike Ψ ε y) / ↑y else 0) * ↑x ^ (s - 1)) (x, y)
Tactic:
simp [hxy]
State after:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hz : 0 < x ∧ 0 < y
hS : 0 < x → x ≤ y → 2 ^ (-ε) ≤ y → 2 ^ ε < y
hxy : x / y ≤ 1
⊢ (if False then ↑(DeltaSpike Ψ ε y) / ↑y * ↑x ^ (s - 1) else 0) =
    Function.uncurry (fun x y => (if 0 < x / y ∧ x / y ≤ 1 then ↑(DeltaSpike Ψ ε y) / ↑y else 0) * ↑x ^ (s - 1)) (x, y)

State before:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hz : 0 < x ∧ 0 < y
hS : 0 < x → x ≤ y → 2 ^ (-ε) ≤ y → 2 ^ ε < y
hxy : x / y ≤ 1
⊢ (if False then ↑(DeltaSpike Ψ ε y) / ↑y * ↑x ^ (s - 1) else 0) =
    Function.uncurry (fun x y => (if 0 < x / y ∧ x / y ≤ 1 then ↑(DeltaSpike Ψ ε y) / ↑y else 0) * ↑x ^ (s - 1)) (x, y)
Tactic:
have hy : y ∉ Icc (2 ^ (-ε)) (2 ^ ε) := by
  simp only [mem_Icc, not_and, not_le]; exact hS hz.1 <| (div_le_one hz.2).mp hxy
State after:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hz : 0 < x ∧ 0 < y
hS : 0 < x → x ≤ y → 2 ^ (-ε) ≤ y → 2 ^ ε < y
hxy : x / y ≤ 1
hy : y ∉ Icc (2 ^ (-ε)) (2 ^ ε)
⊢ (if False then ↑(DeltaSpike Ψ ε y) / ↑y * ↑x ^ (s - 1) else 0) =
    Function.uncurry (fun x y => (if 0 < x / y ∧ x / y ≤ 1 then ↑(DeltaSpike Ψ ε y) / ↑y else 0) * ↑x ^ (s - 1)) (x, y)

State before:
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hz : 0 < x ∧ 0 < y
hS : 0 < x → x ≤ y → 2 ^ (-ε) ≤ y → 2 ^ ε < y
hxy : x / y ≤ 1
hy : y ∉ Icc (2 ^ (-ε)) (2 ^ ε)
⊢ (if False then ↑(DeltaSpike Ψ ε y) / ↑y * ↑x ^ (s - 1) else 0) =
    Function.uncurry (fun x y => (if 0 < x / y ∧ x / y ≤ 1 then ↑(DeltaSpike Ψ ε y) / ↑y else 0) * ↑x ^ (s - 1)) (x, y)
Tactic:
simp [DeltaSpikeSupport εpos hz.2.le suppΨ hy]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hz : 0 < x ∧ 0 < y
hS : 0 < x → x ≤ y → 2 ^ (-ε) ≤ y → 2 ^ ε < y
hxy : x / y ≤ 1
⊢ y ∉ Icc (2 ^ (-ε)) (2 ^ ε)
Tactic:
simp only [mem_Icc, not_and, not_le]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hz : 0 < x ∧ 0 < y
hS : 0 < x → x ≤ y → 2 ^ (-ε) ≤ y → 2 ^ ε < y
hxy : x / y ≤ 1
⊢ 2 ^ (-ε) ≤ y → 2 ^ ε < y

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
x y : ℝ
hz : 0 < x ∧ 0 < y
hS : 0 < x → x ≤ y → 2 ^ (-ε) ≤ y → 2 ^ ε < y
hxy : x / y ≤ 1
⊢ 2 ^ (-ε) ≤ y → 2 ^ ε < y
Tactic:
exact hS hz.1 <| (div_le_one hz.2).mp hxy
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ IntegrableOn F' (Ioi 0 ×ˢ Ioi 0) volume
Tactic:
apply Integrable.piecewise Smeas ?_ integrableOn_zero
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ IntegrableOn
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    S (volume.restrict (Ioi 0 ×ˢ Ioi 0))

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ IntegrableOn
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    S (volume.restrict (Ioi 0 ×ˢ Ioi 0))
Tactic:
simp only [IntegrableOn, Measure.restrict_restrict_of_subset SsubI]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ Integrable (fun x => f x.2 * ↑x.1 ^ (s - 1)) (volume.restrict S)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ Integrable (fun x => f x.2 * ↑x.1 ^ (s - 1)) (volume.restrict S)
Tactic:
apply MeasureTheory.Integrable.mono_measure ?_
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ volume.restrict S ≤ ?m.803483

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ Measure (ℝ × ℝ)

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ Integrable (fun x => f x.2 * ↑x.1 ^ (s - 1)) ?m.803483

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ volume.restrict S ≤ ?m.803483

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ Measure (ℝ × ℝ)

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ Integrable (fun x => f x.2 * ↑x.1 ^ (s - 1)) ?m.803483
Tactic:
apply MeasureTheory.Measure.restrict_mono' (HasSubset.Subset.eventuallyLE SsubT) le_rfl
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ Integrable (fun x => f x.2 * ↑x.1 ^ (s - 1)) (volume.restrict (Tx ×ˢ Ty))

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ Integrable (fun x => f x.2 * ↑x.1 ^ (s - 1)) (volume.restrict (Tx ×ˢ Ty))
Tactic:
have : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty) := by
  rw [Measure.prod_restrict, MeasureTheory.Measure.volume_eq_prod]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ Integrable (fun x => f x.2 * ↑x.1 ^ (s - 1)) (volume.restrict (Tx ×ˢ Ty))

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ Integrable (fun x => f x.2 * ↑x.1 ^ (s - 1)) (volume.restrict (Tx ×ˢ Ty))
Tactic:
conv => rw [this]; lhs; intro; rw [mul_comm]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ Integrable (fun x => ↑x.1 ^ (s - 1) * f x.2) ((volume.restrict Tx).prod (volume.restrict Ty))

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ Integrable (fun x => ↑x.1 ^ (s - 1) * f x.2) ((volume.restrict Tx).prod (volume.restrict Ty))
Tactic:
apply MeasureTheory.Integrable.prod_mul (f := fun x ↦ (x : ℂ) ^ (s - 1))
  (μ := Measure.restrict volume Tx)
State after:
case hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ Integrable (fun x => ↑x ^ (s - 1)) (volume.restrict Tx)

case hg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ Integrable f (volume.restrict Ty)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
⊢ volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
Tactic:
rw [Measure.prod_restrict, MeasureTheory.Measure.volume_eq_prod]
State after:
no goals

State before:
case hf
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ Integrable (fun x => ↑x ^ (s - 1)) (volume.restrict Tx)
Tactic:
apply integrableOn_Ioc_iff_integrableOn_Ioo.mpr ?_
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ IntegrableOn (fun x => ↑x ^ (s - 1)) (Ioo 0 (2 ^ ε)) volume

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ IntegrableOn (fun x => ↑x ^ (s - 1)) (Ioo 0 (2 ^ ε)) volume
Tactic:
apply (intervalIntegral.integrableOn_Ioo_cpow_iff (s := s - 1) (t := (2 : ℝ) ^ ε) ?_).mpr
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ -1 < (s - 1).re

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ 0 < 2 ^ ε

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ -1 < (s - 1).re
Tactic:
simp [hs]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ 0 < 2 ^ ε
Tactic:
apply rpow_pos_of_pos (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 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals

State before:
case hg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ Integrable f (volume.restrict Ty)
Tactic:
apply (ContinuousOn.div ?_ ?_ ?_).integrableOn_compact isCompact_Icc
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ ContinuousOn (fun x => ↑(DeltaSpike Ψ ε x)) (Icc (2 ^ (-ε)) (2 ^ ε))

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ ContinuousOn (fun x => ↑x) (Icc (2 ^ (-ε)) (2 ^ ε))

𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ ∀ x ∈ Icc (2 ^ (-ε)) (2 ^ ε), ↑x ≠ 0

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ ContinuousOn (fun x => ↑(DeltaSpike Ψ ε x)) (Icc (2 ^ (-ε)) (2 ^ ε))
Tactic:
exact (DeltaSpikeOfRealContinuous εpos diffΨ).continuousOn
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ ContinuousOn (fun x => ↑x) (Icc (2 ^ (-ε)) (2 ^ ε))
Tactic:
exact continuous_ofReal.continuousOn
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
⊢ ∀ x ∈ Icc (2 ^ (-ε)) (2 ^ ε), ↑x ≠ 0
Tactic:
intro x hx
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
x : ℝ
hx : x ∈ Icc (2 ^ (-ε)) (2 ^ ε)
⊢ ↑x ≠ 0

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
x : ℝ
hx : x ∈ Icc (2 ^ (-ε)) (2 ^ ε)
⊢ ↑x ≠ 0
Tactic:
simp only [mem_Icc] at hx
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
x : ℝ
hx : 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
⊢ ↑x ≠ 0

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
x : ℝ
hx : 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
⊢ ↑x ≠ 0
Tactic:
simp only [ofReal_ne_zero]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
x : ℝ
hx : 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
⊢ x ≠ 0

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
x : ℝ
hx : 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
⊢ x ≠ 0
Tactic:
linarith [(by apply rpow_pos_of_pos (by norm_num) : (0 : ℝ) < 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 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
x : ℝ
hx : 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
⊢ 0 < 2 ^ (-ε)
Tactic:
apply rpow_pos_of_pos (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 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
this : volume.restrict (Tx ×ˢ Ty) = (volume.restrict Tx).prod (volume.restrict Ty)
x : ℝ
hx : 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
⊢ 0 < 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 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
⊢ 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s
Tactic:
rw [mul_comm, ← MellinConvolutionTransform f' g s (by convert int_F using 1; field_simp [F, f, f'])]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
⊢ 𝓜 (MellinConvolution g f') s = 𝓜 (MellinConvolution f' g) s

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
⊢ 𝓜 (MellinConvolution g f') s = 𝓜 (MellinConvolution f' g) s
Tactic:
dsimp [MellinTransform]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioi 0, MellinConvolution g f' x * ↑x ^ (s - 1) =
    ∫ (x : ℝ) in Ioi 0, MellinConvolution f' g x * ↑x ^ (s - 1)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioi 0, MellinConvolution g f' x * ↑x ^ (s - 1) =
    ∫ (x : ℝ) in Ioi 0, MellinConvolution f' g x * ↑x ^ (s - 1)
Tactic:
rw [setIntegral_congr (by simp)]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
⊢ EqOn (fun x => MellinConvolution g f' x * ↑x ^ (s - 1)) (fun x => MellinConvolution f' g x * ↑x ^ (s - 1)) (Ioi 0)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
⊢ EqOn (fun x => MellinConvolution g f' x * ↑x ^ (s - 1)) (fun x => MellinConvolution f' g x * ↑x ^ (s - 1)) (Ioi 0)
Tactic:
intro x hx
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
⊢ (fun x => MellinConvolution g f' x * ↑x ^ (s - 1)) x = (fun x => MellinConvolution f' g x * ↑x ^ (s - 1)) x

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
x : ℝ
hx : x ∈ Ioi 0
⊢ (fun x => MellinConvolution g f' x * ↑x ^ (s - 1)) x = (fun x => MellinConvolution f' g x * ↑x ^ (s - 1)) x
Tactic:
simp_rw [MellinConvolutionSymmetric _ _ <| mem_Ioi.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 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
⊢ IntegrableOn (Function.uncurry fun x y => f' y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
Tactic:
convert int_F using 1
State after:
case h.e'_5
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
⊢ (Function.uncurry fun x y => f' y * g (x / y) / ↑y * ↑x ^ (s - 1)) = F

State before:
case h.e'_5
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
⊢ (Function.uncurry fun x y => f' y * g (x / y) / ↑y * ↑x ^ (s - 1)) = F
Tactic:
field_simp [F, f, 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 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
⊢ MeasurableSet (Ioi 0)
Tactic:
simp
State after:
no goals

State before:
case h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
this : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s
⊢ 𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s = 𝓜 (MellinConvolution g f') s
Tactic:
congr
State after:
case h.e'_2.e_f
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
this : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s
⊢ (fun x => ↑(Smooth1 Ψ ε x)) = MellinConvolution g f'

State before:
case h.e'_2.e_f
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
this : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s
⊢ (fun x => ↑(Smooth1 Ψ ε x)) = MellinConvolution g f'
Tactic:
funext x
State after:
case h.e'_2.e_f.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
this : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s
x : ℝ
⊢ ↑(Smooth1 Ψ ε x) = MellinConvolution g f' x

State before:
case h.e'_2.e_f.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
this : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s
x : ℝ
⊢ ↑(Smooth1 Ψ ε x) = MellinConvolution g f' x
Tactic:
convert integral_ofReal.symm
State after:
case h.e'_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
this : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s
x : ℝ
⊢ MellinConvolution g f' x =
    ∫ (x_1 : ℝ) in Ioi 0, ↑((fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) x_1 * DeltaSpike Ψ ε (x / x_1) / ↑x_1)

State before:
case h.e'_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
this : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s
x : ℝ
⊢ MellinConvolution g f' x =
    ∫ (x_1 : ℝ) in Ioi 0, ↑((fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) x_1 * DeltaSpike Ψ ε (x / x_1) / ↑x_1)
Tactic:
simp only [MellinConvolution, RCLike.ofReal_div, ite_mul, one_mul, zero_mul, @apply_ite ℝ ℂ,
  algebraMap.coe_zero, f, g]
State after:
case h.e'_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
this : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s
x : ℝ
⊢ ∫ (y : ℝ) in Ioi 0, (if 0 < y ∧ y ≤ 1 then f' (x / y) else 0) / ↑y =
    ∫ (x_1 : ℝ) in Ioi 0, (if 0 < x_1 ∧ x_1 ≤ 1 then ↑(DeltaSpike Ψ ε (x / x_1)) else 0) / ↑↑x_1

State before:
case h.e'_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
this : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s
x : ℝ
⊢ ∫ (y : ℝ) in Ioi 0, (if 0 < y ∧ y ≤ 1 then f' (x / y) else 0) / ↑y =
    ∫ (x_1 : ℝ) in Ioi 0, (if 0 < x_1 ∧ x_1 ≤ 1 then ↑(DeltaSpike Ψ ε (x / x_1)) else 0) / ↑↑x_1
Tactic:
rfl
State after:
no goals

State before:
case h.e'_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
εpos : 0 < ε
s : ℂ
hs : 0 < s.re
f' : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x)
f : ℝ → ℂ := fun x => ↑(DeltaSpike Ψ ε x) / ↑x
g : ℝ → ℂ := fun x => if 0 < x ∧ x ≤ 1 then 1 else 0
F : ℝ × ℝ → ℂ := Function.uncurry fun x y => f y * g (x / y) * ↑x ^ (s - 1)
S : Set (ℝ × ℝ) := {(x, y) | 0 < x ∧ x ≤ y ∧ 2 ^ (-ε) ≤ y ∧ y ≤ 2 ^ ε}
F' : ℝ × ℝ → ℂ :=
  S.piecewise
    (fun x =>
      match x with
      | (x, y) => f y * ↑x ^ (s - 1))
    fun x => 0
Tx : Set ℝ := Ioc 0 (2 ^ ε)
Ty : Set ℝ := Icc (2 ^ (-ε)) (2 ^ ε)
Seq : S = Tx ×ˢ Ty ∩ {(x, y) | x ≤ y}
SsubI : S ⊆ Ioi 0 ×ˢ Ioi 0
SsubT : S ⊆ Tx ×ˢ Ty
Smeas : MeasurableSet S
int_F : IntegrableOn F (Ioi 0 ×ˢ Ioi 0) volume
this : 𝓜 (MellinConvolution g f') s = 𝓜 g s * 𝓜 f' s
⊢ 1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s) = 𝓜 g s * 𝓜 f' s
Tactic:
rw [MellinOf1 s hs, MellinOfDeltaSpike Ψ εpos s]
State after:
no goals