ImmProfileCompatibility.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.edgeProfile_immInternalPathEdges line 10
Source documentation
The list-based layer profile of an actual internal IMM path is its vertex coordinate.
```
@[simp] theorem edgeProfile_immInternalPathEdges (d : ℕ)
    (p : Fin d → Fin (d + 1)) (t : Fin (d + 1)) :
    edgeProfile (immInternalPathEdges d p) (immInternalPathEdges_labels d p) t =
      immInternalCoordinate d p t := by
…
```
Mentions: OAI.Problem335.edgeProfile, OAI.Problem335.immInternalPathEdges, OAI.Problem335.immInternalPathEdges_labels, OAI.Problem335.immInternalCoordinate

theorem OAI.Problem335.layerLabels_eq_immPathProfiles line 18

Source documentation

All four list profiles agree with the layer labels defining pairing weights.

theorem layerLabels_eq_immPathProfiles (d : ℕ)
    (x : Fin d → Pairings.Labels (Fin (d + 1))) (t : Fin (d + 1)) :
    MomentPairing.layerLabels 0 x t =
      (⟨edgeProfile (immInternalPathEdges d (fun i => (x i).p))
          (immInternalPathEdges_labels d _) t,
        edgeProfile (immInternalPathEdges d (fun i => (x i).q))
          (immInternalPathEdges_labels d _) t,
        edgeProfile (immInternalPathEdges d (fun i => (x i).r))
          (immInternalPathEdges_labels d _) t,
        edgeProfile (immInternalPathEdges d (fun i => (x i).s))
          (immInternalPathEdges_labels d _) t⟩ :
            Pairings.Labels (Fin (d + 1) × Fin (d + 1))) := by
…

Mentions: OAI.Problem335.Pairings.Labels, OAI.Problem335.MomentPairing.layerLabels, OAI.Problem335.edgeProfile, OAI.Problem335.immInternalPathEdges, OAI.Problem335.immInternalPathEdges_labels