Relabeling.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MatroidProphet.Relabeling.orderEquiv line 15
Source documentation
Bijective enumeration of complete arrival lists; the arrival index is unchanged.
```
def orderEquiv (e : α ≃ Fin n) : LabeledOrder α n ≃ ArrivalOrder n where
…
```
Mentions: OAI.MatroidProphet.Relabeling.LabeledOrder, OAI.MatroidProphet.ArrivalOrder
def OAI.MatroidProphet.Relabeling.transportedSecretaryDecision line 22
Source documentation
Exact decision on original labels, reading only the current available history.
```
def transportedSecretaryDecision (e : α ≃ Fin n) (A : SecretaryRule n Q)
    (k : Fin n) (q : Q) (h : LabeledHistory α k) : Bool :=
…
```
Mentions: OAI.MatroidProphet.SecretaryRule, OAI.MatroidProphet.Relabeling.LabeledHistory
def OAI.MatroidProphet.Relabeling.transportedSecretaryAcceptedThrough line 27
def OAI.MatroidProphet.Relabeling.transportedSecretaryReward line 35
theorem OAI.MatroidProphet.Relabeling.measurable_transportedSecretaryDecision line 40
theorem OAI.MatroidProphet.Relabeling.transportedSecretaryDecision_eq line 53
theorem OAI.MatroidProphet.Relabeling.transportedSecretaryAcceptedThrough_eq_map line 62
Source documentation
Every acceptance, at every prefix, is transported by the label bijection.
```
theorem transportedSecretaryAcceptedThrough_eq_map [Fintype α]
    (e : α ≃ Fin n) (A : SecretaryRule n Q) (q : Q) (w : α → ℝ)
    (π : LabeledOrder α n) (t : ℕ) :
    transportedSecretaryAcceptedThrough e A q w π t =
      (secretaryAcceptedThrough A q (encodeWeights e w) (π.trans e) t).map
        e.symm.toEmbedding := by
…
```
Mentions: OAI.MatroidProphet.SecretaryRule, OAI.MatroidProphet.Relabeling.LabeledOrder, OAI.MatroidProphet.Relabeling.transportedSecretaryAcceptedThrough, OAI.MatroidProphet.secretaryAcceptedThrough, OAI.MatroidProphet.Relabeling.encodeWeights
theorem OAI.MatroidProphet.Relabeling.transportedSecretaryReward_eq line 77
Source documentation
The accepted real-valued payoff is unchanged, without positivity assumptions.
```
theorem transportedSecretaryReward_eq [Fintype α]
    (e : α ≃ Fin n) (A : SecretaryRule n Q) (q : Q) (w : α → ℝ)
    (π : LabeledOrder α n) :
    transportedSecretaryReward e A q w π =
      secretaryReward A q (encodeWeights e w) (π.trans e) := by
…
```
Mentions: OAI.MatroidProphet.SecretaryRule, OAI.MatroidProphet.Relabeling.LabeledOrder, OAI.MatroidProphet.Relabeling.transportedSecretaryReward, OAI.MatroidProphet.secretaryReward, OAI.MatroidProphet.Relabeling.encodeWeights
theorem OAI.MatroidProphet.Relabeling.transportedSecretary_feasible line 86
Source documentation
Feasibility includes all seeds, all prefixes and the empty ground set.
```
theorem transportedSecretary_feasible [Fintype α]
    (M : Matroid α) (e : α ≃ Fin n) (A : SecretaryRule n Q)
    (hA : SecretaryFeasible (M.mapEquiv e) A)
    (q : Q) (w : α → ℝ) (hw : ∀ a, 0 ≤ w a)
    (π : LabeledOrder α n) (t : ℕ) :
    M.Indep (transportedSecretaryAcceptedThrough e A q w π t : Set α) := by
…
```
Mentions: OAI.MatroidProphet.SecretaryRule, OAI.MatroidProphet.SecretaryFeasible, OAI.MatroidProphet.Relabeling.LabeledOrder, OAI.MatroidProphet.Relabeling.transportedSecretaryAcceptedThrough
theorem OAI.MatroidProphet.Relabeling.samePrefix_encode_iff line 98
Source documentation
Equality of actual ordered prefixes is invariant under reindexing.
```
theorem samePrefix_encode_iff (e : α ≃ Fin n) (K : ℕ)
    (σ π : LabeledOrder α n) :
    SamePrefix K (σ.trans e) (π.trans e) ↔
      ∀ k : Fin n, k.val < K → σ k = π k := by
…
```
Mentions: OAI.MatroidProphet.Relabeling.LabeledOrder, OAI.MatroidProphet.SamePrefix
theorem OAI.MatroidProphet.Relabeling.transportedSecretary_rejects_prefix line 105
Source documentation
Observation-prefix labels are never accepted after reindexing.
```
theorem transportedSecretary_rejects_prefix [Fintype α]
    (e : α ≃ Fin n) (A : SecretaryRule n Q) (q : Q) (w : α → ℝ)
    (π : LabeledOrder α n) (t : ℕ) (a : α)
    (ha : (π.symm a).val < (A.prefixLength q).val) :
    a ∉ transportedSecretaryAcceptedThrough e A q w π t := by
…
```
Mentions: OAI.MatroidProphet.SecretaryRule, OAI.MatroidProphet.Relabeling.LabeledOrder, OAI.MatroidProphet.Relabeling.transportedSecretaryAcceptedThrough

theorem OAI.MatroidProphet.Relabeling.uniform_measure_map_equiv line 114

Source documentation

Uniform finite laws are preserved by a genuine equivalence, including singleton laws.

theorem uniform_measure_map_equiv {β γ : Type*} [Fintype β] [Fintype γ]
    [Nonempty β] [Nonempty γ] [MeasurableSpace β] [MeasurableSpace γ]
    [MeasurableSingletonClass β] [MeasurableSingletonClass γ] (e : β ≃ γ) :
    (PMF.uniformOfFintype β).toMeasure.map e = (PMF.uniformOfFintype γ).toMeasure := by
…

def OAI.MatroidProphet.Relabeling.labeledUniformArrivalLaw line 134
Source documentation
The original-label arrival law is literally uniform over all enumerations.
```
noncomputable def labeledUniformArrivalLaw [Fintype α] (e : α ≃ Fin n)
    [MeasurableSpace (LabeledOrder α n)] : Measure (LabeledOrder α n) := by
…
```
Mentions: OAI.MatroidProphet.Relabeling.LabeledOrder
theorem OAI.MatroidProphet.Relabeling.labeledUniformArrivalLaw_map line 140

theorem OAI.MatroidProphet.Relabeling.secretary_guarantee_labeled line 152

Source documentation

Full expected guarantee on the original labels. The fixed rule and seed law are chosen before the input vector and the probability space. Reindexing assumes no independence for the executed order and retains every full-seed adversary.

theorem secretary_guarantee_labeled.{u} [Fintype α]
    [MeasurableSpace (LabeledOrder α n)] [MeasurableSingletonClass (LabeledOrder α n)]
    (M : Matroid α) (e : α ≃ Fin n) (A : SecretaryRule n Q)
    (ν : Measure Q) (c : ℝ) (h : SecretaryGuarantee.{u} (M.mapEquiv e) A ν c)
    (w : α → ℝ) (hw : ∀ a, 0 ≤ w a)
    {Ω : Type u} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]
    (R : Ω → Q) (σ π : Ω → LabeledOrder α n)
    (hR : Measurable R) (hσ : Measurable σ) (hπ : Measurable π)
    (hRlaw : μ.map R = ν) (hσlaw : μ.map σ = labeledUniformArrivalLaw e)
    (hind : IndepFun R σ μ)
    (hprefix : ∀ᵐ ω ∂μ, ∀ k : Fin n, k.val < (A.prefixLength (R ω)).val →
      σ ω k = π ω k) :
…

Mentions: OAI.MatroidProphet.Relabeling.LabeledOrder, OAI.MatroidProphet.SecretaryRule, OAI.MatroidProphet.Relabeling.labeledUniformArrivalLaw

theorem OAI.MatroidProphet.Relabeling.exists_labeled_secretary line 187

Source documentation

An actual unconditional secretary witness for every finite label type. The enumeration is fixed before weights or randomness; its choice imposes no positive-size, positive-rank, or nonloop assumption.

theorem exists_labeled_secretary.{u} [Fintype α]
    [MeasurableSpace α] [MeasurableSingletonClass α]
    [MeasurableSpace (LabeledOrder α n)] [MeasurableSingletonClass (LabeledOrder α n)]
    (M : Matroid α) (hE : M.E = Set.univ) (e : α ≃ Fin n) :
    ∃ (q : ℕ) (ν : Measure (Fin q)), IsProbabilityMeasure ν ∧
      ∃ (A : SecretaryRule n (Fin q)),
        (∀ k : Fin n, Measurable (fun x : Fin q × LabeledHistory α k =>
          transportedSecretaryDecision e A k x.1 x.2)) ∧
        (∀ (r : Fin q) (w : α → ℝ), (∀ a, 0 ≤ w a) →
          ∀ (π : LabeledOrder α n) (t : ℕ),
            M.Indep (transportedSecretaryAcceptedThrough e A r w π t : Set α)) ∧
        ∀ (w : α → ℝ), (∀ a, 0 ≤ w a) →
…

Mentions: OAI.MatroidProphet.Relabeling.LabeledOrder, OAI.MatroidProphet.SecretaryRule, OAI.MatroidProphet.Relabeling.LabeledHistory, OAI.MatroidProphet.Relabeling.transportedSecretaryDecision, OAI.MatroidProphet.Relabeling.transportedSecretaryAcceptedThrough