RationalCoreExtension.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Bounded complex-linear extension from the rational core

def OAI.KadisonKastler.complexifyRational line 24
Source documentation
A continuous rational-linear map commuting with multiplication by i is complex-linear. Real-linearity follows from continuity.
```
def complexifyRational (f : H →L[ℚ] F)
    (hI : ∀ x, f (Complex.I • x) = Complex.I • f x) : H →L[ℂ] F where
…
```
theorem OAI.KadisonKastler.complexifyRational_apply line 39
def OAI.KadisonKastler.RationalComplexCore.extendRational line 48
Source documentation
Extend a bounded rational-linear map on the dense core.
```
def extendRational (f : C.space →ₗ[ℚ] F) : H →L[ℚ] F :=
…
```

theorem OAI.KadisonKastler.RationalComplexCore.extendRational_coe line 52

Source documentation

The extension agrees with every core value.

theorem extendRational_coe (f : C.space →ₗ[ℚ] F) {B : ℝ}
    (hb : ∀ x, ‖f x‖ ≤ B * ‖(x : H)‖) (x : C.space) :
    C.extendRational f (x : H) = f x :=
…

theorem OAI.KadisonKastler.RationalComplexCore.norm_extendRational_le line 58

Source documentation

The norm bound is unchanged by the dense extension.

theorem norm_extendRational_le (f : C.space →ₗ[ℚ] F) {B : ℝ}
    (hb : ∀ x, ‖f x‖ ≤ B * ‖(x : H)‖) (x : H) :
    ‖C.extendRational f x‖ ≤ B * ‖x‖ :=
…

theorem OAI.KadisonKastler.RationalComplexCore.extendRational_mul_I line 64

Source documentation

Commutation with i persists from the core to its norm completion.

theorem extendRational_mul_I (f : C.space →ₗ[ℚ] F) {B : ℝ}
    (hb : ∀ x, ‖f x‖ ≤ B * ‖(x : H)‖)
    (hI : ∀ x, f (C.mulI x) = Complex.I • f x) (x : H) :
    C.extendRational f (Complex.I • x) = Complex.I • C.extendRational f x := by
…

def OAI.KadisonKastler.RationalComplexCore.extendComplex line 81

Source documentation

The final complex-linear extension, with no change of bound.

def extendComplex (f : C.space →ₗ[ℚ] F) {B : ℝ}
    (hb : ∀ x, ‖f x‖ ≤ B * ‖(x : H)‖)
    (hI : ∀ x, f (C.mulI x) = Complex.I • f x) : H →L[ℂ] F :=
…

theorem OAI.KadisonKastler.RationalComplexCore.extendComplex_coe line 87
theorem OAI.KadisonKastler.RationalComplexCore.norm_extendComplex_le line 92