FourPathLocal.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.LocalMoments.ShiftRelation line 13
Source documentation
A valid source-occupation shift arising from two paths at a single layer.
```
def ShiftRelation {σ : Type*} (derivative : Bool) (M M' : σ → ℕ) (p q : σ) : Prop :=
…
```
lemma OAI.Problem335.LocalMoments.shiftRelation_normal line 17
lemma OAI.Problem335.LocalMoments.shiftRelation_derivative line 24
lemma OAI.Problem335.LocalMoments.shiftRelation_multiplication line 31
def OAI.Problem335.LocalMoments.localPolynomial line 39
Source documentation
The complete local second-trace polynomial. The all-equal case belongs to normal pairing.
```
def localPolynomial {σ : Type*} [DecidableEq σ] (derivative : Bool)
    (M : σ → ℕ) (p q r : σ) : ℝ :=
…
```

theorem OAI.Problem335.LocalMoments.fourCoefficient_eq_localPolynomial line 47

Source documentation

Matching signed coordinate differences and the actual source shift imply precisely the normal/diagonal local polynomial table from the four-path expansion.

theorem fourCoefficient_eq_localPolynomial {σ : Type*} [DecidableEq σ]
    (derivative : Bool) (M M' : σ → ℕ) (p q r s : σ)
    (hmatch : Finsupp.single p (1 : ℤ) - Finsupp.single q 1 =
      Finsupp.single r 1 - Finsupp.single s 1)
    (hshift : ShiftRelation derivative M M' p q) :
    fourCoefficient derivative (M p) (M' q) (M r) (M' s) =
      localPolynomial derivative M p q r := by
…

Mentions: OAI.Problem335.LocalMoments.ShiftRelation, OAI.Problem335.LocalMoments.fourCoefficient, OAI.Problem335.LocalMoments.localPolynomial

lemma OAI.Problem335.LocalMoments.localPolynomial_nonneg line 71

theorem OAI.Problem335.LocalMoments.four_path_products_eq_localPolynomial_product line 80

Source documentation

The local table applies simultaneously at all layers, converting the four path coefficient products into a product of occupation polynomials.

theorem four_path_products_eq_localPolynomial_product {ι σ : Type*} [DecidableEq σ]
    (layers : Finset ι) (derivative : ι → Bool) (M M' : ι → σ → ℕ)
    (p q r s : ι → σ)
    (hmatch : ∀ t ∈ layers,
      Finsupp.single (p t) (1 : ℤ) - Finsupp.single (q t) 1 =
        Finsupp.single (r t) 1 - Finsupp.single (s t) 1)
    (hshift : ∀ t ∈ layers, ShiftRelation (derivative t) (M t) (M' t) (p t) (q t)) :
    (∏ t ∈ layers, coefficient (derivative t) (M t (p t))) *
      (∏ t ∈ layers, coefficient (derivative t) (M' t (q t))) *
      (∏ t ∈ layers, coefficient (derivative t) (M t (r t))) *
      (∏ t ∈ layers, coefficient (derivative t) (M' t (s t))) =
      ∏ t ∈ layers, localPolynomial (derivative t) (M t) (p t) (q t) (r t) := by
…

Mentions: OAI.Problem335.LocalMoments.ShiftRelation, OAI.Problem335.LocalMoments.coefficient, OAI.Problem335.LocalMoments.localPolynomial