English
Lower semicontinuity of a certain auxiliary bound: if pointwise limits hold with Ffs, then the bound remains below for nearby indices.
Русский
Нижняя полупостоянность сопряженного приближения: переход к пределам сохраняет неравенство.
LaTeX
$$$\forall x\in s\,\,\big(\mathrm{ Tendsto }(F_i x)\, p\, (nhds(f x))\big) \Rightarrow \forall v< eVariationOn f s, \forall^{\infty} i\, v< eVariationOn(F_i) s$$$
Lean4
theorem lowerSemicontinuous_aux {ι : Type*} {F : ι → α → E} {p : Filter ι} {f : α → E} {s : Set α}
(Ffs : ∀ x ∈ s, Tendsto (fun i => F i x) p (𝓝 (f x))) {v : ℝ≥0∞} (hv : v < eVariationOn f s) :
∀ᶠ n : ι in p, v < eVariationOn (F n) s :=
by
obtain ⟨⟨n, ⟨u, um, us⟩⟩, hlt⟩ :
∃ p : ℕ × { u : ℕ → α // Monotone u ∧ ∀ i, u i ∈ s },
v < ∑ i ∈ Finset.range p.1, edist (f ((p.2 : ℕ → α) (i + 1))) (f ((p.2 : ℕ → α) i)) :=
lt_iSup_iff.mp hv
have :
Tendsto (fun j => ∑ i ∈ Finset.range n, edist (F j (u (i + 1))) (F j (u i))) p
(𝓝 (∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)))) :=
by
apply tendsto_finset_sum
exact fun i _ => Tendsto.edist (Ffs (u i.succ) (us i.succ)) (Ffs (u i) (us i))
exact (this.eventually_const_lt hlt).mono fun i h => h.trans_le (sum_le (F i) n um us)
