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

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
⊢ ∫ (y : ℝ) in Ioi 0, f (y * a) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y
Tactic:
have := integral_comp_mul_right_Ioi (fun y ↦ f y / y) 0 ha
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (x : ℝ) in Ioi 0, (fun y => f y / ↑y) (x * a) = a⁻¹ • ∫ (x : ℝ) in Ioi (0 * a), (fun y => f y / ↑y) x
⊢ ∫ (y : ℝ) in Ioi 0, f (y * a) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (x : ℝ) in Ioi 0, (fun y => f y / ↑y) (x * a) = a⁻¹ • ∫ (x : ℝ) in Ioi (0 * a), (fun y => f y / ↑y) x
⊢ ∫ (y : ℝ) in Ioi 0, f (y * a) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y
Tactic:
simp only [RCLike.ofReal_mul, zero_mul, eq_inv_smul_iff₀ (ne_of_gt ha)] at this
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : a • ∫ (x : ℝ) in Ioi 0, f (x * a) / (↑x * ↑a) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
⊢ ∫ (y : ℝ) in Ioi 0, f (y * a) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : a • ∫ (x : ℝ) in Ioi 0, f (x * a) / (↑x * ↑a) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
⊢ ∫ (y : ℝ) in Ioi 0, f (y * a) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y
Tactic:
rw [← integral_smul] at this
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
⊢ ∫ (y : ℝ) in Ioi 0, f (y * a) / ↑y = ∫ (y : ℝ) in Ioi 0, f y / ↑y

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

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
⊢ EqOn (fun y => f (y * a) / ↑y) (fun x => a • (f (x * a) / (↑x * ↑a))) (Ioi 0)
Tactic:
intro _ _
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
x✝ : ℝ
a✝ : x✝ ∈ Ioi 0
⊢ (fun y => f (y * a) / ↑y) x✝ = (fun x => a • (f (x * a) / (↑x * ↑a))) x✝

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
x✝ : ℝ
a✝ : x✝ ∈ Ioi 0
⊢ (fun y => f (y * a) / ↑y) x✝ = (fun x => a • (f (x * a) / (↑x * ↑a))) x✝
Tactic:
simp only [RCLike.real_smul_eq_coe_mul]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
x✝ : ℝ
a✝ : x✝ ∈ Ioi 0
⊢ f (x✝ * a) / ↑x✝ = ↑a * (f (x✝ * a) / (↑x✝ * ↑a))

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
x✝ : ℝ
a✝ : x✝ ∈ Ioi 0
⊢ f (x✝ * a) / ↑x✝ = ↑a * (f (x✝ * a) / (↑x✝ * ↑a))
Tactic:
rw [mul_comm (a : 𝕂), div_mul, mul_div_assoc, div_self ?_, mul_one]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
x✝ : ℝ
a✝ : x✝ ∈ Ioi 0
⊢ ↑a ≠ 0

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
x✝ : ℝ
a✝ : x✝ ∈ Ioi 0
⊢ ↑a ≠ 0
Tactic:
exact (RCLike.ofReal_ne_zero).mpr <| ne_of_gt ha
State after:
no goals

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → 𝕂
a : ℝ
ha : 0 < a
this : ∫ (a_1 : ℝ) in Ioi 0, a • (f (a_1 * a) / (↑a_1 * ↑a)) = ∫ (x : ℝ) in Ioi 0, f x / ↑x
⊢ MeasurableSet (Ioi 0)
Tactic:
simp
State after:
no goals