OAI/Probability/MatroidSecretary/Secretary/TripleKernel.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Explicit normalized one-label reconstruction kernel from secretary.tex, lines 64--81. These are finite identities, including the zero-mask case.

  1. lemma OAI.MatroidProphet.Secretary.tripleWeight_sum line 16
  2. lemma OAI.MatroidProphet.Secretary.tripleWeight_nonneg line 20
  3. lemma OAI.MatroidProphet.Secretary.tripleWeight_zero line 25
  4. lemma OAI.MatroidProphet.Secretary.mainRevealRate_eq_source line 29
  5. lemma OAI.MatroidProphet.Secretary.mainRevealRate_pos line 33
  6. lemma OAI.MatroidProphet.Secretary.mainRevealRate_lt_one line 36
  7. lemma OAI.MatroidProphet.Secretary.mainRevealRate_complement line 39
  8. lemma OAI.MatroidProphet.Secretary.tripleRevealed_eq_false line 44
  9. lemma OAI.MatroidProphet.Secretary.conditionalTripleWeight_nonneg line 49
  10. lemma OAI.MatroidProphet.Secretary.conditionalTripleWeight_sum line 60
  11. lemma OAI.MatroidProphet.Secretary.conditionalTripleWeight_support line 70
  12. lemma OAI.MatroidProphet.Secretary.conditionalTripleWeight_joint line 78

    Source documentation

    Multiplying the explicit conditional kernel by the observed-bit law recovers the original joint law, not just a marginal event probability.

    lemma conditionalTripleWeight_joint (b : Bool) (x : MaskTriple) :
    revealBitWeight b * conditionalTripleWeight b x =
      if tripleRevealed x = b then tripleWeight thinningRate x else 0 := by
…

    Mentions: OAI.MatroidProphet.Secretary.MaskTriple, OAI.MatroidProphet.Secretary.revealBitWeight, OAI.MatroidProphet.Secretary.conditionalTripleWeight, OAI.MatroidProphet.Secretary.tripleRevealed, OAI.MatroidProphet.Secretary.tripleWeight, OAI.MatroidProphet.thinningRate

  13. lemma OAI.MatroidProphet.Secretary.conditionalTripleWeight_reconstruct line 87
  14. lemma OAI.MatroidProphet.Secretary.revealBitWeight_pos line 93
  15. lemma OAI.MatroidProphet.Secretary.revealBitWeight_sum line 98
  16. lemma OAI.MatroidProphet.Secretary.tripleWeight_source_pos line 101
  17. lemma OAI.MatroidProphet.Secretary.card_revealed_triples line 107

    Source documentation

    Exactly seven triples are compatible with an observed label.

    lemma card_revealed_triples :
    Fintype.card {x : MaskTriple // tripleRevealed x = true} = 7 := by decide

    Mentions: OAI.MatroidProphet.Secretary.MaskTriple, OAI.MatroidProphet.Secretary.tripleRevealed

  18. lemma OAI.MatroidProphet.Secretary.conditionalTripleWeight_pos_iff line 110