FiniteSeedTheorems.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Exact finite-seed encoding, measurability, and law preservation.

lemma OAI.MatroidProphet.finiteSeedEncode_injective line 15
lemma OAI.MatroidProphet.finiteSeedDecode_encode line 27
lemma OAI.MatroidProphet.measurable_finiteSeedEncode line 34
lemma OAI.MatroidProphet.measurable_finiteSeedDecode line 38
theorem OAI.MatroidProphet.finiteSeed_map_roundtrip line 42
Source documentation
The full original law is recovered, not merely the law of a used statistic.
```
theorem finiteSeed_map_roundtrip (μ : Measure α) :
    (μ.map (finiteSeedEncode α)).map (finiteSeedDecode α) = μ := by
…
```
Mentions: OAI.MatroidProphet.finiteSeedEncode, OAI.MatroidProphet.finiteSeedDecode
theorem OAI.MatroidProphet.finiteSeed_decode_measurePreserving line 49
Source documentation
Decoding the encoded law preserves every event of the original seed.
```
theorem finiteSeed_decode_measurePreserving (μ : Measure α) :
    MeasurePreserving (finiteSeedDecode α) (μ.map (finiteSeedEncode α)) μ :=
…
```
Mentions: OAI.MatroidProphet.finiteSeedDecode, OAI.MatroidProphet.finiteSeedEncode
theorem OAI.MatroidProphet.finiteSeed_integral_decode line 54
Source documentation
Arbitrary real payoff statistics have exactly the same expectation.
```
theorem finiteSeed_integral_decode (μ : Measure α) (g : α → ℝ) :
    (∫ r, g (finiteSeedDecode α r) ∂μ.map (finiteSeedEncode α)) = ∫ a, g a ∂μ := by
…
```
Mentions: OAI.MatroidProphet.finiteSeedDecode, OAI.MatroidProphet.finiteSeedEncode

theorem OAI.MatroidProphet.finiteSeed_indepFun_iff line 62

Source documentation

Encoding a full seed does not change its independence from any other data.

theorem finiteSeed_indepFun_iff {Ω β : Type*} [MeasurableSpace Ω] [MeasurableSpace β]
    (μ : Measure Ω) (X : Ω → β) (R : Ω → α) :
    ProbabilityTheory.IndepFun X (finiteSeedEncode α ∘ R) μ ↔
      ProbabilityTheory.IndepFun X R μ := by
…

Mentions: OAI.MatroidProphet.finiteSeedEncode

theorem OAI.MatroidProphet.reindexOnlineSeed_decisionAt line 78
theorem OAI.MatroidProphet.reindexOnlineSeed_acceptedThrough line 82
theorem OAI.MatroidProphet.reindexOnlineSeed_reward line 87
theorem OAI.MatroidProphet.reindexOnlineSeed_feasible line 92
Source documentation
Total decoding also preserves feasibility on encodings outside the support.
```
theorem reindexOnlineSeed_feasible (M : Matroid (Fin n)) (hA : Feasible M A) :
    Feasible M (reindexOnlineSeed A f) := by
…
```
Mentions: OAI.MatroidProphet.Feasible, OAI.MatroidProphet.reindexOnlineSeed
theorem OAI.MatroidProphet.reindexHiddenSeed_acceptedThrough line 99
theorem OAI.MatroidProphet.reindexHiddenSeed_reward line 104
theorem OAI.MatroidProphet.reindexHiddenSeed_worstReward line 108
theorem OAI.MatroidProphet.reindexHiddenSeed_integral line 112
Source documentation
No independence of the adversary from the reindexed seed is used.
```
theorem reindexHiddenSeed_integral (ν' : Measure (Seed bits'))
    (ν : Measure (Seed bits)) (hlaw : ν'.map f = ν) (w : Weights n) :
    (∫ r, hiddenWorstReward (reindexHiddenSeed H f) w r ∂ν') =
      ∫ r, hiddenWorstReward H w r ∂ν := by
…
```
Mentions: OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.hiddenWorstReward, OAI.MatroidProphet.reindexHiddenSeed