Theorems · Theorem · measure theory

MeasureTheory.mul_le_addHaar_image_of_lt_det

∀ {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},
  ↑m < ENNReal.ofReal |A.det| →
    ∀ᶠ (δ : NNReal) in nhdsWithin 0 (Set.Ioi 0),
      ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' 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 least m for any m < det A.

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