Theorems · Theorem · functional analysis

TemperedDistribution.smulLeftCLM_smulLeftCLM_apply

∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : AddCommGroup F]
  [inst_3 : Module ℂ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousConstSMul ℂ F] {g₁ g₂ : E → ℂ},
  Function.HasTemperateGrowth g₁ →
    Function.HasTemperateGrowth g₂ →
      ∀ (f : TemperedDistribution E F),
        (TemperedDistribution.smulLeftCLM F g₂) ((TemperedDistribution.smulLeftCLM F g₁) f) =
          (TemperedDistribution.smulLeftCLM F (g₁ * g₂)) f

Defined in

Mathlib.Analysis.Distribution.TemperedDistribution

Cited by

4 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousConstSMul