The Foelner mean associated to a Foelner filter

noncomputable def InvtMean.foelner {G : Type u_1} {ι : Type u_2} [MeasurableSpace G] [Group G] (μ : MeasureTheory.Measure G) (l : Filter ι) [l.NeBot] (F : ι → Set G) (hF : IsFoelner G μ l F) : InvtMean G ℂ ℂ

Equations

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

@[simp]

theorem InvtMean.foelner_count_indicator_one_finset {G : Type u_1} {ι : Type u_2} [MeasurableSpace G] [Group G] {l : Filter ι} [l.NeBot] [MeasurableSingletonClass G] [Fintype G] (A : Finset G) : (foelner MeasureTheory.Measure.count l (fun (x : ι) => Set.univ) ⋯).real ((↑A).indicator fun (x : G) => 1) = ↑A.dens

@[simp]

theorem InvtMean.foelner_count_indicator_one {G : Type u_1} {ι : Type u_2} [MeasurableSpace G] [Group G] {l : Filter ι} [l.NeBot] [MeasurableSingletonClass G] [Fintype G] (A : Set G) : (foelner MeasureTheory.Measure.count l (fun (x : ι) => Set.univ) ⋯).real (A.indicator fun (x : G) => 1) = ↑⋯.toFinset.dens

@[simp]

theorem InvtMean.IsMeasFun.foelner_of_discrete {G : Type u_1} {ι : Type u_2} [MeasurableSpace G] [Group G] {μ : MeasureTheory.Measure G} {l : Filter ι} [l.NeBot] {F : ι → Set G} [MeasurableSingletonClass G] [Finite G] {hF : IsFoelner G μ l F} {f : G → ℂ} : (foelner μ l F hF).IsMeasFun f

@[simp]

theorem InvtMean.IsMeasSet.foelner_of_discrete {G : Type u_1} {ι : Type u_2} [MeasurableSpace G] [Group G] {μ : MeasureTheory.Measure G} {l : Filter ι} [l.NeBot] {F : ι → Set G} [MeasurableSingletonClass G] [Finite G] {hF : IsFoelner G μ l F} {s : Set G} : (foelner μ l F hF).IsMeasSet s