PatchingWords.lean`

46 declarations, 0 contain sorry, 0 declared as axioms

Ordered signed mixed words in Popa 1308.3982v3, Lemma 3.2. The L2 continuity estimate keeps the order of every coefficient.

def OAI.Generator.Tracial.signedLetter line 16
def OAI.Generator.Tracial.patchingWord line 19
theorem OAI.Generator.Tracial.signedLetter_norm line 23
theorem OAI.Generator.Tracial.signedLetter_sub line 31
theorem OAI.Generator.Tracial.signedLetter_norm₂ line 35
theorem OAI.Generator.Tracial.patchingWord_norm_le_one line 38
theorem OAI.Generator.Tracial.patchingWord_norm₂_sub_le line 51

theorem OAI.Generator.Tracial.mixed_trace_sub_le line 88

Source documentation

Uniform trace continuity of every actual signed mixed word.

theorem mixed_trace_sub_le (τ : TracialRepresentation M)
    (v w x₀ : M.toStarSubalgebra) (hv : ‖v‖ ≤ 1) (hw : ‖w‖ ≤ 1) (h₀ : ‖x₀‖ ≤ 1)
    (xs : List (Bool × M.toStarSubalgebra)) (hx : ∀ a ∈ xs, ‖a.2‖ ≤ 1) :
    ‖τ.trace (x₀*patchingWord v xs)-τ.trace (x₀*patchingWord w xs)‖ ≤
      xs.length*τ.norm₂ (v-w) := by
…

Mentions: OAI.Generator.Tracial.patchingWord

theorem OAI.Generator.Tracial.exists_cornerUnitary_small_signed_traces line 100

Source documentation

Actual simultaneous control of signed one-patch terms, including arbitrary ambient coefficients. This uses the constructed corner unitaries in P.

theorem exists_cornerUnitary_small_signed_traces (τ : TracialRepresentation M)
    {P : VonNeumannAlgebra H} (hPM : P ≤ M)
    (hdiffP : ∀ p : P.toStarSubalgebra, IsStarProjection p → p ≠ 0 →
      ∃ q : P.toStarSubalgebra, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p*q=q ∧ q*p=q)
    (p : AlgebraProjection P) (hp : p.val ≠ 0) (F G : Finset M.toStarSubalgebra)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ v : CornerUnitary p, ∀ x ∈ F, ∀ y ∈ G, ∀ s : Bool,
      ‖τ.trace (x*signedLetter (coordinateInclusion hPM v.val) s*y)‖ < ε := by
…

Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.CornerUnitary, OAI.Generator.Tracial.signedLetter, OAI.Generator.Tracial.coordinateInclusion

def OAI.Generator.Tracial.patchingCoefficients line 140

Source documentation

The last coefficient is an endpoint; all earlier coefficients are internal.

def patchingCoefficients (F : Set M.toStarSubalgebra) : List (Bool × M.toStarSubalgebra) → Prop
  | [] => True
  | [a] => a.2 ∈ F ∪ {1}
  | a::b::xs => a.2 ∈ F ∧ patchingCoefficients F (b::xs)

theorem OAI.Generator.Tracial.patchingCoefficients_norm line 145
def OAI.Generator.Tracial.PatchingAdmissible line 164
theorem OAI.Generator.Tracial.mixed_trace_limit line 170
theorem OAI.Generator.Tracial.patchingAdmissible_limit line 181
def OAI.Generator.Tracial.zeroPartialUnitary line 205
theorem OAI.Generator.Tracial.patchingAdmissible_zero line 208

theorem OAI.Generator.Tracial.exists_maximal_patchingAdmissible line 225

Source documentation

A maximal element in the scalar mixed-word admissible set.

theorem exists_maximal_patchingAdmissible (f : AlgebraProjection M) (F : Set M.toStarSubalgebra)
    (hF : ∀ x ∈ F, ‖x‖ ≤ 1) (n : ℕ) (ε : ℕ → ℝ) :
    ∃ v : PartialUnitary M, PatchingAdmissible τ f F n ε v ∧
      ∀ w : PartialUnitary M, PatchingAdmissible τ f F n ε w → v ≤ w → w ≤ v := by
…

Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.PartialUnitary, OAI.Generator.Tracial.PatchingAdmissible

theorem OAI.Generator.Tracial.inclusion_mem_of_bounded_L2_limit line 251
def OAI.Generator.Tracial.PatchingAdmissibleIn line 268
theorem OAI.Generator.Tracial.patchingAdmissibleIn_limit line 272
theorem OAI.Generator.Tracial.exists_maximal_patchingAdmissibleIn line 284
Source documentation
The actual maximal admissible partial unitary lies in P, with mixed-word errors measured in the ambient tracial algebra M. No support-growth bound.
```
theorem exists_maximal_patchingAdmissibleIn (f : AlgebraProjection M)
    (F : Set M.toStarSubalgebra) (hF : ∀ x ∈ F, ‖x‖ ≤ 1) (n : ℕ) (ε : ℕ → ℝ) :
    ∃ v : PartialUnitary M, PatchingAdmissibleIn (P := P) τ f F n ε v ∧
…
```
Mentions: OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.PartialUnitary, OAI.Generator.Tracial.PatchingAdmissibleIn

def OAI.Generator.Tracial.boundedLists line 308

Source documentation

All lists of length at most n over a finite alphabet.

def boundedLists {α : Type*} (A : Finset α) : ℕ → Finset (List α)
  | 0 => {[]}
  | n+1 => by
    classical
    exact insert [] ((A ×ˢ boundedLists A n).image (fun z => z.1 :: z.2))

theorem OAI.Generator.Tracial.mem_boundedLists line 314
def OAI.Generator.Tracial.signedAlphabet line 325
Source documentation
A finite alphabet of signs and coefficients.
```
def signedAlphabet (F : Finset M.toStarSubalgebra) : Finset (Bool × M.toStarSubalgebra) :=
…
```
theorem OAI.Generator.Tracial.mem_signedAlphabet line 328
def OAI.Generator.Tracial.admissibleWordFamily line 333
Source documentation
Every word admitted by the source definition, with its leading coefficient.
```
def admissibleWordFamily (F : Finset M.toStarSubalgebra) (n : ℕ) :
    Finset (M.toStarSubalgebra × List (Bool × M.toStarSubalgebra)) := by
…
```
theorem OAI.Generator.Tracial.patchingCoefficients_mem line 339
theorem OAI.Generator.Tracial.mem_admissibleWordFamily line 353
def OAI.Generator.Tracial.middleWordFamily line 371
Source documentation
The uncompressed middle coefficient between the first two patch letters. Every coefficient here is internal to the original word.
```
def middleWordFamily (F : Finset M.toStarSubalgebra) (n : ℕ) :
    Finset (M.toStarSubalgebra × List (Bool × M.toStarSubalgebra)) := by
…
```
theorem OAI.Generator.Tracial.mem_middleWordFamily line 376

def OAI.Generator.Tracial.outerWordFamily line 388

Source documentation

Actual fixed outer coefficients needed for one-patch terms.

def outerWordFamily (v : M.toStarSubalgebra) (F : Finset M.toStarSubalgebra) (n : ℕ) :
    Finset M.toStarSubalgebra := by
…

theorem OAI.Generator.Tracial.mem_outerWordFamily line 394
theorem OAI.Generator.Tracial.patchingCoefficients_of_internal line 414
theorem OAI.Generator.Tracial.patchingCoefficients_append_endpoint line 425
theorem OAI.Generator.Tracial.patchingWord_append line 437
def OAI.Generator.Tracial.middleMomentError line 445
Source documentation
A_i is zero for an empty middle segment, since its sole coefficient is centered.
```
def middleMomentError (ε : ℕ → ℝ) (r : ℕ) : ℝ := if r=0 then 0 else ε r
```
theorem OAI.Generator.Tracial.admissible_middle_trace line 447

theorem OAI.Generator.Tracial.admissible_middle_second_trace line 462

Source documentation

Appending a positive v and prepending v* gives an admitted word of length r+2. The two new endpoint coefficients are exactly 1.

theorem admissible_middle_second_trace (v : PartialUnitary M) (f : AlgebraProjection M)
    (F : Set M.toStarSubalgebra) (n : ℕ) (ε : ℕ → ℝ)
    (hv : PatchingAdmissible τ f F n ε v)
    (x : M.toStarSubalgebra) (xs : List (Bool × M.toStarSubalgebra))
    (hx : x ∈ F) (hxs : ∀ a ∈ xs,a.2 ∈ F) (hlen : xs.length+2 ≤ n) :
    ‖τ.trace (star v.val*(x*patchingWord v.val xs)*v.val)‖ ≤
      ε (xs.length+2)*(τ.trace v.support.val).re := by
…

Mentions: OAI.Generator.Tracial.PartialUnitary, OAI.Generator.Tracial.AlgebraProjection, OAI.Generator.Tracial.PatchingAdmissible, OAI.Generator.Tracial.patchingWord

theorem OAI.Generator.Tracial.middleWordFamily_moments line 483
def OAI.Generator.Tracial.patchingExpansion line 506
theorem OAI.Generator.Tracial.sum_map_left_mul line 513
theorem OAI.Generator.Tracial.signedLetter_add line 519
theorem OAI.Generator.Tracial.patchingExpansion_sum line 523
theorem OAI.Generator.Tracial.patchingExpansion_length line 541
theorem OAI.Generator.Tracial.patchingExpansion_degree_le line 548
theorem OAI.Generator.Tracial.patchingExpansion_zero_filter line 563
Source documentation
The unique term containing no patch letters is exactly the original word.
```
theorem patchingExpansion_zero_filter (v w : M.toStarSubalgebra)
    (xs : List (Bool × M.toStarSubalgebra)) :
    (patchingExpansion v w xs).filter (fun z => z.1==0)=[(0,patchingWord v xs)] := by
…
```
Mentions: OAI.Generator.Tracial.patchingExpansion, OAI.Generator.Tracial.patchingWord