Square roots near the identity in a Banach algebra

Squaring, a ↦ a * a, has derivative x ↦ 2 * x at the identity of a Banach algebra over ℝ, and that derivative is invertible. The inverse function theorem therefore produces a smooth partial inverse near 1: every element close enough to 1 has a square root close to 1, the square root depends smoothly on the element, and it is the only square root near 1, because squaring is injective there.

This file packages that partial inverse as TauCeti.sqrtNearOne together with the three facts downstream arguments need: it fixes 1, it is smooth at 1, and it is a two-sided inverse of squaring on a neighbourhood of 1. The two-sided statements are phrased as Filter.Eventually assertions rather than by exhibiting a neighbourhood, since that is how they get used.

The motivating application is the Morse lemma, in TauCeti.Analysis.Calculus.Morse.NormalForm: the operator (D²f x)⁻¹ ∘ B v comparing the averaged Hessian along a segment with the Hessian at a nondegenerate critical point is close to the identity, and the change of coordinates flattening f is built from its square root. Nothing here is a substitute for the continuous functional calculus: CFC.sqrt computes the positive square root of a positive element of a C⋆-algebra, whereas what is needed here is a square root near 1 in a bare Banach algebra, with smooth dependence on the element.

Main declarations

• TauCeti.sqrtNearOne: the local inverse of squaring at the identity.
• TauCeti.sqrtNearOne_one, TauCeti.contDiffAt_sqrtNearOne: it fixes 1 and is smooth there.
• TauCeti.eventually_mul_self_sqrtNearOne: near 1 it is a right inverse of squaring, so its value really is a square root.
• TauCeti.eventually_sqrtNearOne_mul_self: near 1 it is a left inverse of squaring, which is the uniqueness statement: an element close to 1 is recovered from its square.

References

The construction is the inverse function theorem in Banach spaces, as in S. Lang, Real and Functional Analysis, Chapter XIV.

noncomputable def TauCeti.sqrtNearOne (A : Type u_1) [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] : A → A

The square root near the identity of a Banach algebra: the local inverse of squaring supplied by the inverse function theorem at 1. It is only meaningful near 1; see TauCeti.eventually_mul_self_sqrtNearOne.

Equations

• TauCeti.sqrtNearOne A = HasStrictFDerivAt.localInverse (fun (a : A) => a * a) (ContinuousLinearEquiv.smulLeft (Units.mk0 2 TauCeti.sqrtNearOne._proof_4✝)) 1 ⋯

theorem TauCeti.analyticAt_sqrtNearOne {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] : AnalyticAt ℝ (sqrtNearOne A) 1

The square root near the identity is analytic at the identity. This gives a single neighborhood on which it is smooth to every finite order.

@[simp]

theorem TauCeti.sqrtNearOne_one {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] : sqrtNearOne A 1 = 1

The square root near the identity fixes the identity.

theorem TauCeti.eventually_mul_self_sqrtNearOne {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] : ∀ᶠ (a : A) in nhds 1, sqrtNearOne A a * sqrtNearOne A a = a

Near the identity, TauCeti.sqrtNearOne really produces a square root.

theorem TauCeti.eventually_sqrtNearOne_mul_self {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] : ∀ᶠ (b : A) in nhds 1, sqrtNearOne A (b * b) = b

Near the identity, an element is recovered from its square by TauCeti.sqrtNearOne. This is the uniqueness half: two elements close to 1 with the same square are equal.

theorem TauCeti.contDiffAt_sqrtNearOne {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] : ContDiffAt ℝ (↑⊤) (sqrtNearOne A) 1

The square root near the identity is smooth at the identity.

theorem TauCeti.continuousAt_sqrtNearOne {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] [CompleteSpace A] : ContinuousAt (sqrtNearOne A) 1

The square root near the identity is continuous at the identity.