OAI/GroupTheory/PolycyclicRecognition/Geometry/ProfileDerivativeLabel.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.derivative_eq_support_symmetry line 20

   Source documentation

   A horizontal linear derivative factors through height and is a support isometry once the convex-increment and segment-volume inequalities hold. This first step lands in the full isometry group of the segment norm.

   theorem derivative_eq_support_symmetry
       {V W I B J : Type*} [AddCommGroup V] [Module ℝ V]
       [AddCommGroup W] [Module ℝ W] [FiniteDimensional ℝ W]
       [Fintype I] [Fintype B] [Nonempty B]
       (D : SupportDatum W I B) (π M : V →ₗ[ℝ] W) (hπ : Function.Surjective π)
       (A : J → linearSupportSymmetryGroup D)
       (hconv : ∀ v, M v ∈ convexHull ℝ (range fun j => (A j).val (π v)))
       (hlower : ∀ v, D.segmentSupport (π v) ≤ D.segmentSupport (M v)) :
       ∃ T : linearSupportSymmetryGroup D, M = T.val.toLinearMap.comp π := by
   …

   Mentions: OAI.PolycyclicRecognition.SupportDatum, OAI.PolycyclicRecognition.linearSupportSymmetryGroup

2. theorem OAI.PolycyclicRecognition.derivative_eq_one_of_labels line 69

   Source documentation

   The convex orbit constraint selects a member of the original family, even when that family is smaller than the full segment-norm isometry group.

   theorem derivative_eq_one_of_labels
       {V W I B J : Type*} [AddCommGroup V] [Module ℝ V]
       [AddCommGroup W] [Module ℝ W] [FiniteDimensional ℝ W]
       [Fintype I] [Fintype B] [Nonempty B] [Finite J]
       (D : SupportDatum W I B) (π M : V →ₗ[ℝ] W) (hπ : Function.Surjective π)
       (A : J → linearSupportSymmetryGroup D)
       (hconv : ∀ v, M v ∈ convexHull ℝ (range fun j => (A j).val (π v)))
       (hlower : ∀ v, D.segmentSupport (π v) ≤ D.segmentSupport (M v)) :
       ∃ j, M = (A j).val.toLinearMap.comp π := by
   …

   Mentions: OAI.PolycyclicRecognition.SupportDatum, OAI.PolycyclicRecognition.linearSupportSymmetryGroup

3. theorem OAI.PolycyclicRecognition.derivative_eq_one_of_template_labels line 95

   Source documentation

   In particular, a family of template-preserving labels stays in that same family under the infinitesimal profile argument.

   theorem derivative_eq_one_of_template_labels
       {V W I B J : Type*} [AddCommGroup V] [Module ℝ V]
       [NormedAddCommGroup W] [NormedSpace ℝ W] [FiniteDimensional ℝ W]
       [Fintype I] [Fintype B] [Nonempty B] [Finite J]
       (D : SupportDatum W I B) (π M : V →ₗ[ℝ] W) (hπ : Function.Surjective π)
       (A : J → templateSymmetryGroup D)
       (hconv : ∀ v, M v ∈ convexHull ℝ (range fun j => (A j).val (π v)))
       (hlower : ∀ v, D.segmentSupport (π v) ≤ D.segmentSupport (M v)) :
       ∃ j, M = (A j).val.toLinearMap.comp π := by
   …

   Mentions: OAI.PolycyclicRecognition.SupportDatum, OAI.PolycyclicRecognition.templateSymmetryGroup