LocalMedianDrawLaw.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The local bounded-key random source implements the same whole-table median pass as the complete program. Copies are independent, while all entries within a copy retain their shared online and group draws.

def OAI.EditApproximation.physicalLocalMedianUpdateTable line 24
Source documentation
The executable local pass: scale and round each full-copy value, take the upper median, and clamp each result to the common finite seed type.
```
noncomputable def physicalLocalMedianUpdateTable
    (draws : Fin copies → PhysicalLocalProgramDraw (R := R)
…
```
Mentions: OAI.EditApproximation.PhysicalLocalProgramDraw
theorem OAI.EditApproximation.physicalLocalMedianUpdateTable_eq line 38
theorem OAI.EditApproximation.physicalLocalProgramCopyDrawLaw_map line 61
Source documentation
The restriction to used keys preserves independence between complete program copies, as well as the law of each copy.
```
theorem physicalLocalProgramCopyDrawLaw_map :
    (Measure.pi fun _ : Fin copies => physicalLocalProgramDrawLaw (R := R)
…
```
Mentions: OAI.EditApproximation.physicalLocalProgramDrawLaw
theorem OAI.EditApproximation.physicalLocalMedianUpdateTable_law line 87
Source documentation
Equality of the entire returned seed-table distribution. No independent per-entry resampling is introduced by replacing complete copies with local bounded-key copies.
```
theorem physicalLocalMedianUpdateTable_law :
    (Measure.pi fun _ : Fin copies => physicalLocalProgramDrawLaw (R := R)
…
```
Mentions: OAI.EditApproximation.physicalLocalProgramDrawLaw
theorem OAI.EditApproximation.physicalLocalMedianUpdateTable_event line 108
Source documentation
Any whole-seed event, including the simultaneous good-seed event, has the same probability for the actual local median pass.
```
theorem physicalLocalMedianUpdateTable_event
    (event : Set (ClampedPhysicalSeed M J target.length N)) :
    (Measure.pi fun _ : Fin copies => physicalLocalProgramDrawLaw (R := R)
…
```
Mentions: OAI.EditApproximation.ClampedPhysicalSeed, OAI.EditApproximation.physicalLocalProgramDrawLaw