English
If f_i are measurable for a countable index set ι, then the set of parameters b for which the family {f_i(b)} is bounded above is a measurable set.
Русский
Если f_i измеримы для счетного индекса i, то множество параметров b, для которых семейство {f_i(b)} ограничено сверху, является измеримым.
LaTeX
$$((∀ i, Measurable (f i)) → MeasurableSet {b | BddAbove (range (fun i ↦ f i b))})$$
Lean4
theorem measurableSet_bddAbove_range {ι} [Countable ι] {f : ι → δ → α} (hf : ∀ i, Measurable (f i)) :
MeasurableSet {b | BddAbove (range (fun i ↦ f i b))} :=
by
rcases isEmpty_or_nonempty α with hα | hα
· have : ∀ b, range (fun i ↦ f i b) = ∅ := fun b ↦ eq_empty_of_isEmpty _
simp [this]
have A : ∀ (i : ι) (c : α), MeasurableSet {x | f i x ≤ c} :=
by
intro i c
exact measurableSet_le (hf i) measurable_const
have B : ∀ (c : α), MeasurableSet {x | ∀ i, f i x ≤ c} :=
by
intro c
rw [setOf_forall]
exact MeasurableSet.iInter (fun i ↦ A i c)
obtain ⟨u, hu⟩ : ∃ (u : ℕ → α), Tendsto u atTop atTop := exists_seq_tendsto (atTop : Filter α)
have : {b | BddAbove (range (fun i ↦ f i b))} = {x | ∃ n, ∀ i, f i x ≤ u n} :=
by
apply Subset.antisymm
· rintro x ⟨c, hc⟩
obtain ⟨n, hn⟩ : ∃ n, c ≤ u n := (tendsto_atTop.1 hu c).exists
exact ⟨n, fun i ↦ (hc ((mem_range_self i))).trans hn⟩
· rintro x ⟨n, hn⟩
refine ⟨u n, ?_⟩
rintro - ⟨i, rfl⟩
exact hn i
rw [this, setOf_exists]
exact MeasurableSet.iUnion (fun n ↦ B (u n))
