KernelModel.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite conditional seed kernels

The observation map can include the branch and the sacrificed mask. Its domain is the complete source seed, so conditioning does not discard unused coins. These definitions are independent of every proposed selection-rule proof.

def OAI.MatroidProphet.Secretary.fiberMass line 21
Source documentation
The source mass of a fiber of the observation map.
```
noncomputable def fiberMass (p : α → ℝ) (f : α → β) (b : β) : ℝ :=
…
```
def OAI.MatroidProphet.Secretary.fiberKernel line 26
Source documentation
The conditional source mass, totalized by a fixed point mass on empty fibers. The fallback only concerns observations of source probability zero.
```
noncomputable def fiberKernel (p : α → ℝ) (f : α → β) (fallback : α)
    (b : β) (a : α) : ℝ :=
…
```