[Merged by Bors] - feat: better uniqueness results for the Haar measure#9909
[Merged by Bors] - feat: better uniqueness results for the Haar measure#9909
Conversation
| @[to_additive "Given two left-invariant measures which are finite on compacts, | ||
| `addHaarScalarFactor μ' μ` is a scalar such that `∫ f dμ' = (addHaarScalarFactor μ' μ) ∫ f dμ` for | ||
| any compactly supported continuous function `f`."] | ||
| noncomputable def haarScalarFactor (μ' μ : Measure G) [IsFiniteMeasureOnCompacts μ] |
There was a problem hiding this comment.
why noncomputable? It should be possible to prove that the factor does not depend on the choice of the chosen functions…
There was a problem hiding this comment.
noncomputable means that I'm not providing an algorithm by which Lean's kernel could evaluate the number. Since real numbers are already noncomputable by definition, there is no way this function could be computable.
| lemma exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport | ||
| (μ' μ : Measure G) [IsFiniteMeasureOnCompacts μ] [IsFiniteMeasureOnCompacts μ'] | ||
| [IsMulLeftInvariant μ] [IsMulLeftInvariant μ'] [IsOpenPosMeasure μ] : | ||
| lemma exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport (μ' μ : Measure G) |
There was a problem hiding this comment.
There is something bizarre here (for me, at least) that mu and mu' have different kind of hypotheses.
Can one compare two left invariant measures without knowing that one of them is positive on open subsets and the other one is finite on compacts?
There was a problem hiding this comment.
If mu is the zero measure, you can not write mu' = c mu for some c. On the other hand, it's not a problem if mu' is the zero measure. That's why there is an assumption that mu is positive on open sets while there is no such assumption for mu', here and below.
There was a problem hiding this comment.
I have expanded the docstring of haarScalarFactor to insist on this point.
|
|
||
| Assume for simplicity that all measures are normalized, so that the scalar factors are all `1`. | ||
| First, from the fact that `μ` and `μ'` integrate in the same way compactly supported functions, | ||
| they give the same measure to compact "zero sets", i.e., sets of the form `f⁻¹ {1}` |
There was a problem hiding this comment.
maybe change "zero sets" to "level sets" (and 'f-1{1}' to 'f-1{a} for a neq 0').
There was a problem hiding this comment.
Zero set is unfortunately a standard terminology in this corner of the litterature. That's why I am putting it in the docstring, to make sure that people looking for this can locate the relevant lemmas.
|
|
||
| /-- Two left invariant measures give the same mass to level sets of continuous compactly supported | ||
| functions, up to the scalar `haarScalarFactor μ' μ`. | ||
| Superseded by `measure_isMulInvariant_eq_smul_of_isCompact_closure`, which works for any set with |
There was a problem hiding this comment.
If it's superseded, should it be kept? or should the proof be just an application of the more general result?
There was a problem hiding this comment.
All the lemmas whose docstring mentions "superseded" are intermediate steps in the proof of the main theorem below, measure_isMulInvariant_eq_smul_of_isCompact_closure. So I can't remove them. The role of this docstring is to explain that the user shouldn't use them because there is a better version available below.
There was a problem hiding this comment.
I have expanded the docstrings to clarify that these are intermediate lemmas.
jcommelin
left a comment
There was a problem hiding this comment.
This all looks very very solid! Great!
bors merge
We show that two Haar measures give the same measure to sets with compact closure, and to open sets, without any regularity assumptions. This is based on McQuillan's answer on https://mathoverflow.net/questions/456670.
|
Build failed (retrying...): |
We show that two Haar measures give the same measure to sets with compact closure, and to open sets, without any regularity assumptions. This is based on McQuillan's answer on https://mathoverflow.net/questions/456670.
|
Build failed (retrying...): |
We show that two Haar measures give the same measure to sets with compact closure, and to open sets, without any regularity assumptions. This is based on McQuillan's answer on https://mathoverflow.net/questions/456670.
|
Pull request successfully merged into master. Build succeeded: |
We show that two Haar measures give the same measure to sets with compact closure, and to open sets, without any regularity assumptions. This is based on McQuillan's answer on https://mathoverflow.net/questions/456670.
We show that two Haar measures give the same measure to sets with compact closure, and to open sets, without any regularity assumptions. This is based on McQuillan's answer on https://mathoverflow.net/questions/456670.
We show that two Haar measures give the same measure to sets with compact closure, and to open sets, without any regularity assumptions. This is based on McQuillan's answer on https://mathoverflow.net/questions/456670.
I will of course split this into several PRs. Here are the first ones: