addHaar_ball_center — Mathlib

English

The Haar measure of a ball is the same when centered at any point due to translation invariance.

Русский

Гааровa мера шара не зависит от центра, благодаря инвариантности переноса.

LaTeX

$$μ(ball(x,r)) = μ(ball(0,r))$$

Lean4

theorem addHaar_ball_center {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] (μ : Measure E)
    [IsAddHaarMeasure μ] (x : E) (r : ℝ) : μ (ball x r) = μ (ball (0 : E) r) :=
  by
  have : ball (0 : E) r = (x + ·) ⁻¹' ball x r := by simp [preimage_add_ball]
  rw [this, measure_preimage_add]

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