FiniteSupportEnergy.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Restricting a finite weighted graph to its positive states

lemma OAI.ContingencyTables.IntegerWeightedTransport.pairTerm_eq_zero_left line 14
lemma OAI.ContingencyTables.IntegerWeightedTransport.pairTerm_eq_zero_right line 19

theorem OAI.ContingencyTables.IntegerWeightedTransport.symmetricEnergy_restrict line 25

Source documentation

Only endpoints with nonzero weight need to occur in the embedding. The ambient graph may still contain zero-weight vertices.

theorem symmetricEnergy_restrict (E : Finset (Y×Y)) (f H : Y → ℝ)
    (hf : ∀ y,0 ≤ f y) (i : X → Y) (hi : Function.Injective i)
    (hsupport : ∀ p ∈ E,(f p.1≠0 → ∃ x,i x=p.1) ∧ (f p.2≠0 → ∃ x,i x=p.2)) :
    symmetricEnergy E f H=
      (∑ x,∑ y,if (i x,i y) ∈ E then
        min (f (i x)) (f (i y))*(H (i x)-H (i y))^2 else 0)/2 := by
…

Mentions: OAI.ContingencyTables.IntegerWeightedTransport.symmetricEnergy

theorem OAI.ContingencyTables.IntegerWeightedTransport.symmetricEnergy_restrict_observable line 56