English
If C is a semiring, m is AddContent, and m is finite on C, then the outer measure built from m is Carathéodory-measurable on s for each s ∈ C.
Русский
Если C — полуребро, m — содержимое AddContent, и m ограничено на C, то внешняя мера, построенная из m, является Карратоодориева измеримой на любой s ∈ C.
LaTeX
$$$\\text{If } hs: s \\in C,\\quad (\\operatorname{OuterMeasure.ofFunction} m addContent\\_empty).IsCaratheodory\\; s.$$$
Lean4
theorem isCaratheodory_ofFunction_of_mem (hC : IsSetSemiring C) (m : AddContent C) (m_top : ∀ s ∉ C, m s = ∞)
(hs : s ∈ C) : (OuterMeasure.ofFunction m addContent_empty).IsCaratheodory s :=
by
rw [OuterMeasure.isCaratheodory_iff_le']
intro t
conv_rhs => rw [OuterMeasure.ofFunction_eq_iInf_mem _ _ m_top]
refine le_iInf fun f ↦ le_iInf fun hf ↦ le_iInf fun hf_subset ↦ ?_
let A : ℕ → Finset (Set α) := fun i ↦ hC.disjointOfDiff (hf i) (hC.inter_mem _ (hf i) _ hs)
have h_diff_eq_sUnion i : f i \ s = ⋃₀ A i := by simp [A, IsSetSemiring.sUnion_disjointOfDiff]
classical
have h_m_eq i : m (f i) = m (f i ∩ s) + ∑ u ∈ A i, m u :=
eq_add_disjointOfDiff_of_subset hC (hC.inter_mem (f i) (hf i) s hs) (hf i) inter_subset_left
simp_rw [h_m_eq]
rw [ENNReal.tsum_add]
refine add_le_add ?_ ?_
· refine iInf_le_of_le (fun i ↦ f i ∩ s) <| iInf_le_of_le ?_ le_rfl
rw [← iUnion_inter]
exact Set.inter_subset_inter_left _ hf_subset
· apply
le_trans <|
(OuterMeasure.ofFunction m addContent_empty).mono <| (iUnion_diff s f) ▸ diff_subset_diff_left hf_subset
simp only [OuterMeasure.measureOf_eq_coe, A]
apply le_trans <| measure_iUnion_le (μ := OuterMeasure.ofFunction m addContent_empty) (fun i ↦ f i \ s)
apply ENNReal.tsum_le_tsum
intro i
simp_rw [sUnion_eq_biUnion] at h_diff_eq_sUnion
rw [h_diff_eq_sUnion]
obtain h6 := MeasureTheory.measure_biUnion_finset_le (μ := OuterMeasure.ofFunction m addContent_empty) (A i) id
simp only [id_eq] at h6
exact le_trans h6 <| Finset.sum_le_sum <| fun b _ ↦ OuterMeasure.ofFunction_le b
