OAI/GroupTheory/PolycyclicRecognition/Analysis/ReflectedSegmentSupport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The exponent gain from two reflected segments

The reflection-doubling identity follows from finite balanced support data and gives the support gain for a pair of reflected segments.

  1. theorem OAI.PolycyclicRecognition.SupportDatum.compact_segment line 22
  2. theorem OAI.PolycyclicRecognition.SupportDatum.weightSupport_union line 28
  3. theorem OAI.PolycyclicRecognition.SupportDatum.weightSupport_opposite_segments line 47
  4. theorem OAI.PolycyclicRecognition.SupportDatum.basisTemplateSupport_opposite_segments line 58
  5. theorem OAI.PolycyclicRecognition.SupportDatum.templateSupport_opposite_segments line 67
  6. theorem OAI.PolycyclicRecognition.SupportDatum.reflected_segment_support line 82

    Source documentation

    Opposite images have twice the single-segment volume exponent.

    theorem reflected_segment_support
    (A C : PolycyclicRecognition.templateSymmetryGroup D) {w : W}
    (hw : w ≠ 0) (hreflect : C.val w = -A.val w) :
    D.templateSupport (A.val '' segment ℝ 0 w) = D.segmentSupport w ∧
    D.templateSupport (C.val '' segment ℝ 0 w) = D.segmentSupport w ∧
    D.templateSupport ((A.val '' segment ℝ 0 w) ∪ (C.val '' segment ℝ 0 w)) =
      2 * D.segmentSupport w ∧ 0 < D.segmentSupport w := by
…

    Mentions: OAI.PolycyclicRecognition.templateSymmetryGroup