OAI/Combinatorics/ContingencyTables/Transport/FiniteSymmetricEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Repair edges are charged once in a symmetric physical graph

  1. def OAI.ContingencyTables.IntegerWeightedTransport.pairTerm line 11
  2. def OAI.ContingencyTables.IntegerWeightedTransport.symmetricEnergy line 14
  3. lemma OAI.ContingencyTables.IntegerWeightedTransport.pairTerm_nonnegative line 17
  4. lemma OAI.ContingencyTables.IntegerWeightedTransport.pairTerm_reverse line 20
  5. theorem OAI.ContingencyTables.IntegerWeightedTransport.symmetricEnergy_mono line 27
  6. theorem OAI.ContingencyTables.IntegerWeightedTransport.repair_energy_le line 35

    Source documentation

    Distinct defects give distinct unoriented repair edges. Both directed copies together use twice their weight and hence cancel the energy's half.

    theorem repair_energy_le {X D : Type*} [Fintype D] (E : Finset (X×X))
    (f H : X → ℝ) (hf : ∀ x,0 ≤ f x) (x y : D → X)
    (hx : Function.Injective x) (hxy : ∀ d e,x d≠y e)
    (hforward : ∀ d,(x d,y d) ∈ E) (hreverse : ∀ d,(y d,x d) ∈ E) :
    (∑ d,pairTerm f H (x d,y d)) ≤ symmetricEnergy E f H := by
…

    Mentions: OAI.ContingencyTables.IntegerWeightedTransport.pairTerm, OAI.ContingencyTables.IntegerWeightedTransport.symmetricEnergy