LayeredFourPath.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.LayeredFourPath.signedOccupation line 12
Source documentation
Signed occupations, retaining the layer coordinate explicitly.
```
def signedOccupation {T σ : Type*} (M : T → σ → ℕ) : T → σ → ℤ :=
…
```
def OAI.Problem335.LayeredFourPath.signedShift line 16
Source documentation
Every path chooses exactly one coordinate in every layer.
```
def signedShift {T σ : Type*} [DecidableEq σ]
    (side : T → Bool) (p : T → σ) : T → σ → ℤ :=
…
```

def OAI.Problem335.LayeredFourPath.amplitude line 21

Source documentation

The Fock coefficient of a layered path.

def amplitude {T σ : Type*} [Fintype T]
    (side : T → Bool) (M : T → σ → ℕ) (p : T → σ) : ℝ :=
…

theorem OAI.Problem335.LayeredFourPath.coordinate_matching_of_signedShift line 26

Source documentation

Compatibility of global signed shifts gives the local pairing identity at every layer.

theorem coordinate_matching_of_signedShift {T σ : Type*} [DecidableEq σ]
    (side : T → Bool) (p q r s : T → σ)
    (h : signedShift side p - signedShift side q =
      signedShift side r - signedShift side s) (t : T) :
    Finsupp.single (p t) (1 : ℤ) - Finsupp.single (q t) 1 =
      Finsupp.single (r t) 1 - Finsupp.single (s t) 1 := by
…

Mentions: OAI.Problem335.LayeredFourPath.signedShift

theorem OAI.Problem335.LayeredFourPath.local_shift_of_signedOccupation line 39

Source documentation

An actual shifted source automatically satisfies the local occupation relation.

theorem local_shift_of_signedOccupation {T σ : Type*} [DecidableEq σ]
    (side : T → Bool) (M M' : T → σ → ℕ) (p q : T → σ)
    (h : signedOccupation M' =
      signedOccupation M + signedShift side p - signedShift side q) (t : T) :
    LocalMoments.ShiftRelation (side t) (M t) (M' t) (p t) (q t) := by
…

Mentions: OAI.Problem335.LayeredFourPath.signedOccupation, OAI.Problem335.LayeredFourPath.signedShift, OAI.Problem335.LocalMoments.ShiftRelation

theorem OAI.Problem335.LayeredFourPath.amplitude_four_eq_local_product line 54

Source documentation

The entire valid four-path coefficient is the product of the local occupation table.

theorem amplitude_four_eq_local_product {T σ : Type*} [Fintype T] [DecidableEq σ]
    (side : T → Bool) (M M' : T → σ → ℕ) (p q r s : T → σ)
    (hmatch : signedShift side p - signedShift side q =
      signedShift side r - signedShift side s)
    (hshift : signedOccupation M' =
      signedOccupation M + signedShift side p - signedShift side q) :
    amplitude side M p * amplitude side M' q * amplitude side M r * amplitude side M' s =
      ∏ t, LocalMoments.localPolynomial (side t) (M t) (p t) (q t) (r t) := by
…

Mentions: OAI.Problem335.LayeredFourPath.signedShift, OAI.Problem335.LayeredFourPath.signedOccupation, OAI.Problem335.LayeredFourPath.amplitude, OAI.Problem335.LocalMoments.localPolynomial

theorem OAI.Problem335.LayeredFourPath.zeroExtended_amplitude_four_le_local_product line 69

Source documentation

Lift the valid-source identity to a zero extension. Missing shifted source occupations contribute zero, so an upper estimate needs no source-validity-closure hypothesis.

theorem zeroExtended_amplitude_four_le_local_product
    {I T σ : Type*} [Fintype T] [DecidableEq σ]
    (side : T → Bool) (M : I → T → σ → ℕ)
    (hinj : Function.Injective (fun i => signedOccupation (M i)))
    (i : I) (p q r s : T → σ)
    (hmatch : signedShift side p - signedShift side q =
      signedShift side r - signedShift side s) :
    amplitude side (M i) p *
        Function.extend (fun k => signedOccupation (M k))
          (fun k => amplitude side (M k) q) (fun _ => 0)
          (signedOccupation (M i) + signedShift side p - signedShift side q) *
      amplitude side (M i) r *
…

Mentions: OAI.Problem335.LayeredFourPath.signedOccupation, OAI.Problem335.LayeredFourPath.signedShift, OAI.Problem335.LayeredFourPath.amplitude