case inr
ι : Type ?u.7319192
𝕜 : Type ?u.7319195
E : Type u_1
F : Type ?u.7319201
A : Type ?u.7319204
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
this :
  ∀ {a b : ℝ}, IntervalIntegrable f volume a b → a ≤ b → IntervalIntegrable (fun x => f (x + c)) volume (a - c) (b - c)
h : ¬a ≤ b
⊢ IntervalIntegrable (fun x => f (x + c)) volume (a - c) (b - c)

ι : Type ?u.7319192
𝕜 : Type ?u.7319195
E : Type u_1
F : Type ?u.7319201
A : Type ?u.7319204
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a✝ b✝ : ℝ
μ : MeasureTheory.Measure ℝ
c a b : ℝ
hf : IntervalIntegrable f volume a b
h : a ≤ b
⊢ IntervalIntegrable (fun x => f (x + c)) volume (a - c) (b - c)
ι : Type ?u.7319192
𝕜 : Type ?u.7319195
E : Type u_1
F : Type ?u.7319201
A : Type ?u.7319204
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
⊢ IntervalIntegrable (fun x => f (x + c)) volume (a - c) (b - c)
wlog h : a ≤ b generalizing a b
ι : Type ?u.7319192
𝕜 : Type ?u.7319195
E : Type u_1
F : Type ?u.7319201
A : Type ?u.7319204
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a✝ b✝ : ℝ
μ : MeasureTheory.Measure ℝ
c a b : ℝ
hf : IntegrableOn f [[a, b]]
h : a ≤ b
⊢ IntegrableOn (fun x => f (x + c)) [[a - c, b - c]]
ι : Type ?u.7319192
𝕜 : Type ?u.7319195
E : Type u_1
F : Type ?u.7319201
A : Type ?u.7319204
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a✝ b✝ : ℝ
μ : MeasureTheory.Measure ℝ
c a b : ℝ
hf : IntervalIntegrable f volume a b
h : a ≤ b
⊢ IntervalIntegrable (fun x => f (x + c)) volume (a - c) (b - c)
rw [intervalIntegrable_iff'] at hf ⊢
ι : Type ?u.7319192
𝕜 : Type ?u.7319195
E : Type u_1
F : Type ?u.7319201
A✝ : Type ?u.7319204
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a✝ b✝ : ℝ
μ : MeasureTheory.Measure ℝ
c a b : ℝ
hf : IntegrableOn f [[a, b]]
h : a ≤ b
A : MeasurableEmbedding fun x => x + c
⊢ IntegrableOn (fun x => f (x + c)) [[a - c, b - c]]
ι : Type ?u.7319192
𝕜 : Type ?u.7319195
E : Type u_1
F : Type ?u.7319201
A : Type ?u.7319204
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a✝ b✝ : ℝ
μ : MeasureTheory.Measure ℝ
c a b : ℝ
hf : IntegrableOn f [[a, b]]
h : a ≤ b
⊢ IntegrableOn (fun x => f (x + c)) [[a - c, b - c]]
have A : MeasurableEmbedding fun x => x + c :=
  (Homeomorph.addRight c).closedEmbedding.measurableEmbedding
ι : Type ?u.7319192
𝕜 : Type ?u.7319195
E : Type u_1
F : Type ?u.7319201
A✝ : Type ?u.7319204
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a✝ b✝ : ℝ
μ : MeasureTheory.Measure ℝ
c a b : ℝ
hf : IntegrableOn f [[a, b]]
h : a ≤ b
A : MeasurableEmbedding fun x => x + c
⊢ IntegrableOn (fun x => f (x + c)) [[a - c, b - c]]
ι : Type ?u.7319192
𝕜 : Type ?u.7319195
E : Type u_1
F : Type ?u.7319201
A✝ : Type ?u.7319204
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a✝ b✝ : ℝ
μ : MeasureTheory.Measure ℝ
c a b : ℝ
hf : IntegrableOn f [[a, b]]
h : a ≤ b
A : MeasurableEmbedding fun x => x + c
⊢ IntegrableOn (fun x => f (x + c)) [[a - c, b - c]]
rw [← map_add_right_eq_self volume c] at hf
case h.e'_6
ι : Type ?u.7319192
𝕜 : Type ?u.7319195
E : Type u_1
F : Type ?u.7319201
A✝ : Type ?u.7319204
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a✝ b✝ : ℝ
μ : MeasureTheory.Measure ℝ
c a b : ℝ
hf : IntegrableOn f [[a, b]]
h : a ≤ b
A : MeasurableEmbedding fun x => x + c
⊢ [[a - c, b - c]] = (fun x => x + c) ⁻¹' [[a, b]]
ι : Type ?u.7319192
𝕜 : Type ?u.7319195
E : Type u_1
F : Type ?u.7319201
A✝ : Type ?u.7319204
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a✝ b✝ : ℝ
μ : MeasureTheory.Measure ℝ
c a b : ℝ
hf : IntegrableOn f [[a, b]]
h : a ≤ b
A : MeasurableEmbedding fun x => x + c
⊢ IntegrableOn (fun x => f (x + c)) [[a - c, b - c]]
convert (MeasurableEmbedding.integrableOn_map_iff A).mp hf using 1
no goals
case h.e'_6
ι : Type ?u.7319192
𝕜 : Type ?u.7319195
E : Type u_1
F : Type ?u.7319201
A✝ : Type ?u.7319204
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A✝
f g : ℝ → E
a✝ b✝ : ℝ
μ : MeasureTheory.Measure ℝ
c a b : ℝ
hf : IntegrableOn f [[a, b]]
h : a ≤ b
A : MeasurableEmbedding fun x => x + c
⊢ [[a - c, b - c]] = (fun x => x + c) ⁻¹' [[a, b]]
rw [preimage_add_const_uIcc]
no goals
case inr
ι : Type ?u.7319192
𝕜 : Type ?u.7319195
E : Type u_1
F : Type ?u.7319201
A : Type ?u.7319204
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedRing A
f g : ℝ → E
a b : ℝ
μ : MeasureTheory.Measure ℝ
hf : IntervalIntegrable f volume a b
c : ℝ
this :
  ∀ {a b : ℝ}, IntervalIntegrable f volume a b → a ≤ b → IntervalIntegrable (fun x => f (x + c)) volume (a - c) (b - c)
h : ¬a ≤ b
⊢ IntervalIntegrable (fun x => f (x + c)) volume (a - c) (b - c)
exact IntervalIntegrable.symm (this hf.symm (le_of_not_le h))