E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
⊢ (∫ (x : ℝ) in Ioi a, g (b * x)) = abs b⁻¹ • ∫ (x : ℝ) in Ioi (b * a), g x
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
a b : ℝ
hb : 0 < b
⊢ (∫ (x : ℝ) in Ioi a, g (b * x)) = abs b⁻¹ • ∫ (x : ℝ) in Ioi (b * a), g x
have : ∀ c : ℝ, MeasurableSet (Ioi c) := fun c => measurableSet_Ioi
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
⊢ (∫ (x : ℝ), indicator (Ioi a) (fun x => g (b * x)) x) = ∫ (x : ℝ), indicator (Ioi (b * a)) (fun x => g x) (b * x)
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
⊢ (∫ (x : ℝ) in Ioi a, g (b * x)) = abs b⁻¹ • ∫ (x : ℝ) in Ioi (b * a), g x
rw [← integral_indicator (this a), ← integral_indicator (this (b * a)),
  ← Measure.integral_comp_mul_left]
case e_f
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
⊢ (fun x => indicator (Ioi a) (fun x => g (b * x)) x) = fun x => indicator (Ioi (b * a)) (fun x => g x) (b * x)
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
⊢ (∫ (x : ℝ), indicator (Ioi a) (fun x => g (b * x)) x) = ∫ (x : ℝ), indicator (Ioi (b * a)) (fun x => g x) (b * x)
congr
case e_f.h
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
x : ℝ
⊢ indicator (Ioi a) (fun x => g (b * x)) x = indicator (Ioi (b * a)) (fun x => g x) (b * x)
case e_f
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
⊢ (fun x => indicator (Ioi a) (fun x => g (b * x)) x) = fun x => indicator (Ioi (b * a)) (fun x => g x) (b * x)
ext1 x
case e_f.h
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
x : ℝ
⊢ indicator (Ioi a) (fun x => g (b * x)) x = indicator (Ioi a) ((fun x => g x) ∘ HMul.hMul b) x
case e_f.h
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
x : ℝ
⊢ indicator (Ioi a) (fun x => g (b * x)) x = indicator (Ioi (b * a)) (fun x => g x) (b * x)
rw [← indicator_comp_right, preimage_const_mul_Ioi _ hb, mul_div_cancel_left _ hb.ne']
no goals
case e_f.h
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
g : ℝ → E
a b : ℝ
hb : 0 < b
this : ∀ (c : ℝ), MeasurableSet (Ioi c)
x : ℝ
⊢ indicator (Ioi a) (fun x => g (b * x)) x = indicator (Ioi a) ((fun x => g x) ∘ HMul.hMul b) x
rfl