RootBalanceSymmetry.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A finite balance criterion for symmetry of invariant roots

A reflexive transitive relation on a finite set is symmetric if every vertex has the same incoming and outgoing degree. This applies to the root-invariance relation when its degrees are balanced.

theorem OAI.DukePrimeDegree.symmetric_of_finite_preorder_balance line 23

Source documentation

In a finite preorder, balanced in- and out-degrees rule out a strict comparison. This includes the reflexive loop in both counts.

theorem symmetric_of_finite_preorder_balance
    {I : Type*} [Fintype I] (R : I → I → Prop)
    (hrefl : ∀ i, R i i)
    (htrans : ∀ ⦃i j k⦄, R i j → R j k → R i k)
    (hbalance : ∀ i,
      (Finset.univ.filter (R i)).card =
        (Finset.univ.filter (fun j => R j i)).card) :
    Std.Symm R := by
…

theorem OAI.DukePrimeDegree.rootInvarianceRelation_symmetric_of_balance line 54

Source documentation

Balanced degrees make the root-invariance relation symmetric.

theorem rootInvarianceRelation_symmetric_of_balance {n : ℕ}
    (μ : Measure (X n))
    (hbalance : ∀ i,
      (Finset.univ.filter (rootInvarianceRelation μ i)).card =
        (Finset.univ.filter (fun j => rootInvarianceRelation μ j i)).card) :
    Std.Symm (rootInvarianceRelation μ) :=
…