strongly_measurable.is_lub

Stream: Is there code for X?

[Alex Kontorovich]

We have docs#measurable.is_lub which shows that the pointwise least-upper-bound function of a countable family of measurable functions is itself measurable. Do you happen to know off the top of your head whether the same statement with measurable replaced by strongly_measurable is even true? (Same for ae_measurable replaced with ae_strongly_measurable? And measurable_supr, measurable.ennreal_tsum, etc.) Thanks! (CC @Sebastien Gouezel @Yury G. Kudryashov )

[Yury G. Kudryashov]

I think that the answer is "yes". I can try to prove it tonight.

[Yury G. Kudryashov]

What assumptions on the codomain work for you?

[Yury G. Kudryashov]

For measurable.ennreal_tsum, you can use docs#strongly_measurable_of_tendsto

[Yury G. Kudryashov]

(should work in more general cases too)

[Alex Kontorovich]

I suppose something like this? Thanks!

theorem strongly_measurable.is_lub {α : Type*} {δ : Type*} [topological_space α]
  [measurable_space α] [borel_space α] [measurable_space δ] [linear_order α]
  [order_topology α] [topological_space.second_countable_topology α]
  {ι : Sort*} [countable ι] {f : ι → δ → α} {g : δ → α}
  (hf : ∀ (i : ι), strongly_measurable (f i))
  (hg : ∀ (b : δ), is_lub {a : α | ∃ (i : ι), f i b = a} (g b)) :
strongly_measurable g := sorry

[Yury G. Kudryashov]

Here is a proof:

open measure_theory set filter topological_space
open_locale filter topological_space

variables {ι α β : Type*} [measurable_space α] [topological_space β]

instance finset.is_empty_subtype_nonempty [is_empty ι] :
  is_empty {s : finset ι // s.nonempty} :=
⟨λ ⟨s, hs⟩, hs.ne_empty s.eq_empty_of_is_empty⟩

instance finset.nonempty_subtype_nonempty [h : nonempty ι] :
  nonempty {s : finset ι // s.nonempty} :=
h.map $ λ i, ⟨{i}, finset.singleton_nonempty i⟩

instance finset.semilattice_sup_subtype_nonempty [decidable_eq ι] :
  semilattice_sup {s : finset ι // s.nonempty} :=
subtype.semilattice_sup $ λ s t hs ht, hs.mono $ finset.subset_union_left _ _

lemma is_lub.finset_sup' {ι α : Type*} [semilattice_sup α] {f : ι → α} {a : α}
  (ha : is_lub (range f) a) :
  is_lub (range $ λ s : {s : finset ι // s.nonempty}, s.1.sup' s.2 f) a :=
⟨forall_range_iff.2 $ λ s, finset.sup'_le _ _ $ λ b hb, ha.1 $ mem_range_self _,
  λ b hb, ha.2 $ forall_range_iff.2 $ λ i,
    hb ⟨⟨{i}, finset.singleton_nonempty _⟩, finset.sup'_singleton _⟩⟩

lemma is_lub.finset_sup {ι α : Type*} [semilattice_sup α] [order_bot α] {f : ι → α} {a : α}
  (ha : is_lub (range f) a) :
  is_lub (range $ λ s : finset ι, s.sup f) a :=
⟨forall_range_iff.2 $ λ s, finset.sup_le $ λ b hb, ha.1 $ mem_range_self _,
  λ b hb, ha.2 $ forall_range_iff.2 $ λ i, hb ⟨{i}, finset.sup_singleton⟩⟩

lemma tendsto_finset_sup'_is_lub {ι α : Type*} [semilattice_sup α] [topological_space α]
  [Sup_convergence_class α] {f : ι → α} {a : α} (ha : is_lub (range f) a) :
  tendsto (λ s : {s : finset ι // s.nonempty}, s.1.sup' s.2 f) at_top (𝓝 a) :=
tendsto_at_top_is_lub (λ s₁ s₂ h, finset.sup'_le _ _ $ λ i hi, finset.le_sup' _ $ h hi)
  ha.finset_sup'

lemma finset.strongly_measurable_sup' {ι α β : Type*} [measurable_space α] [topological_space β]
  [semilattice_sup β] [has_continuous_sup β] {f : ι → α → β} {s : finset ι} (hs : s.nonempty)
  (hf : ∀ i ∈ s, strongly_measurable (f i)) : strongly_measurable (s.sup' hs f) :=
finset.sup'_induction _ _ (λ _ h₁ _ h₂, h₁.sup h₂) hf

lemma finset.strongly_measurable_sup'_pw {ι α β : Type*} [measurable_space α] [topological_space β]
  [semilattice_sup β] [has_continuous_sup β] {f : ι → α → β} {s : finset ι} (hs : s.nonempty)
  (hf : ∀ i ∈ s, strongly_measurable (f i)) : strongly_measurable (λ x, s.sup' hs (λ i, f i x)) :=
by simpa only [← finset.sup'_apply] using finset.strongly_measurable_sup' hs hf

lemma strongly_measurable_lub [countable ι] [semilattice_sup β] [metrizable_space β]
  [Sup_convergence_class β] [has_continuous_sup β] {f : ι → α → β} {g : α → β}
  (hf : ∀ i, strongly_measurable (f i)) (hg : ∀ x, is_lub (range $ λ i, f i x) (g x)) :
  strongly_measurable g :=
begin
  letI := classical.dec_eq ι,
  casesI is_empty_or_nonempty ι,
  { simp only [range_eq_empty, is_lub_empty_iff] at hg,
    exact strongly_measurable_const' (λ x y, (hg x _).antisymm (hg y _)) },
  have := λ x, tendsto_finset_sup'_is_lub (hg x),
  refine strongly_measurable_of_tendsto _ (λ s, _) (tendsto_pi_nhds.2 this),
  exact finset.strongly_measurable_sup'_pw _ (λ i _, hf i)
end

UPD: new proof works for more βs.

[Yury G. Kudryashov]

If you'll PR this, then please add order-dual versions.

[Alex Kontorovich]

Thanks again @Yury G. Kudryashov! Heather @Heather Macbeth and I just posted the PR #18380.

[Yury G. Kudryashov]

CI fails (finset.is_empty_subtype_nonempty is too early). Also, you'll have to forward-port it...