Theorems · Theorem · abstract harmonic analysis

MeasureTheory.convolution_precompR_apply

∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {E'' : Type uE''} {F : Type uF}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup E'']
  [inst_3 : NormedAddCommGroup F] {f : G → E} [inst_4 : RCLike 𝕜] [inst_5 : NormedSpace 𝕜 E] [inst_6 : NormedSpace 𝕜 E']
  [inst_7 : NormedSpace 𝕜 E''] [inst_8 : NormedSpace ℝ F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : MeasurableSpace G]
  {μ : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [inst_11 : NormedAddCommGroup G] [BorelSpace G]
  {g : G → E'' →L[𝕜] E'},
  MeasureTheory.LocallyIntegrable f μ →
    HasCompactSupport g →
      Continuous g →
        ∀ (x₀ : G) (x : E''),
          (MeasureTheory.convolution f g (ContinuousLinearMap.precompR E'' L) μ x₀) x =
            MeasureTheory.convolution f (fun a => (g a) x) L μ x₀

Defined in

Mathlib.Analysis.Convolution

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedAddCommGroupNormedAddCommGroupNormedAddCommGroupRCLikeNormedSpaceNormedSpaceNormedSpaceNormedSpaceNormedSpaceMeasurableSpaceNormedAddCommGroupBorelSpace