RelabelingTheorems.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Exact transport from arbitrary finite labels to the Fin n information model.

lemma OAI.MatroidProphet.Relabeling.sum_le_finiteOptimum line 15
lemma OAI.MatroidProphet.Relabeling.finiteOptimum_nonneg line 24
lemma OAI.MatroidProphet.Relabeling.finiteOptimum_le line 28
theorem OAI.MatroidProphet.Relabeling.finiteOptimum_mapEquiv line 39
Source documentation
Changing finite labels preserves the exact offline optimum, for arbitrary real weights.
```
theorem finiteOptimum_mapEquiv [Fintype α] [Fintype β]
    (M : Matroid α) (e : α ≃ β) (w : α → ℝ) :
    finiteOptimum (M.mapEquiv e) (encodeWeights e w) = finiteOptimum M w := by
…
```
Mentions: OAI.MatroidProphet.Relabeling.finiteOptimum, OAI.MatroidProphet.Relabeling.encodeWeights
theorem OAI.MatroidProphet.Relabeling.finiteOptimum_fin line 56
theorem OAI.MatroidProphet.Relabeling.encodeWeights_nonnegative_iff line 59
theorem OAI.MatroidProphet.Relabeling.mapEquiv_ground_univ line 67
theorem OAI.MatroidProphet.Relabeling.mapEquiv_loop_iff line 71
theorem OAI.MatroidProphet.Relabeling.exists_fin_representation line 77
Source documentation
Every finite labeled matroid has a full-ground Fin n representative with exactly the original offline benchmark and all loop labels retained.
```
theorem exists_fin_representation [Fintype α] (M : Matroid α) (hE : M.E = Set.univ) :
    ∃ (e : α ≃ Fin (Fintype.card α)),
      (M.mapEquiv e).E = Set.univ ∧
      (∀ w : α → ℝ, optimum (M.mapEquiv e) (encodeWeights e w) = finiteOptimum M w) ∧
      (∀ a, (M.mapEquiv e).IsLoop (e a) ↔ M.IsLoop a) := by
…
```
Mentions: OAI.MatroidProphet.optimum, OAI.MatroidProphet.Relabeling.encodeWeights, OAI.MatroidProphet.Relabeling.finiteOptimum
theorem OAI.MatroidProphet.Relabeling.measurable_encodeWeights line 89
Source documentation
Coordinate reindexing is Borel, with no regularity assumption on weights.
```
theorem measurable_encodeWeights (e : α ≃ β) : Measurable (encodeWeights e) := by
…
```
Mentions: OAI.MatroidProphet.Relabeling.encodeWeights
theorem OAI.MatroidProphet.Relabeling.measurable_encodeHistory line 94
theorem OAI.MatroidProphet.Relabeling.measurable_transportedDecision line 103
Source documentation
The transported rule is measurable in precisely its permissible inputs.
```
theorem measurable_transportedDecision [Fintype α] [MeasurableSpace α]
    [MeasurableSingletonClass α] {n bits : ℕ} (e : α ≃ Fin n)
    (A : OnlineRule n bits) (k : Fin n) :
    Measurable (fun x : Seed bits × ((α → ℝ) × LabeledHistory α k) =>
      transportedDecision e A k x.1 x.2.1 x.2.2) := by
…
```
Mentions: OAI.MatroidProphet.OnlineRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Relabeling.LabeledHistory, OAI.MatroidProphet.Relabeling.transportedDecision
theorem OAI.MatroidProphet.Relabeling.encodeHistory_labeledHistory line 113
theorem OAI.MatroidProphet.Relabeling.transportedDecision_eq_decisionAt line 120
theorem OAI.MatroidProphet.Relabeling.transportedAcceptedThrough_eq_map line 128
Source documentation
Exact accepted-set equality holds at every prefix, not just at termination.
```
theorem transportedAcceptedThrough_eq_map [Fintype α] {n bits : ℕ}
    (e : α ≃ Fin n) (A : OnlineRule n bits) (r : Seed bits)
    (s v : α → ℝ) (π : LabeledOrder α n) (t : ℕ) :
    transportedAcceptedThrough e A r s v π t =
      (acceptedThrough A r (encodeWeights e s) (encodeWeights e v)
        (π.trans e) t).map e.symm.toEmbedding := by
…
```
Mentions: OAI.MatroidProphet.OnlineRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Relabeling.LabeledOrder, OAI.MatroidProphet.Relabeling.transportedAcceptedThrough, OAI.MatroidProphet.acceptedThrough, OAI.MatroidProphet.Relabeling.encodeWeights
theorem OAI.MatroidProphet.Relabeling.transportedReward_eq_reward line 143
Source documentation
The cardinal relabeling preserves the actual sum of accepted weights exactly.
```
theorem transportedReward_eq_reward [Fintype α] {n bits : ℕ}
    (e : α ≃ Fin n) (A : OnlineRule n bits) (r : Seed bits)
    (s v : α → ℝ) (π : LabeledOrder α n) :
    transportedReward e A r s v π =
      reward A r (encodeWeights e s) (encodeWeights e v) (π.trans e) := by
…
```
Mentions: OAI.MatroidProphet.OnlineRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Relabeling.LabeledOrder, OAI.MatroidProphet.Relabeling.transportedReward, OAI.MatroidProphet.reward, OAI.MatroidProphet.Relabeling.encodeWeights

theorem OAI.MatroidProphet.Relabeling.transported_feasible line 151

Source documentation

Every-prefix feasibility transfers without dropping loops or exceptional inputs.

theorem transported_feasible [Fintype α] {n bits : ℕ}
    (M : Matroid α) (e : α ≃ Fin n) (A : OnlineRule n bits)
    (hA : Feasible (M.mapEquiv e) A) (r : Seed bits)
    (s v : α → ℝ) (π : LabeledOrder α n) (t : ℕ)
    (hs : ∀ a, 0 ≤ s a) (hv : ∀ a, 0 ≤ v a) :
    M.Indep (transportedAcceptedThrough e A r s v π t : Set α) := by
…

Mentions: OAI.MatroidProphet.OnlineRule, OAI.MatroidProphet.Feasible, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Relabeling.LabeledOrder, OAI.MatroidProphet.Relabeling.transportedAcceptedThrough

theorem OAI.MatroidProphet.Relabeling.transportedAcceptedThrough_mono line 163
Source documentation
The relabeled implementation retains every previous acceptance irrevocably.
```
theorem transportedAcceptedThrough_mono [Fintype α] {n bits : ℕ}
    (e : α ≃ Fin n) (A : OnlineRule n bits) (r : Seed bits)
    (s v : α → ℝ) (π : LabeledOrder α n) {t t' : ℕ} (htt' : t ≤ t') :
    transportedAcceptedThrough e A r s v π t ⊆
      transportedAcceptedThrough e A r s v π t' := by
…
```
Mentions: OAI.MatroidProphet.OnlineRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Relabeling.LabeledOrder, OAI.MatroidProphet.Relabeling.transportedAcceptedThrough