Invariant means

structure InvtMean (G : Type u_1) (𝕜 : Type u_2) (E : Type u_3) [Group G] [RCLike 𝕜] [NormedAddCommGroup E] [PartialOrder E] [NormedSpace 𝕜 E] : Type (max u_1 u_3)

• IsMeasFun : (G → E) → Prop
• isMeasFun_const (z : E) : self.IsMeasFun fun (x : G) => z
• isMeasFun_add (f : G → E) (hf : self.IsMeasFun f) (g : G → E) (hg : self.IsMeasFun g) : self.IsMeasFun (f + g)
• isMeasFun_smul (c : 𝕜) (f : G → E) (hf : self.IsMeasFun f) : self.IsMeasFun (c • f)
• isMeasFun_translate (x : G) (f : G → E) (hf : self.IsMeasFun f) : self.IsMeasFun (τ_[x] f)
• isBddFun_of_isMeasFun (f : G → E) (hf : self.IsMeasFun f) : Bornology.IsBddFun f
• toFun : (G → E) → E
• map_zero : self.toFun 0 = 0
• map_add (f : G → E) (hf : self.IsMeasFun f) (g : G → E) (hg : self.IsMeasFun g) : self.toFun (f + g) = self.toFun f + self.toFun g
• map_smul (f : G → E) (hf : self.IsMeasFun f) (c : 𝕜) : self.toFun (c • f) = c • self.toFun f
• map_nonneg (f : G → E) (hf₀ : 0 ≤ f) (hf : self.IsMeasFun f) : 0 ≤ self.toFun f
• map_translate (f : G → E) (hf : self.IsMeasFun f) (x : G) : self.toFun (τ_[x] f) = self.toFun f

@[instance_reducible]

instance InvtMean.instCoeFunForallForall {G : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Group G] [RCLike 𝕜] [NormedAddCommGroup E] [PartialOrder E] [NormedSpace 𝕜 E] : CoeFun (InvtMean G 𝕜 E) fun (x : InvtMean G 𝕜 E) => (G → E) → E

Equations

• InvtMean.instCoeFunForallForall = { coe := InvtMean.toFun }

@[simp]

theorem InvtMean.IsMeasFun.const {G : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Group G] [RCLike 𝕜] [NormedAddCommGroup E] [PartialOrder E] [NormedSpace 𝕜 E] {m : InvtMean G 𝕜 E} {z : E} : m.IsMeasFun (Function.const G z)

@[simp]

theorem InvtMean.IsMeasFun.fun_const {G : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Group G] [RCLike 𝕜] [NormedAddCommGroup E] [PartialOrder E] [NormedSpace 𝕜 E] {m : InvtMean G 𝕜 E} {z : E} : m.IsMeasFun fun (x : G) => z

Eta-expanded form of InvtMean.IsMeasFun.const

@[simp]

theorem InvtMean.IsMeasFun.zero {G : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Group G] [RCLike 𝕜] [NormedAddCommGroup E] [PartialOrder E] [NormedSpace 𝕜 E] {m : InvtMean G 𝕜 E} : m.IsMeasFun 0

theorem InvtMean.IsMeasFun.add {G : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Group G] [RCLike 𝕜] [NormedAddCommGroup E] [PartialOrder E] [NormedSpace 𝕜 E] {m : InvtMean G 𝕜 E} {f g : G → E} (hf : m.IsMeasFun f) (hg : m.IsMeasFun g) : m.IsMeasFun (f + g)

theorem InvtMean.IsMeasFun.fun_add {G : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Group G] [RCLike 𝕜] [NormedAddCommGroup E] [PartialOrder E] [NormedSpace 𝕜 E] {m : InvtMean G 𝕜 E} {f g : G → E} (hf : m.IsMeasFun f) (hg : m.IsMeasFun g) : m.IsMeasFun fun (i : G) => f i + g i

Eta-expanded form of InvtMean.IsMeasFun.add

theorem InvtMean.IsMeasFun.smul {G : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Group G] [RCLike 𝕜] [NormedAddCommGroup E] [PartialOrder E] [NormedSpace 𝕜 E] {m : InvtMean G 𝕜 E} {f : G → E} {c : 𝕜} (hf : m.IsMeasFun f) : m.IsMeasFun (c • f)

theorem InvtMean.IsMeasFun.translate {G : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Group G] [RCLike 𝕜] [NormedAddCommGroup E] [PartialOrder E] [NormedSpace 𝕜 E] {m : InvtMean G 𝕜 E} {f : G → E} {x : G} (hf : m.IsMeasFun f) : m.IsMeasFun (τ_[x] f)

theorem InvtMean.IsMeasFun.neg {G : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Group G] [RCLike 𝕜] [NormedAddCommGroup E] [PartialOrder E] [NormedSpace 𝕜 E] {m : InvtMean G 𝕜 E} {f : G → E} (hf : m.IsMeasFun f) : m.IsMeasFun (-f)

theorem InvtMean.IsMeasFun.fun_neg {G : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Group G] [RCLike 𝕜] [NormedAddCommGroup E] [PartialOrder E] [NormedSpace 𝕜 E] {m : InvtMean G 𝕜 E} {f : G → E} (hf : m.IsMeasFun f) : m.IsMeasFun fun (i : G) => -f i

Eta-expanded form of InvtMean.IsMeasFun.neg

@[simp]

theorem InvtMean.isMeasFun_neg {G : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Group G] [RCLike 𝕜] [NormedAddCommGroup E] [PartialOrder E] [NormedSpace 𝕜 E] {m : InvtMean G 𝕜 E} {f : G → E} : m.IsMeasFun (-f) ↔ m.IsMeasFun f

@[simp]

theorem InvtMean.fun_isMeasFun_neg {G : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Group G] [RCLike 𝕜] [NormedAddCommGroup E] [PartialOrder E] [NormedSpace 𝕜 E] {m : InvtMean G 𝕜 E} {f : G → E} : (m.IsMeasFun fun (i : G) => -f i) ↔ m.IsMeasFun f

Eta-expanded form of InvtMean.isMeasFun_neg

theorem InvtMean.IsMeasFun.isBddFun {G : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [Group G] [RCLike 𝕜] [NormedAddCommGroup E] [PartialOrder E] [NormedSpace 𝕜 E] {m : InvtMean G 𝕜 E} {f : G → E} (hf : m.IsMeasFun f) : Bornology.IsBddFun f

@[simp]

theorem InvtMean.IsMeasFun.natCast {G : Type u_1} {𝕜 : Type u_2} {R : Type u_4} [Group G] [RCLike 𝕜] [NormedRing R] [PartialOrder R] [NormedSpace 𝕜 R] {m : InvtMean G 𝕜 R} {n : ℕ} : m.IsMeasFun ↑n

@[simp]

theorem InvtMean.IsMeasFun.intCast {G : Type u_1} {𝕜 : Type u_2} {R : Type u_4} [Group G] [RCLike 𝕜] [NormedRing R] [PartialOrder R] [NormedSpace 𝕜 R] {m : InvtMean G 𝕜 R} {n : ℤ} : m.IsMeasFun ↑n

@[simp]

theorem InvtMean.IsMeasFun.one {G : Type u_1} {𝕜 : Type u_2} {R : Type u_4} [Group G] [RCLike 𝕜] [NormedRing R] [PartialOrder R] [NormedSpace 𝕜 R] {m : InvtMean G 𝕜 R} : m.IsMeasFun 1

@[simp]

theorem InvtMean.IsMeasFun.ofNat {G : Type u_1} {𝕜 : Type u_2} {R : Type u_4} [Group G] [RCLike 𝕜] [NormedRing R] [PartialOrder R] [NormedSpace 𝕜 R] {m : InvtMean G 𝕜 R} {n : ℕ} [n.AtLeastTwo] : m.IsMeasFun (OfNat.ofNat n)

def InvtMean.IsMeasSet {G : Type u_1} {𝕜 : Type u_2} {R : Type u_4} [Group G] [RCLike 𝕜] [NormedRing R] [PartialOrder R] [NormedSpace 𝕜 R] (m : InvtMean G 𝕜 R) (A : Set G) : Prop

A set A is m-measurable if 𝟭_[A] is m-measurable.

Equations

• m.IsMeasSet A = m.IsMeasFun (A.indicator fun (x : G) => 1)

def InvtMean.real {G : Type u_1} [Group G] (m : InvtMean G ℂ ℂ) (f : G → ℝ) : ℝ

Equations

• m.real f = (m.toFun fun (g : G) => ↑(f g)).re

@[simp]

theorem InvtMean.real_mk {G : Type u_1} [Group G] (IsMeasFun : (G → ℂ) → Prop) (isMeasFun_const : ∀ (z : ℂ), IsMeasFun fun (x : G) => z) (isMeasFun_add : ∀ (f : G → ℂ), IsMeasFun f → ∀ (g : G → ℂ), IsMeasFun g → IsMeasFun (f + g)) (isMeasFun_smul : ∀ (c : ℂ) (f : G → ℂ), IsMeasFun f → IsMeasFun (c • f)) (isMeasFun_translate : ∀ (x : G) (f : G → ℂ), IsMeasFun f → IsMeasFun (τ_[x] f)) (isBddFun_of_isMeasFun : ∀ (f : G → ℂ), IsMeasFun f → Bornology.IsBddFun f) (toFun : (G → ℂ) → ℂ) (map_zero : toFun 0 = 0) (map_add : ∀ (f : G → ℂ), IsMeasFun f → ∀ (g : G → ℂ), IsMeasFun g → toFun (f + g) = toFun f + toFun g) (map_smul : ∀ (f : G → ℂ), IsMeasFun f → ∀ (c : ℂ), toFun (c • f) = c • toFun f) (map_nonneg : ∀ (f : G → ℂ), 0 ≤ f → IsMeasFun f → 0 ≤ toFun f) (map_translate : ∀ (f : G → ℂ), IsMeasFun f → ∀ (x : G), toFun (τ_[x] f) = toFun f) (f : G → ℝ) : { IsMeasFun := IsMeasFun, isMeasFun_const := isMeasFun_const, isMeasFun_add := isMeasFun_add, isMeasFun_smul := isMeasFun_smul, isMeasFun_translate := isMeasFun_translate, isBddFun_of_isMeasFun := isBddFun_of_isMeasFun, toFun := toFun, map_zero := map_zero, map_add := map_add, map_smul := map_smul, map_nonneg := map_nonneg, map_translate := map_translate }.real f = (toFun fun (g : G) => ↑(f g)).re

@[instance_reducible]

instance InvtMean.instCoeFunComplexForallForallReal {G : Type u_1} [Group G] : CoeFun (InvtMean G ℂ ℂ) fun (x : InvtMean G ℂ ℂ) => (G → ℝ) → ℝ

Equations

• InvtMean.instCoeFunComplexForallForallReal = { coe := InvtMean.real }

def InvtMean.l2 {G : Type u_1} {E : Type u_3} [Group G] [NormedAddCommGroup E] (m : InvtMean G ℂ ℂ) : Set (G → E)

Equations

• L^2(m) = {f : G → E | m.IsMeasFun fun (g : G) => ↑‖f g‖ ^ 2}

def InvtMean.«termL^2(_)» : Lean.ParserDescr

Equations

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

noncomputable def InvtMean.l2Norm {G : Type u_1} [Group G] (m : InvtMean G ℂ ℂ) (f : G → ℂ) : ℝ

Equations

• m.l2Norm f = √(m.real fun (g : G) => ‖f g‖ ^ 2)

@[simp]

theorem InvtMean.l2Norm_indicator_one {G : Type u_1} [Group G] (m : InvtMean G ℂ ℂ) (A : Set G) : m.l2Norm (A.indicator fun (x : G) => 1) = √(m.real (A.indicator fun (x : G) => 1))