DensityContractsTheorems.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Proofs of the complete source-facing density, paths and generator contracts.

lemma OAI.MatroidProphet.densityExpansion_closure_argument line 12
Source documentation
Closing the lower constraint leaves exactly the same feasible flat family.
```
lemma densityExpansion_closure_argument (M : Matroid α) (hE : M.E = univ)
    (κ : ℕ) (D P : Set α) :
    densityExpansion M hE κ D (M.closure P) = densityExpansion M hE κ D P := by
…
```
Mentions: OAI.MatroidProphet.densityExpansion
lemma OAI.MatroidProphet.densityExpansion_residual_conditionalRank line 24
theorem OAI.MatroidProphet.source_density_expansion line 38
Source documentation
Full lem:density, without assuming existence or correctness of its expansion.
```
theorem source_density_expansion (M : Matroid α) (hE : M.E = univ)
    (κ : ℕ) (D : Set α) : DensityExpansionContract M hE κ D := by
…
```
Mentions: OAI.MatroidProphet.DensityExpansionContract
theorem OAI.MatroidProphet.source_path_properties line 49
Source documentation
Full lem:paths; the birth is certified least on the complete integer timeline.
```
theorem source_path_properties (M : Matroid α) (hE : M.E = univ)
    (κ : ℕ) (D C : ℕ → Set α) : PathPropertiesContract M hE κ D C := by
…
```
Mentions: OAI.MatroidProphet.PathPropertiesContract
theorem OAI.MatroidProphet.source_generator_budget line 76
Source documentation
Full lem:generators, including monotonicity outside the bounded computation.
```
theorem source_generator_budget (M : Matroid α) (hE : M.E = univ)
    (κ : ℕ) (hκ : 0 < κ) (D C : ℕ → Set α) :
    GeneratorBudgetContract M hE κ D C := by
…
```
Mentions: OAI.MatroidProphet.GeneratorBudgetContract