English
A monotone-on property for extended real maps extended to the real case via nnorm and isSelfAdjoint alignment.
Русский
Монотонность в контексте отображений на вещественных величинах через nnorm и выравнивание на самосопряженные элементы.
LaTeX
$$$$ \operatorname{monotoneOn}igl( f(x) = 1 - (1 + x)^{-1}, \; x \ge 0 \bigr) $$$$
Lean4
theorem monotoneOn_one_sub_one_add_inv_real : MonotoneOn (cfcₙ (fun x : ℝ => 1 - (1 + x)⁻¹)) (Set.Ici (0 : A)) :=
by
intro a (ha : 0 ≤ a) b (hb : 0 ≤ b) hab
calc
_ = cfcₙ (fun x : ℝ≥0 => 1 - (1 + x)⁻¹) a :=
by
rw [cfcₙ_nnreal_eq_real _ _ ha]
refine cfcₙ_congr ?_
intro x hx
have hx' : 0 ≤ x := by grind
simp [hx']
_ ≤ cfcₙ (fun x : ℝ≥0 => 1 - (1 + x)⁻¹) b := (CFC.monotoneOn_one_sub_one_add_inv ha hb hab)
_ = cfcₙ (fun x : ℝ => 1 - (1 + x)⁻¹) b :=
by
rw [cfcₙ_nnreal_eq_real _ _ hb]
refine cfcₙ_congr ?_
intro x hx
have hx' : 0 ≤ x := by grind
simp [hx']
