English
If a signed measure s assigns negative value to a measurable set i, there exists a measurable subset j ⊆ i with s restricted to j nonpositive and s(j) < 0.
Русский
Если сигнальная мера s на множестве i принимает négат. значение, существует измеримое подмножество j ⊆ i такое, что s ≤[j] 0 и s(j) < 0.
LaTeX
$$$\exists j \; (\text{MeasurableSet } j) \land (j \subseteq i) \land s \le[j] 0 \land s(j) < 0$$$
Lean4
/-- A measurable set of negative measure has a negative subset of negative measure. -/
theorem exists_subset_restrict_nonpos (hi : s i < 0) : ∃ j : Set α, MeasurableSet j ∧ j ⊆ i ∧ s ≤[j] 0 ∧ s j < 0 :=
by
have hi₁ : MeasurableSet i := by_contradiction fun h => ne_of_lt hi <| s.not_measurable h
by_cases h : s ≤[i] 0; · exact ⟨i, hi₁, Set.Subset.refl _, h, hi⟩
by_cases hn : ∀ n : ℕ, ¬s ≤[i \ ⋃ l < n, restrictNonposSeq s i l] 0
swap; · exact exists_subset_restrict_nonpos' hi₁ hi hn
set A := i \ ⋃ l, restrictNonposSeq s i l with hA
set bdd : ℕ → ℕ := fun n => findExistsOneDivLT s (i \ ⋃ k ≤ n, restrictNonposSeq s i k)
have hn' : ∀ n : ℕ, ¬s ≤[i \ ⋃ l ≤ n, restrictNonposSeq s i l] 0 :=
by
intro n
convert hn (n + 1) using 5 <;>
· ext l
simp only [exists_prop, Set.mem_iUnion, and_congr_left_iff]
exact fun _ => Nat.lt_succ_iff.symm
have h₁ : s i = s A + ∑' l, s (restrictNonposSeq s i l) :=
by
rw [hA, ← s.of_disjoint_iUnion, add_comm, of_add_of_diff]
· exact MeasurableSet.iUnion fun _ => restrictNonposSeq_measurableSet _
exacts [hi₁, Set.iUnion_subset fun _ => restrictNonposSeq_subset _, fun _ => restrictNonposSeq_measurableSet _,
restrictNonposSeq_disjoint]
have h₂ : s A ≤ s i := by
rw [h₁]
apply le_add_of_nonneg_right
exact tsum_nonneg fun n => le_of_lt (measure_of_restrictNonposSeq h _ (hn n))
have h₃' : Summable fun n => (1 / (bdd n + 1) : ℝ) :=
by
have : Summable fun l => s (restrictNonposSeq s i l) :=
HasSum.summable (s.m_iUnion (fun _ => restrictNonposSeq_measurableSet _) restrictNonposSeq_disjoint)
refine .of_nonneg_of_le (fun n => ?_) (fun n => ?_) (this.comp_injective Nat.succ_injective)
· exact le_of_lt Nat.one_div_pos_of_nat
· exact le_of_lt (restrictNonposSeq_lt n (hn' n))
have h₃ : Tendsto (fun n => (bdd n : ℝ) + 1) atTop atTop :=
by
simp only [one_div] at h₃'
exact Summable.tendsto_atTop_of_pos h₃' fun n => Nat.cast_add_one_pos (bdd n)
have h₄ : Tendsto (fun n => (bdd n : ℝ)) atTop atTop := by convert atTop.tendsto_atTop_add_const_right (-1) h₃; simp
have A_meas : MeasurableSet A := hi₁.diff (MeasurableSet.iUnion fun _ => restrictNonposSeq_measurableSet _)
refine ⟨A, A_meas, Set.diff_subset, ?_, h₂.trans_lt hi⟩
by_contra hnn
rw [restrict_le_restrict_iff _ _ A_meas] at hnn; push_neg at hnn
obtain ⟨E, hE₁, hE₂, hE₃⟩ := hnn
have : ∃ k, 1 ≤ bdd k ∧ 1 / (bdd k : ℝ) < s E :=
by
rw [tendsto_atTop_atTop] at h₄
obtain ⟨k, hk⟩ := h₄ (max (1 / s E + 1) 1)
refine ⟨k, ?_, ?_⟩
· have hle := le_of_max_le_right (hk k le_rfl)
norm_cast at hle
· have : 1 / s E < bdd k := by linarith only [le_of_max_le_left (hk k le_rfl)]
rw [one_div] at this ⊢
exact inv_lt_of_inv_lt₀ hE₃ this
obtain ⟨k, hk₁, hk₂⟩ := this
have hA' : A ⊆ i \ ⋃ l ≤ k, restrictNonposSeq s i l :=
by
apply Set.diff_subset_diff_right
intro x; simp only [Set.mem_iUnion]
rintro ⟨n, _, hn₂⟩
exact ⟨n, hn₂⟩
refine findExistsOneDivLT_min (hn' k) (Nat.sub_lt hk₁ Nat.zero_lt_one) ⟨E, Set.Subset.trans hE₂ hA', hE₁, ?_⟩
convert hk₂; norm_cast
exact tsub_add_cancel_of_le hk₁
