English
There exists a local inverse of exp 𝕂 x on the ball: exp 𝕂 x has inverse exp 𝕂 (-x) inside the ball.
Русский
Существует локальный обратный для экспоненты: exp(−x) является обратной для exp(x) внутри шара.
LaTeX
$$Invertible (exp 𝕂 x) with invOf := exp 𝕂 (−x) on the ball$$
Lean4
/-- `NormedSpace.exp 𝕂 x` has explicit two-sided inverse `NormedSpace.exp 𝕂 (-x)`. -/
noncomputable def invertibleExpOfMemBall [CharZero 𝕂] {x : 𝔸} (hx : x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius) :
Invertible (exp 𝕂 x) where
invOf := exp 𝕂 (-x)
invOf_mul_self :=
by
have hnx : -x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius :=
by
rw [EMetric.mem_ball, ← neg_zero, edist_neg_neg]
exact hx
rw [← exp_add_of_commute_of_mem_ball (Commute.neg_left <| Commute.refl x) hnx hx, neg_add_cancel, exp_zero]
mul_invOf_self :=
by
have hnx : -x ∈ EMetric.ball (0 : 𝔸) (expSeries 𝕂 𝔸).radius :=
by
rw [EMetric.mem_ball, ← neg_zero, edist_neg_neg]
exact hx
rw [← exp_add_of_commute_of_mem_ball (Commute.neg_right <| Commute.refl x) hx hnx, add_neg_cancel, exp_zero]
