OAI/GroupTheory/PolycyclicRecognition/Geometry/ProfileWeightSigns.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.SupportDatum.profile_weight_signs_constant line 18

   Source documentation

   The segment-volume bound and the finite support formula give constant weight signs along an absolutely continuous profile line, as soon as the generic finite label action supplies nonzero weights and a fixed count of positive signs.

   theorem profile_weight_signs_constant
       {W I B : Type*} [NormedAddCommGroup W] [NormedSpace ℝ W]
       [FiniteDimensional ℝ W] [Fintype I] [Fintype B] [Nonempty B]
       (D : PolycyclicRecognition.SupportDatum W I B)
       (h q : ℝ → W) (hc : Continuous h) {T c : ℝ} (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))
       (hbound : ∀ b, ∀ᵐ t ∂volume.restrict (Icc 0 T), D.basisSupport b (q t) ≤ c)
       (hlower : T * c ≤ D.templateSupport (h '' Icc 0 T))
       (hnonzero : ∀ i, ∀ᵐ t ∂volume.restrict (Ioc 0 T), D.weight i (q t) ≠ 0)
       (n : ℕ) (hcard : ∀ᵐ t ∂volume.restrict (Ioc 0 T),
   …

   Mentions: OAI.PolycyclicRecognition.SupportDatum