Measurability of supremum of continuous/measurable functions

Stream: Is there code for X?

[Jeremy Tan]

This is low-priority, but do we have the result in https://math.stackexchange.com/a/4685735/357390 that shows that the supremum of a measurable function over any set (even uncountable) is measurable as long as the function is also continuous over the set of the supremum?

[Jeremy Tan]

(Can somebody move this to #Is there code for X? I sent this from my mobile phone web browser and the UI is somewhat buggy)

[Notification Bot]

This topic was moved here from #general > Measurability of supremum of continuous/measurable functions by Bhavik Mehta.

[Jeremy Tan]

I've got a first version working:

import Mathlib.MeasureTheory.Constructions.BorelSpace.Order

open Set TopologicalSpace ENNReal

variable {ι X : Type*} [PseudoEMetricSpace ι] [SeparableSpace ι] [MeasurableSpace X]

/-- Given `T : Set ι` over a separable pseudometric space `ι`, let `f : ι → X → ℝ≥0∞` be
* measurable in `x` for all `t ∈ T`
* **continuous** on `T` for all `x`

Then the supremum of `f` over `T` is measurable. -/
lemma measurable_biSup_of_continuousOn {T : Set ι} {f : ι → X → ℝ≥0∞}
    (mf : ∀ t ∈ T, Measurable (f t)) (cf : ∀ x, ContinuousOn (f · x) T) :
    Measurable (⨆ t ∈ T, f t) := by
  refine measurable_of_Ioi fun c ↦ ?_
  obtain ⟨J, sJ, cJ, dJ⟩ := (IsSeparable.of_separableSpace T).exists_countable_dense_subset
  suffices (⨆ t ∈ T, f t) ⁻¹' Ioi c = ⋃ j ∈ J, {x | c < f j x} by
    rw [this]; refine MeasurableSet.biUnion cJ fun j mj ↦ ?_
    exact measurableSet_lt measurable_const (mf j (sJ mj))
  ext x
  simp_rw [mem_preimage, mem_Ioi, iSup_apply, lt_biSup_iff, mem_iUnion₂, mem_setOf_eq, exists_prop]
  constructor <;> rintro ⟨t, mt, ht⟩
  · simp_rw [continuousOn_iff] at cf
    obtain ⟨u, ou, mu, hu⟩ := cf _ _ mt _ isOpen_Ioi ht
    specialize dJ mt; rw [mem_closure_iff] at dJ
    specialize dJ u ou mu; obtain ⟨j, mj⟩ := dJ; use j, mj.2
    simpa using (inter_subset_inter subset_rfl sJ).trans hu mj
  · use t, sJ mt

[Jeremy Tan]

Now I want to generalise it to the following, but I don't know how to prove xxx. How do I prove xxx?

import Mathlib.MeasureTheory.Constructions.BorelSpace.Order

open Set TopologicalSpace ENNReal

variable {ι X : Type*} [PseudoEMetricSpace ι] [SeparableSpace ι] [MeasurableSpace X]

lemma xxx {T J U : Set ι} (sJ : J ⊆ T) (dJ : T ⊆ closure J) (sU : U ⊆ T) :
    U ⊆ closure (U ∩ J) := by
  sorry

/-- Given `T : Set ι` over a separable pseudometric space `ι`, let `f : ι → X → ℝ≥0∞` be
* measurable in `x` for all `t ∈ T`
* **continuous** on `T` for all `x`

Then the supremum of `f` over `T` is measurable. -/
lemma measurable_biSup_of_continuousOn
    {T : Set ι} {f : ι → X → ℝ≥0∞} (mf : ∀ t ∈ T, Measurable (f t))
    (cf : ∀ x, ∀ t ∈ T, ∃ U ⊆ T, t ∈ U ∧ ContinuousWithinAt (f · x) U t) :
    Measurable (⨆ t ∈ T, f t) := by
  refine measurable_of_Ioi fun c ↦ ?_
  obtain ⟨J, sJ, cJ, dJ⟩ := (IsSeparable.of_separableSpace T).exists_countable_dense_subset
  suffices (⨆ t ∈ T, f t) ⁻¹' Ioi c = ⋃ j ∈ J, {x | c < f j x} by
    rw [this]; refine MeasurableSet.biUnion cJ fun j mj ↦ ?_
    exact measurableSet_lt measurable_const (mf j (sJ mj))
  ext x
  simp_rw [mem_preimage, mem_Ioi, iSup_apply, lt_biSup_iff, mem_iUnion₂, mem_setOf_eq, exists_prop]
  constructor <;> rintro ⟨t, mt, ht⟩
  · specialize cf x _ mt; obtain ⟨U, sU, mU, hU⟩ := cf
    have key : U ⊆ closure (U ∩ J) := by
      exact xxx sJ dJ sU
    rw [ContinuousWithinAt, tendsto_nhds] at hU
    specialize hU _ isOpen_Ioi ht; rw [mem_nhdsWithin] at hU
    obtain ⟨V, oV, mV, hV⟩ := hU
    specialize key mU; rw [mem_closure_iff] at key
    specialize key V oV mV; obtain ⟨j, mj⟩ := key; use j, mj.2.2
    simpa using hV ⟨mj.1, mj.2.1⟩
  · use t, sJ mt

[Jeremy Tan]

In my use case for Carleson T = {R : ℝ × ℝ | (2 ^ n)⁻¹ < R.1 ∧ R.1 < R.2 ∧ R.2 < 2 ^ n} and U = {R : ℝ × ℝ | t.1 ≤ R.1 ∧ R.1 < R.2 ∧ R.2 ≤ t.2}, so xxx should hold

[Aaron Liu]

It's false and I have a counterexample

[Aaron Liu]

For xxx, I mean

[Jeremy Tan]

Then what assumptions should I have to prove the generalisation?

[Aaron Liu]

I don't know

[Aaron Liu]

My counterexample is let T be the rationals, let J be the dyadics, and let U be the singleton {1 / 3}

[Lua Viana Reis]

Perhaps ask that U is a subset of its limit points?

[Lua Viana Reis]

No, this also doesn't work for xxx by the same example of Aaron, but having U be the rationals that are not dyadic.

[Jeremy Tan]

What about the specific instance I mentioned above?

[Lua Viana Reis]

I'm not sure what t is in your example, but can't you just assume that U is open?

[Lua Viana Reis]

by having it be strict t.1 < R.1 ∧ R.1 < R.2 ∧ R.2 < t.2

[Jeremy Tan]

Lua Viana Reis said:

I'm not sure what t is in your example, but can't you just assume that U is open?

t is some point in T. And no, I can't assume U is open, because I also need t ∈ U

[Jeremy Tan]

(The specific PR is fpvandoorn/carleson#429)

[Lua Viana Reis]

But @Jeremy Tan, I'm a bit confused, if it's continuous in your U(t) for all t in T, then it's continuous in T, no?

[Lua Viana Reis]

Oh, sorry, the continuity point itself is changing with t, this is probably not true

[Jeremy Tan]

The blueprint in the Carleson project has these lemmas:

lemma rightContinuous_carlesonOperatorIntegrand (mf : Measurable f) :
    ContinuousWithinAt (carlesonOperatorIntegrand K θ · R₂ f x) (Ici R₁) R₁ := by
  sorry

lemma leftContinuous_carlesonOperatorIntegrand (mf : Measurable f) :
    ContinuousWithinAt (carlesonOperatorIntegrand K θ R₁ · f x) (Iic R₂) R₂ := by
  sorry

where carlesonOperatorIntegrand is an integral over an annulus whose radii are R₁, R₂.

With these lemmas alone all I can prove is that with T,U as stated above, the function f := carlesonOperatorIntegrand K θ R.1 R.2 f x is ContinuousWithinAt over U. I'm starting to think that in fact the function is bidirectionally continuous, which would allow me to use the ContinuousOn version directly… but I've probably digressed too much. (Pinging @Floris van Doorn as the maintainer of Carleson)

[Jeremy Tan]

I'm now trying explicitly setting J to be the set of rational-number pairs in T

[Lua Viana Reis]

Jeremy Tan said:

With these lemmas alone all I can prove is that with T,U as stated above, the function f := carlesonOperatorIntegrand K θ R.1 R.2 f x is ContinuousWithinAt over U.

how can you prove that it's continuous at t on the whole U(t) without extra assumptions? a priori it's only continuous on the union of two segments extending from t, no? (the lemmas only show the limit along those two curves exist)

[Lua Viana Reis]

which would make the original question harder, because now there isn't a countable set that is dense in every U(t)

[Jeremy Tan]

Jeremy Tan said:

I'm now trying explicitly setting J to be the set of rational-number pairs in T

I've proven the original thing I wanted measurable_lcoConvergent in this way, reducing it to two Theorem 3.0.1 sublemmas. It has been pushed to fpvandoorn/carleson#429