Lebesgue density theorem, parametrized version

Stream: maths

[Yury G. Kudryashov]

I need the following fact.

Let E and F be finite dimensional real normed spaces.
Let μ and ν be additive Haar measures on these spaces.
Let s : Set (E × F) be a measurable set (in the original informal text, s is a closed set).
Then for (μ.prod ν)-ae (x, y) ∈ s, x is a μ-density point of {z | (z, y) ∈ s}.

The original informal text deduces by applying Lebesgue density theorem to each {z | (z, y) ∈ s}. AFAICT, we also need to show that the set {(x, y) | x is a μ-density pt of {z | (z, y) ∈ s}} is a measurable set. What are the right assumptions for this statement?

[Yury G. Kudryashov]

Clearly, "finite dimensional normed spaces + Haar measures" is too strong.

[Yury G. Kudryashov]

I think that I can drop all assumptions on F (possibly, except for ν being an s-finite measure). Does it make sense to weaken assumptions on E?

[Yury G. Kudryashov]

I can show that the ratio of the measures is a measurable function, thus the set of points where it tends to 1 along positive rational numbers is a measurable set (w/o assuming that μ is a Haar measure), but I need some assumptions to switch to the limit along positive real numbers.

[Sébastien Gouëzel]

Isn't the set of density points the set of points where the ratio $\mu(s \cap B(x, r)) / \mu(B(x, r))$ tends to $1$ along rational $r$, and the same for closed balls? If so, everyting is expressed countably, so everything is measurable.

[Sébastien Gouëzel]

Thinking back about this, there is even no need to take both open and closed balls. If you define density points using open balls, you can use that $\mu(B(x,t))$ is the limit as $r$ tends to $t$ from below of $\mu(B(x, r))$ to deduce that convergence along the rationals implies convergence along the reals. And if you use closed balls, note that $\mu(\overline{B}(x,t))$ is the limit as $r$ tends to $t$ from above of $\mu(\overline{B}(x, r))$ to conclude in the same way.

[Sébastien Gouëzel]

This only works at points where the measure is locally finite, but if the measure is not locally finite then we don't have a density point as the ratio $\mu(s \cap B(x, r)) / \mu(B(x,r))$ is always zero, so convergence along the rationals iff along the reals is also true.

[Yury G. Kudryashov]

I tried to do it after midnight, and was approximating from the wrong side, thanks!