Theorems · Theorem · measure theory

MeasureTheory.continuous_integral_apply_inv_mul

∀ {G : Type u_1} [inst : TopologicalSpace G] [LocallyCompactSpace G] [inst_2 : Group G] [IsTopologicalGroup G]
  [inst_4 : MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [MeasureTheory.IsFiniteMeasureOnCompacts μ]
  {E : Type u_2} [inst_7 : NormedAddCommGroup E] [inst_8 : NormedSpace ℝ E] {g : G → E},
  Continuous g → HasCompactSupport g → Continuous fun x => ∫ (y : G), g (y⁻¹ * x) ∂μ

The parameterized integral x ↦ ∫ y, g (y⁻¹ * x) ∂μ depends continuously on y when g is a compactly supported continuous function on a topological group G, and μ is finite on compact sets.

Defined in

Mathlib.MeasureTheory.Measure.Haar.Unique

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceLocallyCompactSpaceGroupIsTopologicalGroupMeasurableSpaceBorelSpaceMeasureTheory.IsFiniteMeasureOnCompactsNormedAddCommGroupNormedSpace