Theorem: MellinConvolutionTransform (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
⊢ 𝓜 (MellinConvolution f g) s = 𝓜 f s * 𝓜 g s
Tactic:
dsimp [MellinTransform, MellinConvolution]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioi 0, (∫ (y : ℝ) in Ioi 0, f y * g (x / y) / ↑y) * ↑x ^ (s - 1) =
    (∫ (x : ℝ) in Ioi 0, f x * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioi 0, (∫ (y : ℝ) in Ioi 0, f y * g (x / y) / ↑y) * ↑x ^ (s - 1) =
    (∫ (x : ℝ) in Ioi 0, f x * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)
Tactic:
set f₁ : ℝ × ℝ → ℂ := fun ⟨x, y⟩ ↦ f y * g (x / y) / (y : ℂ) * (x : ℂ) ^ (s - 1)
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
⊢ ∫ (x : ℝ) in Ioi 0, (∫ (y : ℝ) in Ioi 0, f y * g (x / y) / ↑y) * ↑x ^ (s - 1) =
    (∫ (x : ℝ) in Ioi 0, f x * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
⊢ ∫ (x : ℝ) in Ioi 0, (∫ (y : ℝ) in Ioi 0, f y * g (x / y) / ↑y) * ↑x ^ (s - 1) =
    (∫ (x : ℝ) in Ioi 0, f x * ↑x ^ (s - 1)) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)
Tactic:
calc
  _ = ∫ (x : ℝ) in Ioi 0, ∫ (y : ℝ) in Ioi 0, f₁ (x, y) := ?_
  _ = ∫ (y : ℝ) in Ioi 0, ∫ (x : ℝ) in Ioi 0, f₁ (x, y) := setIntegral_integral_swap _ hf
  _ = ∫ (y : ℝ) in Ioi 0, ∫ (x : ℝ) in Ioi 0, f y * g (x / y) / ↑y * ↑x ^ (s - 1) := rfl
  _ = ∫ (y : ℝ) in Ioi 0, ∫ (x : ℝ) in Ioi 0, f y * g (x * y / y) / ↑y * ↑(x * y) ^ (s - 1) * y := ?_
  _ = ∫ (y : ℝ) in Ioi 0, ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)) := ?_
  _ = ∫ (y : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1) := ?_
  _ = _ := integral_mul_right _ _
<;> try (rw [setIntegral_congr (by simp)]; intro y hy; simp only [ofReal_mul])
State after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ (∫ (y_1 : ℝ) in Ioi 0, f y_1 * g (y / y_1) / ↑y_1) * ↑y ^ (s - 1) = ∫ (y_1 : ℝ) in Ioi 0, f₁ (y, y_1)

case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x / y) / ↑y * ↑x ^ (s - 1) =
    ∫ (x : ℝ) in Ioi 0, f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y

case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y =
    ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))

case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)) =
    f y * ↑y ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)

State before:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
⊢ ∫ (y : ℝ) (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)) =
    ∫ (y : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)
Tactic:
(rw [setIntegral_congr (by simp)]; intro y hy; simp only [ofReal_mul])
State after:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)) =
    f y * ↑y ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)

State before:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
⊢ ∫ (y : ℝ) (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)) =
    ∫ (y : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)
Tactic:
rw [setIntegral_congr (by simp)]
State after:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
⊢ EqOn (fun y => ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)))
    (fun x => f x * ↑x ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)) (Ioi 0)

State before:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
⊢ EqOn (fun y => ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)))
    (fun x => f x * ↑x ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)) (Ioi 0)
Tactic:
intro y hy
State after:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))) y =
    (fun x => f x * ↑x ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)) y

State before:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))) y =
    (fun x => f x * ↑x ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)) y
Tactic:
simp only [ofReal_mul]
State after:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)) =
    f y * ↑y ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
⊢ MeasurableSet (Ioi 0)
Tactic:
simp
State after:
no goals

State before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ (∫ (y_1 : ℝ) in Ioi 0, f y_1 * g (y / y_1) / ↑y_1) * ↑y ^ (s - 1) = ∫ (y_1 : ℝ) in Ioi 0, f₁ (y, y_1)
Tactic:
simp only [integral_mul_right]
State after:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ (∫ (y_1 : ℝ) in Ioi 0, f y_1 * g (y / y_1) / ↑y_1) * ↑y ^ (s - 1) =
    (∫ (a : ℝ) in Ioi 0, f a * g (y / a) / ↑a) * ↑y ^ (s - 1)

State before:
case calc_1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ (∫ (y_1 : ℝ) in Ioi 0, f y_1 * g (y / y_1) / ↑y_1) * ↑y ^ (s - 1) =
    (∫ (a : ℝ) in Ioi 0, f a * g (y / a) / ↑a) * ↑y ^ (s - 1)
Tactic:
rfl
State after:
no goals

State before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x / y) / ↑y * ↑x ^ (s - 1) =
    ∫ (x : ℝ) in Ioi 0, f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y
Tactic:
simp only [integral_mul_right]
State after:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x / y) / ↑y * ↑x ^ (s - 1) =
    (∫ (a : ℝ) in Ioi 0, f y * g (a * y / y) / ↑y * (↑a * ↑y) ^ (s - 1)) * ↑y

State before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x / y) / ↑y * ↑x ^ (s - 1) =
    (∫ (a : ℝ) in Ioi 0, f y * g (a * y / y) / ↑y * (↑a * ↑y) ^ (s - 1)) * ↑y
Tactic:
have := integral_comp_mul_right_Ioi (fun x ↦ f y * g (x / y) / (y : ℂ) * (x : ℂ) ^ (s - 1)) 0 hy
State after:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
this :
  ∫ (x : ℝ) in Ioi 0, (fun x => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (x * y) =
    y⁻¹ • ∫ (x : ℝ) in Ioi (0 * y), (fun x => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) x
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x / y) / ↑y * ↑x ^ (s - 1) =
    (∫ (a : ℝ) in Ioi 0, f y * g (a * y / y) / ↑y * (↑a * ↑y) ^ (s - 1)) * ↑y

State before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
this :
  ∫ (x : ℝ) in Ioi 0, (fun x => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (x * y) =
    y⁻¹ • ∫ (x : ℝ) in Ioi (0 * y), (fun x => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) x
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x / y) / ↑y * ↑x ^ (s - 1) =
    (∫ (a : ℝ) in Ioi 0, f y * g (a * y / y) / ↑y * (↑a * ↑y) ^ (s - 1)) * ↑y
Tactic:
have y_ne_zeroℂ : (y : ℂ) ≠ 0 := slitPlane_ne_zero (Or.inl hy)
State after:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
this :
  ∫ (x : ℝ) in Ioi 0, (fun x => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (x * y) =
    y⁻¹ • ∫ (x : ℝ) in Ioi (0 * y), (fun x => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) x
y_ne_zeroℂ : ↑y ≠ 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x / y) / ↑y * ↑x ^ (s - 1) =
    (∫ (a : ℝ) in Ioi 0, f y * g (a * y / y) / ↑y * (↑a * ↑y) ^ (s - 1)) * ↑y

State before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
this :
  ∫ (x : ℝ) in Ioi 0, (fun x => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (x * y) =
    y⁻¹ • ∫ (x : ℝ) in Ioi (0 * y), (fun x => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) x
y_ne_zeroℂ : ↑y ≠ 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x / y) / ↑y * ↑x ^ (s - 1) =
    (∫ (a : ℝ) in Ioi 0, f y * g (a * y / y) / ↑y * (↑a * ↑y) ^ (s - 1)) * ↑y
Tactic:
field_simp at this ⊢
State after:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
y_ne_zeroℂ : ↑y ≠ 0
this :
  (∫ (x : ℝ) in Ioi 0, f y * g (x * y / y) * (↑x * ↑y) ^ (s - 1) / ↑y) * ↑y =
    ∫ (x : ℝ) in Ioi 0, f y * g (x / y) * ↑x ^ (s - 1) / ↑y
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x / y) * ↑x ^ (s - 1) / ↑y =
    (∫ (a : ℝ) in Ioi 0, f y * g (a * y / y) * (↑a * ↑y) ^ (s - 1) / ↑y) * ↑y

State before:
case calc_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
y_ne_zeroℂ : ↑y ≠ 0
this :
  (∫ (x : ℝ) in Ioi 0, f y * g (x * y / y) * (↑x * ↑y) ^ (s - 1) / ↑y) * ↑y =
    ∫ (x : ℝ) in Ioi 0, f y * g (x / y) * ↑x ^ (s - 1) / ↑y
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x / y) * ↑x ^ (s - 1) / ↑y =
    (∫ (a : ℝ) in Ioi 0, f y * g (a * y / y) * (↑a * ↑y) ^ (s - 1) / ↑y) * ↑y
Tactic:
rw [this]
State after:
no goals

State before:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y =
    ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))
Tactic:
rw [setIntegral_congr (by simp)]
State after:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ EqOn (fun x => f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y)
    (fun x => f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))) (Ioi 0)

State before:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ EqOn (fun x => f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y)
    (fun x => f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))) (Ioi 0)
Tactic:
intro x hx
State after:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
x : ℝ
hx : x ∈ Ioi 0
⊢ (fun x => f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y) x =
    (fun x => f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))) x

State before:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
x : ℝ
hx : x ∈ Ioi 0
⊢ (fun x => f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y) x =
    (fun x => f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))) x
Tactic:
have y_ne_zeroℝ : y ≠ 0 := ne_of_gt (mem_Ioi.mp hy)
State after:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
x : ℝ
hx : x ∈ Ioi 0
y_ne_zeroℝ : y ≠ 0
⊢ (fun x => f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y) x =
    (fun x => f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))) x

State before:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
x : ℝ
hx : x ∈ Ioi 0
y_ne_zeroℝ : y ≠ 0
⊢ (fun x => f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y) x =
    (fun x => f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))) x
Tactic:
have y_ne_zeroℂ : (y : ℂ) ≠ 0 := by exact_mod_cast y_ne_zeroℝ
State after:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
x : ℝ
hx : x ∈ Ioi 0
y_ne_zeroℝ : y ≠ 0
y_ne_zeroℂ : ↑y ≠ 0
⊢ (fun x => f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y) x =
    (fun x => f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))) x

State before:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
x : ℝ
hx : x ∈ Ioi 0
y_ne_zeroℝ : y ≠ 0
y_ne_zeroℂ : ↑y ≠ 0
⊢ (fun x => f y * g (x * y / y) / ↑y * (↑x * ↑y) ^ (s - 1) * ↑y) x =
    (fun x => f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))) x
Tactic:
field_simp [mul_cpow_ofReal_nonneg (LT.lt.le hx) (LT.lt.le hy)]
State after:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
x : ℝ
hx : x ∈ Ioi 0
y_ne_zeroℝ : y ≠ 0
y_ne_zeroℂ : ↑y ≠ 0
⊢ f y * g x * (↑x ^ (s - 1) * ↑y ^ (s - 1)) = f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))

State before:
case calc_3
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
x : ℝ
hx : x ∈ Ioi 0
y_ne_zeroℝ : y ≠ 0
y_ne_zeroℂ : ↑y ≠ 0
⊢ f y * g x * (↑x ^ (s - 1) * ↑y ^ (s - 1)) = f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1))
Tactic:
ring
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ MeasurableSet (Ioi 0)
Tactic:
simp
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
x : ℝ
hx : x ∈ Ioi 0
y_ne_zeroℝ : y ≠ 0
⊢ ↑y ≠ 0
Tactic:
exact_mod_cast y_ne_zeroℝ
State after:
no goals

State before:
case calc_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f g : ℝ → ℂ
s : ℂ
hf : IntegrableOn (Function.uncurry fun x y => f y * g (x / y) / ↑y * ↑x ^ (s - 1)) (Ioi 0 ×ˢ Ioi 0) volume
f₁ : ℝ × ℝ → ℂ :=
  fun x =>
    match x with
    | (x, y) => f y * g (x / y) / ↑y * ↑x ^ (s - 1)
y : ℝ
hy : y ∈ Ioi 0
⊢ ∫ (x : ℝ) in Ioi 0, f y * ↑y ^ (s - 1) * (g x * ↑x ^ (s - 1)) =
    f y * ↑y ^ (s - 1) * ∫ (x : ℝ) in Ioi 0, g x * ↑x ^ (s - 1)
Tactic:
apply integral_mul_left
State after:
no goals