OAI/GroupTheory/PolycyclicRecognition/Analysis/SegmentSupportTimes.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Prescribed endpoint times realizing the segment support exponents

  1. theorem OAI.PolycyclicRecognition.SupportDatum.weightSupport_segment_endpoints line 16
  2. def OAI.PolycyclicRecognition.SupportDatum.segmentSupportTime line 27

    Source documentation

    A linear weight on the segment chooses the final time exactly when its value on the direction is nonnegative.

    def segmentSupportTime (v : W) (T : ℝ) (i : I) : ℝ :=
…
  3. theorem OAI.PolycyclicRecognition.SupportDatum.segmentSupportTime_mem line 30
  4. theorem OAI.PolycyclicRecognition.SupportDatum.weight_at_segmentSupportTime line 36

    Source documentation

    These fixed times give precisely the exponents used by the normalized segment boxes, rather than arbitrary height support positions.

    theorem weight_at_segmentSupportTime (w₀ v : W) {T : ℝ} (hT : 0 ≤ T) (i : I) :
    D.weight i (w₀ + D.segmentSupportTime v T i • v) =
      D.weightSupport (segment ℝ w₀ (w₀ + T • v)) i := by
…