Theorems · Theorem · measure theory

MeasureTheory.addHaar_image_eq_zero_of_det_fderivWithin_eq_zero_aux

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure],
  (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
    ∀ (R : ℝ),
      s ⊆ Metric.closedBall 0 R →
        ∀ (ε : NNReal), 0 < ε → (∀ x ∈ s, (f' x).det = 0) → μ (f '' s) ≤ ↑ε * μ (Metric.closedBall 0 R)

A version of Sard's lemma in fixed dimension: given a differentiable function from E to E and a set where the differential is not invertible, then the image of this set has zero measure. Here, we give an auxiliary statement towards this result.

Defined in

Mathlib.MeasureTheory.Function.Jacobian

Cited by

1 results in Mathlib

Foundations

Depth 269 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsAddHaarMeasure