LeanPool.SardMoreira.OuterMeasureDeriv #
A measure satisfies ClosedBallCoveringMeasure if every set has an ε-good
covering by countably many closed balls with radii drawn from arbitrary sets
of admissible radii. This holds for Besicovitch-covering measures and for
uniformly locally doubling measures.
- exists_closedBall_covering_tsum_measure_le {ε : ENNReal} (hε : ε ≠ 0) (f : α → Set ℝ) (s : Set α) (hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty) : ∃ (t : Set α) (r : α → ℝ), t.Countable ∧ t ⊆ s ∧ (∀ x ∈ t, r x ∈ f x) ∧ s ⊆ ⋃ x ∈ t, Metric.closedBall x (r x) ∧ ∑' (x : ↑t), μ (Metric.closedBall (↑x) (r ↑x)) ≤ μ s + ε
The defining property of
ClosedBallCoveringMeasure: for any positive error toleranceεand any functionfassigning each point an arbitrarily-small admissible radius, the setsadmits a countable cover by closed balls centred inswith admissible radii whose total measure exceedsμ sby at mostε.
Instances
Suppose that ν (s ∩ closedBall x r) = O(μ (closedBall x r)) at all points of a set s
and ν (s ∩ closedBall x r) = o(μ (closedBall x r)) at a.e. points of the set.
Then ν s = 0.
The actual statement can't use Asymptotics.IsBigO and Asymptotics.IsLittleO,
because the LHS and the RHS are in ℝ≥0∞, not ℝ.
Note that we do not assume measurability of s or C.
Let f : α → β be a map from a space with Besicovitch property to any space.
Let μ be a σ-finite outer regular measure on α, let ν be an outer measure on β,
let s be a set in the domain, let C be a constant such that μ s ≠ 0 or C ≠ ∞.
Suppose that for each x ∈ s and a positive ε,
for a set of positive r that accumulates to zero,
we have ν (f '' (s ∩ Metric.closedBall x r)) ≤ (C + ε) * μ (Metric.closedBall x r).
Then ν (f '' s) ≤ C * μ s.
Briefly speaking, this means that ν (f '' s) ≤ C * μ s
provided that a similar estimate holds for sufficiently small ball around each point x ∈ s.
See also Besicovitch.measure_image_le_mul.
Let f : α → β be a map from a space with Besicovitch property to any space.
Let μ be a σ-finite outer regular measure on α, let ν be a measure on β,
let s be a set in the domain, let C be a constant such that μ s ≠ 0 or C ≠ ∞.
Suppose that for each x ∈ s and a positive ε,
for a set of positive r that accumulates to zero,
we have ν (f '' (s ∩ Metric.closedBall x r)) ≤ (C + ε) * μ (Metric.closedBall x r).
Then ν (f '' s) ≤ C * μ s.
Briefly speaking, this means that ν (f '' s) ≤ C * μ s
provided that a similar estimate holds for sufficiently small ball around each point x ∈ s.
See also Besicovitch.outerMeasure_image_le_mul.