exists_positive_of_not_mutuallySingular

English

If two finite measures μ and ν are not mutually singular, there exists ε>0 and a measurable set E such that ν(E)>0 and for every measurable A, ε·ν(A∩E) ≤ μ(A∩E).

Русский

Если две конечные меры μ и ν не являются взаимно сингулярными, то существует ε>0 и измеримое множество E такое, что ν(E)>0 и для любого измеримого множества A выполняется неравенство ε·ν(A∩E) ≤ μ(A∩E).

LaTeX

$$$$ \\exists \\varepsilon > 0, \\; \\exists E \\text{ measurable}, \\; 0 < \\nu(E) \\; \\land\\; \\forall A \\ (\nMeasurableSet A \\rightarrow \\varepsilon \\cdot \\nu(A \\cap E) \\le \\mu(A \\cap E)\\n) $$$$

Lean4

/-- If two finite measures `μ` and `ν` are not mutually singular, there exists some `ε > 0` and
a measurable set `E`, such that `ν(E) > 0` and `E` is positive with respect to `μ - εν`.

This lemma is useful for the Lebesgue decomposition theorem. -/
theorem exists_positive_of_not_mutuallySingular (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    (h : ¬μ ⟂ₘ ν) :
    ∃ ε : ℝ≥0, 0 < ε ∧ ∃ E : Set α, MeasurableSet E ∧ 0 < ν E ∧ ∀ A, MeasurableSet A → ε * ν (A ∩ E) ≤ μ (A ∩ E) := by
  -- for all `n : ℕ`, obtain the Hahn decomposition for `μ - (1 / n) ν`

  have h_decomp (n : ℕ) :
    ∃ s : Set α,
      MeasurableSet s ∧
        (∀ t, MeasurableSet t → ((1 / (n + 1) : ℝ≥0) • ν) (t ∩ s) ≤ μ (t ∩ s)) ∧
          (∀ t, MeasurableSet t → μ (t ∩ sᶜ) ≤ ((1 / (n + 1) : ℝ≥0) • ν) (t ∩ sᶜ)) :=
    by
    obtain ⟨s, hs, hs_le, hs_ge⟩ := hahn_decomposition μ ((1 / (n + 1) : ℝ≥0) • ν)
    refine ⟨s, hs, fun t ht ↦ ?_, fun t ht ↦ ?_⟩
    · exact hs_le (t ∩ s) (ht.inter hs) inter_subset_right
    · exact hs_ge (t ∩ sᶜ) (ht.inter hs.compl) inter_subset_right
  choose f hf₁ hf₂ hf₃ using h_decomp
  let A := ⋂ n, (f n)ᶜ
  have hAmeas : MeasurableSet A := MeasurableSet.iInter fun n ↦ (hf₁ n).compl
  have hA₂ (n : ℕ) (t : Set α) (ht : MeasurableSet t) : μ (t ∩ A) ≤ ((1 / (n + 1) : ℝ≥0) • ν) (t ∩ A) :=
    by
    specialize hf₃ n (t ∩ A) (ht.inter hAmeas)
    have : A ∩ (f n)ᶜ = A := inter_eq_left.mpr (iInter_subset _ n)
    rwa [inter_assoc, this] at hf₃
  have hA₃ (n : ℕ) : μ A ≤ (1 / (n + 1) : ℝ≥0) * ν A := by simpa using hA₂ n univ .univ
  have hμ : μ A = 0 := by
    lift μ A to ℝ≥0 using measure_ne_top _ _ with μA
    lift ν A to ℝ≥0 using measure_ne_top _ _ with νA
    rw [ENNReal.coe_eq_zero]
    by_cases hb : 0 < νA
    · suffices ∀ b, 0 < b → μA ≤ b by
        by_contra h
        have h' := this (μA / 2) (half_pos (zero_lt_iff.2 h))
        rw [← @Classical.not_not (μA ≤ μA / 2)] at h'
        exact h' (not_le.2 (NNReal.half_lt_self h))
      intro c hc
      have : ∃ n : ℕ, 1 / (n + 1 : ℝ) < c * (νA : ℝ)⁻¹ :=
        by
        refine exists_nat_one_div_lt ?_
        positivity
      rcases this with ⟨n, hn⟩
      have hb₁ : (0 : ℝ) < (νA : ℝ)⁻¹ := by rw [_root_.inv_pos]; exact hb
      have h' : 1 / (↑n + 1) * νA < c :=
        by
        rw [← NNReal.coe_lt_coe, ← mul_lt_mul_iff_left₀ hb₁, NNReal.coe_mul, mul_assoc, ← NNReal.coe_inv, ←
          NNReal.coe_mul, mul_inv_cancel₀, ← NNReal.coe_mul, mul_one, NNReal.coe_inv]
        · exact hn
        · exact hb.ne'
      refine le_trans ?_ h'.le
      rw [← ENNReal.coe_le_coe, ENNReal.coe_mul]
      exact hA₃ n
    · rw [not_lt, le_zero_iff] at hb
      simpa [hb] using
        hA₃
          0
            -- since `μ` and `ν` are not mutually singular, `μ A = 0` implies `ν Aᶜ > 0`

  rw [MutuallySingular] at h; push_neg at h
  have := h _ hAmeas hμ
  simp_rw [A, compl_iInter, compl_compl] at this
  obtain ⟨n, hn⟩ := exists_measure_pos_of_not_measure_iUnion_null this
  exact ⟨1 / (n + 1), by simp, f n, hf₁ n, hn, hf₂ n⟩

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