CoordinateHomLinear.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Continuous homomorphisms in smooth exponential coordinates

Only differentiability of multiplication at the identity, its two unit identities, and the straight-line one-parameter law are needed. The scaling limit of multiplication proves additivity without an automatic-smoothness assumption on the homomorphism.

theorem OAI.PolycyclicRecognition.hasDerivAt_scaled_product line 31

Source documentation

The derivative of exponential-coordinate multiplication at the origin is addition, by differentiating its unit identities along the two axes.

theorem hasDerivAt_scaled_product (m : V → V → V)
    (hm : DifferentiableAt ℝ (fun p : V × V => m p.1 p.2) (0, 0))
    (hleft : ∀ x, m 0 x = x) (hright : ∀ x, m x 0 = x) (x y : V) :
    HasDerivAt (fun t : ℝ => m (t • x) (t • y)) (x + y) 0 := by
…

theorem OAI.PolycyclicRecognition.exists_linearMap_of_coordinate_hom line 58

Source documentation

A continuous multiplicative-coordinate map which is linear on each radial line is additive, hence defines a continuous real-linear map.

theorem exists_linearMap_of_coordinate_hom (m : V → V → V)
    (hm : DifferentiableAt ℝ (fun p : V × V => m p.1 p.2) (0, 0))
    (hleft : ∀ x, m 0 x = x) (hright : ∀ x, m x 0 = x)
    (f : V → W) (hf : Continuous f)
    (hmul : ∀ x y, f (m x y) = f x + f y)
    (hsmul : ∀ (t : ℝ) x, f (t • x) = t • f x) :
    ∃ A : V →L[ℝ] W, ∀ x, A x = f x := by
…