def IsAPRiemann {G : Type u_1} {E : Type u_2} [Group G] [PartialOrder E] [NormedAddCommGroup E] [NormedSpace ℝ E] (f : G → E) : Prop

A function f from a group G to a normed space E is almost-periodically Riemann-integrable if for all ε > 0 it is possible to write f as a pointwise convex combination of UAP whose means are all at most ε apart.

Equations

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

theorem IsUAP.isAPRiemann {G : Type u_1} {E : Type u_2} [Group G] [PartialOrder E] [NormedAddCommGroup E] [NormedSpace ℝ E] {f : G → E} (hf : IsUAP f) : IsAPRiemann f

theorem isAPRiemann_iff_exists_le_ge_isUAP {G : Type u_1} [Group G] {f : G → ℝ} : IsAPRiemann f ↔ ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ g ≤ f, IsUAP g ∧ ∃ h ≥ f, IsUAP h ∧ (InvtMean.vn ℝ).toFun h - (InvtMean.vn ℝ).toFun g ≤ ε

A real-valued function is AP-Riemann integrable iff it is sandwiched arbitrarily well between two UAP functions.

theorem IsAPRiemann.exists_le_ge_isUAP {G : Type u_1} [Group G] {f : G → ℝ} : IsAPRiemann f → ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ g ≤ f, IsUAP g ∧ ∃ h ≥ f, IsUAP h ∧ (InvtMean.vn ℝ).toFun h - (InvtMean.vn ℝ).toFun g ≤ ε

Alias of the forward direction of isAPRiemann_iff_exists_le_ge_isUAP.

---

A real-valued function is AP-Riemann integrable iff it is sandwiched arbitrarily well between two UAP functions.

theorem IsAPRiemann.of_exists_le_ge_isUAP {G : Type u_1} [Group G] {f : G → ℝ} : (∀ ⦃ε : ℝ⦄, 0 < ε → ∃ g ≤ f, IsUAP g ∧ ∃ h ≥ f, IsUAP h ∧ (InvtMean.vn ℝ).toFun h - (InvtMean.vn ℝ).toFun g ≤ ε) → IsAPRiemann f

Alias of the reverse direction of isAPRiemann_iff_exists_le_ge_isUAP.

---

A real-valued function is AP-Riemann integrable iff it is sandwiched arbitrarily well between two UAP functions.

theorem IsAPRiemann.mean_congr {G : Type u_1} [Group G] {f : G → ℝ} {m m' : InvtMean G ℝ ℝ} (hf : IsAPRiemann f) (hfm : m.IsMeasFun f) (hfm' : m'.IsMeasFun f) : m.toFun f = m'.toFun f

Any two means that measure an AP-Riemann integrable function f agree on what its mean is.