E : Type u_2
F : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
s : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : IsAddHaarMeasure μ
inst✝ : CompleteSpace F
f : LocalHomeomorph E E
hf' : ∀ (x : E), x ∈ f.source → HasFDerivAt (↑f) (f' x) x
g : E → F
this : ↑f '' f.source = f.target
⊢ (∫ (x : E) in f.target, g x ∂μ) = ∫ (x : E) in f.source, abs (ContinuousLinearMap.det (f' x)) • g (↑f x) ∂μ
E : Type u_2
F : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
s : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : IsAddHaarMeasure μ
inst✝ : CompleteSpace F
f : LocalHomeomorph E E
hf' : ∀ (x : E), x ∈ f.source → HasFDerivAt (↑f) (f' x) x
g : E → F
⊢ (∫ (x : E) in f.target, g x ∂μ) = ∫ (x : E) in f.source, abs (ContinuousLinearMap.det (f' x)) • g (↑f x) ∂μ
have : f '' f.source = f.target := LocalEquiv.image_source_eq_target f.toLocalEquiv
E : Type u_2
F : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
s : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : IsAddHaarMeasure μ
inst✝ : CompleteSpace F
f : LocalHomeomorph E E
hf' : ∀ (x : E), x ∈ f.source → HasFDerivAt (↑f) (f' x) x
g : E → F
this : ↑f '' f.source = f.target
⊢ (∫ (x : E) in ↑f '' f.source, g x ∂μ) = ∫ (x : E) in f.source, abs (ContinuousLinearMap.det (f' x)) • g (↑f x) ∂μ
E : Type u_2
F : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
s : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : IsAddHaarMeasure μ
inst✝ : CompleteSpace F
f : LocalHomeomorph E E
hf' : ∀ (x : E), x ∈ f.source → HasFDerivAt (↑f) (f' x) x
g : E → F
this : ↑f '' f.source = f.target
⊢ (∫ (x : E) in f.target, g x ∂μ) = ∫ (x : E) in f.source, abs (ContinuousLinearMap.det (f' x)) • g (↑f x) ∂μ
rw [← this]
E : Type u_2
F : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
s : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : IsAddHaarMeasure μ
inst✝ : CompleteSpace F
f : LocalHomeomorph E E
hf' : ∀ (x : E), x ∈ f.source → HasFDerivAt (↑f) (f' x) x
g : E → F
this : ↑f '' f.source = f.target
⊢ ∀ (x : E), x ∈ f.source → HasFDerivWithinAt (↑f) (f' x) f.source x
E : Type u_2
F : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
s : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : IsAddHaarMeasure μ
inst✝ : CompleteSpace F
f : LocalHomeomorph E E
hf' : ∀ (x : E), x ∈ f.source → HasFDerivAt (↑f) (f' x) x
g : E → F
this : ↑f '' f.source = f.target
⊢ (∫ (x : E) in ↑f '' f.source, g x ∂μ) = ∫ (x : E) in f.source, abs (ContinuousLinearMap.det (f' x)) • g (↑f x) ∂μ
apply integral_image_eq_integral_abs_det_fderiv_smul μ f.open_source.measurableSet _ f.injOn
E : Type u_2
F : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
s : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : IsAddHaarMeasure μ
inst✝ : CompleteSpace F
f : LocalHomeomorph E E
hf' : ∀ (x : E), x ∈ f.source → HasFDerivAt (↑f) (f' x) x
g : E → F
this : ↑f '' f.source = f.target
x : E
hx : x ∈ f.source
⊢ HasFDerivWithinAt (↑f) (f' x) f.source x
E : Type u_2
F : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
s : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : IsAddHaarMeasure μ
inst✝ : CompleteSpace F
f : LocalHomeomorph E E
hf' : ∀ (x : E), x ∈ f.source → HasFDerivAt (↑f) (f' x) x
g : E → F
this : ↑f '' f.source = f.target
⊢ ∀ (x : E), x ∈ f.source → HasFDerivWithinAt (↑f) (f' x) f.source x
intro x hx
no goals
E : Type u_2
F : Type u_1
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
s : Set E
f✝ : E → E
f' : E → E →L[ℝ] E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : IsAddHaarMeasure μ
inst✝ : CompleteSpace F
f : LocalHomeomorph E E
hf' : ∀ (x : E), x ∈ f.source → HasFDerivAt (↑f) (f' x) x
g : E → F
this : ↑f '' f.source = f.target
x : E
hx : x ∈ f.source
⊢ HasFDerivWithinAt (↑f) (f' x) f.source x
exact (hf' x hx).hasFDerivWithinAt