[Merged by Bors] - feat: everywhere positive sets for a measure#10139
[Merged by Bors] - feat: everywhere positive sets for a measure#10139
Conversation
| /-- If two measures coincide locally, then a set which is everywhere positive for the former is | ||
| also everywhere positive for the latter. -/ | ||
| lemma IsEverywherePos.of_forall_exists_nhds_eq (hs : IsEverywherePos μ s) | ||
| (h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u) : IsEverywherePos ν s := by |
There was a problem hiding this comment.
Does this concept of two measures coinciding locally occur enough that we should have a definition + API for it?
There was a problem hiding this comment.
I don't think so, because we have just one application for now. I will reconsider when we have a second application :-)
There was a problem hiding this comment.
Deleted comment that measures form a sheaf — of course, that requires some countability assumption unless one mostly cares about measures of sigma-compact sets. On the other hand, I wonder whether the sheaf-theoretical version of measures would be. What are the objects that are locally defined by measures? What does it mean that two measures coincide locally?
There was a problem hiding this comment.
It really depends on the sigma-algebra you consider. On the sigma algebra of Baire sets (generated by compact G-delta sets), measures form indeed a sheaf. On the Borel sigma-algebra, they don't (an example I like is: let \mu be zero on sets which are contained in a countable union of balls of radius 1, and +\infty otherwise. On a non-separable Hilbert space, this is a measure which is locally zero, with trivial support, but still nonzero).
|
✌️ sgouezel can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Oliver Nash <github@olivernash.org>
|
bors r+ |
A set `s` is everywhere positive with respect to a measure `mu` if, for every point in `s`, all its neighborhoods inside `s` have positive measure. We create a new file about this notion. The main result of the file is Halmos theorem (1950): the Haar measure on a locally compact group is completion-regular, i.e., finite-measure sets can be approximated from inside by level sets of compactly supported continuous functions. (its proof uses subtle properties of everywhere positive sets, although this is not apparent in the statement).
|
Build failed (retrying...): |
A set `s` is everywhere positive with respect to a measure `mu` if, for every point in `s`, all its neighborhoods inside `s` have positive measure. We create a new file about this notion. The main result of the file is Halmos theorem (1950): the Haar measure on a locally compact group is completion-regular, i.e., finite-measure sets can be approximated from inside by level sets of compactly supported continuous functions. (its proof uses subtle properties of everywhere positive sets, although this is not apparent in the statement).
|
Build failed (retrying...): |
A set `s` is everywhere positive with respect to a measure `mu` if, for every point in `s`, all its neighborhoods inside `s` have positive measure. We create a new file about this notion. The main result of the file is Halmos theorem (1950): the Haar measure on a locally compact group is completion-regular, i.e., finite-measure sets can be approximated from inside by level sets of compactly supported continuous functions. (its proof uses subtle properties of everywhere positive sets, although this is not apparent in the statement).
|
Build failed: |
|
bors r+ |
A set `s` is everywhere positive with respect to a measure `mu` if, for every point in `s`, all its neighborhoods inside `s` have positive measure. We create a new file about this notion. The main result of the file is Halmos theorem (1950): the Haar measure on a locally compact group is completion-regular, i.e., finite-measure sets can be approximated from inside by level sets of compactly supported continuous functions. (its proof uses subtle properties of everywhere positive sets, although this is not apparent in the statement).
|
Pull request successfully merged into master. Build succeeded: |
|
|
||
| variable {α : Type*} [TopologicalSpace α] [MeasurableSpace α] | ||
|
|
||
| /-- A set `s` is *everywhere positive* (also called *self-supporting*) with respect to a |
There was a problem hiding this comment.
Isn't there a notion of support for a measure? This seems to be equivalent to the fact that the support of the restriction of the measure to s is equal to s.
There was a problem hiding this comment.
(By reading the file further down, I understand that you're defining that, without defining the support of the measure in general)
There was a problem hiding this comment.
Yes, I could have phrased it in terms of support, by requiring that the support of the restriction of the measure to s contains s.
| rw [hu] | ||
| exact hs.diff u_open.measurableSet | ||
|
|
||
| protected lemma _root_.IsClosed.everywherePosSubset (hs : IsClosed s) : |
There was a problem hiding this comment.
The support is closed, that's a general property, so the support will be closed in s, for the induced topology, whatever s is closed or not.
There was a problem hiding this comment.
Yes, that's what the previous lemma says.
|
|
||
| open Pointwise | ||
|
|
||
| /-- If a compact closed set is everywhere positive with respect to a left-invariant measure on a |
There was a problem hiding this comment.
Probably, this does not require that the mesure is left invariant, but much less : for example, if translating the measure multiplies it by a >0 function…
There was a problem hiding this comment.
Indeed, the proof just requires that the measure is quasi-invariant by left-multiplication (i.e., left-multiplication respects zero measure sets), which by the way only depends on the measure class and not the measure itself. If I'm not mistaken, in each measure class which is quasi-invariant by left multiplication, there is a measure which is exactly invariant (maybe one needs some sigma-finiteness here to apply Radon-Nikodym), so the current statement does not really lose much generality -- we'll generalize if/when we need it!
A set `s` is everywhere positive with respect to a measure `mu` if, for every point in `s`, all its neighborhoods inside `s` have positive measure. We create a new file about this notion. The main result of the file is Halmos theorem (1950): the Haar measure on a locally compact group is completion-regular, i.e., finite-measure sets can be approximated from inside by level sets of compactly supported continuous functions. (its proof uses subtle properties of everywhere positive sets, although this is not apparent in the statement).
A set `s` is everywhere positive with respect to a measure `mu` if, for every point in `s`, all its neighborhoods inside `s` have positive measure. We create a new file about this notion. The main result of the file is Halmos theorem (1950): the Haar measure on a locally compact group is completion-regular, i.e., finite-measure sets can be approximated from inside by level sets of compactly supported continuous functions. (its proof uses subtle properties of everywhere positive sets, although this is not apparent in the statement).
A set
sis everywhere positive with respect to a measuremuif, for every point ins, all its neighborhoods insideshave positive measure. We create a new file about this notion.The main result of the file is Halmos theorem (1950): the Haar measure on a locally compact group is completion-regular, i.e., finite-measure sets can be approximated from inside by level sets of compactly supported continuous functions. (its proof uses subtle properties of everywhere positive sets, although this is not apparent in the statement).