aemeasurable_toNNReal_abs_det_fderivWithin

English

The NNReal-valued absolute determinant function of the derivative is almost everywhere measurable on the restricted domain.

Русский

Пусть |det f'(x)| приводится к NNReal и измеримо почти всюду на ограниченной области.

LaTeX

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

Lean4

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

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