# Everywhere positive sets in measure spaces #

A set `s`

in a topological space with a measure `μ`

is *everywhere positive* (also called
*self-supporting*) if any neighborhood `n`

of any point of `s`

satisfies `μ (s ∩ n) > 0`

.

## Main definitions and results #

`μ.IsEverywherePos s`

registers that, for any point in`s`

, all its neighborhoods have positive measure inside`s`

.`μ.everywherePosSubset s`

is the subset of`s`

made of those points all of whose neighborhoods have positive measure inside`s`

.`everywherePosSubset_ae_eq`

shows that`s`

and`μ.everywherePosSubset s`

coincide almost everywhere if`μ`

is inner regular and`s`

is measurable.`isEverywherePos_everywherePosSubset`

shows that`μ.everywherePosSubset s`

satisfies the property`μ.IsEverywherePos`

if`μ`

is inner regular and`s`

is measurable.

The latter two statements have also versions when `μ`

is inner regular for finite measure sets,
assuming additionally that `s`

has finite measure.

`IsEverywherePos.IsGδ`

proves that an everywhere positive compact closed set is a Gδ set, in a topological group with a left-invariant measure. This is a nontrivial statement, used crucially in the study of the uniqueness of Haar measures.`innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top`

: for a Haar measure, any finite measure set can be approximated from inside by level sets of continuous compactly supported functions. This property is also known as completion-regularity of Haar measures.

A set `s`

is *everywhere positive* (also called *self-supporting*) with respect to a
measure `μ`

if it has positive measure around each of its points, i.e., if all neighborhoods `n`

of points of `s`

satisfy `μ (s ∩ n) > 0`

.

## Equations

- μ.IsEverywherePos s = ∀ x ∈ s, ∀ n ∈ nhdsWithin x s, 0 < μ n

## Instances For

- The everywhere positive subset of a set is the subset made of those points all of whose neighborhoods have positive measure inside the set.

## Equations

- μ.everywherePosSubset s = {x : α | x ∈ s ∧ ∀ n ∈ nhdsWithin x s, 0 < μ n}

## Instances For

The everywhere positive subset of a set is obtained by removing an open set.

Any compact set contained in `s \ μ.everywherePosSubset s`

has zero measure.

In a space with an inner regular measure, any measurable set coincides almost everywhere with its everywhere positive subset.

In a space with an inner regular measure for finite measure sets, any measurable set of finite measure coincides almost everywhere with its everywhere positive subset.

In a space with an inner regular measure, the everywhere positive subset of a measurable set
is itself everywhere positive. This is not obvious as `μ.everywherePosSubset s`

is defined as
the points whose neighborhoods intersect `s`

along positive measure subsets, but this does not
say they also intersect `μ.everywherePosSubset s`

along positive measure subsets.

In a space with an inner regular measure for finite measure sets, the everywhere positive subset
of a measurable set of finite measure is itself everywhere positive. This is not obvious as
`μ.everywherePosSubset s`

is defined as the points whose neighborhoods intersect `s`

along positive
measure subsets, but this does not say they also intersect `μ.everywherePosSubset s`

along positive
measure subsets.

If two measures coincide locally, then a set which is everywhere positive for the former is also everywhere positive for the latter.

If two measures coincide locally, then a set is everywhere positive for the former iff it is everywhere positive for the latter.

An open set is everywhere positive for a measure which is positive on open sets.

If a compact closed set is everywhere positive with respect to a left-invariant measure on a topological group, then it is a Gδ set. This is nontrivial, as there is no second-countability or metrizability assumption in the statement, so a general compact closed set has no reason to be a countable intersection of open sets.

**Halmos' theorem: Haar measure is completion regular.** More precisely, any finite measure
set can be approximated from inside by a level set of a continuous function with compact support.