RelabelingModel.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MatroidProphet.Relabeling.finiteOptimum line 11
Source documentation
The offline benchmark on an arbitrary finite label type.
```
noncomputable def finiteOptimum {α : Type*} [Fintype α]
    (M : Matroid α) (w : α → ℝ) : ℝ := by
…
```
def OAI.MatroidProphet.Relabeling.encodeWeights line 18
Source documentation
Reindex all weights, retaining every label including loops and zero weights.
```
def encodeWeights {α β : Type*} (e : α ≃ β) (w : α → ℝ) : β → ℝ :=
…
```
def OAI.MatroidProphet.Relabeling.labeledPairedCoordinates line 22
Source documentation
Every sample and online coordinate, indexed by original label and copy.
```
def labeledPairedCoordinates {α Ω : Type*} (S V : Ω → α → ℝ)
    (i : α × Bool) : Ω → ℝ :=
…
```
abbrev OAI.MatroidProphet.Relabeling.LabeledOrder line 27
Source documentation
An arrival order on α lists every label exactly once.
```
abbrev LabeledOrder (α : Type*) (n : ℕ) := Fin n ≃ α
```
abbrev OAI.MatroidProphet.Relabeling.LabeledHistory line 30
Source documentation
The available prefix, with arbitrary original labels.
```
abbrev LabeledHistory (α : Type*) {n : ℕ} (k : Fin n) :=
…
```
def OAI.MatroidProphet.Relabeling.encodeHistory line 34
Source documentation
Reindex the labels of an observed history without changing any observed value.
```
def encodeHistory {α : Type*} {n : ℕ} (e : α ≃ Fin n) (k : Fin n)
    (h : LabeledHistory α k) : History n k :=
…
```
Mentions: OAI.MatroidProphet.Relabeling.LabeledHistory, OAI.MatroidProphet.History
def OAI.MatroidProphet.Relabeling.labeledHistory line 39
Source documentation
The history supplied by a genuine arrival stream on the original labels.
```
def labeledHistory {α : Type*} {n : ℕ} (w : α → ℝ)
    (π : LabeledOrder α n) (k : Fin n) : LabeledHistory α k :=
…
```
Mentions: OAI.MatroidProphet.Relabeling.LabeledOrder, OAI.MatroidProphet.Relabeling.LabeledHistory
def OAI.MatroidProphet.Relabeling.transportedDecision line 44
Source documentation
The transported decision uses only the seed, original samples, and history.
```
def transportedDecision {α : Type*} {n bits : ℕ} (e : α ≃ Fin n)
    (A : OnlineRule n bits) (k : Fin n) (r : Seed bits)
    (s : α → ℝ) (h : LabeledHistory α k) : Bool :=
…
```
Mentions: OAI.MatroidProphet.OnlineRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Relabeling.LabeledHistory
def OAI.MatroidProphet.Relabeling.transportedAcceptedThrough line 50
Source documentation
Irrevocable accepted labels in the original labeled stream.
```
noncomputable def transportedAcceptedThrough {α : Type*} [Fintype α]
    {n bits : ℕ} (e : α ≃ Fin n) (A : OnlineRule n bits)
    (r : Seed bits) (s v : α → ℝ) (π : LabeledOrder α n) (t : ℕ) : Finset α := by
…
```
Mentions: OAI.MatroidProphet.OnlineRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Relabeling.LabeledOrder
def OAI.MatroidProphet.Relabeling.transportedReward line 58
Source documentation
Real reward, with no rounding or loss in the relabeling.
```
noncomputable def transportedReward {α : Type*} [Fintype α]
    {n bits : ℕ} (e : α ≃ Fin n) (A : OnlineRule n bits)
    (r : Seed bits) (s v : α → ℝ) (π : LabeledOrder α n) : ℝ :=
…
```
Mentions: OAI.MatroidProphet.OnlineRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Relabeling.LabeledOrder