Theorems · Theorem · measure theory

MeasureTheory.hausdorffMeasure_homothety_image

∀ {𝕜 : Type u_4} {E : Type u_5} {P : Type u_6} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : MeasurableSpace P] [inst_4 : MetricSpace P] [inst_5 : NormedAddTorsor E P]
  [inst_6 : BorelSpace P] {d : ℝ},
  0 ≤ d →
    ∀ (x : P) {c : 𝕜},
      c ≠ 0 →
        ∀ (s : Set P),
          (MeasureTheory.Measure.hausdorffMeasure d) (⇑(AffineMap.homothety x c) '' s) =
            ‖c‖₊ ^ d • (MeasureTheory.Measure.hausdorffMeasure d) s

Scaling by c around x scales the measure by ‖c‖₊ ^ d.

Defined in

Mathlib.MeasureTheory.Measure.Hausdorff

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedFieldNormedAddCommGroupNormedSpaceMeasurableSpaceMetricSpaceNormedAddTorsorBorelSpace