aemeasurable_ofReal_abs_det_fderivWithin

English

The absolute determinant of the derivative is almost everywhere measurable on the set.

Русский

Модуль детерминанта производной почти повсюду измерим на множестве.

LaTeX

$$$$ \text{ae-measurable} \ x \mapsto |\det f'(x)| \,, \ x \in s.$$$$

Lean4

theorem aemeasurable_ofReal_abs_det_fderivWithin (hs : MeasurableSet s)
    (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) :
    AEMeasurable (fun x => ENNReal.ofReal |(f' x).det|) (μ.restrict s) :=
  by
  apply ENNReal.measurable_ofReal.comp_aemeasurable
  refine continuous_abs.measurable.comp_aemeasurable ?_
  refine ContinuousLinearMap.continuous_det.measurable.comp_aemeasurable ?_
  exact aemeasurable_fderivWithin μ hs hf'

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