Weak Fulkerson duality

The weak-duality direction of Fulkerson duality (one_le_length): a density admissible for the Fulkerson dual Γ.FulkersonDual has length at least 1 against every density admissible for Γ.

The core argument (one_le_length_of_pos) runs on the E → ℝ side and is then pulled back: for strictly positive η the pairing has compact sublevel sets over Density.toReal '' Γ.Adm (LeanModulus.Common.Pairing), so its minimum is attained at an extreme point (LeanModulus.Common.ExtremePoints), which corresponds to a member of Γ.FulkersonDual (LeanModulus.Common.ToReal). The general case follows by perturbing η by δ • 1 and letting δ → 0.

theorem FamilyOfObjects.exists_fulkersonDual_isMinOn {E : Type u_1} [Fintype E] (Γ : FamilyOfObjects E) {η : Density E} (hη : ∀ (e : E), 0 < η e) (hne : Γ.Adm.Nonempty) : ∃ γ ∈ Γ.FulkersonDual, IsMinOn (⇑η.pairing) (Density.toReal '' Γ.Adm) (Density.toReal γ)

The pairing with a strictly positive density attains its minimum over the image of a nonempty admissible set at (the coercion of) a member of the Fulkerson dual.

theorem FamilyOfObjects.one_le_length_of_pos {E : Type u_1} [Fintype E] (Γ : FamilyOfObjects E) {η : Density E} (hη : ∀ (e : E), 0 < η e) (hηAdm : η ∈ Γ.FulkersonDual.Adm) {ρ : Density E} (hρ : ρ ∈ Γ.Adm) : 1 ≤ η.length ρ

Weak duality, strictly positive case: if η > 0 is admissible for the Fulkerson dual of Γ, then every density admissible for Γ has η-length at least 1.

theorem FamilyOfObjects.one_le_length {E : Type u_1} [Fintype E] (Γ : FamilyOfObjects E) {η : Density E} (hηAdm : η ∈ Γ.FulkersonDual.Adm) {ρ : Density E} (hρ : ρ ∈ Γ.Adm) : 1 ≤ η.length ρ

Weak duality: if η is admissible for the Fulkerson dual of Γ, then every density admissible for Γ has η-length at least 1. The strict-positivity hypothesis of one_le_length_of_pos is removed by perturbing to η + δ • 1 — still dual-admissible since lengths are monotone — and letting δ → 0.