AffineLabels.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

One global label from finite pointwise linear choices

The profile affinity criterion shows that a linear derivative agrees at each vector with one of finitely many linear symmetry maps. The label cannot depend on the vector: otherwise finitely many proper linear kernels would cover the real vector space.

theorem OAI.PolycyclicRecognition.exists_eq_of_pointwise_linear_selection line 22

Source documentation

A real linear map which agrees pointwise with a finite family of real linear maps agrees with one member of the family everywhere.

theorem exists_eq_of_pointwise_linear_selection
    {ι : Type u} [Finite ι] {W : Type v} [AddCommGroup W] [Module ℝ W]
    (B : W →ₗ[ℝ] W) (A : ι → W →ₗ[ℝ] W)
    (hpointwise : ∀ w, ∃ i, B w = A i w) :
    ∃ i, B = A i := by
…

theorem OAI.PolycyclicRecognition.exists_eq_of_pointwise_continuous_symmetry line 47

Source documentation

In particular, pointwise choices from finitely many continuous linear symmetries give one continuous linear symmetry on the entire space.

theorem exists_eq_of_pointwise_continuous_symmetry
    {ι : Type u} [Finite ι] {W : Type v} [NormedAddCommGroup W] [NormedSpace ℝ W]
    (B : W →L[ℝ] W) (A : ι → W ≃L[ℝ] W)
    (hpointwise : ∀ w, ∃ i, B w = A i w) :
    ∃ i, B = (A i).toContinuousLinearMap := by
…