AdaptiveMarginalLaw.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Adaptive passes need the correct marginal for the actual incoming seed. Independence between unused, counterfactual seed-indexed draws is unnecessary. This permits one common keyed random source.

theorem OAI.EditApproximation.adaptiveSeedLaw_eq_of_marginals line 28

Source documentation

The common random source can correlate draws for distinct hypothetical incoming seeds; only its independence from the actual incoming seed matters.

theorem adaptiveSeedLaw_eq_of_marginals (incoming : Measure Seed) [IsProbabilityMeasure incoming]
    (next : ∀ seed, Draw seed → Seed) :
    (incoming.prod randomLaw).map
        (fun pair : Seed × Ω => next pair.1 (sample pair.1 pair.2)) =
      adaptiveSeedLaw drawLaw incoming next := by
…

Mentions: OAI.EditApproximation.adaptiveSeedLaw

theorem OAI.EditApproximation.adaptiveAnswerLaw_eq_of_marginals line 64

Source documentation

The same replacement preserves the final integer answer law, rather than only a seed transition.

theorem adaptiveAnswerLaw_eq_of_marginals (incoming : Measure Seed) [IsProbabilityMeasure incoming]
    (answer : ∀ seed, Draw seed → ℕ) :
    (incoming.prod randomLaw).map
        (fun pair : Seed × Ω => answer pair.1 (sample pair.1 pair.2)) =
      (incoming.prod (Measure.pi drawLaw)).map
        (fun pair : Seed × (∀ seed, Draw seed) => answer pair.1 (pair.2 pair.1)) := by
…