measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'_of_measurableSet

English

Auxiliary lemma used to deduce μ s = ∞ when s lies in the complement of σFiniteSetWRT' and ν s ≠ 0.

Русский

Вспомогательная лемма: при s ⊆ (μ.sigmaFiniteSetWRT'(ν))^c и ν(s) ≠ 0 получаем μ(s) = ∞.

LaTeX

$$$$\text{If } hs\colon MeasurableSet(s),\; hs\subseteq (\mu\sigmaFiniteSetWRT'(\nu))^c,\; \nu(s)\neq 0 \Rightarrow \mu(s)=\infty.$$$$

Lean4

/-- Auxiliary lemma for `measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'`. -/
theorem measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'_of_measurableSet [IsFiniteMeasure ν] (hs : MeasurableSet s)
    (hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ) (hνs : ν s ≠ 0) : μ s = ∞ :=
  by
  suffices ¬SigmaFinite (μ.restrict s) by
    by_contra h
    have h_lt_top : Fact (μ s < ∞) := ⟨Ne.lt_top h⟩
    exact this inferInstance
  intro hsσ
  have h_lt : ν (μ.sigmaFiniteSetWRT' ν) < ν (μ.sigmaFiniteSetWRT' ν ∪ s) :=
    by
    rw [measure_union _ hs]
    · exact ENNReal.lt_add_right (measure_ne_top _ _) hνs
    · exact disjoint_compl_right.mono_right hs_subset
  have h_le : ν (μ.sigmaFiniteSetWRT' ν ∪ s) ≤ ν (μ.sigmaFiniteSetWRT' ν) :=
    by
    conv_rhs => rw [measure_sigmaFiniteSetWRT']
    refine (le_iSup (f := fun (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν ∪ s))) ↦ _) ?_).trans ?_
    · have := sigmaFinite_restrict_sigmaFiniteSetWRT' μ ν
      infer_instance
    ·
      exact
        le_iSup₂ (f := fun s _ ↦ ⨆ (_ : SigmaFinite (μ.restrict _)), ν s) (μ.sigmaFiniteSetWRT' ν ∪ s)
          (measurableSet_sigmaFiniteSetWRT'.union hs)
  exact h_lt.not_ge h_le

Похожие утверждения