instIsMulLeftInvariantHausdorffMeasureOfIsIsometricSMul

English

For an antilipschitz map, the preimage of a set has measure bounded by a function of the image's measure.

Русский

Для антилипшицевой карты предобраз множества имеет ограничение по мере в зависимости от меры образа.

LaTeX

$$$\mu_H^{d}(f^{-1}(s)) \le (K)^d \mu_H^{d}(s)$$$

Lean4

@[to_additive]
instance {d : ℝ} [Group X] [IsIsometricSMul X X] : IsMulLeftInvariant (μH[d] : Measure X) where
  map_mul_left_eq_self x := (IsometryEquiv.constSMul x).map_hausdorffMeasure _

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