## 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 nnreals 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. -/
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. -/
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

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)

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)

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)

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