PR summary f51efbe0b8

Import changes for modified files

No significant changes to the import graph

Declarations diff

+ measurable_iSup_of_lowerSemicontinuous

## 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.

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

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.

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

Can you fix the build failure, please?

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!

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

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