Theorem: Real.hasTemperateGrowth_l2inner_const (ForML/Trigonometric.lean)

State before:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
ι : Type u_3
inst✝ : Fintype ι
w : ι → ℝ
⊢ Function.HasTemperateGrowth fun v => ∑ i : ι, v i * w i
Tactic:
change Function.HasTemperateGrowth ((fun v : EuclideanSpace ℝ ι => inner v w) ∘ ⇑(EuclideanSpace.equiv ι ℝ).symm.toContinuousLinearMap)
State after:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
ι : Type u_3
inst✝ : Fintype ι
w : ι → ℝ
⊢ Function.HasTemperateGrowth ((fun v => ⟪v, w⟫_ℝ) ∘ ⇑↑(ContinuousLinearEquiv.symm (EuclideanSpace.equiv ι ℝ)))

State before:
E : Type u_1
F : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
ι : Type u_3
inst✝ : Fintype ι
w : ι → ℝ
⊢ Function.HasTemperateGrowth ((fun v => ⟪v, w⟫_ℝ) ∘ ⇑↑(ContinuousLinearEquiv.symm (EuclideanSpace.equiv ι ℝ)))
Tactic:
exact (Real.hasTemperateGrowth_inner_const _).comp (Function.hasTemperateGrowth_clm _)
State after:
no goals