ReducedCreationBlocks.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The creation and zero-block consequences of the reduced-word action. Only its action on elementary words is needed; the operator block bounds are derived by the isometric word coordinates and density.

def OAI.KadisonSimilarity.reducedCreator line 18
Source documentation
Insert the centered first letter and then use the reduced-word inclusion.
```
def reducedCreator (C : HilbertTensor E K →ₗᵢ[ℂ] H) (b : E) : K →L[ℂ] H :=
…
```
Mentions: OAI.KadisonSimilarity.HilbertTensor
theorem OAI.KadisonSimilarity.reducedCreator_apply line 22
theorem OAI.KadisonSimilarity.norm_reducedCreator_le line 26

theorem OAI.KadisonSimilarity.reduced_word_creation_blocks line 35

Source documentation

The reduced-word formula on words not beginning in the chosen free factor implies both the vanishing diagonal block and the L² creation bound.

theorem reduced_word_creation_blocks
    (J : K →ₗᵢ[ℂ] H) (C : HilbertTensor E K →ₗᵢ[ℂ] H)
    (P T : H →L[ℂ] H) (b : E)
    (hcomplement : J.toContinuousLinearMap.comp J.toContinuousLinearMap.adjoint = 1 - P)
    (hcreator : ∀ x, P (C (hilbertTensorInsert b x)) = C (hilbertTensorInsert b x))
    (hword : ∀ x, T (J x) = C (hilbertTensorInsert b x)) :
    (1 - P) * T * (1 - P) = 0 ∧ ‖P * T * (1 - P)‖ ≤ ‖b‖ := by
…

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

theorem OAI.KadisonSimilarity.norm_narrow_arc_of_reduced_word_action line 71

Source documentation

The elementary reduced-word action is sufficient for the narrow-arc compression estimate. The creation bound and zero block are conclusions.

theorem norm_narrow_arc_of_reduced_word_action
    (Ω eΩ : E) (hΩ : ‖Ω‖ = 1) (Q : K →L[ℂ] K)
    (hQ : Q.adjoint = Q) (hQsq : Q * Q = Q) (hQnorm : ‖Q‖ ≤ 1)
    (e T : HilbertTensor E K →L[ℂ] HilbertTensor E K)
    (he : e.adjoint = e) (hesq : e * e = e) (hT : T.adjoint = T)
    (heword : ∀ x, e (hilbertTensorInsert Ω x) = hilbertTensorInsert eΩ x)
    {L : Type*} [NormedAddCommGroup L] [InnerProductSpace ℂ L] [CompleteSpace L]
    {B : Type*} [NormedAddCommGroup B] [InnerProductSpace ℂ B]
    (J : L →ₗᵢ[ℂ] HilbertTensor E K) (C : HilbertTensor B L →ₗᵢ[ℂ] HilbertTensor E K)
    (b : B)
    (hcomplement : J.toContinuousLinearMap.comp J.toContinuousLinearMap.adjoint =
      1 - firstLetterProjection Ω Q)
…

Mentions: OAI.KadisonSimilarity.HilbertTensor, OAI.KadisonSimilarity.hilbertTensorInsert, OAI.KadisonSimilarity.firstLetterProjection