Theorem: MeasureTheory.integral_comp_inv_I0i_haar (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
⊢ ∫ (y : ℝ) in Ioi 0, f (1 / y) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y
Tactic:
have := integral_comp_rpow_Ioi (fun y ↦ f y / y) (p := -1) (by simp)
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
⊢ ∫ (y : ℝ) in Ioi 0, f (1 / y) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
⊢ ∫ (y : ℝ) in Ioi 0, f (1 / y) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y
Tactic:
rw [← this, setIntegral_congr (by simp)]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
⊢ EqOn (fun y => f (1 / y) / ↑y) (fun x => (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1))) (Ioi 0)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
⊢ EqOn (fun y => f (1 / y) / ↑y) (fun x => (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1))) (Ioi 0)
Tactic:
intro y hy
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => f (1 / y) / ↑y) y = (fun x => (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1))) y

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => f (1 / y) / ↑y) y = (fun x => (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1))) y
Tactic:
have : (y : 𝕂) ≠ 0 := (RCLike.ofReal_ne_zero).mpr <| LT.lt.ne' hy
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this✝ :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
y : ℝ
hy : y ∈ Ioi 0
this : ↑y ≠ 0
⊢ (fun y => f (1 / y) / ↑y) y = (fun x => (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1))) y

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this✝ :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
y : ℝ
hy : y ∈ Ioi 0
this : ↑y ≠ 0
⊢ (fun y => f (1 / y) / ↑y) y = (fun x => (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1))) y
Tactic:
field_simp [RCLike.real_smul_eq_coe_mul]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this✝ :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
y : ℝ
hy : y ∈ Ioi 0
this : ↑y ≠ 0
⊢ f (1 / y) = ↑(y ^ (-1 - 1)) * f (y ^ (-1)) * ↑y / ↑(y ^ (-1))

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this✝ :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
y : ℝ
hy : y ∈ Ioi 0
this : ↑y ≠ 0
⊢ f (1 / y) = ↑(y ^ (-1 - 1)) * f (y ^ (-1)) * ↑y / ↑(y ^ (-1))
Tactic:
ring_nf
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this✝ :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
y : ℝ
hy : y ∈ Ioi 0
this : ↑y ≠ 0
⊢ f y⁻¹ = ↑(y ^ (-2)) * f (y ^ (-1)) * ↑y * (↑(y ^ (-1)))⁻¹

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this✝ :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
y : ℝ
hy : y ∈ Ioi 0
this : ↑y ≠ 0
⊢ f y⁻¹ = ↑(y ^ (-2)) * f (y ^ (-1)) * ↑y * (↑(y ^ (-1)))⁻¹
Tactic:
rw [rpow_neg_one, mul_assoc, rpow_neg <| le_of_lt <| mem_Ioi.mp hy]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this✝ :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
y : ℝ
hy : y ∈ Ioi 0
this : ↑y ≠ 0
⊢ f y⁻¹ = ↑(y ^ 2)⁻¹ * f y⁻¹ * (↑y * (↑y⁻¹)⁻¹)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this✝ :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
y : ℝ
hy : y ∈ Ioi 0
this : ↑y ≠ 0
⊢ f y⁻¹ = ↑(y ^ 2)⁻¹ * f y⁻¹ * (↑y * (↑y⁻¹)⁻¹)
Tactic:
field_simp [pow_two]
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
⊢ -1 ≠ 0
Tactic:
simp
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
this :
  ∫ (x : ℝ) in Ioi 0, (|(-1)| * x ^ (-1 - 1)) • (fun y => f y / ↑y) (x ^ (-1)) =
    ∫ (y : ℝ) in Ioi 0, (fun y => f y / ↑y) y
⊢ MeasurableSet (Ioi 0)
Tactic:
simp
State after:
no goals