OAI/Probability/MatroidSecretary/Secretary/Prefix.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Finite combinatorial probability for the random secretary prefix. The Bernoulli mask used to draw the prefix length is part of the initial seed; its cardinality has the binomial law, and it is independent of the uniformly random arrival permutation. No product-law assertion conditional on that full seed is made.

Source: sections/secretary.tex, eq:secretary-prefix-mask, lines 54–66; SHA256 3554fe0f7296782edf63cc7f1305c377e7a7b9d8f8948b9510ea4ad02a702d63. These supporting laws include n=0, k=0, k=n, and Bernoulli rates 0 and 1.

  1. lemma OAI.MatroidProphet.Secretary.bitsWeight_constant line 30
  2. lemma OAI.MatroidProphet.Secretary.bernoulli_cardinality_mass line 41
  3. lemma OAI.MatroidProphet.Secretary.bitsWeight_perm line 59
  4. lemma OAI.MatroidProphet.Secretary.bitsExpectation_perm line 64
  5. lemma OAI.MatroidProphet.Secretary.prefix_filter_eq_map line 73
  6. lemma OAI.MatroidProphet.Secretary.prefix_filter_card line 85
  7. lemma OAI.MatroidProphet.Secretary.integral_uniform_eq_average line 90
  8. theorem OAI.MatroidProphet.Secretary.uniform_prefix_average line 100

    Source documentation

    Conditional only on the prefix length, the actual uniform-permutation prefix has the uniform law on all subsets of that cardinality.

    theorem uniform_prefix_average {n : ℕ} {k : ℕ} (hk : k ≤ n)
    (f : Finset (Fin n) → ℝ) :
    (∑ σ : Equiv.Perm (Fin n),
      f (univ.filter fun e : Fin n => (σ.symm e).val < k)) /
        Fintype.card (Equiv.Perm (Fin n)) =
      (∑ S ∈ (univ : Finset (Fin n)).powersetCard k, f S) /
        Nat.choose n k := by
…
  9. theorem OAI.MatroidProphet.Secretary.uniform_prefix_atom line 113

    Source documentation

    Exact fixed-length atom law, including cardinality mismatch.

    theorem uniform_prefix_atom {n : ℕ} {k : ℕ} (hk : k ≤ n)
    (S : Finset (Fin n)) :
    (∑ σ : Equiv.Perm (Fin n),
      if (univ.filter fun e : Fin n => (σ.symm e).val < k) = S then (1 : ℝ) else 0) /
        Fintype.card (Equiv.Perm (Fin n)) =
      if k = S.card then (Nat.choose n k : ℝ)⁻¹ else 0 := by
…
  10. theorem OAI.MatroidProphet.Secretary.integral_uniform_prefix line 125

    Source documentation

    Measure-theoretic form of the fixed-length prefix averaging law.

    theorem integral_uniform_prefix {n : ℕ} {k : ℕ} (hk : k ≤ n)
    [MeasurableSpace (Equiv.Perm (Fin n))]
    [MeasurableSingletonClass (Equiv.Perm (Fin n))]
    (f : Finset (Fin n) → ℝ) :
    (∫ σ, f (univ.filter fun e : Fin n => (σ.symm e).val < k)
      ∂(PMF.uniformOfFintype (Equiv.Perm (Fin n))).toMeasure) =
      (∑ S ∈ (univ : Finset (Fin n)).powersetCard k, f S) /
        Nat.choose n k := by
…