FreeCuts.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Creation, preservation, and annihilation cuts

The algebraic relations record the first-copy restrictions of the Fock operators. They imply an exact cut decomposition for words in distinct copy positions. The norm estimate is then a finite recurrence.

def OAI.KadisonKastler.annihilationProduct line 21
def OAI.KadisonKastler.centeredLetterProduct line 23
def OAI.KadisonKastler.freeCutSum line 26
theorem OAI.KadisonKastler.mul_freeCutSum_eq_mul_annihilationProduct line 33
Source documentation
An annihilation or preservation operator from a different copy kills the creation and preservation terms of the first tail letter.
```
theorem mul_freeCutSum_eq_mul_annihilationProduct (C D A : ι → B) (x : B) (l : List ι)
    (hC : ∀ i ∈ l, x * C i = 0) (hD : ∀ i ∈ l, x * D i = 0) :
    x * freeCutSum C D A l = x * annihilationProduct A l := by
…
```
Mentions: OAI.KadisonKastler.freeCutSum, OAI.KadisonKastler.annihilationProduct

theorem OAI.KadisonKastler.centeredLetterProduct_eq_freeCutSum line 45

Source documentation

The centered word is exactly the sum of its creation/annihilation cuts and its cuts with one preservation.

theorem centeredLetterProduct_eq_freeCutSum (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)
    (l : List ι) (hl : l.Nodup) :
    centeredLetterProduct C D A l = freeCutSum C D A l := by
…

Mentions: OAI.KadisonKastler.centeredLetterProduct, OAI.KadisonKastler.freeCutSum

theorem OAI.KadisonKastler.norm_annihilationProduct_le line 74

theorem OAI.KadisonKastler.norm_freeCutSum_le line 89

Source documentation

The cut recurrence has n preservation terms and n+1 terms without preservation. Its bound includes the empty word.

theorem norm_freeCutSum_le (C D A : ι → B) {t : ℝ} (ht : 0 ≤ t)
    (hone : ‖(1 : B)‖ ≤ 1) (hC : ∀ i, ‖C i‖ ≤ t)
    (hD : ∀ i, ‖D i‖ ≤ 1) (hA : ∀ i, ‖A i‖ ≤ t) (l : List ι) :
    ‖freeCutSum C D A l‖ ≤
      (l.length : ℝ) * t ^ (l.length - 1) + (l.length + 1 : ℝ) * t ^ l.length := by
…

Mentions: OAI.KadisonKastler.freeCutSum

theorem OAI.KadisonKastler.norm_centeredLetterProduct_le line 126

Source documentation

The single-centered-word bound from the actual algebraic cut decomposition, conditional only on its four explicit zero-product relations and the individual letter bounds.

theorem norm_centeredLetterProduct_le (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)
    {t : ℝ} (ht : 0 ≤ t) (hone : ‖(1 : B)‖ ≤ 1)
    (hC : ∀ i, ‖C i‖ ≤ t) (hD : ∀ i, ‖D i‖ ≤ 1) (hA : ∀ i, ‖A i‖ ≤ t)
    (l : List ι) (hl : l.Nodup) :
    ‖centeredLetterProduct C D A l‖ ≤
      (l.length : ℝ) * t ^ (l.length - 1) + (l.length + 1 : ℝ) * t ^ l.length := by
…

Mentions: OAI.KadisonKastler.centeredLetterProduct

theorem OAI.KadisonKastler.sqrt_nat_pow line 139

theorem OAI.KadisonKastler.norm_centeredLetterProduct_le_inv_sqrt line 147

Source documentation

The preceding actual cut decomposition gives the single-word estimate used in the scalar-restoration calculation.

theorem norm_centeredLetterProduct_le_inv_sqrt (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)⁻¹)
    (l : List ι) (hl : l.Nodup) :
    ‖centeredLetterProduct C D A l‖ ≤
      (2 * l.length + 1 : ℝ) / Real.sqrt (d ^ (l.length - 1)) := by
…

Mentions: OAI.KadisonKastler.centeredLetterProduct