CutFlux.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Finite directed-cut estimates used by the mass-action argument.

theorem OAI.Problem326.CutFlux.transGen_crosses line 14

Source documentation

A directed path leaving a set contains an edge leaving that set.

theorem transGen_crosses {V : Type uV} {r : V → V → Prop} {P : V → Prop}
    {u v : V} (h : Relation.TransGen r u v) (hu : P u) (hv : ¬ P v) :
    ∃ a b, r a b ∧ P a ∧ ¬ P b := by
…

theorem OAI.Problem326.CutFlux.upward_of_downward line 26

Source documentation

Every downward threshold crossing has an upward crossing when each edge has a directed return path. No finiteness hypothesis is needed here.

theorem upward_of_downward {V : Type uV} {E : Type uE} (s t : E → V) (a : V → ℝ)
    (hreturn : ∀ e, Relation.TransGen
      (fun u v => ∃ f, s f = u ∧ t f = v) (t e) (s e))
    (c : ℝ) (e : E) (he : a (t e) ≤ c ∧ c < a (s e)) :
    ∃ f, a (s f) ≤ c ∧ c < a (t f) := by
…

theorem OAI.Problem326.CutFlux.threshold_flux_nonneg_of_source_order line 40

Source documentation

The total upward flux across an ordered cut dominates the downward flux. The rate assumption is phrased per edge, so it also handles an empty edge set without introducing a minimum over the empty set.

theorem threshold_flux_nonneg_of_source_order {V : Type uV} {E : Type uE} [Fintype E]
    (s t : E → V) (a w : V → ℝ) (κ : E → ℝ) (δ : ℝ)
    (hreturn : ∀ e, Relation.TransGen
      (fun u v => ∃ f, s f = u ∧ t f = v) (t e) (s e))
    (hw : ∀ v, 0 < w v) (hκ : ∀ e, 0 < κ e) (hδ : 0 ≤ δ)
    (horder : ∀ e f, a (s e) < a (s f) → w (s f) ≤ δ * w (s e))
    (hrate : ∀ e, δ * (∑ f, κ f) < κ e) (c : ℝ) :
    0 ≤ (∑ e ∈ Finset.univ.filter (fun e => a (s e) ≤ c ∧ c < a (t e)),
          κ e * w (s e)) -
        (∑ e ∈ Finset.univ.filter (fun e => a (t e) ≤ c ∧ c < a (s e)),
          κ e * w (s e)) := by
…

theorem OAI.Problem326.CutFlux.threshold_flux_nonneg line 93

Source documentation

The all-vertex version of the threshold flux inequality.

theorem threshold_flux_nonneg {V : Type uV} {E : Type uE} [Fintype E]
    (s t : E → V) (a w : V → ℝ) (κ : E → ℝ) (δ : ℝ)
    (hreturn : ∀ e, Relation.TransGen
      (fun u v => ∃ f, s f = u ∧ t f = v) (t e) (s e))
    (hw : ∀ v, 0 < w v) (hκ : ∀ e, 0 < κ e) (hδ : 0 ≤ δ)
    (horder : ∀ u v, a u < a v → w v ≤ δ * w u)
    (hrate : ∀ e, δ * (∑ f, κ f) < κ e) (c : ℝ) :
    0 ≤ (∑ e ∈ Finset.univ.filter (fun e => a (s e) ≤ c ∧ c < a (t e)),
          κ e * w (s e)) -
        (∑ e ∈ Finset.univ.filter (fun e => a (t e) ≤ c ∧ c < a (s e)),
          κ e * w (s e)) := by
…

theorem OAI.Problem326.CutFlux.total_flux_nonneg line 107
theorem OAI.Problem326.CutFlux.total_flux_nonneg_of_source_order line 119