ConditionalLaw.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Exact normalization, support, and joint-law identities for finite conditional seed reconstruction. This is supporting work for cor:secretary; it does not assume a prefix law or supply the online secretary construction by itself.

theorem OAI.MatroidProphet.Secretary.fiberMass_nonneg line 22
theorem OAI.MatroidProphet.Secretary.le_fiberMass line 31
theorem OAI.MatroidProphet.Secretary.source_zero_of_fiberMass_zero line 40
theorem OAI.MatroidProphet.Secretary.fiberKernel_nonneg line 47
theorem OAI.MatroidProphet.Secretary.fiberKernel_sum line 57
theorem OAI.MatroidProphet.Secretary.fiberKernel_support line 71
theorem OAI.MatroidProphet.Secretary.fiberMass_mul_fiberKernel line 78
Source documentation
The exact joint law, including observations of zero source probability.
```
theorem fiberMass_mul_fiberKernel (p : α → ℝ) (hp : ∀ a, 0 ≤ p a)
    (f : α → β) (fallback : α) (b : β) (a : α) :
    fiberMass p f b * fiberKernel p f fallback b a =
      if f a = b then p a else 0 := by
…
```
Mentions: OAI.MatroidProphet.Secretary.fiberMass, OAI.MatroidProphet.Secretary.fiberKernel
theorem OAI.MatroidProphet.Secretary.fiberMass_sum line 94
theorem OAI.MatroidProphet.Secretary.fiberKernel_joint_expectation line 104
Source documentation
Reconstruction preserves the full joint distribution of observation and seed. The test function may depend on unused source coordinates and on the observation.
```
theorem fiberKernel_joint_expectation (p : α → ℝ) (hp : ∀ a, 0 ≤ p a)
    (f : α → β) (fallback : α) (g : β → α → ℝ) :
    (∑ b, fiberMass p f b * (∑ a, fiberKernel p f fallback b a * g b a)) =
      ∑ a, p a * g (f a) a := by
…
```
Mentions: OAI.MatroidProphet.Secretary.fiberMass, OAI.MatroidProphet.Secretary.fiberKernel
theorem OAI.MatroidProphet.Secretary.fiberKernel_marginal line 114
def OAI.MatroidProphet.Secretary.fiberPMF line 121
Source documentation
A bona fide conditional probability mass function on the complete seed.
```
noncomputable def fiberPMF (p : α → ℝ) (hp : ∀ a, 0 ≤ p a)
    (f : α → β) (fallback : α) (b : β) : PMF α :=
…
```
theorem OAI.MatroidProphet.Secretary.fiberPMF_apply line 129
def OAI.MatroidProphet.Secretary.fiberMarginalPMF line 135
Source documentation
The observation marginal as an actual PMF, with its normalization proved.
```
noncomputable def fiberMarginalPMF (p : α → ℝ) (hp : ∀ a, 0 ≤ p a)
    (hpsum : ∑ a, p a = 1) (f : α → β) : PMF β :=
…
```
theorem OAI.MatroidProphet.Secretary.fiberMarginalPMF_apply line 142
theorem OAI.MatroidProphet.Secretary.fiberPMF_joint_atom line 147