English
If G is a locally compact group, then its Pontryagin dual Ĝ is locally compact as well.
Русский
Если G — локально компактная группа, то её дуал Дуаля Понтрягиана \\hat{G} тоже локально компактна.
LaTeX
$$$\\text{LocallyCompactSpace}(\\widehat{G})$$$
Lean4
instance [LocallyCompactSpace H] : LocallyCompactSpace (PontryaginDual H) :=
by
let Vn : ℕ → Set Circle := fun n ↦ Circle.exp '' {x | |x| < Real.pi / 2 ^ (n + 1)}
have hVn : ∀ n x, x ∈ Vn n ↔ |Complex.arg x| < Real.pi / 2 ^ (n + 1) :=
by
refine fun n x ↦ ⟨?_, fun hx ↦ ⟨Complex.arg x, hx, Circle.exp_arg x⟩⟩
rintro ⟨t, ht : |t| < _, rfl⟩
have ht' := ht.trans_le (div_le_self Real.pi_nonneg (one_le_pow₀ one_le_two))
rwa [Circle.arg_exp (neg_lt_of_abs_lt ht') (lt_of_abs_lt ht').le]
refine ContinuousMonoidHom.locallyCompactSpace_of_hasBasis Vn ?_ ?_
· intro n x h1 h2
rw [hVn] at h1 h2 ⊢
rwa [Circle.coe_mul, Complex.arg_mul x.coe_ne_zero x.coe_ne_zero, ← two_mul, abs_mul, abs_two, ←
lt_div_iff₀' two_pos, div_div, ← pow_succ] at h2
apply Set.Ioo_subset_Ioc_self
rw [← two_mul, Set.mem_Ioo, ← abs_lt, abs_mul, abs_two, ← lt_div_iff₀' two_pos]
refine h1.trans_le ?_
gcongr
exact le_self_pow₀ one_le_two n.succ_ne_zero
· rw [← Circle.exp_zero, ← isLocalHomeomorph_circleExp.map_nhds_eq 0]
refine
((nhds_basis_zero_abs_lt ℝ).to_hasBasis (fun x hx ↦ ⟨Nat.ceil (Real.pi / x), trivial, fun t ht ↦ ?_⟩) fun k _ ↦
⟨Real.pi / 2 ^ (k + 1), by positivity, le_rfl⟩).map
Circle.exp
rw [Set.mem_setOf_eq] at ht ⊢
refine lt_of_lt_of_le ht ?_
rw [div_le_iff₀' (pow_pos two_pos _), ← div_le_iff₀ hx]
refine (Nat.le_ceil (Real.pi / x)).trans ?_
exact_mod_cast (Nat.le_succ _).trans Nat.lt_two_pow_self.le
