FactorialPositive.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

Nonnegative falling-factorial expansions for the local trace weights.

def OAI.Problem335.factorialMonomial line 13
Source documentation
Evaluation of a falling-factorial monomial at a natural occupation vector.
```
def factorialMonomial {σ : Type u} [Fintype σ]
    (d M : σ → ℕ) : ℕ := ∏ i, (M i).descFactorial (d i)
```
structure OAI.Problem335.FactorialExpansion line 18
Source documentation
A finite expansion with natural (hence nonnegative) coefficients, bounded total order, supported on a specified coordinate set.
```
structure FactorialExpansion {σ : Type u} [Fintype σ]
    (f : (σ → ℕ) → ℕ) (S : Finset σ) (D : ℕ) where
…
```

def OAI.Problem335.FactorialExpansion.add line 35

Source documentation

Addition preserves positivity of the factorial-basis coefficients.

def add {f g : (σ → ℕ) → ℕ} {S : Finset σ} {D : ℕ}
    (F : FactorialExpansion f S D) (G : FactorialExpansion g S D) :
    FactorialExpansion (fun M => f M + g M) S D where
…

Mentions: OAI.Problem335.FactorialExpansion

def OAI.Problem335.FactorialExpansion.mul line 50

Source documentation

A disjoint-coordinate product has the product of the local coefficients.

def mul {f g : (σ → ℕ) → ℕ} {S T : Finset σ} {D E : ℕ}
    (F : FactorialExpansion f S D) (G : FactorialExpansion g T E)
    (hST : Disjoint S T) :
    FactorialExpansion (fun M => f M * g M) (S ∪ T) (D + E) where
…

Mentions: OAI.Problem335.FactorialExpansion

theorem OAI.Problem335.FactorialExpansion.factorialMonomial_single line 86

def OAI.Problem335.FactorialExpansion.coordinate line 91

Source documentation

Lift an explicit univariate expansion to one selected coordinate.

def coordinate (i : σ) (J : Type) [Fintype J] (c e : J → ℕ)
    {f : ℕ → ℕ} {D : ℕ} (he : ∀ j, e j ≤ D)
    (hf : ∀ z, f z = ∑ j, c j * z.descFactorial (e j)) :
    FactorialExpansion (fun M => f (M i)) {i} D where
…

Mentions: OAI.Problem335.FactorialExpansion

def OAI.Problem335.FactorialExpansion.occupation line 107
Source documentation
The occupation itself has order one.
```
def occupation (i : σ) : FactorialExpansion (fun M => M i) {i} 1 :=
…
```
Mentions: OAI.Problem335.FactorialExpansion
def OAI.Problem335.FactorialExpansion.successor line 111
Source documentation
Creation operators contribute the successor occupation.
```
def successor (i : σ) : FactorialExpansion (fun M => M i + 1) {i} 1 :=
…
```
Mentions: OAI.Problem335.FactorialExpansion
theorem OAI.Problem335.FactorialExpansion.square_descFactorial line 116
def OAI.Problem335.FactorialExpansion.square line 122
Source documentation
A repeated annihilation coordinate retains its extra first-order term.
```
def square (i : σ) : FactorialExpansion (fun M => (M i) ^ 2) {i} 2 :=
…
```
Mentions: OAI.Problem335.FactorialExpansion
def OAI.Problem335.FactorialExpansion.successorSquare line 128
Source documentation
The repeated creation-coordinate weight has coefficients 1,3,1.
```
def successorSquare (i : σ) :
    FactorialExpansion (fun M => (M i + 1) ^ 2) {i} 2 :=
…
```
Mentions: OAI.Problem335.FactorialExpansion
def OAI.Problem335.FactorialExpansion.reframe line 142
Source documentation
Copy the coefficient data while enlarging bounds or changing the displayed function by pointwise equality. Unlike a type cast, this keeps all data projections transparent.
```
def reframe {f g : (σ → ℕ) → ℕ} {S T : Finset σ} {D E : ℕ}
    (F : FactorialExpansion f S D) (hfg : ∀ M, f M = g M)
    (hST : S ⊆ T) (hDE : D ≤ E) : FactorialExpansion g T E where
…
```
Mentions: OAI.Problem335.FactorialExpansion
def OAI.Problem335.FactorialExpansion.normalDerivative line 154
Source documentation
The normal pairing in a derivative layer, including equal coordinates.
```
def normalDerivative (i j : σ) :
    FactorialExpansion (fun M => M i * M j) {i, j} 2 := by
…
```
Mentions: OAI.Problem335.FactorialExpansion
def OAI.Problem335.FactorialExpansion.normalMultiplication line 162
Source documentation
The normal pairing in a multiplication layer, including equal coordinates.
```
def normalMultiplication (i j : σ) :
    FactorialExpansion (fun M => (M i + 1) * (M j + 1)) {i, j} 2 := by
…
```
Mentions: OAI.Problem335.FactorialExpansion
def OAI.Problem335.FactorialExpansion.distinctDerivative line 170
Source documentation
The distinct-coordinate pairing in a derivative layer.
```
def distinctDerivative (i j : σ) (h : i ≠ j) :
    FactorialExpansion (fun M => M i * (M j + 1)) {i, j} 2 :=
…
```
Mentions: OAI.Problem335.FactorialExpansion
def OAI.Problem335.FactorialExpansion.distinctMultiplication line 176
Source documentation
The distinct-coordinate pairing in a multiplication layer.
```
def distinctMultiplication (i j : σ) (h : i ≠ j) :
    FactorialExpansion (fun M => (M i + 1) * M j) {i, j} 2 :=
…
```
Mentions: OAI.Problem335.FactorialExpansion
theorem OAI.Problem335.FactorialExpansion.eval_real line 183
Source documentation
The same expansion as a real-valued sum, ready for expectation comparisons.
```
theorem eval_real {f : (σ → ℕ) → ℕ} {S : Finset σ} {D : ℕ}
    (F : FactorialExpansion f S D) (M : σ → ℕ) :
    (f M : ℝ) = ∑ j, (F.coeff j : ℝ) * (factorialMonomial (F.degree j) M : ℝ) := by
…
```
Mentions: OAI.Problem335.FactorialExpansion, OAI.Problem335.factorialMonomial
def OAI.Problem335.FactorialExpansion.constant line 189
Source documentation
A constant has a single order-zero term.
```
def constant (c : ℕ) : FactorialExpansion (fun _ : σ → ℕ => c) ∅ 0 where
…
```
Mentions: OAI.Problem335.FactorialExpansion

theorem OAI.Problem335.FactorialExpansion.nonempty_prod line 200

Source documentation

Products of local weights on pairwise disjoint coordinate sets retain a nonnegative factorial expansion, and their local order bounds add.

theorem nonempty_prod {ι : Type*} (s : Finset ι)
    (f : ι → (σ → ℕ) → ℕ) (S : ι → Finset σ) (D : ι → ℕ)
    (F : ∀ i, FactorialExpansion (f i) (S i) (D i))
    (hS : (s : Set ι).Pairwise fun i j => Disjoint (S i) (S j)) :
    Nonempty (FactorialExpansion (fun M => ∏ i ∈ s, f i M)
      (s.biUnion S) (∑ i ∈ s, D i)) := by
…

Mentions: OAI.Problem335.FactorialExpansion

theorem OAI.Problem335.FactorialExpansion.linear_eval line 231

Source documentation

Any real linear functional can be evaluated termwise in the expansion.

theorem linear_eval {f : (σ → ℕ) → ℕ} {S : Finset σ} {D : ℕ}
    (F : FactorialExpansion f S D)
    (L : ((σ → ℕ) → ℝ) →ₗ[ℝ] ℝ) :
    L (fun M => (f M : ℝ)) =
      ∑ j, (F.coeff j : ℝ) * L (fun M => (factorialMonomial (F.degree j) M : ℝ)) := by
…

Mentions: OAI.Problem335.FactorialExpansion, OAI.Problem335.factorialMonomial

theorem OAI.Problem335.FactorialExpansion.linear_comparison line 245

Source documentation

Termwise moment comparison extends to every nonnegative factorial expansion.

theorem linear_comparison {f : (σ → ℕ) → ℕ} {S : Finset σ} {D : ℕ}
    (F : FactorialExpansion f S D)
    (L R : ((σ → ℕ) → ℝ) →ₗ[ℝ] ℝ) (C : ℝ)
    (h : ∀ d : σ → ℕ, (∑ i, d i) ≤ D → (∀ i, i ∉ S → d i = 0) →
      L (fun M => (factorialMonomial d M : ℝ)) ≤
        C * R (fun M => (factorialMonomial d M : ℝ))) :
    L (fun M => (f M : ℝ)) ≤ C * R (fun M => (f M : ℝ)) := by
…

Mentions: OAI.Problem335.FactorialExpansion, OAI.Problem335.factorialMonomial