OptimumIntegrability.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The exact finite-moment requirement

For a finite matroid and nonnegative measurable weights, integrability of the actual offline optimum is equivalent to integrability of the nonloop coordinates. No loop-coordinate moments are imposed. This is a supporting scope check for introduction.tex, Theorem thm:main, and setup.tex's one-sample simulation argument; it does not replace its competitive claim.

theorem OAI.MatroidProphet.DegenerateCases.optimum_le_sum_nonloops line 23
Source documentation
Only nonloops can contribute to a feasible sum.
```
theorem optimum_le_sum_nonloops {n : ℕ} (M : Matroid (Fin n))
    (w : Weights n) (hw : ∀ e, 0 ≤ w e) :
    optimum M w ≤ ∑ e : Fin n, if M.IsNonloop e then w e else 0 := by
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.optimum

theorem OAI.MatroidProphet.DegenerateCases.integrable_nonloop_of_integrable_optimum line 43

Source documentation

Nonloop moments follow from the assumed finite offline optimum moment.

theorem integrable_nonloop_of_integrable_optimum {n : ℕ}
    (M : Matroid (Fin n)) {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) (V : Ω → Weights n) (hV : Measurable V)
    (hVN : ∀ᵐ ω ∂μ, ∀ e, 0 ≤ V ω e)
    (hopt : Integrable (fun ω => optimum M (V ω)) μ)
    (e : Fin n) (he : M.IsNonloop e) : Integrable (fun ω => V ω e) μ := by
…

Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.optimum

theorem OAI.MatroidProphet.DegenerateCases.integrable_optimum_of_integrable_nonloops line 56

Source documentation

Conversely, finite moments only on the nonloops suffice for finite E[OPT].

theorem integrable_optimum_of_integrable_nonloops {n : ℕ}
    (M : Matroid (Fin n)) {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) (V : Ω → Weights n) (hV : Measurable V)
    (hVN : ∀ᵐ ω ∂μ, ∀ e, 0 ≤ V ω e)
    (hmom : ∀ e, M.IsNonloop e → Integrable (fun ω => V ω e) μ) :
    Integrable (fun ω => optimum M (V ω)) μ := by
…

Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.optimum

theorem OAI.MatroidProphet.DegenerateCases.integrable_optimum_iff line 78

Source documentation

An exact criterion: loop moments are deliberately absent on the right.

theorem integrable_optimum_iff {n : ℕ} (M : Matroid (Fin n))
    {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)
    (V : Ω → Weights n) (hV : Measurable V)
    (hVN : ∀ᵐ ω ∂μ, ∀ e, 0 ≤ V ω e) :
    Integrable (fun ω => optimum M (V ω)) μ ↔
      ∀ e, M.IsNonloop e → Integrable (fun ω => V ω e) μ := by
…

Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.optimum