feat(MeasureTheory/BorelSpace): add measurable_iSup_of_lowerSemicontinuous

[pitmonticone]

Add measurable_biSup_of_continuousOn: the supremum of a family of measurable functions parameterized by a separable pseudometric space is measurable, provided the family is continuous on the parameter set.

Upstreamed from the Carleson project.

Co-authored-by: Jeremy Tan Jie Rui reddeloostw@gmail.com

---

[github-actions]

PR summary f51efbe0b8

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ measurable_iSup_of_lowerSemicontinuous

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[CoolRmal]

The pseudometric space structure is only used to ensure that a subset of a separable space is separable, which then allows you to extract a countable dense sequence through TopologicalSpace.IsSeparable.exists_countable_dense_subset, so I believe this theorem should be proved for iSup (with the [SeparableSpace ι] assumption) instead of biSup, and then you can convertbiSup into iSup using theorems like iSup_subtype'' when you apply this result in the Carleson project. Actually I created the following more general version while I was working on Doob's maximal inequality (see measurable_iSup_of_rightContinuous).

import Mathlib.MeasureTheory.Constructions.BorelSpace.Order

open MeasureTheory TopologicalSpace Set Filter

lemma measurable_biSup_of_continuousOn [CompleteLinearOrder β] [OrderTopology β]
    [SecondCountableTopology β] {ι : Type*} [TopologicalSpace ι] [SeparableSpace ι]
    {f : ι → δ → β} (mf : ∀ t, Measurable (f t)) (cf : ∀ x, LowerSemicontinuous (f · x)) :
    Measurable (⨆ i, f i) := by
  refine measurable_of_Ioi fun c ↦ ?_
  obtain ⟨J, cJ, dJ⟩ := TopologicalSpace.exists_countable_dense ι
  suffices (⨆ i, f i) ⁻¹' Ioi c = ⋃ j ∈ J, {x | c < f j x} by
    rw [this]
    exact MeasurableSet.biUnion cJ fun j mj ↦ (measurableSet_lt measurable_const (mf j))
  ext x
  push _ ∈ _
  simp_rw [iSup_apply, lt_iSup_iff]
  constructor
  · intro ⟨i, hi⟩
    simp only [lowerSemicontinuous_iff] at cf
    obtain ⟨v, hv⟩ := eventually_iff_exists_mem.1 (cf x i c hi)
    have hj := dJ.inter_nhds_nonempty hv.1
    exact ⟨hj.some, mem_of_mem_inter_left hj.some_mem, hv.2 _ (mem_of_mem_inter_right hj.some_mem)⟩
  · intro ⟨i, h, hi⟩
    use i

The situation in Doob's maximal inequality is actually a bit different: I need right continuity there and I also need to take into account the set of points isolated from the right, so I assume that index set ι carries a second countable order topology. Not sure whether there is a more general framework that can unify the version above and the version I proved in Doob's maximal inequality.

This theorem should also be true for functions taking values in a conditionally complete linear order, but the proof is definitely going to be more complicated.

[pitmonticone]

Thanks @CoolRmal! Applied your generalized version with iSup, LowerSemicontinuous, and CompleteLinearOrder.

[grunweg]

Can you fix the build failure, please?

[grunweg]

As a general comment, @pitmonticone: I see you force-pushing changes after you got some non-trivial review comments. That makes is harder to reviewers to see what you changed. Going forward, can you add further changes as separate comments, please? Thanks!

[grunweg]

(I will hopefully have time to review these PRs, but possibly only in a week.)

[pitmonticone]

Yep, my bad. I've done a few of those by mistake. Already fixed in the latest commits. Sorry.