E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ Integrable (indicator (Ioi c) fun x => f (a * x)) ↔ IntegrableOn f (Ioi (a * c))
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ IntegrableOn (fun x => f (a * x)) (Ioi c) ↔ IntegrableOn f (Ioi (a * c))
rw [← integrable_indicator_iff (measurableSet_Ioi : MeasurableSet <| Ioi c)]
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ Integrable (indicator (Ioi c) fun x => f (a * x)) ↔ Integrable (indicator (Ioi (a * c)) f)
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ Integrable (indicator (Ioi c) fun x => f (a * x)) ↔ IntegrableOn f (Ioi (a * c))
rw [← integrable_indicator_iff (measurableSet_Ioi : MeasurableSet <| Ioi <| a * c)]
case h.e'_1.h.e'_5
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ (indicator (Ioi c) fun x => f (a * x)) = fun x => indicator (Ioi (a * c)) f (a * x)
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ Integrable (indicator (Ioi c) fun x => f (a * x)) ↔ Integrable (indicator (Ioi (a * c)) f)
convert integrable_comp_mul_left_iff ((Ioi (a * c)).indicator f) ha.ne' using 2
case h.e'_1.h.e'_5.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
x : ℝ
⊢ indicator (Ioi c) (fun x => f (a * x)) x = indicator (Ioi (a * c)) f (a * x)
case h.e'_1.h.e'_5
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
⊢ (indicator (Ioi c) fun x => f (a * x)) = fun x => indicator (Ioi (a * c)) f (a * x)
ext1 x
case h.e'_1.h.e'_5.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
x : ℝ
⊢ indicator (Ioi c) (fun x => f (a * x)) x = indicator (Ioi c) (f ∘ HMul.hMul a) x
case h.e'_1.h.e'_5.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
x : ℝ
⊢ indicator (Ioi c) (fun x => f (a * x)) x = indicator (Ioi (a * c)) f (a * x)
rw [← indicator_comp_right, preimage_const_mul_Ioi _ ha, mul_comm a c, mul_div_cancel _ ha.ne']
no goals
case h.e'_1.h.e'_5.h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℝ → E
c a : ℝ
ha : 0 < a
x : ℝ
⊢ indicator (Ioi c) (fun x => f (a * x)) x = indicator (Ioi c) (f ∘ HMul.hMul a) x
rfl