OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedMeasuredProduct.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.mpr_program line 15

   Source documentation

   Changing a certified read bound preserves the executed program.

   theorem mpr_program {S : SamplerCoupling α} (h : M = N) (X : Realization w N S) :
       (Eq.mpr (congrArg (fun j => Realization w j S) h) X).program = X.program := by
   …

   Mentions: OAI.LowSpaceSubsetSum.SamplerCoupling

2. def OAI.LowSpaceSubsetSum.WordSeedMeasured.reprogram line 21

   Source documentation

   Transport only the proof-facing program index, leaving the executed result intact.

   def reprogram {S : SamplerCoupling α} {X : Realization w N S}
       {Y : Realization w M S} (E : Execution X) (h : Y.program = X.program) :
       Execution Y where
   …

   Mentions: OAI.LowSpaceSubsetSum.SamplerCoupling, OAI.LowSpaceSubsetSum.WordSeedMeasured.Execution

3. def OAI.LowSpaceSubsetSum.WordSeedMeasured.enlarge line 27
4. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.enlarge_bounded line 32
5. def OAI.LowSpaceSubsetSum.WordSeedMeasured.prod line 36
6. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.prod_bounded line 43
7. def OAI.LowSpaceSubsetSum.WordSeedMeasured.pi line 59
8. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.pi_bounded line 75