English
A HasBasis version for TendstoUniformlyOn: the existence/prop pattern yields the same conclusion as standard HasBasis results.
Русский
Версия HasBasis для TendstoUniformlyOn: существование/свойство в образце порождают тот же вывод, что и в стандартном HasBasis.
LaTeX
$$$TendstoUniformlyOn F f l s \iff \, \forall i, pβ i \rightarrow \exists j, pX j \wedge \forall x \in sX j, \forall a \in s, (f a, F x a) \in sβ i$$$
Lean4
/-- A uniformly Cauchy sequence converges uniformly to its limit -/
theorem tendstoUniformlyOnFilter_of_tendsto (hF : UniformCauchySeqOnFilter F p p')
(hF' : ∀ᶠ x : α in p', Tendsto (fun n => F n x) p (𝓝 (f x))) : TendstoUniformlyOnFilter F f p p' :=
by
rcases p.eq_or_neBot with rfl | _
·
simp only [TendstoUniformlyOnFilter, bot_prod, eventually_bot, implies_true]
-- Proof idea: |f_n(x) - f(x)| ≤ |f_n(x) - f_m(x)| + |f_m(x) - f(x)|. We choose `n`
-- so that |f_n(x) - f_m(x)| is uniformly small across `s` whenever `m ≥ n`. Then for
-- a fixed `x`, we choose `m` sufficiently large such that |f_m(x) - f(x)| is small.
intro u hu
rcases comp_symm_of_uniformity hu with
⟨t, ht, htsymm, htmem⟩
-- We will choose n, x, and m simultaneously. n and x come from hF. m comes from hF'
-- But we need to promote hF' to the full product filter to use it
have hmc : ∀ᶠ x in (p ×ˢ p) ×ˢ p', Tendsto (fun n : ι => F n x.snd) p (𝓝 (f x.snd)) :=
by
rw [eventually_prod_iff]
exact
⟨fun _ => True, by simp, _, hF', by simp⟩
-- To apply filter operations we'll need to do some order manipulation
rw [Filter.eventually_swap_iff]
have := tendsto_prodAssoc.eventually (tendsto_prod_swap.eventually ((hF t ht).and hmc))
apply this.curry.mono
simp only [Equiv.prodAssoc_apply, eventually_and, eventually_const, Prod.snd_swap, Prod.fst_swap, and_imp,
Prod.forall]
-- Complete the proof
intro x n hx hm'
refine Set.mem_of_mem_of_subset (mem_compRel.mpr ?_) htmem
rw [Uniform.tendsto_nhds_right] at hm'
have := hx.and (hm' ht)
obtain ⟨m, hm⟩ := this.exists
exact ⟨F m x, ⟨hm.2, htsymm hm.1⟩⟩
