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

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

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

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
p : ℝ
hp : p ≠ 0
y : ℝ
hy : y ∈ Ioi 0
⊢ (fun y => |p| * f (y ^ p) / y) y = (fun x => (|p| * x ^ (p - 1)) • (f (x ^ p) / x ^ p)) y
Tactic:
have ypos : 0 < y := mem_Ioi.mp hy
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
p : ℝ
hp : p ≠ 0
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
⊢ (fun y => |p| * f (y ^ p) / y) y = (fun x => (|p| * x ^ (p - 1)) • (f (x ^ p) / x ^ p)) y

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
p : ℝ
hp : p ≠ 0
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
⊢ (fun y => |p| * f (y ^ p) / y) y = (fun x => (|p| * x ^ (p - 1)) • (f (x ^ p) / x ^ p)) y
Tactic:
field_simp [rpow_sub_one]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
p : ℝ
hp : p ≠ 0
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
⊢ |p| * f (y ^ p) * (y * y ^ p) = |p| * y ^ p * f (y ^ p) * y

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
p : ℝ
hp : p ≠ 0
y : ℝ
hy : y ∈ Ioi 0
ypos : 0 < y
⊢ |p| * f (y ^ p) * (y * y ^ p) = |p| * y ^ p * f (y ^ p) * y
Tactic:
ring
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
p : ℝ
hp : p ≠ 0
⊢ MeasurableSet (Ioi 0)
Tactic:
simp
State after:
no goals