OAI/GroupTheory/PolycyclicRecognition/Analysis/FlatSwitchSamples.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The recursive independent sampling law on the flat parameter cube

  1. def OAI.PolycyclicRecognition.flatSamplePairs line 15

    Source documentation

    The first block holds first samples and the second block holds second samples.

    def flatSamplePairs (m : ℕ) (t : Fin (m + m) → ℝ) : Fin m → ℝ × ℝ :=
…
  2. def OAI.PolycyclicRecognition.flatSwitchSamples line 18
  3. theorem OAI.PolycyclicRecognition.measurePreserving_finAppend_law line 21
  4. theorem OAI.PolycyclicRecognition.measurePreserving_flatSamplePairs line 40
  5. theorem OAI.PolycyclicRecognition.measurePreserving_flatSwitchSamples line 52