OAI/GroupTheory/PolycyclicRecognition/Analysis/PolarProbeImages.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Centering the translated probes removes the contact-pivot parameter

  1. theorem OAI.PolycyclicRecognition.centered_polar_probe_image line 17

    Source documentation

    The target template used by the measured path restriction is independent of the inward displacement of the source pivot.

    theorem centered_polar_probe_image
    (K : ProperCone ℝ (StrongDual ℝ W)) (ε : ℝ) (w : W)
    (A : W →ₗ[ℝ] V) (k : Fin 3) :
    (fun z => A (z - w)) '' polarSamplingTemplates K ε w k =
      A '' normalizedPolarTemplates K ε k := by
…

    Mentions: OAI.PolycyclicRecognition.polarSamplingTemplates, OAI.PolycyclicRecognition.normalizedPolarTemplates