English
If E is a locally compact normed space and complete over 𝕜, then the corresponding locally compact module is proper.
Русский
Если E локально компактно и полно над 𝕜, то соответствующий локально компактный модуль является корректным.
LaTeX
$$[LocallyCompactSpace E] [CompleteSpace 𝕜] ⇒ ProperSpace 𝕜 (module over E)$$
Lean4
/-- Continuous linear equivalence between continuous linear functions `𝕜ⁿ → E` and `Eⁿ`.
The spaces `𝕜ⁿ` and `Eⁿ` are represented as `ι → 𝕜` and `ι → E`, respectively,
where `ι` is a finite type. -/
def piRing (ι : Type*) [Fintype ι] [DecidableEq ι] : ((ι → 𝕜) →L[𝕜] E) ≃L[𝕜] ι → E :=
{
LinearMap.toContinuousLinearMap.symm.trans
(LinearEquiv.piRing 𝕜 E ι
𝕜) with
continuous_toFun := by
refine continuous_pi fun i => ?_
exact (ContinuousLinearMap.apply 𝕜 E (Pi.single i 1)).continuous
continuous_invFun :=
by
simp_rw [LinearEquiv.invFun_eq_symm, LinearEquiv.trans_symm, LinearEquiv.symm_symm]
-- Note: added explicit type and removed `change` that tried to achieve the same
refine
AddMonoidHomClass.continuous_of_bound
(LinearMap.toContinuousLinearMap.toLinearMap.comp (LinearEquiv.piRing 𝕜 E ι 𝕜).symm.toLinearMap)
(Fintype.card ι : ℝ) fun g => ?_
rw [← nsmul_eq_mul]
refine opNorm_le_bound _ (nsmul_nonneg (norm_nonneg g) (Fintype.card ι)) fun t => ?_
simp_rw [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, Function.comp_apply,
LinearMap.coe_toContinuousLinearMap', LinearEquiv.piRing_symm_apply]
apply le_trans (norm_sum_le _ _)
rw [smul_mul_assoc]
refine Finset.sum_le_card_nsmul _ _ _ fun i _ => ?_
rw [norm_smul, mul_comm]
gcongr <;> apply norm_le_pi_norm }
