Theorems · Theorem · measure theory

IsAddFoelner.tendsto_nhds_mean

∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : AddGroup G]
  [inst_2 : AddAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X},
  IsAddFoelner G μ (↑u) F →
    ∀ (s : Set X), Filter.Tendsto (fun i => μ (s ∩ F i) / μ (F i)) (↑u) (nhds (IsAddFoelner.mean μ u F s))

Defined in: Mathlib.MeasureTheory.Group.FoelnerFilter
Cited by: 3 results in Mathlib
Foundations: Depth 171 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasurableSpace AddGroup AddAction

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites32

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Setstatement and proof · cited by 53,352
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
ENNRealstatement and proof · cited by 9,879
Top.topproof · cited by 9,680
nhdsstatement and proof · cited by 5,554
AddGroupstatement and proof · cited by 4,410
Filter.Tendstostatement · cited by 3,814
Filter.Eventuallyproof · cited by 3,134
one_mulproof · cited by 2,841
Set.Iccproof · cited by 1,702

Cited by3

Results whose statement or proof uses this declaration.

IsAddFoelner.mean_univ_eq_zeroproof · cited by 1
IsAddFoelner.mean_vadd_eq_mean_vaddproof · cited by 1
IsAddFoelner.mean_union_eq_add_of_disjointproof · cited by 1