structure InvtMean (G : Type u_1) [Group G] : Type u_1

• IsMeasFun : (G → ℂ) → Prop
• isMeasFun_const (z : ℂ) : self.IsMeasFun fun (x : G) => z
• isMeasFun_translate (g : G) (f : G → ℂ) (hf : self.IsMeasFun f) : self.IsMeasFun fun (h : G) => f (g⁻¹ * h)
• bdd_of_isMeasFun (f : G → ℂ) (hf : self.IsMeasFun f) : ∃ (C : ℝ), ∀ (g : G), ‖f g‖ ≤ C
• toFun : (G → ℂ) → ℂ
• map_zero : self.toFun 0 = 0
• map_add (f₁ : G → ℂ) (h₁ : self.IsMeasFun f₁) (f₂ : G → ℂ) (h₂ : self.IsMeasFun f₂) : self.toFun (f₁ + f₂) = self.toFun f₁ + self.toFun f₂
• map_smul (f : G → ℂ) (hf : self.IsMeasFun f) (z : ℂ) : self.toFun (z • f) = z • self.toFun f
• map_nonneg (f : G → ℂ) (hf₀ : 0 ≤ f) : 0 ≤ self.toFun f
• map_translate (f : G → ℂ) (hf : self.IsMeasFun f) (g : G) : (self.toFun fun (h : G) => f (g⁻¹ * h)) = self.toFun f

@[implicit_reducible]

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

Equations

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

@[simp]

theorem InvtMean.IsMeasFun.const {G : Type u_1} [Group G] {m : InvtMean G} {z : ℂ} : m.IsMeasFun fun (x : G) => z

@[simp]

theorem InvtMean.IsMeasFun.natCast {G : Type u_1} [Group G] {m : InvtMean G} {n : ℕ} : m.IsMeasFun ↑n

@[simp]

theorem InvtMean.IsMeasFun.intCast {G : Type u_1} [Group G] {m : InvtMean G} {n : ℤ} : m.IsMeasFun ↑n

@[simp]

theorem InvtMean.IsMeasFun.zero {G : Type u_1} [Group G] {m : InvtMean G} : m.IsMeasFun 0

@[simp]

theorem InvtMean.IsMeasFun.one {G : Type u_1} [Group G] {m : InvtMean G} : m.IsMeasFun 0

@[simp]

theorem InvtMean.IsMeasFun.ofNat {G : Type u_1} [Group G] {m : InvtMean G} {n : ℕ} [n.AtLeastTwo] : m.IsMeasFun (OfNat.ofNat n)

theorem InvtMean.IsMeasFun.translate {G : Type u_1} [Group G] {m : InvtMean G} {f : G → ℂ} {g : G} (hf : m.IsMeasFun f) : m.IsMeasFun fun (h : G) => f (g⁻¹ * h)

theorem InvtMean.IsMeasFun.bdd {G : Type u_1} [Group G] {m : InvtMean G} {f : G → ℂ} (hf : m.IsMeasFun f) : ∃ (C : ℝ), ∀ (g : G), ‖f g‖ ≤ C

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

@[implicit_reducible]

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

Equations

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

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

Equations

• L^2(m) = {f : G → ℂ | 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))

def InvtMean.IsMeasSet {G : Type u_1} [Group G] (m : InvtMean G) (A : Set G) : Prop

Equations

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