OAI/Algebra/DepthFive/PairingWeights.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.Problem335.Pairings.vertexNonempty line 12
2. def OAI.Problem335.Pairings.vertexPairEq line 19

   Source documentation

   Agreement between the two labels of a normal pairing at a vertex.

   def vertexPairEq {α : Type*} [DecidableEq α] {τ σ : Kind}
       (x : Vertex α τ σ) : ℝ := if x.1.p = x.1.r then 1 else 0

   Mentions: OAI.Problem335.Pairings.Kind, OAI.Problem335.Pairings.Vertex

3. theorem OAI.Problem335.Pairings.average_vertexPairEq line 22
4. def OAI.Problem335.Pairings.normalEndpointCount line 44

   Source documentation

   Number of endpoints at which both adjacent pairing types are normal.

   def normalEndpointCount {L : ℕ} (τ : Fin (L + 1) → Kind)
       (s : Finset (Fin L)) : ℕ :=
   …

   Mentions: OAI.Problem335.Pairings.Kind

5. def OAI.Problem335.Pairings.endpointCoincidence line 49

   Source documentation

   Equality of both normal coordinates at all indicated internal endpoints.

   def endpointCoincidence {α : Type*} [DecidableEq α] {L : ℕ}
       {τ : Fin (L + 1) → Kind} (s : Finset (Fin L)) (x : Assignments α τ) : ℝ :=
   …

   Mentions: OAI.Problem335.Pairings.Kind, OAI.Problem335.Pairings.Assignments

6. theorem OAI.Problem335.Pairings.average_endpoint_group line 53
7. theorem OAI.Problem335.Pairings.average_endpoint_correction line 65
8. theorem OAI.Problem335.Pairings.average_assignment_corrections line 74

   Source documentation

   Exact average of normal-layer corrections for disjoint endpoint sets in actual relaxed vertex assignments, including forced-equality interfaces.

   theorem average_assignment_corrections (α : Type*) [Fintype α] [DecidableEq α]
       [Nonempty α] {L : ℕ} (τ : Fin (L + 1) → Kind)
       {ι : Type*} [Fintype ι] [DecidableEq ι]
       (s : ι → Finset (Fin L)) (hs : Pairwise (fun i j => Disjoint (s i) (s j)))
       (c : ι → ℝ) :
       average (fun x : Assignments α τ => ∏ i, (1 + c i * endpointCoincidence (s i) x)) =
         ∏ i, (1 + c i * (Fintype.card α : ℝ)⁻¹ ^ normalEndpointCount τ (s i)) := by
   …

   Mentions: OAI.Problem335.Pairings.Kind, OAI.Problem335.Pairings.Assignments, OAI.Problem335.Pairings.endpointCoincidence, OAI.Problem335.Pairings.normalEndpointCount

9. theorem OAI.Problem335.Pairings.sum_assignment_corrections line 94

   Source documentation

   The weighted relaxed-assignment count: its unweighted count times the product of the independent normal-layer correction averages.

   theorem sum_assignment_corrections (α : Type*) [Fintype α] [DecidableEq α]
       [Nonempty α] {L : ℕ} (τ : Fin (L + 1) → Kind)
       {ι : Type*} [Fintype ι] [DecidableEq ι]
       (s : ι → Finset (Fin L)) (hs : Pairwise (fun i j => Disjoint (s i) (s j)))
       (c : ι → ℝ) :
       (∑ x : Assignments α τ, ∏ i, (1 + c i * endpointCoincidence (s i) x)) =
         (Fintype.card α : ℝ) ^ (2 * L - adjacentSwitches τ) *
           ∏ i, (1 + c i * (Fintype.card α : ℝ)⁻¹ ^ normalEndpointCount τ (s i)) := by
   …

   Mentions: OAI.Problem335.Pairings.Kind, OAI.Problem335.Pairings.Assignments, OAI.Problem335.Pairings.endpointCoincidence, OAI.Problem335.Pairings.adjacentSwitches, OAI.Problem335.Pairings.normalEndpointCount

10. def OAI.Problem335.Pairings.internalEndpointSet line 111

    Source documentation

    The internal vertices adjacent to a specified layer.

    def internalEndpointSet {L : ℕ} (t : Fin (L + 1)) : Finset (Fin L) :=
    …

11. theorem OAI.Problem335.Pairings.internalEndpointSet_disjoint line 115

    Source documentation

    Distinct nonadjacent layers use disjoint internal vertex coordinates.

    theorem internalEndpointSet_disjoint {L : ℕ} {i j : Fin (L + 1)}
        (hij : i ≠ j) (hforward : i.val + 1 ≠ j.val)
        (hbackward : j.val + 1 ≠ i.val) :
        Disjoint (internalEndpointSet i) (internalEndpointSet j) := by
    …

    Mentions: OAI.Problem335.Pairings.internalEndpointSet

12. theorem OAI.Problem335.Pairings.pairwise_internalEndpointSet_disjoint line 132

    Source documentation

    An injective family of pairwise nonadjacent layers meets the exact independence hypothesis of sum_relaxedPaths_layer_corrections.

    theorem pairwise_internalEndpointSet_disjoint {L : ℕ} {ι : Type*}
        (t : ι → Fin (L + 1)) (ht : Function.Injective t)
        (hseparated : ∀ i j, i ≠ j → (t i).val + 1 ≠ (t j).val) :
        Pairwise (fun i j => Disjoint (internalEndpointSet (t i))
          (internalEndpointSet (t j))) := by
    …

    Mentions: OAI.Problem335.Pairings.internalEndpointSet

13. theorem OAI.Problem335.Pairings.layer_coordinate_eq_iff line 141
14. theorem OAI.Problem335.Pairings.endpointCoincidence_eq_layer_indicator line 181

    Source documentation

    The product of endpoint indicators is exactly the full layer-coordinate coincidence indicator, including either fixed external endpoint.

    theorem endpointCoincidence_eq_layer_indicator {α : Type*} [DecidableEq α]
        {L : ℕ} (a : α) (τ : Fin (L + 1) → Kind) (x : Assignments α τ)
        (t : Fin (L + 1)) :
        endpointCoincidence (internalEndpointSet t) x =
          if (zipLabels (closePaths a (fun v => (x v).val) t.castSucc)
              (closePaths a (fun v => (x v).val) t.succ)).p =
            (zipLabels (closePaths a (fun v => (x v).val) t.castSucc)
              (closePaths a (fun v => (x v).val) t.succ)).r then 1 else 0 := by
    …

    Mentions: OAI.Problem335.Pairings.Kind, OAI.Problem335.Pairings.Assignments, OAI.Problem335.Pairings.endpointCoincidence, OAI.Problem335.Pairings.internalEndpointSet, OAI.Problem335.Pairings.zipLabels, OAI.Problem335.Pairings.closePaths

15. theorem OAI.Problem335.Pairings.sum_relaxedPaths_layer_corrections line 195

    Source documentation

    Exact weighted count in terms of the actual layer coordinates of relaxed endpoint-fixed path quadruples. The sole combinatorial hypothesis is that the selected layers have disjoint internal endpoint sets.

    theorem sum_relaxedPaths_layer_corrections (α : Type*) [Fintype α]
        [DecidableEq α] [Nonempty α] {L : ℕ} (a : α) (τ : Fin (L + 1) → Kind)
        {ι : Type*} [Fintype ι] [DecidableEq ι]
        (t : ι → Fin (L + 1))
        (ht : Pairwise (fun i j => Disjoint (internalEndpointSet (t i))
          (internalEndpointSet (t j)))) (c : ι → ℝ) :
        (∑ x : RelaxedPaths α a τ, ∏ i,
          (1 + c i * if
            (zipLabels (closePaths a x.val (t i).castSucc)
              (closePaths a x.val (t i).succ)).p =
            (zipLabels (closePaths a x.val (t i).castSucc)
              (closePaths a x.val (t i).succ)).r then 1 else 0)) =
    …

    Mentions: OAI.Problem335.Pairings.Kind, OAI.Problem335.Pairings.internalEndpointSet, OAI.Problem335.Pairings.RelaxedPaths, OAI.Problem335.Pairings.zipLabels, OAI.Problem335.Pairings.closePaths