Uniformly almost periodic functions

def IsRelDenseWith (E : Set ℝ) (l : ℝ) : Prop

A set E of reals is relatively dense with respect to l if every (closed-open) interval of length l contains an element of E.

Equations

• IsRelDenseWith E l = ∀ (x : ℝ), ∃ y ∈ Set.Ico 0 l, x + y ∈ E

theorem IsRelDenseWith.subset {E F : Set ℝ} {l : ℝ} (hEF : E ⊆ F) : IsRelDenseWith E l → IsRelDenseWith F l

theorem IsRelDenseWith.pos {E : Set ℝ} {l : ℝ} (hE : IsRelDenseWith E l) : 0 < l

def IsRelDense (E : Set ℝ) : Prop

A set E of reals is relatively dense if it is relatively dense with respect to some l.

Equations

• IsRelDense E = ∃ (l : ℝ), IsRelDenseWith E l

theorem IsRelDense.subset {E F : Set ℝ} (hEF : E ⊆ F) : IsRelDense E → IsRelDense F

def IsLinftyAP (ε t : ℝ) (f : ℝ → ℂ) : Prop

A real number t is an ε, L∞-almost period of a function f : ℝ \r ℝ if ‖f - τ t f‖_∞ ≤ ε.

Equations

• IsLinftyAP ε t f = ∀ (x : ℝ), ‖f (x + t) - f x‖ ≤ ε

theorem IsLinftyAP.mul_fun {C D ε δ t : ℝ} {f g : ℝ → ℂ} (hfbdd : ∀ (x : ℝ), ‖f x‖ ≤ C) (hgbdd : ∀ (x : ℝ), ‖g x‖ ≤ D) (hf : IsLinftyAP ε t f) (hg : IsLinftyAP δ t g) : IsLinftyAP (D * ε + C * δ) t (f * g)

def IsUnifAlmostPeriodic (f : ℝ → ℂ) : Prop

A function f : ℝ → ℂ is uniformly almost periodic if its set of ε, L∞-almost period is relatively dense for all ε > 0.

Equations

• IsUnifAlmostPeriodic f = ∀ ⦃ε : ℝ⦄, 0 < ε → IsRelDense {t : ℝ | IsLinftyAP ε t f}

theorem IsUnifAlmostPeriodic.uniformContinuous {f : ℝ → ℂ} (hf : IsUnifAlmostPeriodic f) : UniformContinuous f

Any uniformly almost periodic function is uniformly continuous.

theorem IsUnifAlmostPeriodic.exists_forall_le {f : ℝ → ℂ} (hf : IsUnifAlmostPeriodic f) : ∃ (C : ℝ), ∀ (x : ℝ), ‖f x‖ ≤ C

Any uniformly almost periodic function is bounded.

theorem IsUnifAlmostPeriodic.isRelDense_inter {ε : ℝ} {f g : ℝ → ℂ} (hf : IsUnifAlmostPeriodic f) (hg : IsUnifAlmostPeriodic g) (hε : 0 < ε) : IsRelDense {t : ℝ | IsLinftyAP ε t f ∧ IsLinftyAP ε t g}

The intersection of the almost periods of two uniformly almost periodic functions is relatively dense.

theorem IsUnifAlmostPeriodic.mul {f g : ℝ → ℂ} (hf : IsUnifAlmostPeriodic f) (hg : IsUnifAlmostPeriodic g) : IsUnifAlmostPeriodic (f * g)