ScheduleWeightBridge.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.BalancedSchedule.internalEdges line 13
Source documentation
The graph edges joining consecutive layers, indexed by internal vertices.
```
def internalEdges (n : ℕ) : Finset (Fin n × Fin n) :=
…
```
theorem OAI.Problem335.BalancedSchedule.internalEdges_eq_pathEdges line 17
Source documentation
On a successor number of layers this is the canonical path graph.
```
theorem internalEdges_eq_pathEdges (n : ℕ) :
    internalEdges (n + 1) = SwitchRestoration.pathEdges n := rfl
```
Mentions: OAI.Problem335.BalancedSchedule.internalEdges, OAI.Problem335.SwitchRestoration.pathEdges
theorem OAI.Problem335.BalancedSchedule.internalEdges_adjacent line 21
Source documentation
Each graph edge joins adjacent layers in either direction.
```
theorem internalEdges_adjacent {n : ℕ} {e : Fin n × Fin n}
    (he : e ∈ internalEdges n) : adjacent e.1 e.2 ∧ adjacent e.2 e.1 := by
…
```
Mentions: OAI.Problem335.BalancedSchedule.internalEdges, OAI.Problem335.BalancedSchedule.adjacent
theorem OAI.Problem335.BalancedSchedule.endpointDegree_internalEdges line 27
Source documentation
Graph incidence degree and internal-end cardinality agree exactly.
```
theorem endpointDegree_internalEdges {n : ℕ} (i : Fin n) :
    SwitchRestoration.endpointDegree (internalEdges n) i = (internalEnds i).card := by
…
```
Mentions: OAI.Problem335.SwitchRestoration.endpointDegree, OAI.Problem335.BalancedSchedule.internalEdges, OAI.Problem335.BalancedSchedule.internalEnds
theorem OAI.Problem335.BalancedSchedule.falseNeighbors_card_eq_nnInternalEnds_card line 57
Source documentation
Normal neighbors of a normal layer are in bijection with its internal vertices having two normal incident layers. This identifies the correction exponents in the graph-word and path-pairing formulations.
```
theorem falseNeighbors_card_eq_nnInternalEnds_card {n : ℕ}
    (τ : Fin n → Bool) (i : Fin n) (hi : τ i = false) :
    (IsolatedWeight.falseNeighbors adjacent τ i).card =
      (nnInternalEnds τ i).card := by
…
```
Mentions: OAI.Problem335.IsolatedWeight.falseNeighbors, OAI.Problem335.BalancedSchedule.adjacent, OAI.Problem335.BalancedSchedule.nnInternalEnds
theorem OAI.Problem335.BalancedSchedule.correction_eq_nnInternalEnds_product line 134
Source documentation
The complete coincidence correction in the internal-vertex formulation.
```
theorem correction_eq_nnInternalEnds_product {n : ℕ}
    (V : Finset (Fin n)) (τ : Fin n → Bool) (A x : ℝ) :
    IsolatedWeight.correction V adjacent A x τ =
      ∏ i ∈ V.filter (fun i => τ i = false),
        (1 + A * x ^ (nnInternalEnds τ i).card) := by
…
```
Mentions: OAI.Problem335.IsolatedWeight.correction, OAI.Problem335.BalancedSchedule.adjacent, OAI.Problem335.BalancedSchedule.nnInternalEnds