DenseLinearOperator.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Operators from dense additive column data

Bounded additive data on a dense subgroup extends by uniform continuity. Compatibility with multiplication by i makes the extension complex linear. Only a countable dense subgroup is needed for the later AE construction.

theorem OAI.KadisonSimilarity.denseAdditive_uniformContinuous line 22

def OAI.KadisonSimilarity.denseAdditiveExtension line 28

Source documentation

The additive extension of bounded data from a dense subgroup.

def denseAdditiveExtension (S : AddSubgroup E) (hdense : Dense (S : Set E))
    (f : S →+ F) (C : ℝ≥0) (hnorm : ∀ x : S, ‖f x‖ ≤ C * ‖x‖) : E →+ F where
…

theorem OAI.KadisonSimilarity.denseAdditiveExtension_continuous line 48
theorem OAI.KadisonSimilarity.denseAdditiveExtension_apply line 57

def OAI.KadisonSimilarity.continuousAdditiveToComplexLinear line 67

Source documentation

A continuous additive map that commutes with i is complex linear.

def continuousAdditiveToComplexLinear (f : E →+ F) (hf : Continuous f)
    (hI : ∀ x, f (Complex.I • x) = Complex.I • f x) : E →L[ℂ] F where
…

theorem OAI.KadisonSimilarity.exists_operator_of_dense_additive line 84

Source documentation

The bounded dense-subgroup data gives an operator of the same norm bound.

theorem exists_operator_of_dense_additive
    (S : AddSubgroup E) (hdense : Dense (S : Set E))
    (hIS : ∀ x ∈ S, Complex.I • x ∈ S) (f : S →+ F) (C : ℝ≥0)
    (hnorm : ∀ x : S, ‖f x‖ ≤ C * ‖x‖)
    (hI : ∀ x : S, f ⟨Complex.I • x.val, hIS x.val x.property⟩ = Complex.I • f x) :
    ∃ T : E →L[ℂ] F, ‖T‖ ≤ C ∧ ∀ x : S, T x = f x := by
…

theorem OAI.KadisonSimilarity.countable_addSubgroupClosure line 116

theorem OAI.KadisonSimilarity.exists_countable_dense_complex_addSubgroup line 126

Source documentation

A separable complex normed space has a countable dense additive subgroup that is stable under multiplication by i.

theorem exists_countable_dense_complex_addSubgroup
    (E : Type*) [NormedAddCommGroup E] [NormedSpace ℂ E]
    [TopologicalSpace.SeparableSpace E] :
    ∃ S : AddSubgroup E, (S : Set E).Countable ∧ Dense (S : Set E) ∧
      ∀ x ∈ S, Complex.I • x ∈ S := by
…