OAI/Probability/MatroidSecretary/Secretary/Observation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatroidProphet.mem_orderPrefix line 10
2. lemma OAI.MatroidProphet.prefixLabels_zero line 14
3. lemma OAI.MatroidProphet.prefixWeights_zero line 18
4. lemma OAI.MatroidProphet.prefixLabels_history line 23
5. lemma OAI.MatroidProphet.measurable_prefixLabels line 44

   Source documentation

   Prefix-label extraction is measurable despite the real-valued history entries.

   lemma measurable_prefixLabels {n : ℕ} (k : Fin n) (K : ℕ) :
       Measurable (prefixLabels (k := k) K) := by
   …

   Mentions: OAI.MatroidProphet.prefixLabels

6. lemma OAI.MatroidProphet.prefixWeights_congr line 55

   Source documentation

   Changing the suffix entries of an available history does not change prefix data.

   lemma prefixWeights_congr {n : ℕ} {k : Fin n} (K : ℕ) (h h' : History n k)
       (hh : ∀ j, j.val < K → h j = h' j) :
       prefixWeights K h = prefixWeights K h' := by
   …

   Mentions: OAI.MatroidProphet.History, OAI.MatroidProphet.prefixWeights

7. lemma OAI.MatroidProphet.prefixLabels_congr line 65
8. lemma OAI.MatroidProphet.measurable_prefixWeights line 72
9. lemma OAI.MatroidProphet.measurable_prefixWeights_seed line 91

   Source documentation

   Seed-dependent cutoff extraction remains measurable jointly with the history.

   lemma measurable_prefixWeights_seed {n : ℕ} {Q : Type*} [MeasurableSpace Q]
       (k : Fin n) (K : Q → Fin (n + 1)) (hK : Measurable K) :
       Measurable (fun x : Q × History n k => prefixWeights (K x.1).val x.2) := by
   …

   Mentions: OAI.MatroidProphet.History, OAI.MatroidProphet.prefixWeights

10. lemma OAI.MatroidProphet.measurable_prefixLabels_seed line 99
11. lemma OAI.MatroidProphet.prefixWeights_history line 107
12. lemma OAI.MatroidProphet.prefixWeights_eq_observed line 147
13. lemma OAI.MatroidProphet.hiddenAcceptedThrough_prefix_empty line 155