GraphCopies.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LeanBlast.SecondKahnKalai.mem_copyOrbit_iff_edgeSupportGraph_iso line 16
def OAI.LeanBlast.SecondKahnKalai.orbitSubgraphEquiv line 29
Source documentation
Distinct edge orbits correspond bijectively to actual unlabelled subgraphs. The target has no isolated vertices, so its image subgraph is uniquely determined by its edges. This also covers the empty graph, with its empty vertex set.
```
def orbitSubgraphEquiv (S : Finset (Edge n)) :
    OrbitCopy (Equiv.Perm (Fin n)) S ≃
      {K : (⊤ : SimpleGraph (Fin n)).Subgraph //
        Nonempty (edgeSupportGraph S ≃g K.coe)} where
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.Edge, OAI.LeanBlast.SecondKahnKalai.OrbitCopy, OAI.LeanBlast.SecondKahnKalai.edgeSupportGraph
theorem OAI.LeanBlast.SecondKahnKalai.orbitCount_eq_copyCount line 48
theorem OAI.LeanBlast.SecondKahnKalai.expectedCopies_edgeSupportGraph line 63
theorem OAI.LeanBlast.SecondKahnKalai.orbit_expectation_constraint line 70
Source documentation
The internal orbit constraint follows from an actual subgraph constraint of the public expectation threshold, with no multiplicity factor.
```
theorem orbit_expectation_constraint {V : Type*} (f : V ↪ Fin n)
    (H : SimpleGraph V) (q : ℝ)
    (hq : ∀ F : H.Subgraph, (1 / 2 : ℝ) ≤ expectedCopies n q F.coe)
    (S : Finset (Edge n)) (hS : S ⊆ graphEdges (H.map f)) :
    (1 / 2 : ℝ) ≤ (orbitCount (Equiv.Perm (Fin n)) S : ℝ) * q ^ S.card := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.expectedCopies, OAI.LeanBlast.SecondKahnKalai.Edge, OAI.LeanBlast.SecondKahnKalai.graphEdges, OAI.LeanBlast.SecondKahnKalai.orbitCount
theorem OAI.LeanBlast.SecondKahnKalai.copyCount_pos_iff_orbit_subset line 79
theorem OAI.LeanBlast.SecondKahnKalai.exists_graphRepresentationWithConstraints line 91