BundleWords.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Continuous bundle words and their finite-tower Hilbert realization.

structure OAI.Kaplansky.BundleWordValue line 19
Source documentation
One monomial restricted to the bottom level, as an actual continuous bundle map into its single output level.
```
structure BundleWordValue (a : ℕ → LineStage K) where
…
```
Mentions: OAI.Kaplansky.LineStage
def OAI.Kaplansky.BundleWordValue.identity line 28
def OAI.Kaplansky.BundleWordValue.raise line 30
def OAI.Kaplansky.BundleWordValue.lower line 35
theorem OAI.Kaplansky.BundleWordValue.raise_level line 46
theorem OAI.Kaplansky.BundleWordValue.lower_level line 47
def OAI.Kaplansky.bundleWordValue line 52
theorem OAI.Kaplansky.bundleWordValue_level_le line 58
def OAI.Kaplansky.towerOperator line 73
theorem OAI.Kaplansky.towerOperator_norm line 79
theorem OAI.Kaplansky.bundleWordValue_raise_single line 86
theorem OAI.Kaplansky.bundleWordValue_lower_single line 93
theorem OAI.Kaplansky.bundleWordValue_shift_eval line 116
Source documentation
The continuous intrinsic monomial is exactly the Hilbert-shift word restricted to level zero, including adjoints at zero and constant words.
```
theorem bundleWordValue_shift_eval (w : List (Bool × Fin 24))
    (y : ProjectiveProduct K) (v : (a 0).Fiber y) :
    applyWord (shiftLetter (fun i j => towerOperator X i y j)
      (fun i j => towerOperator_norm X i y j)) w (lp.single (E := fun j => EuclideanSpace ℂ (a j).Slot) 2 0 v) =
…
```
Mentions: OAI.Kaplansky.applyWord, OAI.Kaplansky.shiftLetter, OAI.Kaplansky.towerOperator, OAI.Kaplansky.towerOperator_norm

def OAI.Kaplansky.finiteTowerHilbert line 142

Source documentation

The finite retained tower embeds into the actual Hilbert direct sum.

def finiteTowerHilbert (a : ℕ → LineStage K) (R : ℕ) (y : ProjectiveProduct K) :
    (LineStage.sum (fun j : Fin (R+1) => a j.val)).Fiber y →ₗ[ℂ]
      lp (fun j => (a j).Fiber y) 2 where
…

Mentions: OAI.Kaplansky.LineStage, OAI.Kaplansky.LineStage.sum

theorem OAI.Kaplansky.finiteTowerHilbert_inj line 157
theorem OAI.Kaplansky.finiteTowerHilbert_injective line 174
Source documentation
No information is lost by embedding the finite bundle in the Hilbert tower.
```
theorem finiteTowerHilbert_injective (a : ℕ → LineStage K) (R : ℕ)
    (y : ProjectiveProduct K) : Function.Injective (finiteTowerHilbert a R y) := by
…
```
Mentions: OAI.Kaplansky.LineStage, OAI.Kaplansky.finiteTowerHilbert

theorem OAI.Kaplansky.finiteTowerHilbert_apply line 193

Source documentation

The coordinate at every retained level is the original bundle vector.

theorem finiteTowerHilbert_apply (a : ℕ → LineStage K) (R : ℕ)
    (y : ProjectiveProduct K) (v : (LineStage.sum (fun k : Fin (R+1) => a k.val)).Fiber y)
    (j : Fin (R+1)) :
    finiteTowerHilbert a R y v j.val = LineStage.sumProj (fun k : Fin (R+1) => a k.val) j y v := by
…

Mentions: OAI.Kaplansky.LineStage, OAI.Kaplansky.LineStage.sum, OAI.Kaplansky.finiteTowerHilbert, OAI.Kaplansky.LineStage.sumProj

theorem OAI.Kaplansky.finiteTowerHilbert_inner line 209
Source documentation
This inclusion preserves the actual Hermitian metrics, which is needed when the operator lower bound is restricted to the finite bundle.
```
theorem finiteTowerHilbert_inner (a : ℕ → LineStage K) (R : ℕ)
    (y : ProjectiveProduct K)
    (v w : (LineStage.sum (fun k : Fin (R+1) => a k.val)).Fiber y) :
    inner ℂ (finiteTowerHilbert a R y v) (finiteTowerHilbert a R y w) = inner ℂ v w := by
…
```
Mentions: OAI.Kaplansky.LineStage, OAI.Kaplansky.LineStage.sum, OAI.Kaplansky.finiteTowerHilbert
def OAI.Kaplansky.finiteTowerHilbertIsometry line 223