English
The set measureOfNegatives(s) is bounded below: there exists a real lower bound for all its elements.
Русский
Нормированная граница снизу для measureOfNegatives(s) существует.
LaTeX
$$$\mathrm{BddBelow}\left( \mathrm{measureOfNegatives}(s) \right)$$$
Lean4
theorem bddBelow_measureOfNegatives : BddBelow s.measureOfNegatives :=
by
simp_rw [BddBelow, Set.Nonempty, mem_lowerBounds]
by_contra! h
have h' : ∀ n : ℕ, ∃ y : ℝ, y ∈ s.measureOfNegatives ∧ y < -n := fun n => h (-n)
choose f hf using h'
have hf' : ∀ n : ℕ, ∃ B, MeasurableSet B ∧ s ≤[B] 0 ∧ s B < -n :=
by
intro n
rcases hf n with ⟨⟨B, ⟨hB₁, hBr⟩, hB₂⟩, hlt⟩
exact ⟨B, hB₁, hBr, hB₂.symm ▸ hlt⟩
choose B hmeas hr h_lt using hf'
set A := ⋃ n, B n with hA
have hfalse : ∀ n : ℕ, s A ≤ -n := by
intro n
refine le_trans ?_ (le_of_lt (h_lt _))
rw [hA, ← Set.diff_union_of_subset (Set.subset_iUnion _ n), of_union Set.disjoint_sdiff_left _ (hmeas n)]
· refine add_le_of_nonpos_left ?_
have : s ≤[A] 0 := restrict_le_restrict_iUnion _ _ hmeas hr
refine nonpos_of_restrict_le_zero _ (restrict_le_zero_subset _ ?_ Set.diff_subset this)
exact MeasurableSet.iUnion hmeas
· exact (MeasurableSet.iUnion hmeas).diff (hmeas n)
rcases exists_nat_gt (-s A) with ⟨n, hn⟩
exact lt_irrefl _ ((neg_lt.1 hn).trans_le (hfalse n))
