Theorems · Theorem · measure theory

MeasureTheory.continuous_integral_apply_neg_add

∀ {G : Type u_1} [inst : TopologicalSpace G] [LocallyCompactSpace G] [inst_2 : AddGroup G] [IsTopologicalAddGroup 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 additive 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

TopologicalSpaceLocallyCompactSpaceAddGroupIsTopologicalAddGroupMeasurableSpaceBorelSpaceMeasureTheory.IsFiniteMeasureOnCompactsNormedAddCommGroupNormedSpace