PairingPartition.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

instance OAI.Problem335.Pairings.(instance at line 9) line 9
def OAI.Problem335.Pairings.classify line 14
Source documentation
Assign the all-equal case to normal pairing, as required for disjoint classes.
```
def classify {α : Type*} [DecidableEq α] (x : Labels α) : Kind :=
…
```
Mentions: OAI.Problem335.Pairings.Labels, OAI.Problem335.Pairings.Kind
theorem OAI.Problem335.Pairings.exactRespects_classify_iff line 17
theorem OAI.Problem335.Pairings.classify_eq_of_exact line 24
def OAI.Problem335.Pairings.layerLabels line 31
Source documentation
The four layer coordinates of endpoint-fixed paths.
```
def layerLabels {α : Type*} {L : ℕ} (a : α) (x : Fin L → Labels α)
    (t : Fin (L + 1)) : Labels (α × α) :=
…
```
Mentions: OAI.Problem335.Pairings.Labels
abbrev OAI.Problem335.Pairings.ExactPaths line 35
abbrev OAI.Problem335.Pairings.CompatiblePaths line 38
def OAI.Problem335.Pairings.compatiblePathsEquivSigma line 46
Source documentation
The compatible quadruples partition uniquely according to their exact pairing word.
```
def compatiblePathsEquivSigma (α : Type*) [DecidableEq α] {L : ℕ} (a : α) :
    CompatiblePaths α (L := L) a ≃
…
```
Mentions: OAI.Problem335.Pairings.CompatiblePaths
theorem OAI.Problem335.Pairings.sum_compatiblePaths_eq_sum_exactPaths line 68
Source documentation
Regroup any finite weighted compatible-path sum by its unique pairing word.
```
theorem sum_compatiblePaths_eq_sum_exactPaths {α R : Type*}
    [Fintype α] [DecidableEq α] [AddCommMonoid R] {L : ℕ}
    (a : α) (w : (Fin L → Labels α) → R) :
    (∑ x : CompatiblePaths α (L := L) a, w x.1) =
…
```
Mentions: OAI.Problem335.Pairings.Labels, OAI.Problem335.Pairings.CompatiblePaths
theorem OAI.Problem335.Pairings.sum_compatiblePaths_pairingWeight line 81
Source documentation
Regroup sums whose weight remembers the canonical pairing word.
```
theorem sum_compatiblePaths_pairingWeight {α R : Type*}
    [Fintype α] [DecidableEq α] [AddCommMonoid R] {L : ℕ}
    (a : α) (w : (Fin (L + 1) → Kind) → (Fin L → Labels α) → R) :
    (∑ x : CompatiblePaths α (L := L) a,
…
```
Mentions: OAI.Problem335.Pairings.Kind, OAI.Problem335.Pairings.Labels, OAI.Problem335.Pairings.CompatiblePaths

theorem OAI.Problem335.Pairings.sum_subtype_le_of_imp line 96

Source documentation

Enlarging a finite summation domain preserves inequalities for nonnegative weights.

theorem sum_subtype_le_of_imp {ι : Type*} [Fintype ι]
    (P Q : ι → Prop) [DecidablePred P] [DecidablePred Q]
    (hPQ : ∀ x, P x → Q x) (w : ι → ℝ) (hw : ∀ x, 0 ≤ w x) :
    (∑ x : {x // P x}, w x.1) ≤ ∑ x : {x // Q x}, w x.1 := by
…

theorem OAI.Problem335.Pairings.sum_exactPaths_le_sum_relaxedPaths line 114
Source documentation
Dropping the diagonal inequalities introduces only nonnegative summands.
```
theorem sum_exactPaths_le_sum_relaxedPaths {α : Type*}
    [Fintype α] [DecidableEq α] {L : ℕ} (a : α)
    (τ : Fin (L + 1) → Kind) (w : (Fin L → Labels α) → ℝ)
    (hw : ∀ x, 0 ≤ w x) :
    (∑ x : ExactPaths α a τ, w x.1) ≤ ∑ x : RelaxedPaths α a τ, w x.1 := by
…
```
Mentions: OAI.Problem335.Pairings.Kind, OAI.Problem335.Pairings.Labels, OAI.Problem335.Pairings.ExactPaths, OAI.Problem335.Pairings.RelaxedPaths
theorem OAI.Problem335.Pairings.sum_compatiblePaths_le_sum_relaxedPaths line 124
Source documentation
Exact grouping followed by relaxation: the combinatorial second-trace upper bound.
```
theorem sum_compatiblePaths_le_sum_relaxedPaths {α : Type*}
    [Fintype α] [DecidableEq α] {L : ℕ} (a : α)
    (w : (Fin (L + 1) → Kind) → (Fin L → Labels α) → ℝ)
    (hw : ∀ τ x, 0 ≤ w τ x) :
    (∑ x : CompatiblePaths α (L := L) a,
…
```
Mentions: OAI.Problem335.Pairings.Kind, OAI.Problem335.Pairings.Labels, OAI.Problem335.Pairings.CompatiblePaths