English
If f and g are continuous and tend to zero along cocompact filters, then their pointwise product tends to zero along cocompact on the product space.
Русский
Если f и g непрерывны и сходятся к нулю по кококомпакт-фильтрам, то их покомпонентное произведение сходится к нулю по кококомпакт на произведении пространств.
LaTeX
$$tendsto_mul_cocompact_nhds_zero$$
Lean4
/-- If `f : α → M` and `g : β → M` are continuous and both tend to zero on the cocompact filter,
then `fun i : α × β ↦ f i.1 * g i.2` also tends to zero on the cocompact filter. -/
theorem tendsto_mul_cocompact_nhds_zero [TopologicalSpace α] [TopologicalSpace β] {f : α → M} {g : β → M}
(f_cont : Continuous f) (g_cont : Continuous g) (hf : Tendsto f (cocompact α) (𝓝 0))
(hg : Tendsto g (cocompact β) (𝓝 0)) : Tendsto (fun i : α × β ↦ f i.1 * g i.2) (cocompact (α × β)) (𝓝 0) :=
by
set l : Filter (M × M) := map (Prod.map f g) (cocompact (α × β)) with l_def
set K : Set (M × M) := (insert 0 (range f)) ×ˢ (insert 0 (range g))
have K_compact : IsCompact K :=
.prod (hf.isCompact_insert_range_of_cocompact f_cont) (hg.isCompact_insert_range_of_cocompact g_cont)
have K_mem_l : K ∈ l :=
eventually_map.mpr <|
.of_forall fun ⟨x, y⟩ ↦ ⟨mem_insert_of_mem _ (mem_range_self _), mem_insert_of_mem _ (mem_range_self _)⟩
have l_compact : Disjoint l (cocompact (M × M)) :=
by
rw [disjoint_cocompact_right]
exact ⟨K, K_mem_l, K_compact⟩
have l_le_coprod : l ≤ (𝓝 0).coprod (𝓝 0) :=
by
rw [l_def, ← coprod_cocompact]
exact hf.prodMap_coprod hg
exact tendsto_mul_nhds_zero_of_disjoint_cocompact l_compact l_le_coprod |>.comp tendsto_map
