OAI/GroupTheory/PolycyclicRecognition/Algebra/TemplateVariationEquality.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.SupportDatum.exists_ordered_weight_signs line 23

   Source documentation

   For a centered absolutely continuous profile, equality of its support lower bound and derivative-speed upper bound forces every weight to exhaust its positive variation at a maximizing time. The scalar integral identities are the fundamental theorem of calculus data for the line restriction.

   theorem exists_ordered_weight_signs
       (h : ℝ → W) (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)) :
       ∃ τ : I → ℝ, (∀ i, τ i ∈ Icc 0 T) ∧
         (∀ i, D.weight i (h (τ i)) = D.weightSupport (h '' Icc 0 T) i) ∧
         (∀ i, ∀ᵐ t ∂volume.restrict (Ioc 0 (τ i)), 0 ≤ D.weight i (q t)) ∧
         (∀ i, ∀ᵐ t ∂volume.restrict (Ioc (τ i) T), D.weight i (q t) ≤ 0) := by
   …