Supports of convolution-type parametric integrals over a group

Convolutions over a group G are parametric integrals s ↦ ∫ r, F s r ∂μ whose integrand vanishes unless r ∈ K and r⁻¹ * s ∈ L, where K and L are the supports of the two factors. This file records the resulting support bounds, for any normed-space valued integrand: the parametric integral is supported in K * L, and for compact K and L both the integrand on G × G and the parametric integral are compactly supported.

Main statements

• TauCeti.support_integral_subset_mul: the parametric integral is supported in K * L.
• TauCeti.hasCompactSupport_uncurry_of_inv_mul_mem: the integrand is compactly supported on G × G.
• TauCeti.hasCompactSupport_integral_of_inv_mul_mem: the parametric integral is compactly supported.

theorem TauCeti.support_integral_subset_mul {G : Type u_1} {E : Type u_2} [Group G] [NormedAddCommGroup E] {F : G → G → E} {K L : Set G} [NormedSpace ℝ E] [MeasurableSpace G] (μ : MeasureTheory.Measure G) (hF : ∀ (s r : G), F s r ≠ 0 → r ∈ K ∧ r⁻¹ * s ∈ L) : (Function.support fun (s : G) => ∫ (r : G), F s r ∂μ) ⊆ K * L

A two-variable integrand which vanishes unless r ∈ K and r⁻¹ * s ∈ L has its parametric integral s ↦ ∫ r, F s r supported in K * L.

theorem TauCeti.hasCompactSupport_uncurry_of_inv_mul_mem {G : Type u_1} {E : Type u_2} [Group G] {F : G → G → E} {K L : Set G} [TopologicalSpace G] [IsTopologicalGroup G] [Zero E] (hK : IsCompact K) (hL : IsCompact L) (hF : ∀ (s r : G), F s r ≠ 0 → r ∈ K ∧ r⁻¹ * s ∈ L) : HasCompactSupport (Function.uncurry F)

A two-variable integrand which vanishes unless r ∈ K and r⁻¹ * s ∈ L, for compact K and L, is compactly supported on G × G.

theorem TauCeti.hasCompactSupport_integral_of_inv_mul_mem {G : Type u_1} {E : Type u_2} [Group G] [NormedAddCommGroup E] {F : G → G → E} {K L : Set G} [TopologicalSpace G] [IsTopologicalGroup G] [NormedSpace ℝ E] [MeasurableSpace G] (μ : MeasureTheory.Measure G) (hK : IsCompact K) (hL : IsCompact L) (hF : ∀ (s r : G), F s r ≠ 0 → r ∈ K ∧ r⁻¹ * s ∈ L) : HasCompactSupport fun (s : G) => ∫ (r : G), F s r ∂μ

The parametric integral s ↦ ∫ r, F s r of an integrand which vanishes unless r ∈ K and r⁻¹ * s ∈ L, for compact K and L, is compactly supported.