English
If μ is inner regular with respect to p on measurable sets, then its restriction to A is inner regular with the same p on measurable sets.
Русский
Если μ имеет внутреннюю регулярность по p на измеримых множествах, то ограничение μ на A сохраняет ту же регулярность по p на измеримых множествах.
LaTeX
$$$InnerRegularWRT(μ; p; MeasurableSet) \Rightarrow InnerRegularWRT(μ|A; p; MeasurableSet).$$$
Lean4
/-- If `μ` is inner regular for measurable finite measure sets with respect to some class of sets,
then its restriction to any set is also inner regular for measurable finite measure sets, with
respect to the same class of sets. -/
theorem restrict (h : InnerRegularWRT μ p (fun s ↦ MeasurableSet s ∧ μ s ≠ ∞)) (A : Set α) :
InnerRegularWRT (μ.restrict A) p (fun s ↦ MeasurableSet s ∧ μ.restrict A s ≠ ∞) :=
by
rintro s ⟨s_meas, hs⟩ r hr
rw [restrict_apply s_meas] at hs
obtain ⟨K, K_subs, pK, rK⟩ : ∃ K, K ⊆ (toMeasurable μ (s ∩ A)) ∩ s ∧ p K ∧ r < μ K :=
by
have : r < μ ((toMeasurable μ (s ∩ A)) ∩ s) := by
apply hr.trans_le
rw [restrict_apply s_meas]
exact measure_mono <| subset_inter (subset_toMeasurable μ (s ∩ A)) inter_subset_left
refine h ⟨(measurableSet_toMeasurable _ _).inter s_meas, ?_⟩ _ this
apply (lt_of_le_of_lt _ hs.lt_top).ne
rw [← measure_toMeasurable (s ∩ A)]
exact measure_mono inter_subset_left
refine ⟨K, K_subs.trans inter_subset_right, pK, ?_⟩
calc
r < μ K := rK
_ = μ.restrict (toMeasurable μ (s ∩ A)) K :=
by
rw [restrict_apply' (measurableSet_toMeasurable μ (s ∩ A))]
congr
apply (inter_eq_left.2 ?_).symm
exact K_subs.trans inter_subset_left
_ = μ.restrict (s ∩ A) K := by rwa [restrict_toMeasurable]
_ ≤ μ.restrict A K := Measure.le_iff'.1 (restrict_mono inter_subset_right le_rfl) K
