OAI/Analysis/KadisonKastler/RelativeHaarBlocks.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KadisonKastler.haarPower_mem_of_mem line 13
2. theorem OAI.KadisonKastler.chain_nonzero line 25
3. structure OAI.KadisonKastler.RelativeHaarBlock line 37

   Source documentation

   A nonempty Haar block with centered base separators and a base prefix.

   structure RelativeHaarBlock (τ : FaithfulTracialState B) (D : StarSubalgebra ℂ B)
       (s : unitary B) where
   …

   Mentions: OAI.KadisonKastler.FaithfulTracialState

4. def OAI.KadisonKastler.RelativeHaarBlock.value line 52
5. def OAI.KadisonKastler.RelativeHaarBlock.single line 55
6. theorem OAI.KadisonKastler.RelativeHaarBlock.value_single line 59
7. def OAI.KadisonKastler.RelativeHaarBlock.append line 63
8. theorem OAI.KadisonKastler.RelativeHaarBlock.value_append line 86
9. theorem OAI.KadisonKastler.RelativeHaarBlock.mem line 93
10. theorem OAI.KadisonKastler.RelativeHaarBlock.expectation_zero line 102
11. def OAI.KadisonKastler.conjugateBlockPrefix line 113

    Source documentation

    A completed alternating prefix: each pair is a conjugated block and a following kernel letter.

    def conjugateBlockPrefix (w : unitary B) (a : B) (l : List (B × B)) : B :=
    …

12. theorem OAI.KadisonKastler.conjugateBlockPrefix_append line 116
13. def OAI.KadisonKastler.completedCoefficients line 124
14. theorem OAI.KadisonKastler.completedCoefficients_word line 128
15. theorem OAI.KadisonKastler.HaarEndpointIndependence.completed_blocks line 149

    Source documentation

    Every completed prefix and final kernel block is annihilated by the published endpoint formula.

    theorem HaarEndpointIndependence.completed_blocks
        {τ : FaithfulTracialState B} {D : StarSubalgebra ℂ B} {X : Submodule ℂ B}
        {w : unitary B} (h : HaarEndpointIndependence τ D X w)
        (a b r : B) (l : List (B × B)) (ha : a ∈ X ∨ a = 1) (hb : b ∈ X ∨ b = 1)
        (hr : r ∈ X) (hl : ∀ z ∈ l, z.1 ∈ X ∧ z.2 ∈ X) :
        TraceOrthogonal τ D
          (conjugateBlockPrefix w a l * ((w : B) * r * star (w : B)) * b) := by
    …

    Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.HaarEndpointIndependence, OAI.KadisonKastler.TraceOrthogonal, OAI.KadisonKastler.conjugateBlockPrefix