OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationRuntimeLaw.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Exact sign-coordinate transport to the input-only runtime experiment

  1. theorem OAI.LowSpaceSubsetSum.FiniteLaw.map_equiv_mass line 17
  2. theorem OAI.LowSpaceSubsetSum.FiniteLaw.map_equiv_eq_of_mass line 26
  3. def OAI.LowSpaceSubsetSum.RepresentationSetup.runtimePrimeEquiv line 40
  4. def OAI.LowSpaceSubsetSum.RepresentationSetup.runtimeTrialEquiv line 53
  5. def OAI.LowSpaceSubsetSum.RepresentationSetup.runtimeExtraEquiv line 67
  6. def OAI.LowSpaceSubsetSum.RepresentationSetup.runtimeBucketEquiv line 81
  7. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.runtimePrime_mass line 98

    Source documentation

    Every conditional sampler depends on the permutation and the guesses, while this coordinate change alters only the independent sign subset.

    theorem runtimePrime_mass (h : R.PrimeHistory) :
    R.runtimeData.zeroSetup.primeLaw.mass (R.runtimePrimeEquiv h) = R.primeLaw.mass h := by
…
  8. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.runtimeTrial_mass line 102
  9. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.runtimeExtra_mass line 106
  10. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.runtimeBucket_mass line 111
  11. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.runtimePrime_law line 116
  12. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.runtimeTrial_law line 119
  13. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.runtimeExtra_law line 122
  14. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.runtimeBucket_law line 126
  15. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.runtimeBucket_probability line 131
  16. def OAI.LowSpaceSubsetSum.RepresentationSetup.runtimeSampler line 139

    Source documentation

    This is the actual input-only sampler, instantiated with the zero-target wrapper. Its definition contains no chosen solution or analysis sign change.

    def runtimeSampler (hn : 10000 ≤ n) :
    SamplerCoupling (R.runtimeData.zeroSetup.BucketTrialHistory (by omega)) :=
…

    Mentions: OAI.LowSpaceSubsetSum.SamplerCoupling

  17. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.runtimeSampler_failure line 143
  18. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.runtimeSampler_event line 149