Translation of ball integrals

For a measure invariant under addition, an integral over a ball can be translated to a ball about the origin. Only measurability of translations is needed; the measure need not be an additive Haar measure, and the function need not be integrable.

Main declarations

• TauCeti.setIntegral_ball_eq_setIntegral_ball_zero_add: translating a ball integral to the origin.

theorem TauCeti.setIntegral_ball_eq_setIntegral_ball_zero_add {E : Type u_1} {F : Type u_2} [SeminormedAddCommGroup E] [MeasurableSpace E] [MeasurableAdd E] {μ : MeasureTheory.Measure E} [μ.IsAddRightInvariant] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E → F) (x₀ : E) (R : ℝ) : ∫ (x : E) in Metric.ball x₀ R, f x ∂μ = ∫ (y : E) in Metric.ball 0 R, f (y + x₀) ∂μ

For a measure invariant under right addition, the integral over ball x₀ R is the integral over ball 0 R of the translate y ↦ f (y + x₀). No integrability hypothesis is needed.