RelabelingProbability.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Probability-law reindexing, including the full-seed almighty-adversary simulation, on arbitrary finite label types.

theorem OAI.MatroidProphet.Relabeling.paired_independent_encode line 16
Source documentation
Mutual independence of all paired source coordinates is preserved exactly by labeling.
```
theorem paired_independent_encode (e : α ≃ Fin n) (μ : Measure Ω)
    (S V : Ω → α → ℝ) (hi : iIndepFun (labeledPairedCoordinates S V) μ) :
    iIndepFun (pairedCoordinates (fun ω => encodeWeights e (S ω))
      (fun ω => encodeWeights e (V ω))) μ := by
…
```
Mentions: OAI.MatroidProphet.Relabeling.labeledPairedCoordinates, OAI.MatroidProphet.pairedCoordinates, OAI.MatroidProphet.Relabeling.encodeWeights

theorem OAI.MatroidProphet.Relabeling.seed_independent_encode line 31

Source documentation

Joint independence from the complete seed survives reindexing both vectors.

theorem seed_independent_encode (e : α ≃ Fin n) (μ : Measure Ω)
    (S V : Ω → α → ℝ) (R : Ω → Seed bits)
    (h : IndepFun (fun ω => (S ω, V ω)) R μ) :
    IndepFun (fun ω => (encodeWeights e (S ω), encodeWeights e (V ω))) R μ := by
…

Mentions: OAI.MatroidProphet.Seed, OAI.MatroidProphet.Relabeling.encodeWeights

theorem OAI.MatroidProphet.Relabeling.matching_laws_encode line 40

Source documentation

Enumeration changes no observed coordinate law.

theorem matching_laws_encode (e : α ≃ Fin n) (μ : Measure Ω)
    (S V : Ω → α → ℝ)
    (h : ∀ a, μ.map (fun ω => S ω a) = μ.map (fun ω => V ω a)) :
    ∀ i, μ.map (fun ω => encodeWeights e (S ω) i) =
      μ.map (fun ω => encodeWeights e (V ω) i) := by
…

Mentions: OAI.MatroidProphet.Relabeling.encodeWeights

theorem OAI.MatroidProphet.Relabeling.measurable_encoded_order line 49

Source documentation

No independence is imposed on the order when changing its label representation.

theorem measurable_encoded_order [Fintype α]
    [MeasurableSpace (LabeledOrder α n)] [MeasurableSingletonClass (LabeledOrder α n)]
    (e : α ≃ Fin n) (π : Ω → LabeledOrder α n) (hπ : Measurable π) :
    Measurable (fun ω => (π ω).trans e) :=
…

Mentions: OAI.MatroidProphet.Relabeling.LabeledOrder

theorem OAI.MatroidProphet.Relabeling.oneSample_of_hidden_labeled line 59

Source documentation

Full one-sample expected-minimum simulation on original finite labels. The hypotheses are exactly the hidden-rule guarantee and source probability hypotheses; in particular the adversarial permutation need not be independent of any sample, value, or seed information.

theorem oneSample_of_hidden_labeled [Fintype α]
    [MeasurableSpace (LabeledOrder α n)] [MeasurableSingletonClass (LabeledOrder α n)]
    (M : Matroid α) (e : α ≃ Fin n) (A : HiddenRule n bits)
    (ν : Measure (Seed bits)) [IsProbabilityMeasure ν] (c : ℝ)
    (hA : ∀ (w : Weights n), (∀ i, 0 ≤ w i) →
      ∀ (r : Seed bits) (π : ArrivalOrder n) (t : ℕ),
        (M.mapEquiv e).Indep (hiddenAcceptedThrough A r w π t : Set (Fin n)))
    (hbound : ∀ (w : Weights n), (∀ i, 0 ≤ w i) →
      c * optimum (M.mapEquiv e) w ≤ ∫ r, hiddenWorstReward A w r ∂ν)
    (μ : Measure Ω) [IsProbabilityMeasure μ]
    (S V : Ω → α → ℝ) (R : Ω → Seed bits)
    (hS : Measurable S) (hV : Measurable V) (hR : Measurable R)
…

Mentions: OAI.MatroidProphet.Relabeling.LabeledOrder, OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenAcceptedThrough, OAI.MatroidProphet.optimum, OAI.MatroidProphet.hiddenWorstReward