integral_target_eq_integral_abs_det_fderiv_smul

English

On a measurable s, with f injective and differentiable, the density-weighted pullback under the restricted map coincides with the image measure on f''s.

Русский

На измеримом s, если f инъективна и дифференцируема, то тензорная плотностная тяга обратно через ограниченную карту совпадает с образовой мерой на f''s.

LaTeX

$$$$ \\mathrm{map}(s\\restrict f) \\Bigl(\\mathrm{comap}(\\uparrow)(\\mu\\withDensity |\\det f'|)\\Bigr) = \\mu\\restriction (f''s) $$$$

Lean4

theorem integral_target_eq_integral_abs_det_fderiv_smul {f : OpenPartialHomeomorph E E}
    (hf' : ∀ x ∈ f.source, HasFDerivAt f (f' x) x) (g : E → F) :
    ∫ x in f.target, g x ∂μ = ∫ x in f.source, |(f' x).det| • g (f x) ∂μ :=
  by
  have : f '' f.source = f.target := PartialEquiv.image_source_eq_target f.toPartialEquiv
  rw [← this]
  apply integral_image_eq_integral_abs_det_fderiv_smul μ f.open_source.measurableSet _ f.injOn
  intro x hx
  exact (hf' x hx).hasFDerivWithinAt

Похожие утверждения