English
For every real c, the ray Ioi(c) is measurable with respect to the Carathéodory σ-algebra induced by the Stieltjes outer measure.
Русский
Для любого вещественного c множество Ioi(c) измеримо относительно каратайодорова σ-алгебры, индуцированной внешней мерой Стилетджеса.
LaTeX
$$MeasurableSet_{f.outer.caratheodory}(Ioi(c))$$
Lean4
theorem outer_trim : f.outer.trim = f.outer :=
by
refine le_antisymm (fun s => ?_) (OuterMeasure.le_trim _)
rw [OuterMeasure.trim_eq_iInf]
refine le_iInf fun t => le_iInf fun ht => ENNReal.le_of_forall_pos_le_add fun ε ε0 h => ?_
rcases ENNReal.exists_pos_sum_of_countable (ENNReal.coe_pos.2 ε0).ne' ℕ with ⟨ε', ε'0, hε⟩
grw [← hε]
rw [← ENNReal.tsum_add]
choose g hg using
show ∀ i, ∃ s, t i ⊆ s ∧ MeasurableSet s ∧ f.outer s ≤ f.length (t i) + ofReal (ε' i)
by
intro i
have hl := ENNReal.lt_add_right ((ENNReal.le_tsum i).trans_lt h).ne (ENNReal.coe_pos.2 (ε'0 i)).ne'
conv at hl =>
lhs
rw [length]
simp only [iInf_lt_iff] at hl
rcases hl with ⟨a, b, h₁, h₂⟩
rw [← f.outer_Ioc] at h₂
exact ⟨_, h₁, measurableSet_Ioc, le_of_lt <| by simpa using h₂⟩
simp only [ofReal_coe_nnreal] at hg
apply iInf_le_of_le (iUnion g) _
apply iInf_le_of_le (ht.trans <| iUnion_mono fun i => (hg i).1) _
apply iInf_le_of_le (MeasurableSet.iUnion fun i => (hg i).2.1) _
exact le_trans (measure_iUnion_le _) (ENNReal.tsum_le_tsum fun i => (hg i).2.2)
