L^2(m)

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

Equations

• AP_L^2(m)(f, ε) = {t : G | m.l2Norm ((fun (g : G) => f (t⁻¹ * g)) - f) ≤ ε * m.l2Norm f}

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

Equations

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

@[simp]

theorem InvtMean.mem_l2AP {G : Type u_1} [Group G] {m : InvtMean G} {f : G → ℂ} {t : G} {ε : ℝ} : t ∈ AP_L^2(m)(f, ε) ↔ m.l2Norm ((fun (g : G) => f (t⁻¹ * g)) - f) ≤ ε * m.l2Norm f

@[simp]

theorem InvtMean.mem_l2AP_indicator_one {G : Type u_1} [Group G] {m : InvtMean G} {A : Set G} {t : G} {ε : ℝ} : t ∈ AP_L^2(m)(A.indicator fun (x : G) => 1, ε) ↔ m.real (((t • A).indicator fun (x : G) => 1) - A.indicator fun (x : G) => 1) ≤ ε ^ 2 * m.real (A.indicator fun (x : G) => 1)

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

Equations

• m.IsL2APWith f K = ∀ ε > 0, CovBySMul G (K ε) Set.univ AP_L^2(m)(f, ε)