BidegreeShiftedOccupation.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem335.ShiftedOccupation.bidegreeWeight_eq_of_layer_sums line 12

def OAI.Problem335.ShiftedOccupation.sourceFinsupp line 28

Source documentation

A natural shifted occupation, represented in the canonical finite-exponent type.

def sourceFinsupp {ι σ : Type*} [Fintype ι] [Fintype σ] [DecidableEq σ]
    (M : (ι × σ) →₀ ℕ) (sign : ι → ℤ) (p q : ι → σ) : (ι × σ) →₀ ℕ :=
…

lemma OAI.Problem335.ShiftedOccupation.sourceFinsupp_apply line 32
lemma OAI.Problem335.ShiftedOccupation.sourceFinsupp_bidegree line 37

theorem OAI.Problem335.ShiftedOccupation.exists_bidegree_source_iff line 49

Source documentation

Existence inside the exact bidegree-index subtype is equivalent to coordinate nonnegativity.

theorem exists_bidegree_source_iff {ι σ : Type*} [Fintype ι] [Fintype σ]
    [DecidableEq σ] (side : ι → Bool) (a b : ℕ)
    (M : (ι × σ) →₀ ℕ)
    (hM : Finsupp.weight (bidegreeWeight (fun x : ι × σ => side x.1)) M = (a, b))
    (sign : ι → ℤ) (p q : ι → σ) :
    (∃ N : {d : (ι × σ) →₀ ℕ |
        Finsupp.weight (bidegreeWeight (fun x : ι × σ => side x.1)) d = (a, b)},
      ∀ x, ((N.1 x : ℕ) : ℤ) = signedSource M sign p q x) ↔
      ∀ x, 0 ≤ signedSource M sign p q x := by
…

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

abbrev OAI.Problem335.ShiftedOccupation.BidegreeSource line 70
Source documentation
The canonical source exponent subtype used by the bidegree monomial basis.
```
abbrev BidegreeSource {ι σ : Type*} (side : ι → Bool) (a b : ℕ) :=
…
```
def OAI.Problem335.ShiftedOccupation.sourceEmbedding line 74
lemma OAI.Problem335.ShiftedOccupation.sourceEmbedding_injective line 78
def OAI.Problem335.ShiftedOccupation.sourceIndex line 89
Source documentation
The unique shifted source as an element of the original bidegree domain.
```
def sourceIndex {ι σ : Type*} [Fintype ι] [Fintype σ] [DecidableEq σ]
    {side : ι → Bool} {a b : ℕ} (M : BidegreeSource (σ := σ) side a b)
…
```
Mentions: OAI.Problem335.ShiftedOccupation.BidegreeSource
lemma OAI.Problem335.ShiftedOccupation.sourceIndex_embedding line 95
lemma OAI.Problem335.ShiftedOccupation.extend_source_valid line 103
lemma OAI.Problem335.ShiftedOccupation.extend_source_invalid line 113