internlm/Lean-Github huggingface dataset:
Theorem: MellinOfSmooth1a
Proof 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
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
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
Theorem: MellinOfSmooth1a
Proof 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]
Proof state after:
no goals
Theorem: MellinOfSmooth1a
Proof 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
Proof 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
Theorem: MellinOfSmooth1a
Proof 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']
Proof state after:
no goals
Theorem: MellinOfSmooth1a
Proof 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
Proof state after:
no goals
Theorem: MellinOfSmooth1a
Proof 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
Proof 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'
Theorem: MellinOfSmooth1a
Proof 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
Proof 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
Theorem: MellinOfSmooth1a
Proof 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
Proof 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)
Theorem: MellinOfSmooth1a
Proof 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]
Proof 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
Theorem: MellinOfSmooth1a
Proof 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
Proof state after:
no goals
Theorem: MellinOfSmooth1a
Proof 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]
Proof state after:
no goals
Theorem: MellinOfSmooth1b
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
⊢ (fun s => ‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s‖) =O[𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}] fun s => 1 / (ε * ‖s‖ ^ 2)
Tactic:
have := MellinOfPsi diffΨ suppΨ (mul_pos εpos σ₁pos) (σ₂ := ε * σ₂)
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
this : (fun s => ‖𝓜 (fun x => ↑(Ψ x)) s‖) =O[𝓟 {s | ε * σ₁ ≤ s.re ∧ s.re ≤ ε * σ₂}] fun s => 1 / ‖s‖
⊢ (fun s => ‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s‖) =O[𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}] fun s => 1 / (ε * ‖s‖ ^ 2)
Theorem: MellinOfSmooth1b
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
this : (fun s => ‖𝓜 (fun x => ↑(Ψ x)) s‖) =O[𝓟 {s | ε * σ₁ ≤ s.re ∧ s.re ≤ ε * σ₂}] fun s => 1 / ‖s‖
⊢ (fun s => ‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s‖) =O[𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}] fun s => 1 / (ε * ‖s‖ ^ 2)
Tactic:
rw [Asymptotics.isBigO_iff] at this ⊢
Proof state after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
this : ∃ c, ∀ᶠ (x : ℂ) in 𝓟 {s | ε * σ₁ ≤ s.re ∧ s.re ≤ ε * σ₂}, ‖‖𝓜 (fun x => ↑(Ψ x)) x‖‖ ≤ c * ‖1 / ‖x‖‖
⊢ ∃ c, ∀ᶠ (x : ℂ) in 𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}, ‖‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) x‖‖ ≤ c * ‖1 / (ε * ‖x‖ ^ 2)‖
Theorem: MellinOfSmooth1b
Proof state before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
this : ∃ c, ∀ᶠ (x : ℂ) in 𝓟 {s | ε * σ₁ ≤ s.re ∧ s.re ≤ ε * σ₂}, ‖‖𝓜 (fun x => ↑(Ψ x)) x‖‖ ≤ c * ‖1 / ‖x‖‖
⊢ ∃ c, ∀ᶠ (x : ℂ) in 𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}, ‖‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) x‖‖ ≤ c * ‖1 / (ε * ‖x‖ ^ 2)‖
Tactic:
obtain ⟨c, hc⟩ := this
Proof state after:
case intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ᶠ (x : ℂ) in 𝓟 {s | ε * σ₁ ≤ s.re ∧ s.re ≤ ε * σ₂}, ‖‖𝓜 (fun x => ↑(Ψ x)) x‖‖ ≤ c * ‖1 / ‖x‖‖
⊢ ∃ c, ∀ᶠ (x : ℂ) in 𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}, ‖‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) x‖‖ ≤ c * ‖1 / (ε * ‖x‖ ^ 2)‖
Theorem: MellinOfSmooth1b
Proof state before:
case intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ᶠ (x : ℂ) in 𝓟 {s | ε * σ₁ ≤ s.re ∧ s.re ≤ ε * σ₂}, ‖‖𝓜 (fun x => ↑(Ψ x)) x‖‖ ≤ c * ‖1 / ‖x‖‖
⊢ ∃ c, ∀ᶠ (x : ℂ) in 𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}, ‖‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) x‖‖ ≤ c * ‖1 / (ε * ‖x‖ ^ 2)‖
Tactic:
use c
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ᶠ (x : ℂ) in 𝓟 {s | ε * σ₁ ≤ s.re ∧ s.re ≤ ε * σ₂}, ‖‖𝓜 (fun x => ↑(Ψ x)) x‖‖ ≤ c * ‖1 / ‖x‖‖
⊢ ∀ᶠ (x : ℂ) in 𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}, ‖‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) x‖‖ ≤ c * ‖1 / (ε * ‖x‖ ^ 2)‖
Theorem: MellinOfSmooth1b
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ᶠ (x : ℂ) in 𝓟 {s | ε * σ₁ ≤ s.re ∧ s.re ≤ ε * σ₂}, ‖‖𝓜 (fun x => ↑(Ψ x)) x‖‖ ≤ c * ‖1 / ‖x‖‖
⊢ ∀ᶠ (x : ℂ) in 𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}, ‖‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) x‖‖ ≤ c * ‖1 / (ε * ‖x‖ ^ 2)‖
Tactic:
simp only [norm_norm, norm_div, norm_one, eventually_principal, mem_setOf_eq] at hc ⊢
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
⊢ ∀ (x : ℂ), σ₁ ≤ x.re ∧ x.re ≤ σ₂ → ‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) x‖ ≤ c * (1 / ‖ε * ‖x‖ ^ 2‖)
Theorem: MellinOfSmooth1b
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
⊢ ∀ (x : ℂ), σ₁ ≤ x.re ∧ x.re ≤ σ₂ → ‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) x‖ ≤ c * (1 / ‖ε * ‖x‖ ^ 2‖)
Tactic:
intro s hs
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
⊢ ‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s‖ ≤ c * (1 / ‖ε * ‖s‖ ^ 2‖)
Theorem: MellinOfSmooth1b
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
⊢ ‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) s‖ ≤ c * (1 / ‖ε * ‖s‖ ^ 2‖)
Tactic:
rw [MellinOfSmooth1a Ψ diffΨ suppΨ εpos <| gt_of_ge_of_gt hs.1 σ₁pos]
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
⊢ ‖1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖ε * ‖s‖ ^ 2‖)
Theorem: MellinOfSmooth1b
Proof state before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
⊢ ‖1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖ε * ‖s‖ ^ 2‖)
Tactic:
have : ‖𝓜 (fun x ↦ ↑(Ψ x)) (ε * s)‖ ≤ c * (1 / ‖ε * s‖) := by
  refine hc (ε * s) ?_
  simp only [mul_re, ofReal_re, ofReal_im, zero_mul, sub_zero]
  exact ⟨(mul_le_mul_left εpos).mpr hs.1, (mul_le_mul_left εpos).mpr hs.2⟩
Proof state after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
this : ‖𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖↑ε * s‖)
⊢ ‖1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖ε * ‖s‖ ^ 2‖)