Theorem: MellinOfSmooth1a
Proof 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
Proof 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