Theorem: SchwartzMap.Distribution.ofHasTemperateGrowth_apply (ForML/IntegralAgainst.lean)

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : IsScalarTower ℝ 𝕜 F
inst✝³ : CompleteSpace F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
g : E → 𝕜
hg : Function.HasTemperateGrowth g
φ : 𝓢(E, F)
⊢ (ofHasTemperateGrowth hg) φ = ∫ (x : E), g x • φ x
Tactic:
rw [ofHasTemperateGrowth, ContinuousLinearMap.comp_apply, integralCLM_apply]
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : IsScalarTower ℝ 𝕜 F
inst✝³ : CompleteSpace F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
g : E → 𝕜
hg : Function.HasTemperateGrowth g
φ : 𝓢(E, F)
⊢ ∫ (x : E), ((hasTemperateGrowth_smul hg) φ) x = ∫ (x : E), g x • φ x

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : IsScalarTower ℝ 𝕜 F
inst✝³ : CompleteSpace F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
g : E → 𝕜
hg : Function.HasTemperateGrowth g
φ : 𝓢(E, F)
⊢ ∫ (x : E), ((hasTemperateGrowth_smul hg) φ) x = ∫ (x : E), g x • φ x
Tactic:
rfl
State after:
no goals