OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedMeasuredTransport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Proof-only transport for the conditional seed programs

The source sampler uses dependent decidable recursors. These lemmas expose which conditional program is selected, preserving its probability law.

  1. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.rec_heq_pos line 17
  2. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.rec_heq_neg line 24
  3. def OAI.LowSpaceSubsetSum.WordSeedMeasured.transportSampler line 31
  4. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.transportSampler_bounded line 38
  5. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.bounded_mono line 46
  6. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.source_fin_pos line 53
  7. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.source_fin_neg line 59
  8. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.source_factor_small line 67
  9. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.source_factor_large line 75