LeanPool.SardMoreira.LebesgueDensity #
theorem
MeasureTheory.Measure.AbsolutelyContinuous.comap
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
{μ ν : Measure β}
(h : μ.AbsolutelyContinuous ν)
(f : α → β)
(hfν : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) ν)
:
(comap f μ).AbsolutelyContinuous (comap f ν)
theorem
MeasurableEmbedding.quasiMeasurePreserving_iff_comap
{α : Type u_1}
{β : Type u_2}
{x✝ : MeasurableSpace α}
{x✝¹ : MeasurableSpace β}
{e : α → β}
(he : MeasurableEmbedding e)
{μ : MeasureTheory.Measure α}
{ν : MeasureTheory.Measure β}
:
theorem
MeasureTheory.Measure.AbsolutelyContinuous.exists_pos_forall_lt_imp_lt_of_isFiniteMeasure
{α : Type u_1}
{x✝ : MeasurableSpace α}
{μ ν : Measure α}
[IsFiniteMeasure μ]
[μ.HaveLebesgueDecomposition ν]
(h : μ.AbsolutelyContinuous ν)
{ε : ENNReal}
(hε : ε ≠ 0)
:
If a finite measure μ is absolutely continuous with respect to a σ-finite measure ν,
then μ s → 0 as ν s → 0. More precisely, for any ε ≠ 0 there exists δ > 0
such that all sets of ν measure less than δ have a μ measure less than ε.
theorem
exists_absolutelyContinuous_forall_pos_exists_lt_gt :
∃ (μ : MeasureTheory.Measure ℝ) (ν : MeasureTheory.Measure ℝ),
μ.AbsolutelyContinuous ν ∧ ∀ (C δ : NNReal), δ ≠ 0 → ∃ (s : Set ℝ), MeasurableSet s ∧ ν s < ↑δ ∧ μ s > ↑C
The previous lemma is not true unless we assume that ν is a finite measure.
Indeed, for ν = volume on ℝ, μ = ν.withDensity (Real.nnabs ·),
we can choose s = Set.Icc a (a + δ / 2) for a large a,
and get an arbitriraly large value of μ s.
theorem
MeasureTheory.Measure.AbsolutelyContinuous.exists_pos_forall_subset_lt_imp_lt
{α : Type u_1}
{x✝ : MeasurableSpace α}
{μ ν : Measure α}
[SigmaFinite ν]
(h : μ.AbsolutelyContinuous ν)
{t : Set α}
(ht : μ t ≠ ⊤)
{ε : ENNReal}
(hε : ε ≠ 0)
:
If a finite measure μ is absolutely continuous with respect to a σ-finite measure ν,
then μ s → 0 as ν s → 0. More precisely, for any ε ≠ 0 there exists δ > 0
such that all sets of ν measure less than δ have a μ measure less than ε.
theorem
MeasureTheory.Measure.AbsolutelyContinuous.exists_pos_forall_lt_imp_lt
{α : Type u_1}
{x✝ : MeasurableSpace α}
{μ ν : Measure α}
[SFinite μ]
[SigmaFinite ν]
(h : μ.AbsolutelyContinuous ν)
{ε : ENNReal}
(hε : ε ≠ 0)
(hrnDeriv : ∃ (C : NNReal), μ.rnDeriv ν ≤ᶠ[μ.cofinite] fun (x : α) => ↑C)
:
theorem
exists_pos_forall_measure_le_toSphere_ge_le
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{x✝ : MeasurableSpace E}
[BorelSpace E]
(μ : MeasureTheory.Measure E)
[μ.IsAddHaarMeasure]
{ε : ENNReal}
(hε : ε ≠ 0)
:
theorem
exists_pos_forall_measure_le_exists_mem_sphere_dist_lt_volume_smul_mem_lt
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{x✝ : MeasurableSpace E}
[BorelSpace E]
(μ : MeasureTheory.Measure E)
[μ.IsAddHaarMeasure]
{ε : NNReal}
(hε : ε ≠ 0)
:
theorem
exists_pos_forall_measure_le_exists_mem_sphere_dist_lt_volume_lineMap_mem_lt
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{ε : NNReal}
(hε : ε ≠ 0)
:
∃ (δ : NNReal),
0 < δ ∧ ∀ {x : MeasurableSpace E} [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (r : ℝ),
r ≠ 0 →
∀ (a : E) (s : Set E),
μ s ≤ ↑δ * μ (Metric.ball a r) →
∀ x ∈ Metric.sphere a r,
∃ y ∈ Metric.sphere a r,
dist y x < ↑ε * r ∧ MeasureTheory.volume {t : ℝ | 0 ≤ t ∧ (AffineMap.lineMap a y) t ∈ s} < ↑ε
theorem
Measurable.measure_apply
{α : Type u_1}
{β : Type u_2}
[MeasurableSpace α]
[MeasurableSpace β]
(μ : MeasureTheory.Measure α)
[MeasureTheory.SFinite μ]
(s : β → Set α)
(hs : MeasurableSet {p : α × β | p.1 ∈ s p.2})
:
Measurable fun (b : β) => μ (s b)
If $s_b$ is a family of sets such that $\{(a, b) \mid a \in s_b\}$ is a measurable set, then for any s-finite measure $\mu$, the function $b \mapsto \mu(s_b)$ is measurable.
This is a version of measurable_measure_prod_mk_right.
theorem
eventually_measure_closedBall_lt_top
{X : Type u_1}
[PseudoMetricSpace X]
[MeasurableSpace X]
(μ : MeasureTheory.Measure X)
[MeasureTheory.IsLocallyFiniteMeasure μ]
(x : X)
:
theorem
eventually_forall_le_continuousWithinAt_Ici_measure_closedBall
{X : Type u_1}
[PseudoMetricSpace X]
[MeasurableSpace X]
[OpensMeasurableSpace X]
(μ : MeasureTheory.Measure X)
[MeasureTheory.IsLocallyFiniteMeasure μ]
(x : X)
:
∀ᶠ (r : ℝ) in nhds 0, ∀ ν ≤ μ, ContinuousWithinAt (fun (x_1 : ℝ) => ν (Metric.closedBall x x_1)) (Set.Ici r) r
theorem
eventually_continuousWithinAt_Ici_measure_inter_closedBall_div
{X : Type u_1}
[PseudoMetricSpace X]
[MeasurableSpace X]
[OpensMeasurableSpace X]
{μ : MeasureTheory.Measure X}
[MeasureTheory.IsLocallyFiniteMeasure μ]
(x : X)
{s : Set X}
(hs : MeasureTheory.NullMeasurableSet s μ)
:
∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), ContinuousWithinAt (fun (r : ℝ) => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (Set.Ici r) r
theorem
IsDenseEmbedding.tendsto_nhdsWithin_preimage_iff_of_eventually_continuousWithinAt
{X : Type u_1}
{Y : Type u_2}
{Z : Type u_3}
[TopologicalSpace X]
[TopologicalSpace Y]
[TopologicalSpace Z]
[RegularSpace Z]
{e : X → Y}
{s : Set Y}
{x : X}
{z : Z}
{f : Y → Z}
{U : Y → Set Y}
[∀ (y : Y), (nhdsWithin y (U y)).NeBot]
(he : IsDenseEmbedding e)
(hs : IsOpen s)
(hU : ∀ (y : Y), IsOpen (U y))
(hcont : ∀ᶠ (y : Y) in nhdsWithin (e x) s, ContinuousWithinAt f (U y) y)
:
Filter.Tendsto (f ∘ e) (nhdsWithin x (e ⁻¹' s)) (nhds z) ↔ Filter.Tendsto f (nhdsWithin (e x) s) (nhds z)
Let e : X → Y be a dense topological embedding, let Z be a regular space.
For each y : Y, let U y be an open set such that y ∈ closure (U y).
Let s be an open set, let x : X be a point.
Suppose that f : Y → Z is continuous within U y at all y ∈ s close to e x.
Then f (e x') tends to z as x' tends to x, e x' ∈ s,
if and only if f y tends to z as y ∈ s tends to e x.
If X = ℚ, Y = ℝ, and e = Rat.cast,
then this lemma can be used to restate convergence of a function defined on real numbers
in terms of convergence of a function on rational numbers,
which is more convenient for measure theory, because there are only countably many rational numbers.
theorem
tendsto_measure_inter_closedBall_div_iff_rat
{X : Type u_1}
[PseudoMetricSpace X]
[MeasurableSpace X]
[OpensMeasurableSpace X]
{μ : MeasureTheory.Measure X}
[MeasureTheory.IsLocallyFiniteMeasure μ]
{x : X}
{a : ENNReal}
{s : Set X}
(hs : MeasureTheory.NullMeasurableSet s μ)
:
Filter.Tendsto (fun (r : ℝ) => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0))
(nhds a) ↔ Filter.Tendsto (fun (r : ℚ) => μ (s ∩ Metric.closedBall x ↑r) / μ (Metric.closedBall x ↑r)) (nhdsWithin 0 (Set.Ioi 0))
(nhds a)
theorem
MeasurableSet.setOf_tendsto_measure_sectl_inter_closedBall_div
{X : Type u_1}
[PseudoMetricSpace X]
[SecondCountableTopology X]
[MeasurableSpace X]
[OpensMeasurableSpace X]
{α : Type u_2}
[MeasurableSpace α]
(μ : MeasureTheory.Measure X)
[MeasureTheory.IsLocallyFiniteMeasure μ]
[MeasureTheory.SFinite μ]
{s : Set (X × α)}
(hs : MeasurableSet s)
{f : X × α → ENNReal}
(hf : Measurable f)
:
MeasurableSet
{p : X × α | Filter.Tendsto
(fun (r : ℝ) => μ ((fun (x : X) => (x, p.2)) ⁻¹' s ∩ Metric.closedBall p.1 r) / μ (Metric.closedBall p.1 r))
(nhdsWithin 0 (Set.Ioi 0)) (nhds (f p))}
theorem
MeasurableSet.setOf_tendsto_measure_inter_closedBall_div
{X : Type u_1}
[PseudoMetricSpace X]
[SecondCountableTopology X]
[MeasurableSpace X]
[OpensMeasurableSpace X]
(μ : MeasureTheory.Measure X)
[MeasureTheory.IsLocallyFiniteMeasure μ]
[MeasureTheory.SFinite μ]
{s : Set X}
(hs : MeasurableSet s)
{f : X → ENNReal}
(hf : Measurable f)
:
MeasurableSet
{x : X | Filter.Tendsto (fun (r : ℝ) => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0))
(nhds (f x))}
theorem
Besicovitch.ae_tendsto_measure_sectl_inter_closedBall_div
{X : Type u_1}
[MetricSpace X]
[SecondCountableTopology X]
[HasBesicovitchCovering X]
[MeasurableSpace X]
[BorelSpace X]
{α : Type u_2}
[MeasurableSpace α]
(μ : MeasureTheory.Measure X)
[MeasureTheory.IsLocallyFiniteMeasure μ]
[MeasureTheory.SFinite μ]
(ν : MeasureTheory.Measure α)
[MeasureTheory.SFinite ν]
{s : Set (X × α)}
(hs : MeasurableSet s)
:
∀ᵐ (p : X × α) ∂μ.prod ν, Filter.Tendsto
(fun (r : ℝ) => μ ((fun (x : X) => (x, p.2)) ⁻¹' s ∩ Metric.closedBall p.1 r) / μ (Metric.closedBall p.1 r))
(nhdsWithin 0 (Set.Ioi 0)) (nhds (s.indicator 1 p))
Parametrized version of ae_tendsto_measure_inter_div_of_measurableSet.
theorem
Besicovitch.ae_tendsto_measure_sectr_inter_closedBall_div
{X : Type u_1}
[MetricSpace X]
[SecondCountableTopology X]
[HasBesicovitchCovering X]
[MeasurableSpace X]
[BorelSpace X]
{α : Type u_2}
[MeasurableSpace α]
(μ : MeasureTheory.Measure α)
(ν : MeasureTheory.Measure X)
[MeasureTheory.IsLocallyFiniteMeasure ν]
[MeasureTheory.SFinite ν]
{s : Set (α × X)}
(hs : MeasurableSet s)
:
∀ᵐ (p : α × X) ∂μ.prod ν, Filter.Tendsto
(fun (r : ℝ) => ν ((fun (x : X) => (p.1, x)) ⁻¹' s ∩ Metric.closedBall p.2 r) / ν (Metric.closedBall p.2 r))
(nhdsWithin 0 (Set.Ioi 0)) (nhds (s.indicator 1 p))
Parametrized version of ae_tendsto_measure_inter_div_of_measurableSet.