GraphExpectedCopies.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LeanBlast.SecondKahnKalai.subgraphToComplete line 18
Source documentation
Regard an actual subgraph as a subgraph of the complete graph. Its vertex set, including all isolated vertices, is unchanged.
```
def subgraphToComplete {G : SimpleGraph (Fin n)} (K : G.Subgraph) :
    (⊤ : SimpleGraph (Fin n)).Subgraph where
…
```
def OAI.LeanBlast.SecondKahnKalai.subgraphFromComplete line 27
Source documentation
A complete-graph subgraph whose edges occur in G is the same actual subgraph of G.
```
def subgraphFromComplete (G : SimpleGraph (Fin n))
    (K : (⊤ : SimpleGraph (Fin n)).Subgraph) (hK : K.spanningCoe ≤ G) :
    G.Subgraph where
…
```

def OAI.LeanBlast.SecondKahnKalai.completeCopyEquiv line 37

Source documentation

Copies are put in bijection without choosing or counting graph embeddings.

def completeCopyEquiv (G : SimpleGraph (Fin n)) (F : SimpleGraph V) :
    {K : G.Subgraph // Nonempty (F ≃g K.coe)} ≃
      {K : (⊤ : SimpleGraph (Fin n)).Subgraph //
        Nonempty (F ≃g K.coe) ∧ K.spanningCoe ≤ G} where
…

theorem OAI.LeanBlast.SecondKahnKalai.copyCount_eq_complete_card line 46
theorem OAI.LeanBlast.SecondKahnKalai.copyCount_eq_sum_complete line 62
theorem OAI.LeanBlast.SecondKahnKalai.edgeCount_spanningCoe line 76
Source documentation
Adding ambient isolated vertices does not change the edge count.
```
theorem edgeCount_spanningCoe {G : SimpleGraph (Fin n)} (K : G.Subgraph) :
    edgeCount K.spanningCoe = edgeCount K.coe := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.edgeCount
theorem OAI.LeanBlast.SecondKahnKalai.card_graphEdges_of_copy line 84
theorem OAI.LeanBlast.SecondKahnKalai.subgraph_survival_probability line 91
theorem OAI.LeanBlast.SecondKahnKalai.expectedCopies_formula line 108
Source documentation
The exact expected number of unlabelled, non-induced copies. The counted objects include their vertex sets, so the identity retains isolated vertices.
```
theorem expectedCopies_formula (n : ℕ) (p : ℝ) (F : SimpleGraph V) :
    expectedCopies n p F =
      ((⊤ : SimpleGraph (Fin n)).copyCount F : ℝ) * p ^ edgeCount F := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.expectedCopies, OAI.LeanBlast.SecondKahnKalai.edgeCount