# Zulip Chat Archive

## Stream: maths

### Topic: filters and limits

#### Johan Commelin (Dec 05 2019 at 09:46):

I have a way of attaching an `nnreal`

to every set in the neighbourhood filter of some point in some space. Now I would like to express the predicate that these `nnreal`

s converge to some limit point for smaller and smaller nhds. The usual `tendsto`

language doesn't seem built for this purpose. How should I do this?

#### Johan Commelin (Dec 05 2019 at 09:47):

Short piece of code:

def relative_index (K : set G) (hK : compact K) (U : set G) (hU : U ∈ 𝓝 (1:G)) : nnreal := (index U K hU hK : nnreal) / (index U A hU hA : nnreal)

#### Johan Commelin (Dec 05 2019 at 09:48):

My file so far:

import topology.algebra.group import measure_theory.borel_space import measure_theory.measure_space import tactic /-! # Haar measure In this file we define the Haar measure: A left-translation invariant measure on a locally compact topological group. ## References Alfsen, E. M. A simplified constructive proof of the existence and uniqueness of Haar measure. Math. Scand. 12 (1963), 106--116. MR0158022 -/ noncomputable theory open_locale classical topological_space open measure_theory variables {G : Type*} variables [group G] [topological_space G] namespace measure_theory namespace measure /-- A measure `μ` on a topological group is left invariant if for all measurable sets `s` and all `g`, we have `μ (gs) = μ s`, where `gs` denotes the translate of `s` by left multiplication with `g`. -/ @[to_additive is_left_add_invariant] def is_left_invariant (μ : measure G) : Prop := ∀ s : set G, is_measurable s → ∀ g : G, μ ((*) g '' s) = μ s end measure end measure_theory namespace topological_group namespace haar_measure_construction open lattice variables [topological_group G] /-- `index_prop S T` is a predicate asserting that `T` is covered by finitely many left-translates of `S`. -/ @[to_additive] lemma index_prop (S T : set G) (hS : S ∈ 𝓝 (1:G)) (hT : compact T) : ∃ n, ∃ s : finset G, (T ⊆ ⋃ g ∈ s, ((*) g '' S)) ∧ s.card = n := begin choose U hU using mem_nhds_sets_iff.1 hS, let ι : G → set G := λ g, (*) g '' U, have hι : ∀ g : G, g ∈ (set.univ : set G) → is_open (ι g), { intros g hg, show is_open ((*) g '' U), rw show ((*) g '' U) = (*) g⁻¹ ⁻¹' U, { ext, exact mem_left_coset_iff g }, apply continuous_mul_left g⁻¹, exact hU.2.1 }, obtain ⟨s, hs, s_fin, s_cover⟩ := compact_elim_finite_subcover_image hT hι _, rcases s_fin.exists_finset_coe with ⟨s, rfl⟩, { refine ⟨_, s, _, rfl⟩, refine set.subset.trans s_cover _, apply set.Union_subset_Union, intro g, apply set.Union_subset_Union, intro hg, apply set.mono_image, exact hU.1, }, intros t ht, rw set.mem_Union, use t, rw set.mem_Union, use set.mem_univ t, rw set.mem_image, exact ⟨1, hU.2.2, mul_one t⟩ end @[to_additive] def index (S T : set G) (hS : S ∈ 𝓝 (1:G)) (hT : compact T) : ℕ := nat.find (index_prop S T hS hT) variables (A : set G) (hA : compact A) @[to_additive] def relative_index (K : set G) (hK : compact K) (U : set G) (hU : U ∈ 𝓝 (1:G)) : nnreal := (index U K hU hK : nnreal) / (index U A hU hA : nnreal) @[to_additive] def prehaar_of_compact (K : set G) (hK : compact K) : ennreal := _ variables [locally_compact_space G] end haar_measure_construction variables [topological_group G] [locally_compact_space G] variables (A : set G) (hA : compact A) @[to_additive] def haar_measure : measure G := _ end topological_group

#### Patrick Massot (Dec 05 2019 at 17:49):

I'm not sure what you are trying to express. You seem to be in a topological group context, so I assume that "smaller and smaller neighborhood" refers to the left or right uniform structure. Then you could write something like:

import topology.algebra.group import data.real.nnreal variables {G : Type*} [group G] [topological_space G] [topological_group G] open_locale topological_space def δ : G × G → G := λ p, p.2 * p.1⁻¹ def tendsto (φ : set G → nnreal) (l : nnreal) := ∀ ε > 0, ∃ V ∈ 𝓝 (1 : G), ∀ U ∈ 𝓝 (1 : G), set.prod U U ⊆ δ ⁻¹' V → abs (φ U - l).val < ε

#### Patrick Massot (Dec 05 2019 at 17:50):

About your `is_left_invariant`

definition, I think you are missing a great opportunity to use the Giry monad!

#### Johan Commelin (Dec 05 2019 at 17:51):

I'll see if I can make that work

#### Johan Commelin (Dec 05 2019 at 17:53):

My `phi`

isn't currently defined on all sets...

Last updated: May 11 2021 at 00:31 UTC