English
The set of nonnegative elements within the unit ball forms a directed family suitable for construction of approximate units.
Русский
Набор неотрицательных элементов внутри единичной сферы образует направленную семью для построения аппроксимированных единиц.
LaTeX
$$$$ \text{DirectedOn}(\le, \{x \mid 0 \le x \} \cap \mathrm{Ball}(0,1)) $$$$
Lean4
theorem directedOn_nonneg_ball : DirectedOn (· ≤ ·) ({x : A | 0 ≤ x} ∩ Metric.ball 0 1) :=
by
let f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
let g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
suffices ∀ a b : A, 0 ≤ a → 0 ≤ b → ‖a‖ < 1 → ‖b‖ < 1 → a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b)
by
rintro a ⟨(ha₁ : 0 ≤ a), ha₂⟩ b ⟨(hb₁ : 0 ≤ b), hb₂⟩
simp only [Metric.mem_ball, dist_zero_right] at ha₂ hb₂
refine ⟨cfcₙ f (cfcₙ g a + cfcₙ g b), ⟨by simp, ?_⟩, ?_, ?_⟩
· simpa only [Metric.mem_ball, dist_zero_right] using norm_cfcₙ_one_sub_one_add_inv_lt_one _
· exact this a b ha₁ hb₁ ha₂ hb₂
· exact add_comm (cfcₙ g a) (cfcₙ g b) ▸ this b a hb₁ ha₁ hb₂ ha₂
rintro a b ha₁ - ha₂ -
calc
a = cfcₙ (f ∘ g) a := by
conv_lhs => rw [← cfcₙ_id ℝ≥0 a]
refine cfcₙ_congr (Set.InvOn.one_sub_one_add_inv.1.eqOn.symm.mono fun x hx ↦ ?_)
exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂
_ = cfcₙ f (cfcₙ g a) :=
by
rw [cfcₙ_comp f g a ?_ (by simp [f, tsub_self]) ?_ (by simp [g]) ha₁]
· fun_prop (disch := intro _ _; positivity)
· have (x) (hx : x ∈ σₙ ℝ≥0 a) : 1 - x ≠ 0 :=
by
refine tsub_pos_of_lt ?_ |>.ne'
exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂
fun_prop (disch := assumption)
_ ≤ cfcₙ f (cfcₙ g a + cfcₙ g b) :=
by
have hab' : cfcₙ g a ≤ cfcₙ g a + cfcₙ g b := le_add_of_nonneg_right cfcₙ_nonneg_of_predicate
exact CFC.monotoneOn_one_sub_one_add_inv cfcₙ_nonneg_of_predicate (cfcₙ_nonneg_of_predicate.trans hab') hab'
