OAI/Analysis/ProductSpaces/Resampling.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentProducts.expandSamples line 18

    Source documentation

    Independent complete samples: descendants, exits, and old coordinates.

    def expandSamples (z : ((ι → Sample) × Sample) × Sample) : Option (Option ι) → Sample
  | none => z.2
  | some none => z.1.2
  | some (some i) => z.1.1 i

    Mentions: OAI.IndependentProducts.Sample

  2. lemma OAI.IndependentProducts.measurePreserving_expandSamples line 23
  3. def OAI.IndependentProducts.FiniteHead.sampleSelector line 44
  4. lemma OAI.IndependentProducts.FiniteHead.sampleSelector_head line 50
  5. lemma OAI.IndependentProducts.FiniteHead.sampleSelector_exit line 59
  6. lemma OAI.IndependentProducts.FiniteHead.sampleSelector_desc line 66
  7. def OAI.IndependentProducts.FiniteHead.stitched line 73
  8. lemma OAI.IndependentProducts.FiniteHead.measurePreserving_stitched line 76
  9. lemma OAI.IndependentProducts.FiniteHead.stitched_head line 82
  10. lemma OAI.IndependentProducts.pathProduct_split line 92
  11. lemma OAI.IndependentProducts.FiniteHead.stitched_path line 106