OAI/GroupTheory/PolycyclicRecognition/Analysis/GenericProfileSigns.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   Duplicate generator rays are normalized and removed before counting positive signs. Thus the constant-count step follows from the actual template symmetry action, rather than being a new hypothesis on the profile.

   theorem generic_profile_signs_constant
       {W I B : Type*} [NormedAddCommGroup W] [InnerProductSpace ℝ W]
       [FiniteDimensional ℝ W] [Fintype I] [Fintype B] [Nonempty B]
       (D : PolycyclicRecognition.SupportDatum W I B)
       (hweights : ∀ i, D.weight i ≠ 0)
       (h q : ℝ → W) (hc : Continuous h) (w : W) (hw : ∀ i, D.weight i w ≠ 0)
       {T : ℝ} (hT : 0 ≤ T)
       (hq : ∀ i, IntervalIntegrable (fun t => D.weight i (q t)) volume 0 T)
       (hFTC : ∀ i t, t ∈ Icc 0 T →
         D.weight i (h t) = ∫ s in 0..t, D.weight i (q s))
       (label : ℝ → templateSymmetryGroup D)
       (hlabel : ∀ᵐ t ∂volume.restrict (Icc 0 T), q t = (label t).val w)
   …

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