ModelScalarRestoration.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Scalar restoration for actual free projection words

Copy positions are injective, but their labels may repeat. The centered subword estimate therefore uses positions as its indices. This gives scalar restoration for each word and for any family of at most r! label functions, including the full family of orderings of a distinct label set.

def OAI.KadisonKastler.FreeDiagonalModel.projectionWord line 30
def OAI.KadisonKastler.FreeDiagonalModel.centeredLabelWord line 33

theorem OAI.KadisonKastler.FreeDiagonalModel.norm_centered_position_word_le line 38

Source documentation

The labels need not be distinct: the four zero products only use the injectivity of the copy positions. This also applies to each subword.

theorem norm_centered_position_word_le {r : ℕ} (position : Fin r → ι)
    (hposition : Function.Injective position) (label : Fin r → α)
    (l : List (Fin r)) (hl : l.Nodup) :
    ‖orderedWord (fun i => M.centered (position i) (label i)) l‖ ≤
      (2 * l.length + 1 : ℝ) /
        Real.sqrt ((Fintype.card α : ℝ) ^ (l.length - 1)) := by
…

Mentions: OAI.KadisonKastler.orderedWord

theorem OAI.KadisonKastler.FreeDiagonalModel.norm_centeredLabelWord_le line 73

theorem OAI.KadisonKastler.FreeDiagonalModel.norm_projectionWord_sub_centeredLabelWord_le line 83

Source documentation

Restoring the scalar part of each letter in a single actual word.

theorem norm_projectionWord_sub_centeredLabelWord_le {r : ℕ} (hr : 0 < r)
    (position : Fin r → ι) (hposition : Function.Injective position)
    (label : Fin r → α) :
    ‖M.projectionWord position label - M.centeredLabelWord position label‖ ≤
      1 / (Fintype.card α : ℝ) ^ r +
        ∑ k ∈ Ico 1 r, (r.choose k : ℝ) *
          ((2 * k + 1 : ℝ) / ((Fintype.card α : ℝ) ^ (r - k) *
            Real.sqrt ((Fintype.card α : ℝ) ^ (k - 1)))) := by
…

theorem OAI.KadisonKastler.FreeDiagonalModel.norm_sum_projectionWord_sub_centeredLabelWord_le line 116

Source documentation

At most r! label functions suffice; no distinctness of their labels is used in the restoration estimate.

theorem norm_sum_projectionWord_sub_centeredLabelWord_le {τ : Type*} {r : ℕ}
    (hr : 0 < r) (position : Fin r → ι) (hposition : Function.Injective position)
    (T : Finset τ) (label : τ → Fin r → α) (hcard : T.card ≤ r.factorial) :
    ‖(∑ t ∈ T, M.projectionWord position (label t)) -
        ∑ t ∈ T, M.centeredLabelWord position (label t)‖ ≤
      scalarRestorationBound r (Fintype.card α) := by
…

Mentions: OAI.KadisonKastler.scalarRestorationBound

theorem OAI.KadisonKastler.FreeDiagonalModel.norm_sum_distinct_projectionWord_sub_centeredWord_le line 139

Source documentation

Apply scalar restoration to all orderings of an r-element set.

theorem norm_sum_distinct_projectionWord_sub_centeredWord_le (W : Finset α)
    {r : ℕ} (hr : 0 < r) (hW : W.card = r) (position : Fin r → ι)
    (hposition : Function.Injective position) :
    ‖(∑ t : OrderedLabelTuple W r, M.projectionWord position t.val) -
        ∑ t : OrderedLabelTuple W r, M.centeredWord W position t‖ ≤
      scalarRestorationBound r (Fintype.card α) := by
…

Mentions: OAI.KadisonKastler.OrderedLabelTuple, OAI.KadisonKastler.scalarRestorationBound

theorem OAI.KadisonKastler.FreeDiagonalModel.norm_sum_centeredLabelWord_le line 153

Source documentation

The crude centered-word estimate for a finite family also permits repeated labels. Its size, rather than the number of distinct labels, controls the sum.

theorem norm_sum_centeredLabelWord_le {τ : Type*} {r : ℕ}
    (position : Fin r → ι) (hposition : Function.Injective position)
    (T : Finset τ) (label : τ → Fin r → α) (hcard : T.card ≤ r.factorial) :
    ‖∑ t ∈ T, M.centeredLabelWord position (label t)‖ ≤
      (r.factorial : ℝ) * (2 * r + 1 : ℝ) /
        Real.sqrt ((Fintype.card α : ℝ) ^ (r - 1)) := by
…

theorem OAI.KadisonKastler.FreeDiagonalModel.norm_sum_projectionWord_le_repeated_constant line 173

Source documentation

Combining the actual centered estimate and restoration gives the repeated-label constant for any family of at most r! words.

theorem norm_sum_projectionWord_le_repeated_constant {τ : Type*} {r : ℕ}
    (hr : 0 < r) (position : Fin r → ι) (hposition : Function.Injective position)
    (T : Finset τ) (label : τ → Fin r → α) (hcard : T.card ≤ r.factorial) :
    ‖∑ t ∈ T, M.projectionWord position (label t)‖ ≤
      freeWordC r / Real.sqrt ((Fintype.card α : ℝ) ^ (r - 1)) := by
…

Mentions: OAI.KadisonKastler.freeWordC