OAI/Combinatorics/ContingencyTables/Transport/IntegerLeafEnergy.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.IntegerWeightedTransport.leafClique line 14
2. lemma OAI.ContingencyTables.IntegerWeightedTransport.oneHole_reindex line 18
3. lemma OAI.ContingencyTables.IntegerWeightedTransport.leafClique_reindex line 24
4. def OAI.ContingencyTables.IntegerWeightedTransport.leafEnergySum line 44
5. theorem OAI.ContingencyTables.IntegerWeightedTransport.recursiveEnergy_eq_leafEnergySum line 50

   Source documentation

   Every recursive leaf is exactly its literal full display, counted once in the Cartesian product of the ordinary balanced profiles.

   theorem recursiveEnergy_eq_leafEnergySum : ∀ (Ms : List ℕ) {I : Type u}
       [Fintype I] [DecidableEq I] (F H : (Coordinates I Ms → ℕ) → ℝ)
       (z : I → ℕ) (h : I → ℝ),
       recursiveEnergy Ms F H z h=leafEnergySum Ms F H z := by
   …

   Mentions: OAI.ContingencyTables.IntegerWeightedTransport.recursiveEnergy, OAI.ContingencyTables.IntegerWeightedTransport.leafEnergySum

6. lemma OAI.ContingencyTables.IntegerWeightedTransport.embedding_injective line 82
7. lemma OAI.ContingencyTables.IntegerWeightedTransport.max_removeOne line 97

   Source documentation

   Distinct valid holes recover their full display by the coordinate maximum. This is the reason different leaf cliques share no edges.

   lemma max_removeOne {C : Type*} [DecidableEq C] (z : C → ℕ) (i j : C)
       (hij : i ≠ j) :
       (fun k => max (removeOne z i k) (removeOne z j k))=z := by
   …

8. lemma OAI.ContingencyTables.IntegerWeightedTransport.removeOne_injective_valid line 112
9. def OAI.ContingencyTables.IntegerWeightedTransport.leafEdgeCodes line 119
10. def OAI.ContingencyTables.IntegerWeightedTransport.leafEdgeState line 124
11. theorem OAI.ContingencyTables.IntegerWeightedTransport.leafEdgeState_injective line 131

    Source documentation

    An oriented exchange edge determines its display, then its branch assignment, then its two hole coordinates.

    theorem leafEdgeState_injective {I : Type u} [Fintype I] [DecidableEq I]
        (Ms : List ℕ) (z : I → ℕ) :
        Set.InjOn (leafEdgeState Ms z) (leafEdgeCodes Ms z) := by
    …

    Mentions: OAI.ContingencyTables.IntegerWeightedTransport.leafEdgeState, OAI.ContingencyTables.IntegerWeightedTransport.leafEdgeCodes

12. def OAI.ContingencyTables.IntegerWeightedTransport.leafEdges line 155
13. def OAI.ContingencyTables.IntegerWeightedTransport.edgeTerm line 160
14. lemma OAI.ContingencyTables.IntegerWeightedTransport.leafClique_eq_valid_sum line 164
15. theorem OAI.ContingencyTables.IntegerWeightedTransport.leafEnergySum_eq_edges line 191

    Source documentation

    Complete leaf cliques have disjoint oriented edges. The resulting energy is exactly the ordinary minimum-endpoint graph sum.

    theorem leafEnergySum_eq_edges {I : Type u} [Fintype I] [DecidableEq I]
        (Ms : List ℕ) (F H : (Coordinates I Ms → ℕ) → ℝ) (z : I → ℕ)
        (hF : ∀ x, 0 ≤ F x) :
        leafEnergySum Ms F H z = (∑ e ∈ leafEdges Ms z, edgeTerm F H e)/2 := by
    …

    Mentions: OAI.ContingencyTables.IntegerWeightedTransport.leafEnergySum, OAI.ContingencyTables.IntegerWeightedTransport.leafEdges, OAI.ContingencyTables.IntegerWeightedTransport.edgeTerm

16. def OAI.ContingencyTables.IntegerWeightedTransport.IntegerExchangeAdjacent line 208
17. def OAI.ContingencyTables.IntegerWeightedTransport.integerGraphEnergy line 212
18. def OAI.ContingencyTables.IntegerWeightedTransport.leafVertices line 216
19. lemma OAI.ContingencyTables.IntegerWeightedTransport.leafEdges_states_adjacent line 222
20. theorem OAI.ContingencyTables.IntegerWeightedTransport.leafEnergySum_le_graphEnergy line 237

    Source documentation

    The full exchange graph may contain further edges; their energies are nonnegative. Every leaf edge occurs once in this graph.

    theorem leafEnergySum_le_graphEnergy {I : Type u} [Fintype I] [DecidableEq I]
        (Ms : List ℕ) (F H : (Coordinates I Ms → ℕ) → ℝ) (z : I → ℕ)
        (hF : ∀ x, 0 ≤ F x) (V : Finset (Coordinates I Ms → ℕ))
        (hV : leafVertices Ms z ⊆ V) :
        leafEnergySum Ms F H z ≤ integerGraphEnergy V F H := by
    …

    Mentions: OAI.ContingencyTables.IntegerWeightedTransport.leafVertices, OAI.ContingencyTables.IntegerWeightedTransport.leafEnergySum, OAI.ContingencyTables.IntegerWeightedTransport.integerGraphEnergy

21. theorem OAI.ContingencyTables.IntegerWeightedTransport.recursiveEnergy_le_graphEnergy line 251