SubwordExpansion.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Ordered subwords and restoration of scalar projection parts

The expansion keeps the original order of every retained subword. The lists of subwords count choices of positions, including their multiplicity. The resulting binomial estimate is the scalar-restoration step in §3.

theorem OAI.KadisonKastler.sum_map_flatMap line 23
theorem OAI.KadisonKastler.sum_list_range line 31
def OAI.KadisonKastler.orderedWord line 41
def OAI.KadisonKastler.retainedSubword line 43
theorem OAI.KadisonKastler.orderedWord_add_scalar line 47
Source documentation
Expand each c i + s • 1 by retaining a sublist of positions.
```
theorem orderedWord_add_scalar (c : ι → B) (s : ℝ) (l : List ι) :
    orderedWord (fun i => c i + s • (1 : B)) l =
      (l.sublists'.map (retainedSubword c s l.length)).sum := by
…
```
Mentions: OAI.KadisonKastler.orderedWord, OAI.KadisonKastler.retainedSubword

theorem OAI.KadisonKastler.orderedWord_add_scalar_by_length line 83

Source documentation

Group the exact ordered expansion by the number of retained positions.

theorem orderedWord_add_scalar_by_length (c : ι → B) (s : ℝ) (l : List ι) :
    orderedWord (fun i => c i + s • (1 : B)) l =
      ∑ k ∈ range (l.length + 1),
        ((l.sublistsLen k).map (retainedSubword c s l.length)).sum := by
…

Mentions: OAI.KadisonKastler.orderedWord, OAI.KadisonKastler.retainedSubword

theorem OAI.KadisonKastler.orderedWord_add_scalar_sub line 92

Source documentation

The full retained word is removed exactly; all remaining terms are proper subwords.

theorem orderedWord_add_scalar_sub (c : ι → B) (s : ℝ) (l : List ι) :
    orderedWord (fun i => c i + s • (1 : B)) l - orderedWord c l =
      ∑ k ∈ range l.length,
        ((l.sublistsLen k).map (retainedSubword c s l.length)).sum := by
…

Mentions: OAI.KadisonKastler.orderedWord, OAI.KadisonKastler.retainedSubword

theorem OAI.KadisonKastler.norm_list_sum_map_le line 108

theorem OAI.KadisonKastler.norm_retainedSubwords_le line 121

Source documentation

A length class contains exactly choose r k positional subwords.

theorem norm_retainedSubwords_le (c : ι → B) {d : ℝ} (hd : 0 < d)
    (l : List ι) {k : ℕ}
    (hc : ∀ w, List.Sublist w l → w.length = k →
      ‖orderedWord c w‖ ≤ (2 * k + 1 : ℝ) / Real.sqrt (d ^ (k - 1))) :
    ‖((l.sublistsLen k).map (retainedSubword c (1 / d) l.length)).sum‖ ≤
      (l.length.choose k : ℝ) *
        ((2 * k + 1 : ℝ) / (d ^ (l.length - k) * Real.sqrt (d ^ (k - 1)))) := by
…

Mentions: OAI.KadisonKastler.orderedWord, OAI.KadisonKastler.retainedSubword

theorem OAI.KadisonKastler.norm_orderedWord_scalar_restoration_le line 147

Source documentation

Restoring the scalar parts of a single projection word. The only analytic input is the proved bound for each nonempty centered subword.

theorem norm_orderedWord_scalar_restoration_le (c : ι → B) {d : ℝ} (hd : 0 < d)
    (hone : ‖(1 : B)‖ ≤ 1) (l : List ι) (hl : 0 < l.length)
    (hc : ∀ w, List.Sublist w l → 0 < w.length →
      ‖orderedWord c w‖ ≤
        (2 * w.length + 1 : ℝ) / Real.sqrt (d ^ (w.length - 1))) :
    ‖orderedWord (fun i => c i + (1 / d) • (1 : B)) l - orderedWord c l‖ ≤
      1 / d ^ l.length + ∑ k ∈ Ico 1 l.length, (l.length.choose k : ℝ) *
        ((2 * k + 1 : ℝ) / (d ^ (l.length - k) * Real.sqrt (d ^ (k - 1)))) := by
…

Mentions: OAI.KadisonKastler.orderedWord

theorem OAI.KadisonKastler.norm_orderedWord_sub_centered_le line 185

Source documentation

The restoration estimate for letters already given as projections (or any letters with the same scalar decomposition).

theorem norm_orderedWord_sub_centered_le (e c : ι → B) {d : ℝ} (hd : 0 < d)
    (hone : ‖(1 : B)‖ ≤ 1) (l : List ι) (hl : 0 < l.length)
    (he : ∀ i ∈ l, e i = c i + (1 / d) • (1 : B))
    (hc : ∀ w, List.Sublist w l → 0 < w.length →
      ‖orderedWord c w‖ ≤
        (2 * w.length + 1 : ℝ) / Real.sqrt (d ^ (w.length - 1))) :
    ‖orderedWord e l - orderedWord c l‖ ≤
      1 / d ^ l.length + ∑ k ∈ Ico 1 l.length, (l.length.choose k : ℝ) *
        ((2 * k + 1 : ℝ) / (d ^ (l.length - k) * Real.sqrt (d ^ (k - 1)))) := by
…

Mentions: OAI.KadisonKastler.orderedWord

theorem OAI.KadisonKastler.norm_sum_orderedWord_scalar_restoration_le line 202

Source documentation

At most r! ordered tuples give the manuscript's scalar restoration bound.

theorem norm_sum_orderedWord_scalar_restoration_le {τ : Type*}
    (e c : ι → B) {d : ℝ} (hd : 0 < d) (hone : ‖(1 : B)‖ ≤ 1)
    (T : Finset τ) (L : τ → List ι) {r : ℕ} (hr : 0 < r)
    (hcard : T.card ≤ r.factorial)
    (hlen : ∀ t ∈ T, (L t).length = r)
    (he : ∀ t ∈ T, ∀ i ∈ L t, e i = c i + (1 / d) • (1 : B))
    (hc : ∀ t ∈ T, ∀ w, List.Sublist w (L t) → 0 < w.length →
      ‖orderedWord c w‖ ≤
        (2 * w.length + 1 : ℝ) / Real.sqrt (d ^ (w.length - 1))) :
    ‖(∑ t ∈ T, orderedWord e (L t)) - ∑ t ∈ T, orderedWord c (L t)‖ ≤
      scalarRestorationBound r d := by
…

Mentions: OAI.KadisonKastler.orderedWord, OAI.KadisonKastler.scalarRestorationBound

theorem OAI.KadisonKastler.norm_sum_projectionWords_sub_centeredCuts_le line 231

Source documentation

In the creation/preservation/annihilation model, the centered-subword input above follows directly from the exact cut decomposition.

theorem norm_sum_projectionWords_sub_centeredCuts_le {τ : Type*}
    (e C D A : ι → B)
    (hAC : ∀ i j, i ≠ j → A i * C j = 0)
    (hAD : ∀ i j, i ≠ j → A i * D j = 0)
    (hDC : ∀ i j, i ≠ j → D i * C j = 0)
    (hDD : ∀ i j, i ≠ j → D i * D j = 0)
    {d : ℝ} (hd : 1 ≤ d) (hone : ‖(1 : B)‖ ≤ 1)
    (hC : ∀ i, ‖C i‖ ≤ (Real.sqrt d)⁻¹)
    (hD : ∀ i, ‖D i‖ ≤ 1) (hA : ∀ i, ‖A i‖ ≤ (Real.sqrt d)⁻¹)
    (T : Finset τ) (L : τ → List ι) {r : ℕ} (hr : 0 < r)
    (hcard : T.card ≤ r.factorial) (hlen : ∀ t ∈ T, (L t).length = r)
    (hnodup : ∀ t ∈ T, (L t).Nodup)
…