FreeProjectionWords.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Summing the cuts of free diagonal projection words

The estimates here concern the structural free diagonal model itself. Every cut is factored through the ordered-tuple matrix, and the factorial factors in the preservation cuts are summed before scalar restoration.

theorem OAI.KadisonKastler.FreeDiagonalModel.norm_sum_noPreservationWordCut_le line 28
theorem OAI.KadisonKastler.FreeDiagonalModel.norm_sum_preservationWordCut_le line 36

theorem OAI.KadisonKastler.FreeDiagonalModel.norm_noPreservationCuts_le line 54

Source documentation

All cuts without a preserved letter have one common denominator.

theorem norm_noPreservationCuts_le {r : ℕ} (hW : W.card = r)
    (position : Fin r → ι) :
    ‖∑ k ∈ range (r + 1), ∑ t : OrderedLabelTuple W r,
      M.noPreservationWordCut W position t k‖ ≤
      (r + 1 : ℝ) * Real.sqrt (r.factorial : ℝ) /
        Real.sqrt ((Fintype.card α : ℝ) ^ r) := by
…

Mentions: OAI.KadisonKastler.OrderedLabelTuple

theorem OAI.KadisonKastler.FreeDiagonalModel.norm_preservationCuts_le line 72

Source documentation

Summing preservation cuts retains the reciprocal-binomial factor, which is uniformly bounded independently of the word length.

theorem norm_preservationCuts_le {r : ℕ} (hr : 1 ≤ r) (hW : W.card = r)
    (position : Fin r → ι) :
    ‖∑ k ∈ range r, ∑ t : OrderedLabelTuple W r,
      M.preservationWordCut W position t k‖ ≤
      (1 + (r : ℝ) / Fintype.card α) *
        (Real.sqrt ((r - 1).factorial : ℝ) /
          Real.sqrt ((Fintype.card α : ℝ) ^ (r - 1))) *
        (∑ k ∈ range r, 1 / Real.sqrt ((r - 1).choose k : ℝ)) := by
…

Mentions: OAI.KadisonKastler.OrderedLabelTuple

theorem OAI.KadisonKastler.FreeDiagonalModel.norm_sum_centeredWord_le line 101

Source documentation

The complete centered sum is bounded by its two families of cuts.

theorem norm_sum_centeredWord_le {r : ℕ} (hr : 1 ≤ r) (hW : W.card = r)
    (position : Fin r → ι) (hposition : Function.Injective position) :
    ‖∑ t : OrderedLabelTuple W r, M.centeredWord W position t‖ ≤
      (1 + (r : ℝ) / Fintype.card α) *
        (Real.sqrt ((r - 1).factorial : ℝ) /
          Real.sqrt ((Fintype.card α : ℝ) ^ (r - 1))) *
        (∑ k ∈ range r, 1 / Real.sqrt ((r - 1).choose k : ℝ)) +
      (r + 1 : ℝ) * Real.sqrt (r.factorial : ℝ) /
        Real.sqrt ((Fintype.card α : ℝ) ^ r) := by
…

Mentions: OAI.KadisonKastler.OrderedLabelTuple

theorem OAI.KadisonKastler.FreeDiagonalModel.norm_sum_distinct_projectionWord_le line 117

Source documentation

The full distinct-label projection sum satisfies the constant-seven bound. The dimension threshold depends only on the word length.

theorem norm_sum_distinct_projectionWord_le {r : ℕ} (hr : 1 ≤ r)
    (hd : freeWordThreshold r ≤ Fintype.card α) (hW : W.card = r)
    (position : Fin r → ι) (hposition : Function.Injective position) :
    ‖∑ t : OrderedLabelTuple W r, M.projectionWord position t.val‖ ≤
      7 * Real.sqrt ((r - 1).factorial : ℝ) /
        Real.sqrt ((Fintype.card α : ℝ) ^ (r - 1)) := by
…

Mentions: OAI.KadisonKastler.freeWordThreshold, OAI.KadisonKastler.OrderedLabelTuple