ShiftedOccupation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.ShiftedOccupation.signedSource line 12
Source documentation
The integer occupation after subtracting one path shift from another.
```
def signedSource {ι σ : Type*} [DecidableEq σ]
    (M : ι × σ → ℕ) (sign : ι → ℤ) (p q : ι → σ) (x : ι × σ) : ℤ :=
…
```
def OAI.Problem335.ShiftedOccupation.source line 18
Source documentation
Conversion to natural occupations; exact whenever all signed entries are nonnegative.
```
def source {ι σ : Type*} [DecidableEq σ]
    (M : ι × σ → ℕ) (sign : ι → ℤ) (p q : ι → σ) : ι × σ → ℕ :=
…
```
lemma OAI.Problem335.ShiftedOccupation.source_cast line 22
lemma OAI.Problem335.ShiftedOccupation.source_unique line 28

lemma OAI.Problem335.ShiftedOccupation.exists_source_iff line 38

Source documentation

Validity of the integer shift is exactly the existence of a natural source occupation.

lemma exists_source_iff {ι σ : Type*} [DecidableEq σ]
    (M : ι × σ → ℕ) (sign : ι → ℤ) (p q : ι → σ) :
    (∃ N : ι × σ → ℕ, ∀ x, (N x : ℤ) = signedSource M sign p q x) ↔
      ∀ x, 0 ≤ signedSource M sign p q x := by
…

Mentions: OAI.Problem335.ShiftedOccupation.signedSource

lemma OAI.Problem335.ShiftedOccupation.signedSource_layer_sum line 50

Source documentation

The two path contributions cancel in each layer, even before imposing validity.

lemma signedSource_layer_sum {ι σ : Type*} [Fintype σ] [DecidableEq σ]
    (M : ι × σ → ℕ) (sign : ι → ℤ) (p q : ι → σ) (t : ι) :
    (∑ a : σ, signedSource M sign p q (t, a)) = ∑ a : σ, (M (t, a) : ℤ) := by
…

Mentions: OAI.Problem335.ShiftedOccupation.signedSource

lemma OAI.Problem335.ShiftedOccupation.source_layer_sum line 56

Source documentation

Every layer total of a valid shifted natural occupation is unchanged.

lemma source_layer_sum {ι σ : Type*} [Fintype σ] [DecidableEq σ]
    (M : ι × σ → ℕ) (sign : ι → ℤ) (p q : ι → σ)
    (h : ∀ x, 0 ≤ signedSource M sign p q x) (t : ι) :
    (∑ a : σ, source M sign p q (t, a)) = ∑ a : σ, M (t, a) := by
…

Mentions: OAI.Problem335.ShiftedOccupation.signedSource, OAI.Problem335.ShiftedOccupation.source

lemma OAI.Problem335.ShiftedOccupation.source_layers_sum line 67

Source documentation

In particular, both bidegrees are preserved for any partition into whole layers.

lemma source_layers_sum {ι σ : Type*} [Fintype σ] [DecidableEq σ]
    (M : ι × σ → ℕ) (sign : ι → ℤ) (p q : ι → σ)
    (h : ∀ x, 0 ≤ signedSource M sign p q x) (layers : Finset ι) :
    (∑ t ∈ layers, ∑ a : σ, source M sign p q (t, a)) =
      ∑ t ∈ layers, ∑ a : σ, M (t, a) := by
…

Mentions: OAI.Problem335.ShiftedOccupation.signedSource, OAI.Problem335.ShiftedOccupation.source