AdversarialMinimum.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.MatroidProphet.integrable_hiddenReward_randomOrder line 13
Source documentation
For a fixed vector, arbitrary measurable seed-dependent orders give an integrable reward under every finite measure. No feasibility or sign assumption is needed, since the seed and order spaces are finite.
```
lemma integrable_hiddenReward_randomOrder {n bits : ℕ} (A : HiddenRule n bits)
    (w : Weights n) {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) [IsFiniteMeasure μ]
    (R : Ω → Seed bits) (π : Ω → ArrivalOrder n)
    (hR : Measurable R) (hπ : Measurable π) :
    Integrable (fun ω => hiddenReward A (R ω) w (π ω)) μ := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Weights, OAI.MatroidProphet.Seed, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenReward

lemma OAI.MatroidProphet.integrable_hiddenWorstReward_comp line 26

Source documentation

The seedwise minimum is integrable after any measurable finite-seed map.

lemma integrable_hiddenWorstReward_comp {n bits : ℕ} (A : HiddenRule n bits)
    (w : Weights n) {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) [IsFiniteMeasure μ]
    (R : Ω → Seed bits) (hR : Measurable R) :
    Integrable (fun ω => hiddenWorstReward A w (R ω)) μ := by
…

Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Weights, OAI.MatroidProphet.Seed, OAI.MatroidProphet.hiddenWorstReward

theorem OAI.MatroidProphet.hiddenWorstReward_integral_le_randomOrder line 38
Source documentation
A reconstructed seed's correct marginal transports the expected minimum to any measurable full-information order. The order need not be independent of the seed, and the ambient space may carry arbitrarily much additional information.
```
theorem hiddenWorstReward_integral_le_randomOrder {n bits : ℕ}
    (A : HiddenRule n bits) (w : Weights n)
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsFiniteMeasure μ]
    (ν : Measure (Seed bits)) (R : Ω → Seed bits) (π : Ω → ArrivalOrder n)
    (hR : Measurable R) (hπ : Measurable π) (hRlaw : μ.map R = ν) :
    (∫ r, hiddenWorstReward A w r ∂ν) ≤
      ∫ ω, hiddenReward A (R ω) w (π ω) ∂μ := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Weights, OAI.MatroidProphet.Seed, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenWorstReward, OAI.MatroidProphet.hiddenReward

theorem OAI.MatroidProphet.hiddenWorstReward_integral_le_replayed line 55

Source documentation

A pointwise accepted-reward identity may be replaced by an almost-everywhere identity. This is useful when a reconstruction kernel has zero-mass seed outcomes.

theorem hiddenWorstReward_integral_le_replayed {n bits : ℕ}
    (A : HiddenRule n bits) (w : Weights n)
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsFiniteMeasure μ]
    (ν : Measure (Seed bits)) (R : Ω → Seed bits) (π : Ω → ArrivalOrder n)
    (hR : Measurable R) (hπ : Measurable π) (hRlaw : μ.map R = ν)
    (payoff : Ω → ℝ)
    (hreplay : payoff =ᵐ[μ] fun ω => hiddenReward A (R ω) w (π ω)) :
    Integrable payoff μ ∧ (∫ r, hiddenWorstReward A w r ∂ν) ≤ ∫ ω, payoff ω ∂μ := by
…

Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Weights, OAI.MatroidProphet.Seed, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenReward, OAI.MatroidProphet.hiddenWorstReward

lemma OAI.MatroidProphet.exists_measurable_worstOrder line 70
Source documentation
There is a measurable adversary attaining the minimum separately at every seed. Thus the minimum used above is genuinely inside expectation, not the minimum of fixed-order expected rewards.
```
lemma exists_measurable_worstOrder {n bits : ℕ} (A : HiddenRule n bits)
    (w : Weights n) :
    ∃ π : Seed bits → ArrivalOrder n, Measurable π ∧
      ∀ r, hiddenReward A r w (π r) = hiddenWorstReward A w r := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Weights, OAI.MatroidProphet.Seed, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenReward, OAI.MatroidProphet.hiddenWorstReward
lemma OAI.MatroidProphet.exists_order_integral_eq_hiddenWorstReward line 85
Source documentation
The lower bound is sharp among measurable full-seed order policies.
```
lemma exists_order_integral_eq_hiddenWorstReward {n bits : ℕ}
    (A : HiddenRule n bits) (w : Weights n) (ν : Measure (Seed bits)) :
    ∃ π : Seed bits → ArrivalOrder n, Measurable π ∧
      (∫ r, hiddenReward A r w (π r) ∂ν) = ∫ r, hiddenWorstReward A w r ∂ν := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Weights, OAI.MatroidProphet.Seed, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenReward, OAI.MatroidProphet.hiddenWorstReward