Uniformly almost-periodic functions

This file defines uniformly almost-periodic functions in a group following von Neumann.

For a group G and a metric space X, a function f : G → X is uniformly almost-periodic if for every ε > 0 one can cover G with finitely many translates of the set of ε-almost-periods {t : G | ∀ x, dist (f (t⁻¹ * x)) (f x) ≤ ε}.

We make von Neumann's theory quantitative by keeping track of the "modulus of almost-periodicity", i.e. for every ε > 0 of a number K ε of translates of the ε-almost-period that suffice to cover G.

Implementation notes

Von Neumann in 1934 defines all three of left almost-periodic (LAP, the one defined above), right almost-periodic (RAP, same as LAP but replacing left translates with right ones) and uniformly almost-periodic (UAP, the combination of both). As proven by Maak a year later, LAP qualitatively implies RAP, meaning we can get away with a single qualitative predicate. Although the quantitative dependence in Maak's result is poor, we do not introduce a separate quantitative predicate for RAP functions. This matches the qualitative predicate. We instead suggest spelling quantitative right-almost periodic functions using precomposition with MulOpposite.unop.

References

• Almost periodic functions in a group. I, John von Neumann
• [Eine neue Definition der fastperiodischen Funktionen, Wilhelm Maak][maak1935]

Metric space codomain

Uniform almost-periods

def uniformAP {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] (f : G → X) (ε : ℝ) : Set G

The uniform ε-almost-periods of a function f from a group G to a metric space X are those elements of the group that move f by at most ε in the L^∞ metric.

Equations

• AP∞(f, ε) = {t : G | ∀ (x : G), dist (f (t⁻¹ * x)) (f x) ≤ ε}

def «termAP∞(_,_)» : Lean.ParserDescr

The uniform ε-almost-periods of a function f from a group G to a metric space X are those elements of the group that move f by at most ε in the L^∞ metric.

Equations

• One or more equations did not get rendered due to their size.

Basic properties

theorem mem_uniformAP {G : Type u_3} {X : Type u_6} [Group G] {t : G} [MetricSpace X] {f : G → X} {ε : ℝ} : t ∈ AP∞(f, ε) ↔ ∀ (x : G), dist (f (t⁻¹ * x)) (f x) ≤ ε

@[simp]

theorem one_mem_uniformAP {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f : G → X} {ε : ℝ} : 1 ∈ AP∞(f, ε) ↔ 0 ≤ ε

@[simp]

theorem uniformAP_nonempty {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f : G → X} {ε : ℝ} : AP∞(f, ε).Nonempty ↔ 0 ≤ ε

theorem mul_inv_mem_uniformAP {G : Type u_3} {X : Type u_6} [Group G] {a b : G} [MetricSpace X] {f : G → X} {ε : ℝ} : a * b⁻¹ ∈ AP∞(f, ε) ↔ ∀ (x : G), dist (f (a * x)) (f (b * x)) ≤ ε

a * b⁻¹ is an ε-almost-period of f iff the two translates f (a * ·) and f (b * ·) are at most ε away in the L^∞ metric.

@[simp]

theorem uniformAP_const {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] (z : X) {ε : ℝ} (hε : 0 ≤ ε) : AP∞(Function.const G z, ε) = Set.univ

@[simp]

theorem uniformAP_fun_const {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] (z : X) {ε : ℝ} (hε : 0 ≤ ε) : AP∞(fun (x : G) => z, ε) = Set.univ

Eta-expanded form of uniformAP_const

theorem uniformAP_subset_of_forall_dist_le {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f g : G → X} {ε δ : ℝ} (hfg : ∀ (x : G), dist (f x) (g x) ≤ δ) : AP∞(g, ε) ⊆ AP∞(f, ε + 2 * δ)

If f is δ-uniformly close to g, every ε-almost-period of g is an ε + 2δ-almost-period of f.

Operations on the domain

theorem mul_mem_uniformAP {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f : G → X} {ε : ℝ} {a b : G} {δ : ℝ} (ha : a ∈ AP∞(f, ε)) (hb : b ∈ AP∞(f, δ)) : a * b ∈ AP∞(f, ε + δ)

theorem uniformAP_mul_uniformAP_subset {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f : G → X} {ε δ : ℝ} : AP∞(f, ε) * AP∞(f, δ) ⊆ AP∞(f, ε + δ)

theorem uniformAP_pow_subset {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f : G → X} {ε : ℝ} (n : ℕ) : AP∞(f, ε) ^ n ⊆ AP∞(f, ↑n * ε)

@[simp]

theorem inv_mem_uniformAP {G : Type u_3} {X : Type u_6} [Group G] {t : G} [MetricSpace X] {f : G → X} {ε : ℝ} : t⁻¹ ∈ AP∞(f, ε) ↔ t ∈ AP∞(f, ε)

@[simp]

theorem uniformAP_inv {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f : G → X} {ε : ℝ} : AP∞(f, ε)⁻¹ = AP∞(f, ε)

@[simp]

theorem uniformAP_comp_mulEquiv {G : Type u_3} {H : Type u_4} {X : Type u_6} [Group G] [Group H] [MetricSpace X] (f : G → X) {ε : ℝ} (φ : H ≃* G) : AP∞(f ∘ ⇑φ, ε) = ⇑φ ⁻¹' AP∞(f, ε)

@[simp]

theorem uniformAP_comp_mul_right {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f : G → X} {ε : ℝ} (a : G) : AP∞(fun (x : G) => f (x * a), ε) = AP∞(f, ε)

The almost-periods are unchanged by right translation of the argument.

Operations on the codomain

theorem uniformAP_prod {G : Type u_3} {X : Type u_6} {Y : Type u_7} [Group G] [MetricSpace X] [MetricSpace Y] {ε : ℝ} {f : G → X × Y} : AP∞(f, ε) = AP∞(Prod.fst ∘ f, ε) ∩ AP∞(Prod.snd ∘ f, ε)

The ε-almost-periods of a product-valued function are the common ε-almost-periods of its two components.

Quantitative uniformly almost-periodic functions

def IsUAPWith {G : Type u_3} {X : Type u_6} [Group G] (K : ℝ → ℝ) [MetricSpace X] (f : G → X) : Prop

For a "modulus of almost-periodicity" K : ℝ → ℝ, a function is uniformly K-almost-periodic if its uniform ε-almost-periods are K_ε-syndetic for all ε > 0.

This is a quantitative version of IsUAP.

Equations

• IsUAPWith K f = ∀ ⦃ε : ℝ⦄, 0 < ε → CovBySMul G (K ε) Set.univ AP∞(f, ε)

theorem IsUAPWith.pos {G : Type u_3} {X : Type u_6} [Group G] {K : ℝ → ℝ} [MetricSpace X] {f : G → X} {ε : ℝ} (hf : IsUAPWith K f) (hε : 0 < ε) : 0 < K ε

theorem IsUAPWith.mono {G : Type u_3} {X : Type u_6} [Group G] {K L : ℝ → ℝ} [MetricSpace X] {f : G → X} (hKL : ∀ ε > 0, K ε ≤ L ε) (hf : IsUAPWith K f) : IsUAPWith L f

@[simp]

theorem IsUAPWith.const {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {z : X} : IsUAPWith 1 (Function.const G z)

@[simp]

theorem IsUAPWith.fun_const {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {z : X} : IsUAPWith (fun (x : ℝ) => 1) fun (x : G) => z

Eta-expanded form of IsUAPWith.const

theorem IsUAPWith.of_tendstoUniformly {G : Type u_3} {X : Type u_6} [Group G] {K : ℝ → ℝ} [MetricSpace X] {f : G → X} {ι : Type u_10} {p : Filter ι} [p.NeBot] {u : ι → G → X} (hu : ∀ᶠ (n : ι) in p, IsUAPWith K (u n)) (h : TendstoUniformly u f p) : IsUAPWith (fun (ε : ℝ) => K (ε / 2)) f

Almost-periodicity is quantitatively preserved by uniform limits along any (nontrivial) filter.

Operations on the domain

theorem IsUAPWith.comp_mulEquiv {G : Type u_3} {H : Type u_4} {X : Type u_6} [Group G] [Group H] {K : ℝ → ℝ} [MetricSpace X] {f : G → X} {φ : H ≃* G} (hf : IsUAPWith K f) : IsUAPWith K (f ∘ ⇑φ)

Almost-periodicity is quantitatively preserved by precomposition with a group isomorphism.

@[simp]

theorem isUAPWith_comp_mulEquiv {G : Type u_3} {H : Type u_4} {X : Type u_6} [Group G] [Group H] {K : ℝ → ℝ} [MetricSpace X] {f : G → X} {φ : H ≃* G} : IsUAPWith K (f ∘ ⇑φ) ↔ IsUAPWith K f

theorem IsUAPWith.comp_mul_right {G : Type u_3} {X : Type u_6} [Group G] {K : ℝ → ℝ} {a : G} [MetricSpace X] {f : G → X} (hf : IsUAPWith K f) : IsUAPWith K fun (x : G) => f (x * a)

theorem IsUAPWith.comp_mul_left {G : Type u_3} {X : Type u_6} [Group G] {K : ℝ → ℝ} {a : G} [MetricSpace X] {f : G → X} (hf : IsUAPWith K f) : IsUAPWith K fun (x : G) => f (a * x)

theorem IsUAPWith.translate {G : Type u_3} {X : Type u_6} [Group G] {K : ℝ → ℝ} {t : G} [MetricSpace X] {f : G → X} (hf : IsUAPWith K f) : IsUAPWith K (τ_[t] f)

@[simp]

theorem isUAPWith_translate {G : Type u_3} {X : Type u_6} [Group G] {K : ℝ → ℝ} {t : G} [MetricSpace X] {f : G → X} : IsUAPWith K (τ_[t] f) ↔ IsUAPWith K f

theorem IsUAPWith.comp_unop {G : Type u_3} {X : Type u_6} [Group G] {K : ℝ → ℝ} [MetricSpace X] {f : G → X} (hf : IsUAPWith K f) : IsUAPWith (fun (ε : ℝ) => K (ε / 4) ^ K (ε / 4)) (f ∘ MulOpposite.unop)

If f is left almost-periodic with modulus K, then it is right almost-periodic with modulus ε ↦ K (ε / 4) ^ K (ε / 4).

theorem IsUAPWith.comp_op {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {K : ℝ → ℝ} {g : Gᵐᵒᵖ → X} (hg : IsUAPWith K g) : IsUAPWith (fun (ε : ℝ) => K (ε / 4) ^ K (ε / 4)) (g ∘ MulOpposite.op)

If f is right almost-periodic with modulus K, then it is left almost-periodic with modulus ε ↦ K (ε / 4) ^ K (ε / 4).

theorem IsUAPWith.comp_inv {G : Type u_3} {X : Type u_6} [Group G] {K : ℝ → ℝ} [MetricSpace X] {f : G → X} (hf : IsUAPWith K f) : IsUAPWith (fun (ε : ℝ) => K (ε / 4) ^ K (ε / 4)) fun (x : G) => f x⁻¹

Operations on the codomain

theorem IsUAPWith.isUniformContinuousOnWith_comp {G : Type u_3} {X : Type u_6} {Y : Type u_7} [Group G] {K : ℝ → ℝ} [MetricSpace X] [MetricSpace Y] {f : G → X} {φ : X → Y} {δ : ℝ → ℝ} {S : Set X} (hδ : ∀ ε > 0, 0 < δ ε) (hf : IsUAPWith K f) (hfS : ∀ (x : G), f x ∈ S) (hφ : Metric.IsUniformContinuousOnWith δ φ S) : IsUAPWith (K ∘ δ) (φ ∘ f)

Postcomposing a K-almost-periodic function f with a map φ that is uniformly continuous with modulus δ on a set containing the range of f gives a K ∘ δ-almost-periodic function.

theorem IsUAPWith.fun_isUniformContinuousOnWith_comp {G : Type u_3} {X : Type u_6} {Y : Type u_7} [Group G] {K : ℝ → ℝ} [MetricSpace X] [MetricSpace Y] {f : G → X} {φ : X → Y} {δ : ℝ → ℝ} {S : Set X} (hδ : ∀ ε > 0, 0 < δ ε) (hf : IsUAPWith K f) (hfS : ∀ (x : G), f x ∈ S) (hφ : Metric.IsUniformContinuousOnWith δ φ S) : IsUAPWith (fun (x : ℝ) => K (δ x)) fun (x : G) => φ (f x)

Eta-expanded form of IsUAPWith.isUniformContinuousOnWith_comp

---

Postcomposing a K-almost-periodic function f with a map φ that is uniformly continuous with modulus δ on a set containing the range of f gives a K ∘ δ-almost-periodic function.

theorem IsUAPWith.lipschitzOnWith_comp {G : Type u_3} {X : Type u_6} {Y : Type u_7} [Group G] {K : ℝ → ℝ} [MetricSpace X] [MetricSpace Y] {f : G → X} {φ : X → Y} {C : NNReal} (hC : 0 < C) {S : Set X} (hf : IsUAPWith K f) (hfS : ∀ (x : G), f x ∈ S) (hφ : LipschitzOnWith C φ S) : IsUAPWith (fun (ε : ℝ) => K (ε / ↑C)) (φ ∘ f)

Postcomposing a K-almost-periodic function with a C-Lipschitz map gives a ε ↦ K (ε / C)-almost-periodic function.

theorem IsUAPWith.fst_comp {G : Type u_3} {X : Type u_6} {Y : Type u_7} [Group G] {K : ℝ → ℝ} [MetricSpace X] [MetricSpace Y] {f : G → X × Y} (hf : IsUAPWith K f) : IsUAPWith K (Prod.fst ∘ f)

A K-almost-periodic function to a product is K-almost-periodic in its first component.

theorem IsUAPWith.fun_fst {G : Type u_3} {X : Type u_6} {Y : Type u_7} [Group G] {K : ℝ → ℝ} [MetricSpace X] [MetricSpace Y] {f : G → X × Y} (hf : IsUAPWith K f) : IsUAPWith K fun (x : G) => (f x).1

Eta-expanded form of IsUAPWith.fst_comp

---

A K-almost-periodic function to a product is K-almost-periodic in its first component.

theorem IsUAPWith.snd_comp {G : Type u_3} {X : Type u_6} {Y : Type u_7} [Group G] {K : ℝ → ℝ} [MetricSpace X] [MetricSpace Y] {f : G → X × Y} (hf : IsUAPWith K f) : IsUAPWith K (Prod.snd ∘ f)

A K-almost-periodic function to a product is K-almost-periodic in its second component.

theorem IsUAPWith.fun_snd {G : Type u_3} {X : Type u_6} {Y : Type u_7} [Group G] {K : ℝ → ℝ} [MetricSpace X] [MetricSpace Y] {f : G → X × Y} (hf : IsUAPWith K f) : IsUAPWith K fun (x : G) => (f x).2

Eta-expanded form of IsUAPWith.snd_comp

---

A K-almost-periodic function to a product is K-almost-periodic in its second component.

theorem IsUAPWith.prodMk {G : Type u_3} {X : Type u_6} {Y : Type u_7} [Group G] {K L : ℝ → ℝ} [MetricSpace X] [MetricSpace Y] {f : G → X} {g : G → Y} (hf : IsUAPWith K f) (hg : IsUAPWith L g) : IsUAPWith (fun (ε : ℝ) => K (ε / 2) * L (ε / 2)) fun (x : G) => (f x, g x)

The product of K- and L-almost-periodic functions is ε ↦ K (ε / 2) * L (ε / 2)-almost-periodic.

Qualitative uniformly almost-periodic functions

def IsUAP {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] (f : G → X) : Prop

A function is uniformly almost-periodic if its uniform ε-almost-periods are syndetic for all ε > 0.

Equations

• IsUAP f = ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ (K : ℝ), CovBySMul G K Set.univ AP∞(f, ε)

theorem IsUAPWith.isUAP {G : Type u_3} {X : Type u_6} [Group G] {K : ℝ → ℝ} [MetricSpace X] {f : G → X} (hf : IsUAPWith K f) : IsUAP f

theorem isUAP_iff_exists_isUAPWith {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f : G → X} : IsUAP f ↔ ∃ (K : ℝ → ℝ), IsUAPWith K f

theorem IsUAP.exists_isUAPWith {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f : G → X} : IsUAP f → ∃ (K : ℝ → ℝ), IsUAPWith K f

Alias of the forward direction of isUAP_iff_exists_isUAPWith.

@[simp]

theorem IsUAP.const {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {z : X} : IsUAP (Function.const G z)

@[simp]

theorem IsUAP.fun_const {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {z : X} : IsUAP fun (x : G) => z

Eta-expanded form of IsUAP.const

theorem IsUAP.isBddFun {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f : G → X} (hf : IsUAP f) : Bornology.IsBddFun f

Operations on the domain

theorem IsUAP.comp_mulEquiv {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f : G → X} {H : Type u_10} [Group H] (φ : H ≃* G) (hf : IsUAP f) : IsUAP (f ∘ ⇑φ)

Almost-periodicity is preserved by precomposition with a group isomorphism.

@[simp]

theorem isUAP_comp_mulEquiv {G : Type u_3} {H : Type u_4} {X : Type u_6} [Group G] [Group H] [MetricSpace X] {f : G → X} {φ : H ≃* G} : IsUAP (f ∘ ⇑φ) ↔ IsUAP f

theorem IsUAP.comp_mul_right {G : Type u_3} {X : Type u_6} [Group G] {a : G} [MetricSpace X] {f : G → X} (hf : IsUAP f) : IsUAP fun (x : G) => f (x * a)

theorem IsUAP.comp_mul_left {G : Type u_3} {X : Type u_6} [Group G] {a : G} [MetricSpace X] {f : G → X} (hf : IsUAP f) : IsUAP fun (x : G) => f (a * x)

theorem IsUAP.translate {G : Type u_3} {X : Type u_6} [Group G] {x : G} [MetricSpace X] {f : G → X} (hf : IsUAP f) : IsUAP (τ_[x] f)

@[simp]

theorem isUAP_translate {G : Type u_3} {X : Type u_6} [Group G] {x : G} [MetricSpace X] {f : G → X} : IsUAP (τ_[x] f) ↔ IsUAP f

@[simp]

theorem isUAP_comp_unop {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f : G → X} : IsUAP (f ∘ MulOpposite.unop) ↔ IsUAP f

A function is right almost-periodic iff it is left almost-periodic.

theorem IsUAP.comp_unop {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f : G → X} : IsUAP f → IsUAP (f ∘ MulOpposite.unop)

Alias of the reverse direction of isUAP_comp_unop.

---

A function is right almost-periodic iff it is left almost-periodic.

theorem IsUAP.comp_inv {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f : G → X} (hf : IsUAP f) : IsUAP fun (x : G) => f x⁻¹

@[simp]

theorem isUAP_comp_inv {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f : G → X} : (IsUAP fun (x : G) => f x⁻¹) ↔ IsUAP f

Operations on the codomain

theorem IsUAP.continuous_comp {G : Type u_3} {X : Type u_6} {Y : Type u_7} [Group G] [MetricSpace X] [MetricSpace Y] {f : G → X} [ProperSpace X] {φ : X → Y} (hf : IsUAP f) (hφ : Continuous φ) : IsUAP (φ ∘ f)

Postcomposing a uniformly almost-periodic function with a continuous function gives a uniformly almost-periodic function.

theorem IsUAP.fun_continuous_comp {G : Type u_3} {X : Type u_6} {Y : Type u_7} [Group G] [MetricSpace X] [MetricSpace Y] {f : G → X} [ProperSpace X] {φ : X → Y} (hf : IsUAP f) (hφ : Continuous φ) : IsUAP fun (x : G) => φ (f x)

Eta-expanded form of IsUAP.continuous_comp

---

Postcomposing a uniformly almost-periodic function with a continuous function gives a uniformly almost-periodic function.

theorem IsUAP.of_tendstoUniformly {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f : G → X} {ι : Type u_10} {p : Filter ι} [p.NeBot] {u : ι → G → X} (hu : ∀ᶠ (n : ι) in p, IsUAP (u n)) (h : TendstoUniformly u f p) : IsUAP f

Almost-periodicity is preserved by uniform limits along any (nontrivial) filter.

theorem isUAP_prod_iff {G : Type u_3} {X : Type u_6} {Y : Type u_7} [Group G] [MetricSpace X] [MetricSpace Y] {f : G → X × Y} : IsUAP f ↔ IsUAP (Prod.fst ∘ f) ∧ IsUAP (Prod.snd ∘ f)

A product-valued function is uniformly almost-periodic iff both of its components are.

theorem closedBall_one_subset_uniformAP_of_isUniformContinuousWith {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f : G → X} {ε : ℝ} [MetricSpace G] [IsIsometricSMul Gᵐᵒᵖ G] {δ : ℝ → ℝ} (hf : Metric.IsUniformContinuousWith δ f) (hε : 0 < ε) : Metric.closedBall 1 (δ ε) ⊆ AP∞(f, ε)

theorem Metric.IsUniformContinuousWith.isUAPWith {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f : G → X} [MetricSpace G] [IsIsometricSMul Gᵐᵒᵖ G] {δ : ℝ → ℝ} [CompactSpace G] (hδ : ∀ ε > 0, 0 < δ ε) (hf : IsUniformContinuousWith δ f) : IsUAPWith (fun (ε : ℝ) => ↑(coveringNumber (δ ε).toNNReal Set.univ).toNat) f

theorem UniformContinuous.isUAP {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f : G → X} [MetricSpace G] [IsIsometricSMul Gᵐᵒᵖ G] [CompactSpace G] (hf : UniformContinuous f) : IsUAP f

theorem Continuous.isUAP {G : Type u_3} {X : Type u_6} [Group G] [MetricSpace X] {f : G → X} [MetricSpace G] [IsIsometricSMul Gᵐᵒᵖ G] [CompactSpace G] (hf : Continuous f) : IsUAP f

Normed additive group codomain

Uniform almost-periods

theorem mem_uniformAP_iff_norm {G : Type u_3} {E : Type u_8} [Group G] {t : G} [NormedAddCommGroup E] {f : G → E} {ε : ℝ} : t ∈ AP∞(f, ε) ↔ ∀ (x : G), ‖f (t⁻¹ * x) - f x‖ ≤ ε

@[simp]

theorem uniformAP_zero {G : Type u_3} {E : Type u_8} [Group G] [NormedAddCommGroup E] {ε : ℝ} (hε : 0 ≤ ε) : AP∞(0, ε) = Set.univ

theorem inter_subset_uniformAP_add {G : Type u_3} {E : Type u_8} [Group G] [NormedAddCommGroup E] {f g : G → E} {ε δ : ℝ} : AP∞(f, ε) ∩ AP∞(g, δ) ⊆ AP∞(f + g, ε + δ)

@[simp]

theorem uniformAP_smul {𝕜 : Type u_2} {G : Type u_3} {E : Type u_8} [RCLike 𝕜] [Group G] {c : 𝕜} [NormedAddCommGroup E] (f : G → E) {ε : ℝ} [NormedSpace 𝕜 E] (hc : c ≠ 0) : AP∞(c • f, ε) = AP∞(f, ε / ‖c‖)

@[simp]

theorem uniformAP_fun_smul {𝕜 : Type u_2} {G : Type u_3} {E : Type u_8} [RCLike 𝕜] [Group G] {c : 𝕜} [NormedAddCommGroup E] (f : G → E) {ε : ℝ} [NormedSpace 𝕜 E] (hc : c ≠ 0) : AP∞(fun (i : G) => c • f i, ε) = AP∞(f, ε / ‖c‖)

Eta-expanded form of uniformAP_smul

Quantitative uniformly almost-periodic functions

@[simp]

theorem IsUAPWith.zero {G : Type u_3} {E : Type u_8} [Group G] [NormedAddCommGroup E] : IsUAPWith 1 0

theorem IsUAPWith.add {G : Type u_3} {E : Type u_8} [Group G] {K L : ℝ → ℝ} [NormedAddCommGroup E] {f g : G → E} (hf : IsUAPWith K f) (hg : IsUAPWith L g) : IsUAPWith (fun (ε : ℝ) => K (ε / 4) * L (ε / 4)) (f + g)

The sum of a K- and an L-almost-periodic function is ε ↦ K (ε / 4) * L (ε / 4)-almost-periodic.

theorem IsUAPWith.fun_add {G : Type u_3} {E : Type u_8} [Group G] {K L : ℝ → ℝ} [NormedAddCommGroup E] {f g : G → E} (hf : IsUAPWith K f) (hg : IsUAPWith L g) : IsUAPWith (fun (ε : ℝ) => K (ε / 4) * L (ε / 4)) fun (i : G) => f i + g i

Eta-expanded form of IsUAPWith.add

---

The sum of a K- and an L-almost-periodic function is ε ↦ K (ε / 4) * L (ε / 4)-almost-periodic.

theorem IsUAPWith.smul {𝕜 : Type u_2} {G : Type u_3} {E : Type u_8} [RCLike 𝕜] [Group G] {K : ℝ → ℝ} {c : 𝕜} [NormedAddCommGroup E] {f : G → E} [NormedSpace 𝕜 E] (hf : IsUAPWith K f) (hc : c ≠ 0) : IsUAPWith (fun (ε : ℝ) => K (ε / ‖c‖)) (c • f)

theorem IsUAPWith.fun_smul {𝕜 : Type u_2} {G : Type u_3} {E : Type u_8} [RCLike 𝕜] [Group G] {K : ℝ → ℝ} {c : 𝕜} [NormedAddCommGroup E] {f : G → E} [NormedSpace 𝕜 E] (hf : IsUAPWith K f) (hc : c ≠ 0) : IsUAPWith (fun (ε : ℝ) => K (ε / ‖c‖)) fun (i : G) => c • f i

Eta-expanded form of IsUAPWith.smul

Qualitative uniformly almost-periodic functions

@[simp]

theorem IsUAP.zero {G : Type u_3} {E : Type u_8} [Group G] [NormedAddCommGroup E] : IsUAP 0

theorem IsUAP.add {G : Type u_3} {E : Type u_8} [Group G] [NormedAddCommGroup E] {f g : G → E} (hf : IsUAP f) (hg : IsUAP g) : IsUAP (f + g)

theorem IsUAP.fun_add {G : Type u_3} {E : Type u_8} [Group G] [NormedAddCommGroup E] {f g : G → E} (hf : IsUAP f) (hg : IsUAP g) : IsUAP fun (i : G) => f i + g i

Eta-expanded form of IsUAP.add

theorem IsUAP.smul {𝕜 : Type u_2} {G : Type u_3} {E : Type u_8} [RCLike 𝕜] [Group G] {c : 𝕜} [NormedAddCommGroup E] {f : G → E} [NormedSpace 𝕜 E] (hf : IsUAP f) : IsUAP (c • f)

theorem IsUAP.fun_smul {𝕜 : Type u_2} {G : Type u_3} {E : Type u_8} [RCLike 𝕜] [Group G] {c : 𝕜} [NormedAddCommGroup E] {f : G → E} [NormedSpace 𝕜 E] (hf : IsUAP f) : IsUAP fun (i : G) => c • f i

Eta-expanded form of IsUAP.smul

theorem IsUAP.isAlmostConvergent {G : Type u_3} {E : Type u_8} [Group G] [NormedAddCommGroup E] {f : G → E} [NormedSpace ℝ E] (hf : IsUAP f) : IsAlmostConvergent f

Star

@[simp]

theorem uniformAP_star {G : Type u_3} {E : Type u_8} [Group G] [NormedAddCommGroup E] {f : G → E} {ε : ℝ} [StarAddMonoid E] [NormedStarGroup E] : AP∞(fun (x : G) => star (f x), ε) = AP∞(f, ε)

theorem IsUAPWith.star {G : Type u_3} {E : Type u_8} [Group G] {K : ℝ → ℝ} [NormedAddCommGroup E] {f : G → E} [StarAddMonoid E] [NormedStarGroup E] (hf : IsUAPWith K f) : IsUAPWith K fun (x : G) => star (f x)

theorem IsUAP.star {G : Type u_3} {E : Type u_8} [Group G] [NormedAddCommGroup E] {f : G → E} [StarAddMonoid E] [NormedStarGroup E] (hf : IsUAP f) : IsUAP fun (x : G) => star (f x)

theorem inter_subset_uniformAP_mul {G : Type u_3} {R : Type u_5} [Group G] [NormedRing R] {f g : G → R} {ε Bf Bg δ : ℝ} (hfb : ∀ (x : G), ‖f x‖ ≤ Bf) (hgb : ∀ (x : G), ‖g x‖ ≤ Bg) : AP∞(f, ε) ∩ AP∞(g, δ) ⊆ AP∞(f * g, Bg * ε + Bf * δ)

If t is an ε-almost-period of a Bf-bounded function f and a δ-almost-period of a Bg-bounded function g, then it is a Bg * ε + Bf * δ-almost-period of f * g.

theorem IsUAPWith.mul {G : Type u_3} {R : Type u_5} [Group G] {K L : ℝ → ℝ} [NormedRing R] {f g : G → R} {Bf Bg : ℝ} (hfb : ∀ (x : G), ‖f x‖ ≤ Bf) (hgb : ∀ (x : G), ‖g x‖ ≤ Bg) (hf : IsUAPWith K f) (hg : IsUAPWith L g) : IsUAPWith (fun (ε : ℝ) => K (ε / (4 * (Bf + Bg + 1))) * L (ε / (4 * (Bf + Bg + 1)))) (f * g)

The product of two uniformly almost-periodic functions is uniformly almost-periodic, with an explicit modulus depending on the bounds on the norms of f and g.

theorem IsUAP.mul {G : Type u_3} {R : Type u_5} [Group G] [NormedRing R] {f g : G → R} (hf : IsUAP f) (hg : IsUAP g) : IsUAP (f * g)

theorem IsUAP.conj {G : Type u_3} {R : Type u_5} [Group G] [NormedCommRing R] [StarRing R] [NormedStarGroup R] {f : G → R} (hf : IsUAP f) : IsUAP fun (x : G) => (starRingEnd R) (f x)