OAI/GroupTheory/PolycyclicRecognition/Algebra/TemplateComparisonTranslation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.SupportDatum.templateSupport_le_of_zero_mem line 19

   Source documentation

   Translation invariance extends the comparison for templates containing zero to every nonempty compact convex template.

   theorem templateSupport_le_of_zero_mem (A : W →L[ℝ] W)
       (h : ∀ C : Set W, IsCompact C → Convex ℝ C → (0 : W) ∈ C →
         P.templateSupport C ≤ P.templateSupport (A '' C))
       (C : Set W) (hC : IsCompact C) (hne : C.Nonempty) (hconv : Convex ℝ C) :
       P.templateSupport C ≤ P.templateSupport (A '' C) := by
   …

2. theorem OAI.PolycyclicRecognition.SupportDatum.template_symmetry_of_zero_mem_comparisons line 41

   Source documentation

   Forward and inverse comparisons force preservation of the full template functional, using only comparisons for templates through zero.

   theorem template_symmetry_of_zero_mem_comparisons (A : W ≃L[ℝ] W)
       (hf : ∀ C : Set W, IsCompact C → Convex ℝ C → (0 : W) ∈ C →
         P.templateSupport C ≤ P.templateSupport (A '' C))
       (hi : ∀ C : Set W, IsCompact C → Convex ℝ C → (0 : W) ∈ C →
         P.templateSupport C ≤ P.templateSupport (A.symm '' C)) :
       A.toLinearEquiv ∈ templateSymmetryGroup P := by
   …

   Mentions: OAI.PolycyclicRecognition.templateSymmetryGroup