FockLayerProfile.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem335.FockLayerProfile.currySigned line 16
Source documentation
Read a signed exponent by its layer and matrix-entry coordinates.
```
def currySigned : ((Fin n × ι × ι) →₀ ℤ) →+ (Fin n → ι × ι → ℤ) where
…
```
lemma OAI.Problem335.FockLayerProfile.currySigned_injective line 21
lemma OAI.Problem335.FockLayerProfile.currySigned_signedOccupation line 26

theorem OAI.Problem335.FockLayerProfile.pathAmplitude_eq_layered line 31

Source documentation

The list-path coefficient is exactly the coefficient of its layer profile.

theorem pathAmplitude_eq_layered (side : Fin n → Bool)
    (p : List (Fin n × ι × ι)) (hp : p.map Prod.fst = List.finRange n)
    (d : (Fin n × ι × ι) →₀ ℕ) :
    (p.map (occupationAmplitude (fun e => side e.1) d)).prod =
      LayeredFourPath.amplitude side (fun t x => d (t, x)) (edgeProfile p hp) := by
…

Mentions: OAI.Problem335.occupationAmplitude, OAI.Problem335.LayeredFourPath.amplitude, OAI.Problem335.edgeProfile

theorem OAI.Problem335.FockLayerProfile.occupationShift_eq_layered line 40
Source documentation
Signed list shifts and signed layer-profile shifts have identical coordinates.
```
theorem occupationShift_eq_layered [DecidableEq ι] (side : Fin n → Bool)
    (p : List (Fin n × ι × ι)) (hp : p.map Prod.fst = List.finRange n) :
    currySigned (occupationShift (fun e => side e.1) p) =
      LayeredFourPath.signedShift side (edgeProfile p hp) := by
…
```
Mentions: OAI.Problem335.FockLayerProfile.currySigned, OAI.Problem335.occupationShift, OAI.Problem335.LayeredFourPath.signedShift, OAI.Problem335.edgeProfile

theorem OAI.Problem335.FockLayerProfile.zeroExtend_eq_layered line 54

Source documentation

Changing from finitely supported signed occupations to layer coordinates preserves zero extension, including arguments outside the finite source.

theorem zeroExtend_eq_layered {I : Type*}
    (d : I → (Fin n × ι × ι) →₀ ℕ) (hd : Function.Injective d)
    (w : I → ℝ) (x : (Fin n × ι × ι) →₀ ℤ) :
    Function.extend (fun i => Problem335.signedOccupation (d i)) w (fun _ => 0) x =
      Function.extend (fun i => LayeredFourPath.signedOccupation (fun t y => d i (t, y)))
        w (fun _ => 0) (currySigned x) := by
…

Mentions: OAI.Problem335.signedOccupation, OAI.Problem335.LayeredFourPath.signedOccupation, OAI.Problem335.FockLayerProfile.currySigned

theorem OAI.Problem335.FockLayerProfile.zeroExtended_pathAmplitude_four_le_local_product line 75

Source documentation

The exact list-path four-amplitude summand is bounded by the local table of its layer profiles. No closure assumption for the shifted source is needed.

theorem zeroExtended_pathAmplitude_four_le_local_product
    {I : Type*} [DecidableEq ι] (side : Fin n → Bool)
    (d : I → (Fin n × ι × ι) →₀ ℕ) (hd : Function.Injective d) (i : I)
    (p q r s : List (Fin n × ι × ι))
    (hp : p.map Prod.fst = List.finRange n)
    (hq : q.map Prod.fst = List.finRange n)
    (hr : r.map Prod.fst = List.finRange n)
    (hs : s.map Prod.fst = List.finRange n)
    (hmatch : occupationShift (fun e => side e.1) p - occupationShift (fun e => side e.1) q =
      occupationShift (fun e => side e.1) r - occupationShift (fun e => side e.1) s) :
    (p.map (occupationAmplitude (fun e => side e.1) (d i))).prod *
      Function.extend (fun k => Problem335.signedOccupation (d k))
…

Mentions: OAI.Problem335.occupationShift, OAI.Problem335.occupationAmplitude, OAI.Problem335.signedOccupation

theorem OAI.Problem335.FockLayerProfile.edgeProfile_ofFn line 114

Source documentation

Profile reconstruction simplifies on an explicitly layer-indexed edge list.

@[simp] theorem edgeProfile_ofFn (f : Fin n → ι × ι)
    (h : (List.ofFn (fun t => (t, f t))).map Prod.fst = List.finRange n) :
    edgeProfile (List.ofFn (fun t => (t, f t))) h = f := by
…

Mentions: OAI.Problem335.edgeProfile

theorem OAI.Problem335.FockLayerProfile.edgeProfile_immInternalPathEdges line 121

Source documentation

Reindexing an IMM path by its internal vertices also reindexes its layer profile.

@[simp] theorem edgeProfile_immInternalPathEdges (d : ℕ) (p : Fin d → Fin (d + 1))
    (h : (immInternalPathEdges d p).map Prod.fst = List.finRange (d + 1)) :
    edgeProfile (immInternalPathEdges d p) h =
      fun t => (Fin.cons (α := fun _ => Fin (d + 1)) 0 p t,
…

Mentions: OAI.Problem335.immInternalPathEdges, OAI.Problem335.edgeProfile

def OAI.Problem335.FockLayerProfile.immProfile line 129
Source documentation
The canonical layer profile of a list-indexed IMM path.
```
def immProfile (n : ℕ) (hn : 0 < n) (p : Fin (immPaths n hn).length) :
    Fin n → Fin n × Fin n :=
…
```
Mentions: OAI.Problem335.immPaths
theorem OAI.Problem335.FockLayerProfile.immPathAmplitude_eq_layered line 134

theorem OAI.Problem335.FockLayerProfile.imm_zeroExtended_amplitude_four_le_local_product line 142

Source documentation

The actual IMM list-path summand, with the second source zero-extended, is bounded by its layerwise occupation table.

theorem imm_zeroExtended_amplitude_four_le_local_product
    {I : Type*} (n : ℕ) (hn : 0 < n) (side : Fin n → Bool)
    (d : I → (Fin n × Fin n × Fin n) →₀ ℕ) (hd : Function.Injective d) (i : I)
    (p q r s : Fin (immPaths n hn).length)
    (hmatch : occupationShift (fun e => side e.1) ((immPaths n hn).get p) -
        occupationShift (fun e => side e.1) ((immPaths n hn).get q) =
      occupationShift (fun e => side e.1) ((immPaths n hn).get r) -
        occupationShift (fun e => side e.1) ((immPaths n hn).get s)) :
    immPathAmplitude n hn (fun e => side e.1) (d i) p *
      Function.extend (fun k => Problem335.signedOccupation (d k))
        (fun k => immPathAmplitude n hn (fun e => side e.1) (d k) q) (fun _ => 0)
        (Problem335.signedOccupation (d i) +
…

Mentions: OAI.Problem335.immPaths, OAI.Problem335.occupationShift, OAI.Problem335.immPathAmplitude, OAI.Problem335.signedOccupation