SourcePrefixLaw.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The concrete source observation law after a uniform random prefix

The initially sampled source seed determines the branch and prefix length. An independent uniform permutation supplies the actual observed prefix. Averaging the length, rather than conditioning on the complete initial seed, recovers the full joint law of the branch and sacrificed source mask.

This is the actual source-law input to conditional-table reconstruction in sections/secretary.tex, equations eq:secretary-prefix-mask and its following kernel argument (SHA256 3554fe0f7296782edf63cc7f1305c377e7a7b9d8f8948b9510ea4ad02a702d63). It does not assume a caller-given source transport law.

theorem OAI.MatroidProphet.Secretary.predrawn_mask_prefix_integral line 30

Source documentation

A predrawn Bernoulli mask supplies only the length; the independent random prefix has the original product-mask law after averaging that length.

theorem predrawn_mask_prefix_integral {n : ℕ} (p : ℝ)
    (f : Finset (Fin n) → ℝ) :
    bitsExpectation (fun _ : Fin n => p) univ (fun B =>
      ∫ σ : ArrivalOrder n,
        f (univ.filter fun e : Fin n => (σ.symm e).val < B.card)
        ∂(PMF.uniformOfFintype (ArrivalOrder n)).toMeasure) =
      bitsExpectation (fun _ : Fin n => p) univ f := by
…

Mentions: OAI.MatroidProphet.bitsExpectation, OAI.MatroidProphet.ArrivalOrder

theorem OAI.MatroidProphet.Secretary.integral_source_random_prefix line 51

Source documentation

Exact test-function identity for the manuscript's concrete full source seed. The branch, prefix length and every unused source coin are sampled before the independent uniform permutation.

theorem integral_source_random_prefix {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (f : Bool → Finset (Fin n) → ℝ) :
    (∫ r, ∫ σ : ArrivalOrder n,
      f (mainBranch r)
        (univ.filter fun e : Fin n =>
          (σ.symm e).val < ((completeHiddenRule M hE).mask r).card)
      ∂(PMF.uniformOfFintype (ArrivalOrder n)).toMeasure ∂sourceSeedLaw n) =
      ∫ r, f (mainBranch r) ((completeHiddenRule M hE).mask r) ∂sourceSeedLaw n := by
…

Mentions: OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.mainBranch, OAI.MatroidProphet.completeHiddenRule, OAI.MatroidProphet.sourceSeedLaw

theorem OAI.MatroidProphet.Secretary.source_random_prefix_joint_law line 69
Source documentation
The full branch/prefix pushforward equals the branch/sacrificed-mask law of our concrete source algorithm. This is the exact input used by the finite conditional-table reconstruction, including empty and full prefixes.
```
theorem source_random_prefix_joint_law {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) :
    ((sourceSeedLaw n).prod
      (PMF.uniformOfFintype (ArrivalOrder n)).toMeasure).map
      (fun z : Seed (mainSeedBits n) × ArrivalOrder n =>
        (mainBranch z.1, orderPrefix z.2 ((completeHiddenRule M hE).mask z.1).card)) =
      (sourceSeedLaw n).map
        (fun r => (mainBranch r, (completeHiddenRule M hE).mask r)) := by
…
```
Mentions: OAI.MatroidProphet.sourceSeedLaw, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.Seed, OAI.MatroidProphet.mainSeedBits, OAI.MatroidProphet.mainBranch, OAI.MatroidProphet.orderPrefix, OAI.MatroidProphet.completeHiddenRule