FreeWordConstants.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Numerical constants for the free projection-word estimates

These are the scalar closing estimates in §3. The norm bounds for the individual operator cuts enter as explicit hypotheses; no free-word operator estimate is assumed as a published theorem.

def OAI.KadisonKastler.freeWordH line 20
def OAI.KadisonKastler.freeWordJ line 23
def OAI.KadisonKastler.freeWordC line 26
theorem OAI.KadisonKastler.one_le_freeWordH line 29
theorem OAI.KadisonKastler.freeWordJ_nonneg line 35
theorem OAI.KadisonKastler.freeWordC_pos line 40
theorem OAI.KadisonKastler.sqrt_pow_succ_split line 46
theorem OAI.KadisonKastler.sqrt_pow_mono line 51

theorem OAI.KadisonKastler.single_centered_word_constant line 57

Source documentation

The bound for one centered word, after absorbing the cuts without preservation into the common denominator.

theorem single_centered_word_constant {d : ℝ} (hd : 1 ≤ d) (l : ℕ) {B : ℝ}
    (hB : B ≤ (l : ℝ) / Real.sqrt (d ^ (l - 1)) +
      (l + 1 : ℝ) / Real.sqrt (d ^ l)) :
    B ≤ (2 * l + 1 : ℝ) / Real.sqrt (d ^ (l - 1)) := by
…

theorem OAI.KadisonKastler.restored_scalar_denominator line 73
Source documentation
Removing at least one centered letter supplies the extra inverse square root needed by the scalar-restoration estimate.
```
theorem restored_scalar_denominator {d : ℝ} (hd : 1 ≤ d) {l r : ℕ}
    (hl : 1 ≤ l) (hlr : l < r) :
    Real.sqrt (d ^ r) ≤ d ^ (r - l) * Real.sqrt (d ^ (l - 1)) := by
…
```
theorem OAI.KadisonKastler.restored_scalar_term line 82
def OAI.KadisonKastler.scalarRestorationBound line 90
theorem OAI.KadisonKastler.scalarRestorationBound_le line 97
Source documentation
Summing all proper centered subwords gives precisely the manuscript's constant r! H_r, including the entirely scalar term.
```
theorem scalarRestorationBound_le {d : ℝ} (hd : 1 ≤ d) (r : ℕ) :
    scalarRestorationBound r d ≤ (r.factorial : ℝ) * freeWordH r / Real.sqrt (d ^ r) := by
…
```
Mentions: OAI.KadisonKastler.scalarRestorationBound, OAI.KadisonKastler.freeWordH

theorem OAI.KadisonKastler.freeWordJ_remainder_le line 125

Source documentation

The term containing J_r fits into one copy of the target scale.

theorem freeWordJ_remainder_le {d : ℝ} (hd : 1 ≤ d) {r : ℕ} (hr : 1 ≤ r)
    (hJ : freeWordJ r ^ 2 ≤ ((r - 1).factorial : ℝ) * d) :
    freeWordJ r / Real.sqrt (d ^ r) ≤
      Real.sqrt ((r - 1).factorial : ℝ) / Real.sqrt (d ^ (r - 1)) := by
…

Mentions: OAI.KadisonKastler.freeWordJ

theorem OAI.KadisonKastler.distinct_freeWord_constant line 146

Source documentation

The preservation cuts contribute at most six target units; the nonpreservation cuts and scalar restoration contribute at most one.

theorem distinct_freeWord_constant {d : ℝ} (hd : 1 ≤ d) {r : ℕ} (hr : 1 ≤ r)
    (hrd : 5 * (r : ℝ) ≤ d)
    (hJ : freeWordJ r ^ 2 ≤ ((r - 1).factorial : ℝ) * d)
    {P N R B : ℝ}
    (hP : P ≤ (1 + r / d) *
      (Real.sqrt ((r - 1).factorial : ℝ) / Real.sqrt (d ^ (r - 1))) *
      (∑ p ∈ range r, 1 / Real.sqrt ((r - 1).choose p : ℝ)))
    (hN : N ≤ (r + 1 : ℝ) * Real.sqrt (r.factorial : ℝ) / Real.sqrt (d ^ r))
    (hR : R ≤ (r.factorial : ℝ) * freeWordH r / Real.sqrt (d ^ r))
    (hB : B ≤ P + N + R) :
    B ≤ 7 * Real.sqrt ((r - 1).factorial : ℝ) / Real.sqrt (d ^ (r - 1)) := by
…

Mentions: OAI.KadisonKastler.freeWordJ, OAI.KadisonKastler.freeWordH

theorem OAI.KadisonKastler.repeated_freeWord_constant line 184

Source documentation

Repeated-label words use the single-word estimate for each of at most r! summands; their constant is independent of the matrix size.

theorem repeated_freeWord_constant {d : ℝ} (hd : 1 ≤ d) (r : ℕ) {P R B : ℝ}
    (hP : P ≤ (r.factorial : ℝ) * (2 * r + 1 : ℝ) / Real.sqrt (d ^ (r - 1)))
    (hR : R ≤ (r.factorial : ℝ) * freeWordH r / Real.sqrt (d ^ r))
    (hB : B ≤ P + R) : B ≤ freeWordC r / Real.sqrt (d ^ (r - 1)) := by
…

Mentions: OAI.KadisonKastler.freeWordH, OAI.KadisonKastler.freeWordC

def OAI.KadisonKastler.freeWordThreshold line 202
Source documentation
A convenient integral threshold, larger than the one displayed in the manuscript, that keeps the distinct-label constant equal to seven.
```
def freeWordThreshold (r : ℕ) : ℕ := ⌈5 * (r : ℝ) + freeWordJ r ^ 2 + 1⌉₊
```
Mentions: OAI.KadisonKastler.freeWordJ
theorem OAI.KadisonKastler.freeWordThreshold_conditions line 204

theorem OAI.KadisonKastler.distinct_freeWord_constant_of_threshold line 221

Source documentation

The complete scalar closing step, starting from the three cut estimates and the explicit integer threshold.

theorem distinct_freeWord_constant_of_threshold {r d : ℕ} (hr : 1 ≤ r)
    (hd : freeWordThreshold r ≤ d) {P N R B : ℝ}
    (hP : P ≤ (1 + (r : ℝ) / d) *
      (Real.sqrt ((r - 1).factorial : ℝ) / Real.sqrt ((d : ℝ) ^ (r - 1))) *
      (∑ p ∈ range r, 1 / Real.sqrt ((r - 1).choose p : ℝ)))
    (hN : N ≤ (r + 1 : ℝ) * Real.sqrt (r.factorial : ℝ) / Real.sqrt ((d : ℝ) ^ r))
    (hR : R ≤ scalarRestorationBound r d) (hB : B ≤ P + N + R) :
    B ≤ 7 * Real.sqrt ((r - 1).factorial : ℝ) / Real.sqrt ((d : ℝ) ^ (r - 1)) := by
…

Mentions: OAI.KadisonKastler.freeWordThreshold, OAI.KadisonKastler.scalarRestorationBound

theorem OAI.KadisonKastler.exists_uniform_freeWordThreshold line 233