English
The map associating a real argument to a nonnegative element yields a monotone map on the nonnegative ball.
Русский
Отображение, связывающее вещественный аргумент с неотрицательным элементом, образует монотонное отображение на неотрицательном шаре.
LaTeX
$$$$ \text{MonotoneOn}(f,\, \{x\,|\, x \ge 0\}) $$$$
Lean4
theorem monotoneOn_one_sub_one_add_inv : MonotoneOn (cfcₙ (fun x : ℝ≥0 ↦ 1 - (1 + x)⁻¹)) (Set.Ici (0 : A)) :=
by
intro a ha b hb hab
simp only [Set.mem_Ici] at ha hb
rw [← inr_le_iff .., nnreal_cfcₙ_eq_cfc_inr a _, nnreal_cfcₙ_eq_cfc_inr b _]
rw [← inr_le_iff a b (.of_nonneg ha) (.of_nonneg hb)] at hab
rw [← inr_nonneg_iff] at ha hb
have h_cfc_one_sub (c : A⁺¹) (hc : 0 ≤ c := by cfc_tac) :
cfc (fun x : ℝ≥0 ↦ 1 - (1 + x)⁻¹) c = 1 - cfc (·⁻¹ : ℝ≥0 → ℝ≥0) (1 + c) :=
by
rw [cfc_tsub _ _ _ (fun x _ ↦ by simp) (hg := by fun_prop (disch := intro _ _; positivity)), cfc_const_one ℝ≥0 c,
cfc_comp' (·⁻¹) (1 + ·) c ?_, cfc_add .., cfc_const_one ℝ≥0 c, cfc_id' ℝ≥0 c]
exact continuousOn_id.inv₀ (Set.forall_mem_image.mpr fun x _ ↦ by dsimp only [id]; positivity)
rw [h_cfc_one_sub (a : A⁺¹), h_cfc_one_sub (b : A⁺¹)]
gcongr
rw [← CFC.rpow_neg_one_eq_cfc_inv, ← CFC.rpow_neg_one_eq_cfc_inv]
exact
rpow_neg_one_le_rpow_neg_one (add_nonneg zero_le_one ha) (by gcongr) <|
isUnit_of_le isUnit_one zero_le_one <| le_add_of_nonneg_right ha
