EntropyGraph.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The finite coefficient argument in the high-entropy case

EKL (2006), Section 3, uses entropy symmetry to balance the row and column sums of the root coefficients. The two-step root lemma makes a composed positive edge full. The following finite argument then gives symmetric coefficients, and full coefficients whenever a third vertex is involved.

lemma OAI.DukePrimeDegree.balanced_cut line 21

theorem OAI.DukePrimeDegree.positive_support_symmetric_of_balanced line 36

Source documentation

A balanced nonnegative coefficient matrix with transitive positive support cannot have a one-way positive edge.

theorem positive_support_symmetric_of_balanced
    (w : ι → ι → ℝ) (hw : ∀ i j, 0 ≤ w i j)
    (hbal : ∀ i, ∑ j, w i j = ∑ j, w j i)
    (htrans : ∀ a b c, a ≠ c → 0 < w a b → 0 < w b c → 0 < w a c)
    {a b : ι} (hab : 0 < w a b) : 0 < w b a := by
…

theorem OAI.DukePrimeDegree.full_coefficient_of_third_neighbor line 76

Source documentation

A third neighbor makes a positive edge full, using the two-step rule.

theorem full_coefficient_of_third_neighbor
    (w : ι → ι → ℝ) (hw : ∀ i j, 0 ≤ w i j)
    (hbal : ∀ i, ∑ j, w i j = ∑ j, w j i)
    (hcomp : ∀ a b c, a ≠ c → 0 < w a b → 0 < w b c → w a c = 1)
    {a b c : ι} (hab : a ≠ b) (_hac : a ≠ c) (hbc : b ≠ c)
    (hwab : 0 < w a b) (hwac : 0 < w a c) : w a b = 1 := by
…

theorem OAI.DukePrimeDegree.coefficients_symmetric_of_balanced_two_step line 92

Source documentation

The entropy coefficients are symmetric once the row balance and the geometric two-step root rule have been established.

theorem coefficients_symmetric_of_balanced_two_step
    (w : ι → ι → ℝ) (hw : ∀ i j, 0 ≤ w i j)
    (hbal : ∀ i, ∑ j, w i j = ∑ j, w j i)
    (hcomp : ∀ a b c, a ≠ c → 0 < w a b → 0 < w b c → w a c = 1) :
    ∀ a b, w a b = w b a := by
…