UniformPermutationImage.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Counting core for the secretary random-prefix law: a uniformly random permutation sends each fixed finite set uniformly onto sets of the same size. No conditioning on the complete secretary seed is asserted here.

Source: sections/secretary.tex, equation eq:secretary-prefix-mask, lines 54--66 of the pinned manuscript; SHA256 3554fe0f7296782edf63cc7f1305c377e7a7b9d8f8948b9510ea4ad02a702d63. These are supporting counting lemmas, not the complete secretary endpoint. The empty ambient type and empty/full fixed subsets are included.

theorem OAI.MatroidProphet.Secretary.permutation_image_count_eq line 27

Source documentation

Equal-cardinality target sets have equally many permutation preimages.

theorem permutation_image_count_eq (s t u : Finset α) (htu : t.card = u.card) :
    (∑ σ : Equiv.Perm α, if s.map σ.toEmbedding = t then (1 : ℝ) else 0) =
      ∑ σ : Equiv.Perm α, if s.map σ.toEmbedding = u then (1 : ℝ) else 0 := by
…

theorem OAI.MatroidProphet.Secretary.permutation_image_count line 51

Source documentation

Exact probability numerator for a prescribed image of a fixed set.

theorem permutation_image_count (s t : Finset α) (hst : s.card = t.card) :
    (∑ σ : Equiv.Perm α, if s.map σ.toEmbedding = t then (1 : ℝ) else 0) =
      (Fintype.card (Equiv.Perm α) : ℝ) / (Fintype.card α).choose s.card := by
…

theorem OAI.MatroidProphet.Secretary.uniform_permutation_image_atom line 84

Source documentation

A prescribed image has probability the reciprocal of the number of sets of that size, and probability zero if its cardinality is different.

theorem uniform_permutation_image_atom (s t : Finset α) :
    (∑ σ : Equiv.Perm α, if s.map σ.toEmbedding = t then (1 : ℝ) else 0) /
        Fintype.card (Equiv.Perm α) =
      if s.card = t.card then ((Fintype.card α).choose s.card : ℝ)⁻¹ else 0 := by
…

theorem OAI.MatroidProphet.Secretary.uniform_permutation_image_average line 103

Source documentation

Averaging over all permutations equals averaging over all possible images of the fixed set. This form can be mixed over a random prefix length.

theorem uniform_permutation_image_average (s : Finset α) (f : Finset α → ℝ) :
    (∑ σ : Equiv.Perm α, f (s.map σ.toEmbedding)) /
        Fintype.card (Equiv.Perm α) =
      (∑ t ∈ (Finset.univ : Finset α).powersetCard s.card, f t) /
        (Fintype.card α).choose s.card := by
…