English
If s has density one at x with respect to closed balls, then for every measurable t with μ t ≠ 0, there exists a neighborhood of 0 in (0, ∞) such that for all small positive r in that neighborhood, the intersection s ∩ ({x} + r t) is nonempty.
Русский
Если в точке x множество s имеет плотность единицу по отношению к замкнутым шарам, то для каждого измеримого t с μ t ≠ 0 существует окрестность 0 в (0, ∞), такая что для всех достаточно маленьких положительных r из этой окрестности пересечение s ∩ ({x} + r t) непусто.
LaTeX
$$$\\displaystyle \\exists \\text{ neighbourhood }(0,\\varepsilon) \\text{ such that } \\forall r \in (0,\\varepsilon),\\ (s \\cap (\\{x\\} + r\\, t)).\\text{Nonempty}$$$
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` intersects the rescaled copies `{x} + r • t` of a given
set `t` with positive measure, for any small enough `r`. -/
theorem eventually_nonempty_inter_smul_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) : ∀ᶠ r in 𝓝[>] (0 : ℝ), (s ∩ ({ x } + r • t)).Nonempty :=
by
obtain ⟨t', t'_meas, t't, t'pos, t'top⟩ : ∃ t', MeasurableSet t' ∧ t' ⊆ t ∧ 0 < μ t' ∧ μ t' < ⊤ :=
exists_subset_measure_lt_top ht h't.bot_lt
filter_upwards [(tendsto_order.1
(tendsto_addHaar_inter_smul_one_of_density_one μ s x h t' t'_meas t'pos.ne' t'top.ne)).1
0 zero_lt_one]
intro r hr
have : μ (s ∩ ({ x } + r • t')) ≠ 0 := fun h' => by simp only [ENNReal.not_lt_zero, ENNReal.zero_div, h'] at hr
have : (s ∩ ({ x } + r • t')).Nonempty := nonempty_of_measure_ne_zero this
apply this.mono (inter_subset_inter Subset.rfl _)
exact add_subset_add Subset.rfl (smul_set_mono t't)
