OAI/Combinatorics/ParityLifts/Masses.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ParityWL.WeightedWitness.mass line 16
2. lemma OAI.ParityWL.WeightedWitness.coordinate_mass line 20
3. lemma OAI.ParityWL.WeightedWitness.mass_univ_adj line 31
4. lemma OAI.ParityWL.WeightedWitness.mass_union line 41
5. lemma OAI.ParityWL.WeightedWitness.mass_eq_zero line 46
6. lemma OAI.ParityWL.WeightedWitness.mass_univ_reachable line 52
7. lemma OAI.ParityWL.WeightedWitness.mass_separator line 61

   Source documentation

   Two types absent from the boundary of a separated vertex set have equal mass.

   lemma WeightedWitness.mass_separator (w : WeightedWitness T F a b)
       {u v : A} (huv : T.Adj u v) (Y S : Finset W)
       (hboundary : ∀ x ∈ Y, ∀ y, F.Adj x y → y ∉ Y → y ∈ S)
       (hu : ∀ x ∈ S, a x ≠ u) (hv : ∀ x ∈ S, a x ≠ v) :
       w.mass Y u = w.mass Y v := by
   …

   Mentions: OAI.ParityWL.WeightedWitness

8. lemma OAI.ParityWL.starParity_value line 93
9. lemma OAI.ParityWL.WeightedWitness.main_mass line 103
10. lemma OAI.ParityWL.WeightedWitness.template_mass line 118
11. def OAI.ParityWL.WeightedWitness.testMass line 135
12. lemma OAI.ParityWL.WeightedWitness.testMass_add line 139
13. lemma OAI.ParityWL.WeightedWitness.testMass_one line 148
14. lemma OAI.ParityWL.WeightedWitness.testMass_zero line 152
15. lemma OAI.ParityWL.WeightedWitness.testMass_coordinate line 159
16. lemma OAI.ParityWL.WeightedWitness.testMass_transfer line 177

    Source documentation

    Transfer of a tested type mass across a separator. The test vanishes on its boundary representatives; target-type vertices are absent from the boundary. This includes every boundary edge rather than dropping such edges.

    lemma WeightedWitness.testMass_transfer (w : WeightedWitness T F a b)
        {u v : A} (huv : T.Adj u v) (Y S : Finset W) (p q : W → Bit)
        (hboundary : ∀ x ∈ Y, ∀ y, F.Adj x y → y ∉ Y → y ∈ S)
        (hv : ∀ x ∈ S, a x ≠ v)
        (hp : ∀ x ∈ S, a x = u → p x = 0)
        (hcompat : ∀ x y, F.Adj x y → a x = u → a y = v → p x = q y) :
        w.testMass Y u p = w.testMass Y v q := by
    …

    Mentions: OAI.ParityWL.WeightedWitness, OAI.ParityWL.Bit

17. lemma OAI.ParityWL.WeightedWitness.testMass_complement line 228
18. lemma OAI.ParityWL.WeightedWitness.global_mismatch line 239

    Source documentation

    The global mismatch identity, including arbitrary zero representative weights.

    lemma WeightedWitness.global_mismatch (w : WeightedWitness T F a b)
        {u v : A} (huv : T.Adj u v) (p q : W → Bit)
        (hc : ∀ x y, F.Adj x y → a x = u → a y = v → p x + q y = 1) :
        w.testMass Finset.univ u p + w.testMass Finset.univ v q =
          w.mass Finset.univ u := by
    …

    Mentions: OAI.ParityWL.WeightedWitness, OAI.ParityWL.Bit