OAI/Analysis/MassAction/CutDecomposition.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The weighted level difference is the integral of the flux over all threshold cuts. This avoids choosing an ordering of the distinct levels.

  1. theorem OAI.Problem326.CutFlux.integrable_interval_indicator line 15
  2. theorem OAI.Problem326.CutFlux.integral_signed_interval line 20
  3. theorem OAI.Problem326.CutFlux.weighted_difference_nonneg_of_threshold_flux line 34

    Source documentation

    If every threshold cut has nonnegative net flux, then the weighted sum of level differences is nonnegative. Edge weights can have either sign.

    theorem weighted_difference_nonneg_of_threshold_flux {E : Type uE} [Fintype E]
    (s t q : E → ℝ)
    (hcut : ∀ c : ℝ,
      0 ≤ (∑ e ∈ Finset.univ.filter (fun e => s e ≤ c ∧ c < t e), q e) -
          (∑ e ∈ Finset.univ.filter (fun e => t e ≤ c ∧ c < s e), q e)) :
    0 ≤ ∑ e, q e * (t e - s e) := by
…