English
If s has density one at x with respect to closed balls, then for any measurable t with μ t ≠ 0 and μ t ≠ ∞, the density of s in {x} + r t relative to {x} + r t tends to 1 as r → 0+.
Русский
Если в точке x множество s имеет плотность единицу по отношению к замкнутым шарам, то для любого измеримого t с μ t ≠ 0 и μ t ≠ ∞ плотность s в {x} + r t по отношению к {x} + r t стремится к 1 при r → 0+.
LaTeX
$$$\displaystyle \lim_{r \to 0^+} \frac{\mu\bigl(s \cap (\{x\} + r\, t)\bigr)}{\mu\bigl(\{x\} + r\, t\bigr)} = 1$$$
Lean4
/-- Consider a point `x` at which a set `s` has density one, with respect to closed balls (i.e.,
a Lebesgue density point of `s`). Then `s` has also density one at `x` with respect to any
measurable set `t`: the proportion of points in `s` belonging to a rescaled copy `{x} + r • t`
of `t` tends to one as `r` tends to zero. -/
theorem tendsto_addHaar_inter_smul_one_of_density_one (s : Set E) (x : E)
(h : Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 1)) (t : Set E)
(ht : MeasurableSet t) (h't : μ t ≠ 0) (h''t : μ t ≠ ∞) :
Tendsto (fun r : ℝ => μ (s ∩ ({ x } + r • t)) / μ ({ x } + r • t)) (𝓝[>] 0) (𝓝 1) :=
by
have : Tendsto (fun r : ℝ => μ (toMeasurable μ s ∩ ({ x } + r • t)) / μ ({ x } + r • t)) (𝓝[>] 0) (𝓝 1) :=
by
apply tendsto_addHaar_inter_smul_one_of_density_one_aux μ _ (measurableSet_toMeasurable _ _) _ _ t ht h't h''t
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' h tendsto_const_nhds
· refine Eventually.of_forall fun r ↦ ?_
gcongr
apply subset_toMeasurable
· filter_upwards [self_mem_nhdsWithin]
rintro r -
apply ENNReal.div_le_of_le_mul
rw [one_mul]
exact measure_mono inter_subset_right
refine this.congr fun r => ?_
congr 1
apply measure_toMeasurable_inter_of_sFinite
simp only [image_add_left, singleton_add]
apply (continuous_add_left (-x)).measurable (ht.const_smul₀ r)
