OAI/Analysis/KadisonSimilarity/FreeProduct/WordPropagationTransfer.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KadisonSimilarity.repeatedWordInclusion line 24

   Source documentation

   The concrete column at a fixed word degree, endpoint, and repeated letter.

   def repeatedWordInclusion (n : ℕ) (R : K →ₗᵢ[ℂ] J n)
       (d : E) (r : F) (hd : ‖d‖ = 1) (hr : ‖r‖ = 1) : K →ₗᵢ[ℂ] H where
   …

2. theorem OAI.KadisonSimilarity.repeatedWordInclusion_apply line 36
3. theorem OAI.KadisonSimilarity.norm_repeatedWordInclusion_error_le line 44

   Source documentation

   A multiplicity error has exactly the same norm in a normalized word column. This supplies the full-output error needed in the Hankel test.

   theorem norm_repeatedWordInclusion_error_le (n : ℕ) (R : K →ₗᵢ[ℂ] J n)
       (d : E) (r : F) (hd : ‖d‖ = 1) (hr : ‖r‖ = 1)
       (Y : H →L[ℂ] H) (B : K →L[ℂ] K) (Bn : J n →L[ℂ] J n)
       (hY : ∀ v, Y (U.inclusion n (hilbertTensorInsert v
           (endpointWord d (fun _ : Fin n => r)))) =
         U.inclusion n (hilbertTensorInsert (Bn v)
           (endpointWord d (fun _ : Fin n => r))))
       {η : ℝ} (hη : 0 ≤ η)
       (hprop : ∀ x, ‖Bn (R x) - R (B x)‖ ≤ η * ‖x‖) :
       ‖Y.comp (repeatedWordInclusion U n R d r hd hr).toContinuousLinearMap -
         (repeatedWordInclusion U n R d r hd hr).toContinuousLinearMap.comp B‖ ≤ η := by
   …

   Mentions: OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.endpointWord, OAI.KadisonSimilarity.repeatedWordInclusion

4. theorem OAI.KadisonSimilarity.repeatedWordInclusion_orthogonal line 70

   Source documentation

   Word columns at different degrees are orthogonal.

   theorem repeatedWordInclusion_orthogonal (n m : ℕ) (hnm : n ≠ m)
       (Rn : K →ₗᵢ[ℂ] J n) (Rm : K →ₗᵢ[ℂ] J m)
       (d : E) (r : F) (hd : ‖d‖ = 1) (hr : ‖r‖ = 1) (x y : K) :
       inner ℂ (repeatedWordInclusion U n Rn d r hd hr x)
         (repeatedWordInclusion U m Rm d r hd hr y) = 0 :=
   …

   Mentions: OAI.KadisonSimilarity.repeatedWordInclusion

5. theorem OAI.KadisonSimilarity.free_corner_from_multiplicity_propagation line 79

   Source documentation

   The finite Fourier test consumes the derived multiplicity propagation bounds, with the orthogonality and full-column errors constructed here.

   theorem free_corner_from_multiplicity_propagation
       {N : ℕ} (hN : 0 < N) (R : ∀ n, K →ₗᵢ[ℂ] J n)
       (d : E) (r : F) (hd : ‖d‖ = 1) (hr : ‖r‖ = 1)
       (Y T : H →L[ℂ] H) (B S : K →L[ℂ] K) (Bn : ∀ n, J n →L[ℂ] J n)
       (hY : ∀ n v, Y (U.inclusion n (hilbertTensorInsert v
           (endpointWord d (fun _ : Fin n => r)))) =
         U.inclusion n (hilbertTensorInsert (Bn n v)
           (endpointWord d (fun _ : Fin n => r))))
       (hYstar : ∀ n v, Y.adjoint (U.inclusion n (hilbertTensorInsert v
           (endpointWord d (fun _ : Fin n => r)))) =
         U.inclusion n (hilbertTensorInsert ((Bn n).adjoint v)
           (endpointWord d (fun _ : Fin n => r))))
   …

   Mentions: OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.endpointWord