OAI/Probability/MatroidSecretary/Secretary/Seed.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MatroidProphet.reindexSecretarySeed_prefixLength line 17
2. theorem OAI.MatroidProphet.reindexSecretarySeed_decisionAt line 20
3. theorem OAI.MatroidProphet.reindexSecretarySeed_acceptedThrough line 25
4. theorem OAI.MatroidProphet.reindexSecretarySeed_reward line 30
5. theorem OAI.MatroidProphet.reindexSecretarySeed_feasible line 36

   Source documentation

   Feasibility remains pointwise on all seeds, not merely almost everywhere.

   theorem reindexSecretarySeed_feasible (M : Matroid (Fin n)) (hA : SecretaryFeasible M A) :
       SecretaryFeasible M (reindexSecretarySeed A f hf) := by
   …

   Mentions: OAI.MatroidProphet.SecretaryFeasible, OAI.MatroidProphet.reindexSecretarySeed

6. theorem OAI.MatroidProphet.secretaryFinSeed_prefixLength line 47
7. theorem OAI.MatroidProphet.secretaryFinSeed_decisionAt line 51
8. theorem OAI.MatroidProphet.secretaryFinSeed_acceptedThrough line 57
9. theorem OAI.MatroidProphet.secretaryFinSeed_reward line 63
10. theorem OAI.MatroidProphet.secretaryFinSeed_feasible line 68
11. instance OAI.MatroidProphet.secretaryFinSeedLaw_isProbability line 74
12. theorem OAI.MatroidProphet.secretaryFinSeedLaw_decode line 80

    Source documentation

    Decoding recovers the full predrawn table law, including every unused entry.

    theorem secretaryFinSeedLaw_decode (ν : Measure Q) :
        (secretaryFinSeedLaw ν).map (Fintype.equivFin Q).symm = ν := by
    …

    Mentions: OAI.MatroidProphet.secretaryFinSeedLaw

13. theorem OAI.MatroidProphet.secretaryFinSeed_random_law line 88

    Source documentation

    The law roundtrip holds for an arbitrary externally realized finite seed.

    theorem secretaryFinSeed_random_law {Ω : Type*} [MeasurableSpace Ω]
        (μ : Measure Ω) (ν : Measure Q) (R : Ω → Fin (Fintype.card Q))
        (hR : Measurable R) (hlaw : μ.map R = secretaryFinSeedLaw ν) :
        μ.map ((Fintype.equivFin Q).symm ∘ R) = ν := by
    …

    Mentions: OAI.MatroidProphet.secretaryFinSeedLaw

14. theorem OAI.MatroidProphet.secretaryFinSeed_indepFun_iff line 96

    Source documentation

    Arrival randomization remains independent after the complete-seed bijection.

    theorem secretaryFinSeed_indepFun_iff {Ω β : Type*}
        [MeasurableSpace Ω] [MeasurableSpace β] (μ : Measure Ω)
        (X : Ω → β) (R : Ω → Q) :
        IndepFun X ((Fintype.equivFin Q) ∘ R) μ ↔ IndepFun X R μ := by
    …

15. theorem OAI.MatroidProphet.secretaryFinSeed_integral line 109

    Source documentation

    An adversary seeing the finite index can see exactly the original complete seed.

    theorem secretaryFinSeed_integral (ν : Measure Q) (w : Weights n)
        (π : Fin (Fintype.card Q) → ArrivalOrder n) :
        (∫ q, secretaryReward (secretaryFinSeed A) q w (π q) ∂secretaryFinSeedLaw ν) =
          ∫ q, secretaryReward A q w (π ((Fintype.equivFin Q) q)) ∂ν := by
    …

    Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.secretaryReward, OAI.MatroidProphet.secretaryFinSeed, OAI.MatroidProphet.secretaryFinSeedLaw

16. theorem OAI.MatroidProphet.secretaryFinSeed_guarantee line 122

    Source documentation

    Reindexing preserves the complete adversary quantifier, not just orders that are deterministic functions of the original seed. Additional ambient randomness is arbitrary and no independence from the executed order is assumed.

    theorem secretaryFinSeed_guarantee.{u} (M : Matroid (Fin n)) (ν : Measure Q) (c : ℝ)
        (h : SecretaryGuarantee.{u} M A ν c) :
        SecretaryGuarantee.{u} M (secretaryFinSeed A) (secretaryFinSeedLaw ν) c := by
    …

    Mentions: OAI.MatroidProphet.secretaryFinSeed, OAI.MatroidProphet.secretaryFinSeedLaw

17. theorem OAI.MatroidProphet.secretaryFinSeed_witness line 137

    Source documentation

    A concrete finite-seed construction fills the finite-index existential used by the public secretary specification, without adding a transport premise there.

    theorem secretaryFinSeed_witness.{u} (M : Matroid (Fin n)) (ν : Measure Q)
        [IsProbabilityMeasure ν] (c : ℝ) (hA : SecretaryFeasible M A)
        (h : SecretaryGuarantee.{u} M A ν c) :
        ∃ (q : ℕ) (ν' : Measure (Fin q)), IsProbabilityMeasure ν' ∧
          ∃ (A' : SecretaryRule n (Fin q)), SecretaryFeasible M A' ∧
            SecretaryGuarantee.{u} M A' ν' c := by
    …

    Mentions: OAI.MatroidProphet.SecretaryFeasible, OAI.MatroidProphet.SecretaryRule

18. theorem OAI.MatroidProphet.secretaryChallenge_of_finiteRules line 151

    Source documentation

    Final packaging of an already constructed family of finite secretary rules. All probability and adversary obligations are unchanged under seed enumeration.

    theorem secretaryChallenge_of_finiteRules.{u, v}
        (Q : ℕ → Type v) [∀ n, Fintype (Q n)] [∀ n, MeasurableSpace (Q n)]
        [∀ n, MeasurableSingletonClass (Q n)] (ν : (n : ℕ) → Measure (Q n))
        [∀ n, IsProbabilityMeasure (ν n)]
        (h : ∀ (n : ℕ) (M : Matroid (Fin n)), M.E = Set.univ →
          ∃ A : SecretaryRule n (Q n), SecretaryFeasible M A ∧
            SecretaryGuarantee.{u} M A (ν n) (((2 : ℝ) ^ 293)⁻¹)) :
        SecretaryChallenge.{u} := by
    …

    Mentions: OAI.MatroidProphet.SecretaryRule, OAI.MatroidProphet.SecretaryFeasible