English
If f is measurable, then the set of a for which IsRatStieltjesPoint f a holds is measurable.
Русский
Если f измерима, то множество {a | IsRatStieltjesPoint f a} измеримо.
LaTeX
$$$\\text{MeasurableSet}\\{a \\mid IsRatStieltjesPoint f a\\}$$$
Lean4
theorem measurableSet_isRatStieltjesPoint [MeasurableSpace α] (hf : Measurable f) :
MeasurableSet {a | IsRatStieltjesPoint f a} :=
by
have h1 : MeasurableSet {a | Monotone (f a)} :=
by
change MeasurableSet {a | ∀ q r (_ : q ≤ r), f a q ≤ f a r}
simp_rw [Set.setOf_forall]
refine MeasurableSet.iInter (fun q ↦ ?_)
refine MeasurableSet.iInter (fun r ↦ ?_)
refine MeasurableSet.iInter (fun _ ↦ ?_)
exact measurableSet_le hf.eval hf.eval
have h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)} := measurableSet_tendsto _ (fun q ↦ hf.eval)
have h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)} := measurableSet_tendsto _ (fun q ↦ hf.eval)
have h4 : MeasurableSet {a | ∀ t : ℚ, ⨅ r : Ioi t, f a r = f a t} :=
by
rw [Set.setOf_forall]
refine MeasurableSet.iInter (fun q ↦ ?_)
exact measurableSet_eq_fun (.iInf fun _ ↦ hf.eval) hf.eval
suffices
{a | IsRatStieltjesPoint f a} =
({a | Monotone (f a)} ∩ {a | Tendsto (f a) atTop (𝓝 1)} ∩ {a | Tendsto (f a) atBot (𝓝 0)} ∩
{a | ∀ t : ℚ, ⨅ r : Ioi t, f a r = f a t})
by
rw [this]
exact (((h1.inter h2).inter h3).inter h4)
ext a
simp only [mem_setOf_eq, mem_inter_iff]
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· exact ⟨⟨⟨h.mono, h.tendsto_atTop_one⟩, h.tendsto_atBot_zero⟩, h.iInf_rat_gt_eq⟩
· exact ⟨h.1.1.1, h.1.1.2, h.1.2, h.2⟩
