Theorems · Theorem · measure theory

MeasureTheory.addHaar_image_le_mul_of_det_lt

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (A : E →L[ℝ] E)
  {m : NNReal},
  ENNReal.ofReal |A.det| < ↑m →
    ∀ᶠ (δ : NNReal) in nhdsWithin 0 (Set.Ioi 0),
      ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → μ (f '' s) ≤ ↑m * μ s

Let f be a function which is sufficiently close (in the Lipschitz sense) to a given linear map A. Then it expands the volume of any set by at most m for any m > det A.

Defined in

Mathlib.MeasureTheory.Function.Jacobian

Cited by

4 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensionalMeasurableSpaceBorelSpaceMeasureTheory.Measure.IsAddHaarMeasure