Almost-convergent functions

structure IsAlmostConvergent {G : Type u_1} {E : Type u_2} [Group G] [NormedAddCommGroup E] [NormedSpace ℝ E] (f : G → E) : Prop

A function f from a group G to a normed space E is almost-convergent if if it is bounded and the closure in the L^∞ norm of the convex hull of its translates contains a unique constant function.

• isBddFun : Bornology.IsBddFun f
• existsUnique_const_mem_closure_convexHull : ∃! z : E, Function.const G z ∈ closure ((convexHull ℝ) (Set.range fun (x : G) => τ_[x] f))

theorem isAlmostConvergent_iff {G : Type u_1} {E : Type u_2} [Group G] [NormedAddCommGroup E] [NormedSpace ℝ E] (f : G → E) : IsAlmostConvergent f ↔ Bornology.IsBddFun f ∧ ∃! z : E, Function.const G z ∈ closure ((convexHull ℝ) (Set.range fun (x : G) => τ_[x] f))

@[simp]

theorem IsAlmostConvergent.const {G : Type u_1} {E : Type u_2} [Group G] [NormedAddCommGroup E] [NormedSpace ℝ E] {z : E} : IsAlmostConvergent (Function.const G z)

@[simp]

theorem IsAlmostConvergent.fun_const {G : Type u_1} {E : Type u_2} [Group G] [NormedAddCommGroup E] [NormedSpace ℝ E] {z : E} : IsAlmostConvergent fun (x : G) => z

Eta-expanded form of IsAlmostConvergent.const

@[simp]

theorem IsAlmostConvergent.zero {G : Type u_1} {E : Type u_2} [Group G] [NormedAddCommGroup E] [NormedSpace ℝ E] : IsAlmostConvergent 0