Product of Haar measures

Stream: Is there code for X?

[Xavier Roblot]

I could not find the fact that a finite product of Haar measures is a Haar measure even though we have the result for two measures: docs#measure_theory.measure.prod.is_haar_measure

[Eric Wieser]

I assume you know docs#measure_theory.measure.pi exists, and just need the missing instance about it

[Xavier Roblot]

Eric Wieser said:

I assume you know docs#measure_theory.measure.pi exists, and just need the missing instance about it

Yes, indeed. I can construct the measure but I need the proof that it is indeed an Haar measure.

[Kevin Buzzard]

But we have the hard theorem that haar measure is uniquely defined (up to scalar) by some list of properties like translation invariance so hopefully it's not too hard to make the instance if it's not there

[Eric Wieser]

I would have thought you can also get it without much work by induction on fin n

[Eric Wieser]

Kevin's proof is probably nicer though

[Eric Wieser]

The pi versions of docs#measure_theory.measure.prod.measure_theory.is_finite_measure_on_compacts and docs#measure_theory.measure.prod.is_open_pos_measure look like the missing pieces. With those you can write:

instance {ι : Type*} {G : ι → Type*} [fintype ι] [Π i, topological_space (G i)]
  {mG : Π i, measurable_space (G i)}
  (μ : Π i, measure (G i)) [Π i, is_open_pos_measure (μ i)] :
  is_open_pos_measure (measure_theory.measure.pi μ) := sorry

instance {ι : Type*} {G : ι → Type*} [fintype ι] [Π i, topological_space (G i)]
  {mG : Π i, measurable_space (G i)}
  (μ : Π i, measure (G i)) [Π i, is_finite_measure_on_compacts (μ i)] :
  is_finite_measure_on_compacts (measure_theory.measure.pi μ) := sorry

@[to_additive]
instance {ι : Type*} {G : ι → Type*} [fintype ι] [Π i, group (G i)] [Π i, topological_space (G i)]
  {mG : Π i, measurable_space (G i)}
  (μ : Π i, measure (G i)) [Π i, is_haar_measure (μ i)]
  [Π i, sigma_finite (μ i)]
  [Π i, has_measurable_mul (G i)] :
  is_haar_measure (measure_theory.measure.pi μ) := {}

[Eric Wieser]

But we also seem to be missing the pi version of docs#is_open_prod_iff, which you'd need to translate the prod proofs replacing prod with pi.

[Xavier Roblot]

Yes, I have come to the same conclusion as Eric that indeed the pi version of docs#is_open_prod_iff is the main roadblock. I have started looking at how to prove it but in fact, I already have trouble coming up with a suitable statement...

[Eric Wieser]

And for that you'll likely want a pi version of docs#filter.has_basis.prod_nhds

[Eric Wieser]

My guess of the statement was

lemma is_open_pi_iff {ι : Type*} {α : ι → Type*} [Π i, topological_space (α i)]
  {s : set (Π i, α i)} :
  is_open s ↔
  (∀ f, f ∈ s →
    ∃ (u : Π i, set (α i)), (∀ i, is_open (u i) ∧ f i ∈ u i) ∧ set.univ.pi u ⊆ s) :=

[Eric Wieser]

I have no idea if you need a finiteness assumption somewhere, but that would presumably become obvious when proving it

[Xavier Roblot]

Thanks, I'll start with that and see how far I can get.

[Eric Wieser]

Eric Wieser said:

I would have thought you can also get it without much work by induction on fin n

You could still take this shortcut, but arguably filling in all the missing API as we're discussing is better for mathlib

[Xavier Roblot]

Yeah, I'll see how difficult it is to do it right, but maybe I'll end up just doing an induction in the end :sweat_smile:

[Eric Wieser]

Here's another statement you might need (also likely missing assumptions)

theorem filter.has_basis.pi {ι : Type*} {α : ι → Type*} {l : Π i, filter (α i)}
  {ι' : ι → Type u_3} {p : Π i, ι' i → Prop} {s : Π i, ι' i → set (α i)}
  (hla : Π i, (l i).has_basis (p i) (s i)) :
(filter.pi l).has_basis (λ (i : Π i, ι' i), ∀ j, p _ (i j))
  (λ (i : Π i, ι' i), set.univ.pi (λ j, s _ (i j))) :=

[Kevin Buzzard]

Just to remark that Haar measures exist for locally compact groups and an arbitrary product of locally compact groups is not in general locally compact.

[Kevin Buzzard]

The way to proceed in the infinite case is to choose a compact subgroup of all but finitely many of the groups and then take the restricted product (which AFAIK we don't have in mathlib) and this is again locally compact (cf the adeles, which I suspect Xavier knows well)

[Eric Wieser]

Right, my comments are naive translations of the product versions, which are likely untrue without some combination of fintype and nonempty. Another nearly true statement we're missing might be

[Xavier Roblot]

Hum, there is already docs#filter.has_basis_pi so that's already something.

[Eric Wieser]

Huh, I missed that completely due to the . vs _ naming

[Eric Wieser]

It might be nice to have a specialization of that for finite ι

[Jireh Loreaux]

Eric, I get around that searching problem by omitting both . and _ when searching

[Xavier Roblot]

#18390 and !4#2110 for the corresponding mathlib4 PR

[Eric Wieser]

Note that there is no need to do a manual mathlib4 PR; just make a blank PR and forward-port with the output of mathport once the mathlib3 PR is merged