How to prove a ball is measurable

Stream: Carleson

[Jeremy Tan]

I'm trying to prove the following in HardyLittlewood.lean and I have come across this very hard reduced goal:

protected theorem MeasureTheory.AEStronglyMeasurable.maximalFunction {p : ℝ}
    {u : X → E} (hu : AEStronglyMeasurable u μ) (h𝓑 : 𝓑.Countable) :
    AEStronglyMeasurable (maximalFunction μ 𝓑 c r p u) μ := by
  refine (aemeasurable_biSup 𝓑 h𝓑 fun i mi ↦ aemeasurable_const.indicator ?_).pow
    aemeasurable_const |>.aestronglyMeasurable
  -- ⊢ MeasurableSet (ball (c i) (r i))
  sorry

This would seem like measurableSet_ball solves it, but that requires OpensMeasurableSpace X which is not provided in the given instances for X, and furthermore I'm not using hu at all. Where am I supposed to use hu?

[Jeremy Tan]

For reference:

variable {X E : Type*} {A : ℝ≥0} [MetricSpace X] [MeasurableSpace X]
  {μ : Measure X} [μ.IsDoubling A] [NormedAddCommGroup E]
  [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E]
  {f : X → E} {x : X} {ι : Type*} {𝓑 : Set ι} {c : ι → X} {r : ι → ℝ}
  [IsFiniteMeasureOnCompacts μ] [ProperSpace X] [Nonempty X] [μ.IsOpenPosMeasure]
  -- feel free to assume `A ≥ 16` or similar

/-- The Hardy-Littlewood maximal function w.r.t. a collection of balls 𝓑.
M_{𝓑, p} in the blueprint. -/
def maximalFunction (μ : Measure X) (𝓑 : Set ι) (c : ι → X) (r : ι → ℝ)
  (p : ℝ) (u : X → E) (x : X) : ℝ≥0∞ :=
  (⨆ i ∈ 𝓑, (ball (c i) (r i)).indicator (x := x)
  fun _ ↦ ⨍⁻ y in ball (c i) (r i), ‖u y‖₊ ^ p ∂μ) ^ p⁻¹

[Jireh Loreaux]

BorelSpace E implies OpensMeasuable E via docs#BorelSpace.opensMeasurable

[Jireh Loreaux]

so you can use measurableSet_ball

[Jeremy Tan]

No, I have ball (c i) (r i) : Set X, not Set E

[Jireh Loreaux]

oops sorry

[Jireh Loreaux]

(deleted)

[Yury G. Kudryashov]

My guess: the informal proof missed this assumption.

[Yury G. Kudryashov]

Or do you actually work with non-Borel σ-algebras in this project?

[Jeremy Tan]

X is a so-called doubling metric measure space:
"A doubling metric measure space $(X,\mu,\rho,a)$ is a complete and locally compact metric space equipped with a $\sigma$-finite non-zero Radon–Borel measure $\mu$ that satisfies the doubling condition that..."

[Jeremy Tan]

@Yury G. Kudryashov the DMMS described above is the most general kind of space we work with in this project, see blueprint

[Floris van Doorn]

If the formalization is missing BorelSpace then this is an oversight. I will add it.

[Jeremy Tan]

Do we lose any significant generality by adding BorelSpace X though?

[Jeremy Tan]

Surely there must be a way to use hu to prove the statement without BorelSpace X!

[Yaël Dillies]

No, there can't be. If you aren't in a Borel space and make u be a constant function, then you can get the indicator function of a non-measurable set

[Jeremy Tan]

I never learned point-set topology, let alone measure theory, in university…

[Yaël Dillies]

It's okay :smile: just pointing out that indeed you need BorelSpace X (or at least half of it, namely OpensMeasurableSpace X)

[Jireh Loreaux]

Of course, I think the hypothesis BorelSpace X should just be added, but at the same time, I was having quite a hard time coming up with an example of a doubling measure, positive on open sets and finite on compact sets which is not Borel. I guess maybe one idea could be to start with such a Borel measure, then throw out certain measure zero sets from the σ-algebra, but still maintain that it is indeed a σ-algebra? Seems a rather complicated counterexample to construct.

[Floris van Doorn]

I've added the hypothesis BorelSpace X now. After we finish the proof we can see if it's easy to weaken it to OpensMeasurableSpace.