instIsMulRightInvariantHausdorffMeasureOfIsIsometricSMulMulOpposite

English

For an antilipschitz map, the forward image satisfies μH^d(s) ≤ K^d μH^d(f(s)).

Русский

Для антилипшицевой карты образ множества удовлетворяет μH^d(s) ≤ K^d μH^d(f(s)).

LaTeX

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

Lean4

@[to_additive]
instance {d : ℝ} [Group X] [IsIsometricSMul Xᵐᵒᵖ X] : IsMulRightInvariant (μH[d] : Measure X) where
  map_mul_right_eq_self x := (IsometryEquiv.constSMul (MulOpposite.op x)).map_hausdorffMeasure _

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