TensorPacketDensity.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Dense elementary tensor tests for bounded maps on regrouped word spaces.

theorem OAI.KadisonSimilarity.continuousLinearMap_ext_hilbertTensorInsert_normed line 22
Source documentation
Hilbert tensor totality needs only a normed codomain.
```
theorem continuousLinearMap_ext_hilbertTensorInsert_normed
    (f g : HilbertTensor X B →L[ℂ] K)
    (h : ∀ a b, f (hilbertTensorInsert a b) = g (hilbertTensorInsert a b)) : f = g := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.hilbertTensorInsert
theorem OAI.KadisonSimilarity.continuous_hilbertTensorPair line 35
def OAI.KadisonSimilarity.tensorPacket line 41
Source documentation
One completed multiplicity word and one completed endpoint word.
```
def tensorPacket {n : ℕ} (p : ((Fin n → X) × B) × (E × (Fin n → F))) :
    HilbertTensor (HilbertTensor (CompletedTensorWord X n) B) (EndpointTensor E F n) :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.EndpointTensor
theorem OAI.KadisonSimilarity.continuousLinearMap_ext_tensorPackets line 47
Source documentation
Completed word packets span their full Hilbert tensor space.
```
theorem continuousLinearMap_ext_tensorPackets {n : ℕ}
    (f g : HilbertTensor (HilbertTensor (CompletedTensorWord X n) B)
      (EndpointTensor E F n) →L[ℂ] K)
    (h : ∀ p, f (tensorPacket p) = g (tensorPacket p)) : f = g := by
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.tensorPacket

theorem OAI.KadisonSimilarity.continuousLinearMap_ext_denseCompletedWords line 71

Source documentation

Dense alphabet vectors determine a map on completed tensor words.

theorem continuousLinearMap_ext_denseCompletedWords {DX : Type*} (vx : DX → X)
    (hx : DenseRange vx) {n : ℕ} (f g : CompletedTensorWord X n →L[ℂ] K)
    (h : ∀ a : Fin n → DX, f (completedTensorWord (fun i => vx (a i))) =
      g (completedTensorWord (fun i => vx (a i)))) : f = g := by
…

Mentions: OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.completedTensorWord

theorem OAI.KadisonSimilarity.continuousLinearMap_ext_denseMultiplicityWords line 83

Source documentation

Dense base vectors and centered alphabets determine multiplicity maps.

theorem continuousLinearMap_ext_denseMultiplicityWords {DX DB : Type*}
    (vx : DX → X) (vb : DB → B) (hx : DenseRange vx) (hb : DenseRange vb) {n : ℕ}
    (f g : HilbertTensor (CompletedTensorWord X n) B →L[ℂ] K)
    (h : ∀ (a : Fin n → DX) (b : DB),
      f (hilbertTensorInsert (completedTensorWord (fun i => vx (a i))) (vb b)) =
      g (hilbertTensorInsert (completedTensorWord (fun i => vx (a i))) (vb b))) : f = g := by
…

Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.completedTensorWord

theorem OAI.KadisonSimilarity.continuousLinearMap_ext_denseEndpointWords line 103

Source documentation

Dense endpoint vectors and centered alphabets determine endpoint maps.

theorem continuousLinearMap_ext_denseEndpointWords {DE DF : Type*}
    (ve : DE → E) (vf : DF → F) (he : DenseRange ve) (hf : DenseRange vf) {n : ℕ}
    (f g : EndpointTensor E F n →L[ℂ] K)
    (h : ∀ (d : DE) (c : Fin n → DF),
      f (endpointWord (ve d) (fun i => vf (c i))) =
        g (endpointWord (ve d) (fun i => vf (c i)))) : f = g := by
…

Mentions: OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.endpointWord

theorem OAI.KadisonSimilarity.continuousLinearMap_ext_denseTensorPackets line 124

Source documentation

Dense choices for each algebra letter suffice in the packet test.

theorem continuousLinearMap_ext_denseTensorPackets
    {DX DB DE DF : Type*} (vx : DX → X) (vb : DB → B) (ve : DE → E) (vf : DF → F)
    (hx : DenseRange vx) (hb : DenseRange vb) (he : DenseRange ve) (hf : DenseRange vf)
    {n : ℕ} (f g : HilbertTensor (HilbertTensor (CompletedTensorWord X n) B)
      (EndpointTensor E F n) →L[ℂ] K)
    (h : ∀ (a : Fin n → DX) (b : DB) (d : DE) (c : Fin n → DF),
      f (tensorPacket ((fun i => vx (a i), vb b), (ve d, fun i => vf (c i)))) =
        g (tensorPacket ((fun i => vx (a i), vb b), (ve d, fun i => vf (c i))))) : f = g := by
…

Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.tensorPacket

theorem OAI.KadisonSimilarity.function_ext_denseTensorPackets line 147

Source documentation

A function-level form avoids comparing bundled maps across independently synthesized completed-tensor instances.

theorem function_ext_denseTensorPackets
    {DX DB DE DF : Type*} (vx : DX → X) (vb : DB → B) (ve : DE → E) (vf : DF → F)
    (hx : DenseRange vx) (hb : DenseRange vb) (he : DenseRange ve) (hf : DenseRange vf)
    {n : ℕ}
    (p q : HilbertTensor (HilbertTensor (CompletedTensorWord X n) B) (EndpointTensor E F n) → K)
    (hp : Continuous p) (hq : Continuous q)
    (hpadd : ∀ x y, p (x + y) = p x + p y) (hqadd : ∀ x y, q (x + y) = q x + q y)
    (hpsmul : ∀ (c : ℂ) x, p (c • x) = c • p x)
    (hqsmul : ∀ (c : ℂ) x, q (c • x) = c • q x)
    (h : ∀ (a : Fin n → DX) (b : DB) (d : DE) (c : Fin n → DF),
      p (tensorPacket ((fun i => vx (a i), vb b), (ve d, fun i => vf (c i)))) =
        q (tensorPacket ((fun i => vx (a i), vb b), (ve d, fun i => vf (c i))))) : p = q := by
…

Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.CompletedTensorWord, OAI.KadisonSimilarity.EndpointTensor, OAI.KadisonSimilarity.tensorPacket