Theorems · Theorem · functional analysis

Function.HasTemperateGrowth.fun_pow

∀ {R : Type u_3} {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedRing R]
  [inst_3 : NormedAlgebra ℝ R] {f : E → R},
  Function.HasTemperateGrowth f → ∀ (k : ℕ), Function.HasTemperateGrowth fun i => f i ^ k

Eta-expanded form of Function.HasTemperateGrowth.pow

Defined in: Mathlib.Analysis.Distribution.TemperateGrowth
Cited by: 2 results in Mathlib
Foundations: Depth 206 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup NormedSpace NormedRing NormedAlgebra

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement · cited by 25,697
NormedAddCommGroupstatement · cited by 15,752
NormedSpacestatement · cited by 12,499
NormedAlgebrastatement · cited by 1,165
NormedRingstatement · cited by 924
Function.HasTemperateGrowthstatement · cited by 88
Function.HasTemperateGrowth.powproof · cited by 1

Cited by2

Results whose statement or proof uses this declaration.

TemperedDistribution.laplacian_eq_fourierMultiplierCLMproof · cited by 1
SchwartzMap.laplacian_eq_fourierMultiplierCLMproof · cited by 0