LocalFactorialExpansion.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The actual local four-path table has bounded nonnegative factorial expansions.

def OAI.Problem335.FactorialExpansion.weaken line 16

Source documentation

Enlarge the permitted support and total-order bound.

def weaken {f : (σ → ℕ) → ℕ} {S T : Finset σ} {D E : ℕ}
    (F : FactorialExpansion f S D) (hS : S ⊆ T) (hD : D ≤ E) :
    FactorialExpansion f T E where
…

Mentions: OAI.Problem335.FactorialExpansion

def OAI.Problem335.LocalMoments.localPolynomialNat line 34
Source documentation
Natural-valued version of the exact local table.
```
def localPolynomialNat (derivative : Bool) (M : σ → ℕ) (p q r : σ) : ℕ :=
…
```
theorem OAI.Problem335.LocalMoments.localPolynomialNat_cast line 39
def OAI.Problem335.LocalMoments.localPolynomialExpansion line 45
Source documentation
All branches of the local four-path table have total factorial order at most two. The normal branch includes coincident coordinates and their first-order corrections.
```
def localPolynomialExpansion [Fintype σ] (derivative : Bool) (p q r : σ) :
    FactorialExpansion (fun M => localPolynomialNat derivative M p q r) {p, q, r} 2 := by
…
```
Mentions: OAI.Problem335.FactorialExpansion, OAI.Problem335.LocalMoments.localPolynomialNat

def OAI.Problem335.LocalMoments.localProductNat line 68

Source documentation

The natural polynomial for a finite set of layers.

def localProductNat {ι : Type*} (layers : Finset ι) (derivative : ι → Bool)
    (p q r : ι → σ) (M : σ → ℕ) : ℕ :=
…

theorem OAI.Problem335.LocalMoments.localProductNat_cast line 72

theorem OAI.Problem335.LocalMoments.localProduct_expansion line 80

Source documentation

This finite product is the exact nonnegative factorial expansion required by the occupation-moment comparison, rather than an assumed positivity property.

theorem localProduct_expansion {ι : Type*} [Fintype σ] (layers : Finset ι)
    (derivative : ι → Bool) (p q r : ι → σ)
    (hdis : (layers : Set ι).Pairwise fun i j =>
      Disjoint ({p i, q i, r i} : Finset σ) {p j, q j, r j}) :
    Nonempty (FactorialExpansion (localProductNat layers derivative p q r)
      (layers.biUnion fun i => {p i, q i, r i}) (2 * layers.card)) := by
…

Mentions: OAI.Problem335.FactorialExpansion, OAI.Problem335.LocalMoments.localProductNat

theorem OAI.Problem335.LocalMoments.layered_support_disjoint line 95

Source documentation

Layer-labelled coordinates automatically have disjoint local supports.

theorem layered_support_disjoint {ι κ : Type*} [DecidableEq ι] [DecidableEq κ]
    (layers : Finset ι) (p q r : ι → κ) :
    (layers : Set ι).Pairwise fun i j =>
      Disjoint ({(i, p i), (i, q i), (i, r i)} : Finset (ι × κ))
        {(j, p j), (j, q j), (j, r j)} := by
…

theorem OAI.Problem335.LocalMoments.layered_localProduct_expansion line 112

Source documentation

Specialization to the actual matrix-layer coordinate shape.

theorem layered_localProduct_expansion {ι κ : Type*}
    [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ]
    (layers : Finset ι) (derivative : ι → Bool) (p q r : ι → κ) :
    Nonempty (FactorialExpansion
      (localProductNat layers derivative (fun i => (i, p i))
        (fun i => (i, q i)) (fun i => (i, r i)))
      (layers.biUnion fun i => {(i, p i), (i, q i), (i, r i)}) (2 * layers.card)) :=
…

Mentions: OAI.Problem335.FactorialExpansion, OAI.Problem335.LocalMoments.localProductNat