OAI/Analysis/IrrationalRotation/Sampling/PrefixReferenceCompletion.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Invariant233.OrderedProductCoupling.collapsePrefixPattern line 13
  2. def OAI.Invariant233.OrderedProductCoupling.prefixPatternEvent line 17
  3. lemma OAI.Invariant233.OrderedProductCoupling.collapsePrefixPattern_measurable line 20
  4. lemma OAI.Invariant233.OrderedProductCoupling.prefixPatternEvent_measurable line 27
  5. lemma OAI.Invariant233.OrderedProductCoupling.prefixPattern_restrict_map line 33
  6. def OAI.Invariant233.OrderedProductCoupling.selectedPrefixPattern line 68
  7. lemma OAI.Invariant233.OrderedProductCoupling.mem_selectedPrefixPattern line 71
  8. lemma OAI.Invariant233.OrderedProductCoupling.selectedPrefixPattern_subset line 84
  9. lemma OAI.Invariant233.OrderedProductCoupling.mem_selectedPrefixPattern_subtype line 89
  10. lemma OAI.Invariant233.OrderedProductCoupling.realTriangularEvent_eq_payload_preimage line 94
  11. lemma OAI.Invariant233.OrderedProductCoupling.assemble_collapse_referencePayload line 108
  12. theorem OAI.Invariant233.OrderedProductCoupling.prefixPatternLaw_eq_realTriangularLaw line 128
  13. theorem OAI.Invariant233.OrderedProductCoupling.prefixReferencePairLaw_absolutelyContinuous line 162
  14. theorem OAI.Invariant233.OrderedProductCoupling.circle_prefix_absolutelyContinuous_triangular_sum line 176