LabeledTransport.lean`

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MatroidProphet.LabeledTransport.optimum line 14
Source documentation
The same offline maximum on an arbitrary finite label type.
```
noncomputable def optimum (M : Matroid α) (w : α → ℝ) : ℝ := by
…
```
theorem OAI.MatroidProphet.LabeledTransport.sum_le_optimum line 19
theorem OAI.MatroidProphet.LabeledTransport.optimum_nonneg line 27
theorem OAI.MatroidProphet.LabeledTransport.mapEquiv_ground line 32
Source documentation
Relabeling preserves the full ground set; it does not discard loops.
```
theorem mapEquiv_ground (M : Matroid α) (hE : M.E = Set.univ)
    (e : α ≃ Fin n) : (M.mapEquiv e).E = Set.univ := by
…
```
theorem OAI.MatroidProphet.LabeledTransport.optimum_eq_indexed line 37
Source documentation
The all-independent-sets benchmark is exactly unchanged by label encoding.
```
theorem optimum_eq_indexed (M : Matroid α) (e : α ≃ Fin n) (w : α → ℝ) :
    optimum M w = MatroidProphet.optimum (M.mapEquiv e) (w ∘ e.symm) := by
…
```
Mentions: OAI.MatroidProphet.LabeledTransport.optimum, OAI.MatroidProphet.optimum
abbrev OAI.MatroidProphet.LabeledTransport.History line 59
abbrev OAI.MatroidProphet.LabeledTransport.ArrivalOrder line 62
Source documentation
A physical arrival order visits every label once, indexed by arrival time.
```
abbrev ArrivalOrder (α : Type*) (n : ℕ) := Fin n ≃ α
```
instance OAI.MatroidProphet.LabeledTransport.arrivalOrderMeasurableSpace line 64
instance OAI.MatroidProphet.LabeledTransport.arrivalOrderMeasurableSingletonClass line 66
structure OAI.MatroidProphet.LabeledTransport.OnlineRule line 72
Source documentation
A rule on physical labels receives only the same sample and history data.
```
structure OnlineRule (α : Type*) [MeasurableSpace α] (n bits : ℕ) where
…
```
def OAI.MatroidProphet.LabeledTransport.encodeHistory line 77
def OAI.MatroidProphet.LabeledTransport.decodeRule line 81
Source documentation
Decode the indexed rule without adding any future-information input.
```
noncomputable def decodeRule (e : α ≃ Fin n) (A : MatroidProphet.OnlineRule n bits) :
    OnlineRule α n bits where
…
```
Mentions: OAI.MatroidProphet.OnlineRule, OAI.MatroidProphet.LabeledTransport.OnlineRule
def OAI.MatroidProphet.LabeledTransport.history line 102
def OAI.MatroidProphet.LabeledTransport.decisionAt line 105
def OAI.MatroidProphet.LabeledTransport.acceptedThrough line 108
def OAI.MatroidProphet.LabeledTransport.reward line 113
theorem OAI.MatroidProphet.LabeledTransport.encode_history line 118
theorem OAI.MatroidProphet.LabeledTransport.decode_decision line 124
theorem OAI.MatroidProphet.LabeledTransport.decode_acceptedThrough line 130
theorem OAI.MatroidProphet.LabeledTransport.decode_reward line 142
theorem OAI.MatroidProphet.LabeledTransport.decode_feasible line 149
Source documentation
Prefix feasibility transports back to the original labels, including loops.
```
theorem decode_feasible (M : Matroid α) (e : α ≃ Fin n)
    (A : MatroidProphet.OnlineRule n bits) (hA : Feasible (M.mapEquiv e) A)
    (r : Seed bits) (s w : α → ℝ) (π : ArrivalOrder α n) (t : ℕ)
    (hs : ∀ a, 0 ≤ s a) (hw : ∀ a, 0 ≤ w a) :
    M.Indep (acceptedThrough (decodeRule e A) r s w π t : Set α) := by
…
```
Mentions: OAI.MatroidProphet.OnlineRule, OAI.MatroidProphet.Feasible, OAI.MatroidProphet.Seed, OAI.MatroidProphet.LabeledTransport.ArrivalOrder, OAI.MatroidProphet.LabeledTransport.acceptedThrough, OAI.MatroidProphet.LabeledTransport.decodeRule