The von Neumann mean

This file defines the von Neumann mean.

References

• Almost periodic functions in a group. I, John von Neumann

noncomputable def InvtMean.vn {G : Type u_1} (𝕜 : Type u_2) {E : Type u_3} [Group G] [RCLike 𝕜] [NormedAddCommGroup E] [PartialOrder E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] : InvtMean G 𝕜 E

The von Neumann mean

Equations

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

@[simp]

theorem InvtMean.IsMeasFun_vn {G : Type u_1} (𝕜 : Type u_2) {E : Type u_3} [Group G] [RCLike 𝕜] [NormedAddCommGroup E] [PartialOrder E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] (f : G → E) : (vn 𝕜).IsMeasFun f = IsUAP f

@[simp]

theorem InvtMean.vn_apply {G : Type u_1} (𝕜 : Type u_2) {E : Type u_3} [Group G] [RCLike 𝕜] [NormedAddCommGroup E] [PartialOrder E] [NormedSpace 𝕜 E] [NormedSpace ℝ E] (f : G → E) : (vn 𝕜).toFun f = if hf : IsUAP f then Exists.choose ⋯ else 0