PairingNeighborCount.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.Pairings.internalEndpointSet_eq_internalEnds line 12
Source documentation
The actual path endpoints coincide with the schedule's internal ends.
```
theorem internalEndpointSet_eq_internalEnds {L : ℕ} (t : Fin (L + 1)) :
    internalEndpointSet t = BalancedSchedule.internalEnds t := by
…
```
Mentions: OAI.Problem335.Pairings.internalEndpointSet, OAI.Problem335.BalancedSchedule.internalEnds
theorem OAI.Problem335.Pairings.normalEndpointCount_eq_nnInternalEnds_card line 19
Source documentation
Boolean word form of the normal-endpoint exponent in the weighted relaxed-path count, using the canonical schedule coincidence set.
```
theorem normalEndpointCount_eq_nnInternalEnds_card {L : ℕ}
    (w : Fin (L + 1) → Bool) (t : Fin (L + 1)) :
    normalEndpointCount (fun i => boolKindEquiv (w i)) (internalEndpointSet t) =
      (BalancedSchedule.nnInternalEnds w t).card := by
…
```
Mentions: OAI.Problem335.Pairings.normalEndpointCount, OAI.Problem335.Pairings.boolKindEquiv, OAI.Problem335.Pairings.internalEndpointSet, OAI.Problem335.BalancedSchedule.nnInternalEnds
theorem OAI.Problem335.Pairings.normalEndpointCount_eq_falseNeighbors_card line 35
Source documentation
At a normal layer the relaxed-path exponent is precisely the canonical graph-word false-neighbor count.
```
theorem normalEndpointCount_eq_falseNeighbors_card {L : ℕ}
    (w : Fin (L + 1) → Bool) (t : Fin (L + 1)) (ht : w t = false) :
    normalEndpointCount (fun i => boolKindEquiv (w i)) (internalEndpointSet t) =
      (IsolatedWeight.falseNeighbors BalancedSchedule.adjacent w t).card := by
…
```
Mentions: OAI.Problem335.Pairings.normalEndpointCount, OAI.Problem335.Pairings.boolKindEquiv, OAI.Problem335.Pairings.internalEndpointSet, OAI.Problem335.IsolatedWeight.falseNeighbors, OAI.Problem335.BalancedSchedule.adjacent
theorem OAI.Problem335.Pairings.correction_eq_normalEndpointCount_product line 44
Source documentation
The complete word correction expressed in the exponents supplied by the actual relaxed-path averaging theorem.
```
theorem correction_eq_normalEndpointCount_product {L : ℕ}
    (V : Finset (Fin (L + 1))) (w : Fin (L + 1) → Bool) (A x : ℝ) :
    IsolatedWeight.correction V BalancedSchedule.adjacent A x w =
      ∏ t ∈ V.filter (fun t => w t = false),
        (1 + A * x ^ normalEndpointCount (fun i => boolKindEquiv (w i))
          (internalEndpointSet t)) := by
…
```
Mentions: OAI.Problem335.IsolatedWeight.correction, OAI.Problem335.BalancedSchedule.adjacent, OAI.Problem335.Pairings.normalEndpointCount, OAI.Problem335.Pairings.boolKindEquiv, OAI.Problem335.Pairings.internalEndpointSet