filters and limits

Stream: maths

[Johan Commelin]

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]

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]

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]

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]

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

[Johan Commelin]

I'll see if I can make that work

[Johan Commelin]

My phi isn't currently defined on all sets...