OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationHistoryCoupling.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Bounded fresh-word sampling of the complete dependent representation trial

  1. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.factorExponents_le_n line 17
  2. def OAI.LowSpaceSubsetSum.RepresentationSetup.nestedCoupling line 36
  3. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.nestedCoupling_uniform line 40
  4. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.nestedCoupling_failure line 43
  5. def OAI.LowSpaceSubsetSum.RepresentationSetup.residuesCoupling line 48
  6. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.residuesCoupling_uniform line 55
  7. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.residuesCoupling_failure line 63
  8. def OAI.LowSpaceSubsetSum.RepresentationSetup.primeHistoryCoupling line 82
  9. def OAI.LowSpaceSubsetSum.RepresentationSetup.trialHistoryCoupling line 86
  10. def OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrimeCoupling line 89
  11. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrimeCoupling_uniform line 92
  12. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.extraPrimeCoupling_failure line 96
  13. def OAI.LowSpaceSubsetSum.RepresentationSetup.extraHistoryCoupling line 100
  14. def OAI.LowSpaceSubsetSum.RepresentationSetup.bucketHistoryCoupling line 104
  15. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.primeHistoryCoupling_uniform line 109
  16. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.trialHistoryCoupling_uniform line 113
  17. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.extraHistoryCoupling_uniform line 117
  18. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.bucketHistoryCoupling_uniform line 124

    Source documentation

    The ideal marginal is the dependent history law, rather than the uniform law on the final sigma type.

    theorem bucketHistoryCoupling_uniform (hn : 10000 ≤ n) :
    (R.bucketHistoryCoupling hn).idealLaw = R.bucketTrialLaw hn := by
…
  19. def OAI.LowSpaceSubsetSum.RepresentationSetup.rangeCallBound line 129
  20. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.guessHistoryCoupling_failure line 132
  21. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.partitionHistoryCoupling_failure line 142
  22. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.bucketHistoryCoupling_failure line 156

    Source documentation

    Three low-factor prime calls and one extra-prime call; all other calls are counted explicitly from the actual permutation, guess, residue and family code.

    theorem bucketHistoryCoupling_failure (hn : 10000 ≤ n) :
    (R.bucketHistoryCoupling hn).failure ≤
      R.rangeCallBound / (2 : ℝ) ^ (n ^ 3) + 4 * Real.exp (-((n : ℝ) ^ 2 / 4)) := by
…
  23. theorem OAI.LowSpaceSubsetSum.RepresentationSetup.bucketHistoryCoupling_event line 188

    Source documentation

    Any proved ideal event transfers directly, with no conditioning on sampler success.

    theorem bucketHistoryCoupling_event (hn : 10000 ≤ n)
    (P : R.BucketTrialHistory (by omega) → Prop) :
    (R.bucketTrialLaw hn).probability P -
        (R.rangeCallBound / (2 : ℝ) ^ (n ^ 3) + 4 * Real.exp (-((n : ℝ) ^ 2 / 4))) ≤
      (R.bucketHistoryCoupling hn).boundedLaw.probability
        (fun h => ∃ x, h = some x ∧ P x) := by
…