1. Physlib
  2. QuantumMechanics
  3. Operators
  4. Unbounded
Imports
/- Copyright (c) 2026 Gregory J. Loges. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Adam Bornemann, Gregory J. Loges -/ module public import Physlib.Mathematics.InnerProductSpace.Submodule public import Physlib.Mathematics.LinearPMap public import Physlib.Meta.TODO.Basic

Unbounded operators

i. Overview

The appropriate mathematical objects for discussing operators in non-relativistic quantum mechanics are partially-defined linear map (LinearPMap) between complex Hilbert spaces, H →ₗ.[ℂ] H'. An import class of operators in NRQM are those which are both densely defined and closable, which we refer to as unbounded. When H = H' operators may also be symmetric, self-adjoint or essentially self-adjoint (closure is self-adjoint).

In this module we collect results on how the properties HasDenseDomain, IsUnbounded, IsSymmetric, IsSelfAdjoint and IsEssentiallySelfAdjoint interact with the basic algebraic operations, closure, adjoints, unitary conjugation and each other.

Notes

    Naming convention : Definitions of LinearPMaps for quantum mechanical unbounded operators should have a name of the form […]Operator and notation should use calligraphic capital letters, e.g. mulOperator f (𝓜 f) for the multiplication operator associated with the function f.

    Implementation : Although operators encountered in quantum mechanics are almost always unbounded, we opt to implement unbounded operators via the property IsUnbounded on LinearPMap rather than as a structure UnboundedOperator extending LinearPMap. The basic reason for this is that addition/subtraction and composition of unbounded operators in general does not result in another unbounded operator. This means, for example, that any attempt to define addition of UnboundedOperators would inevitably require introducing junk values that spoil associativity.

ii. Key results

Definitions

    HasDenseDomain : An operator U : H →ₗ.[ℂ] H' has dense domain if U.domain is dense in H.

    IsUnbounded : An operator is unbounded if it is both densely defined and closable.

    IsSymmetric : An operator T : H →ₗ.[ℂ] H is symmetric if ⟪T x, y⟫_ℂ = ⟪x, T y⟫_ℂ holds for all x y : T.domain.

    IsEssentiallySelfAdjoint : An operator T : H →ₗ.[ℂ] H is essentially self-adjoint if its closure is self-adjoint.

Results

    adjoint_add_le_add_adjoint : The inequality U₁† + U₂† ≤ (U₁ + U₂)† when U₁ + U₂ has dense domain.

    unitaryConj : The conjugation u A u⁻¹ : H' →ₗ.[ℂ] H' of A by a unitary u, with domain u (A.domain).

    IsFormalAdjoint.unitaryConj : Unitary conjugation preserves formal-adjoint pairs.

    HasDenseDomain.unitaryConj_dense_domain : If A has dense domain, then so does u A u⁻¹.

    unitaryConj_sub_smul_surjective : If A - z is surjective for a scalar z : ℂ, then so is u A u⁻¹ - z.

    adjoint_compRestricted_le_compRestricted_adjoint : The inequality U† ∘ᵣ V† ≤ (V ∘ᵣ U)† when V and V ∘ᵣ U have dense domain.

    IsUnbounded.adjoint : The adjoint of an unbounded operator is also unbounded.

    IsUnbounded.adjoint_closure_eq_adjoint : An unbounded operator and its closure have the same adjoint.

    IsUnbounded.adjoint_adjoint_eq_closure : An unbounded operator U satisfies U†† = U.closure.

    IsEssentiallySelfAdjoint.unique_self_adjoint_extension : The closure of an essentially self-adjoint unbounded operator is its unique self-adjoint extension.

iii. Table of contents

    A. Definitions

    B. Basic properties

      B.1. Dense domain

      B.2. Closability

      B.3. Adjoints

      B.4. Continuity / boundedness

      B.5. Unitary conjugation

    C. Classes of operators

      C.1. Unbounded operators

      C.2. Symmetric operators

      C.3. Self-adjoint operators

      C.4. Essentially self-adjoint operators

iv. References

    [Reed and Simon, Methods of Modern Mathematical Physics, Vol. I: Functional Analysis][Reed1972]

    [Konrad Schmüdgen, Unbounded Self-Adjoint Operators on Hilbert Space][Schmudgen2012]

TODO "Prove that `IsStarNormal (T : H →ₗ.[ℂ] H)` is equivalent to `T.domain = T†.domain` and `‖T x‖ = ‖T† x‖` for all `x ∈ T.domain`."TODO "Prove basic properties of `IsStarNormal (T : H →ₗ.[ℂ] H)`, paralleling those for `IsSelfAdjoint (T : H →ₗ.[ℂ] H)`."@[expose] public section

A. Definitions

See LinearPMap.instStar and LinearPMap.isSelfAdjoint_def for the definition of IsSelfAdjoint for LinearPMaps.

A LinearPMap U has dense domain iff U.domain is dense in H.

def HasDenseDomain (U : H →ₗ.[ℂ] H') : Prop := Dense (U.domain : Set H)
lemma hasDenseDomain_def : U.HasDenseDomain ↔ Dense (U.domain : Set H) := Iff.rfl

A LinearPMap is an unbounded operator iff it has dense domain and is closable.

def IsUnbounded (U : H →ₗ.[ℂ] H') : Prop := U.HasDenseDomain ∧ U.IsClosable
lemma isUnbounded_def : U.IsUnbounded ↔ U.HasDenseDomain ∧ U.IsClosable := Iff.rfl

A LinearPMap T is symmetric iff ⟪T x, y⟫_ℂ = ⟪x, T y⟫_ℂ for all x y : T.domain.

def IsSymmetric (T : H →ₗ.[ℂ] H) : Prop := T.IsFormalAdjoint T
lemma isSymmetric_def : T.IsSymmetric ↔ T.IsFormalAdjoint T := Iff.rfl

A LinearPMap is essentially self-adjoint iff its closure is self-adjoint.

def IsEssentiallySelfAdjoint [CompleteSpace H] (T : H →ₗ.[ℂ] H) : Prop := IsSelfAdjoint T.closure
lemma isEssentiallySelfAdjoint_def [CompleteSpace H] : T.IsEssentiallySelfAdjoint ↔ IsSelfAdjoint T.closure := Iff.rfllemma isStarNormal_def [CompleteSpace H] : IsStarNormal T ↔ T† * T = T * T† := isStarNormal_iff _

B. Basic properties

B.1. Dense domain

lemma HasDenseDomain.isUnbounded_iff_isClosable (h : U.HasDenseDomain) : U.IsUnbounded ↔ U.IsClosable := and_iff_right hlemma HasDenseDomain.closure (h : U.HasDenseDomain) : U.closure.HasDenseDomain := h.mono U.le_closure.1lemma closure_domain_le_domain_closure (U : H →ₗ.[ℂ] H') : U.closure.domain ≤ U.domain.closure := H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'⊢ U.closure.domain ≤ ↑U.domain.closure H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h_cl:U.IsClosable⊢ U.closure.domain ≤ ↑U.domain.closureH:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h_cl:¬U.IsClosable⊢ U.closure.domain ≤ ↑U.domain.closure H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h_cl:U.IsClosable⊢ U.closure.domain ≤ ↑U.domain.closure H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h_cl:U.IsClosableψ:Hhψ:ψ ∈ U.closure.domain⊢ ψ ∈ ↑U.domain.closure H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h_cl:U.IsClosableψ:Hhψ:ψ ∈ U.closure.domainφ:H'hψφ:(ψ, φ) ∈ U.graph.topologicalClosure⊢ ψ ∈ ↑U.domain.closure H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h_cl:U.IsClosableψ:Hhψ:ψ ∈ U.closure.domainφ:H'hψφ:(ψ, φ) ∈ U.graph.topologicalClosureb:ℕ → H × H'hb:∀ (n : ℕ), b n ∈ ↑U.graph.toAddSubmonoidhb':Filter.Tendsto b Filter.atTop (nhds (ψ, φ))⊢ ψ ∈ ↑U.domain.closure H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h_cl:U.IsClosableψ:Hhψ:ψ ∈ U.closure.domainφ:H'hψφ:(ψ, φ) ∈ U.graph.topologicalClosureb:ℕ → H × H'hb:∀ (n : ℕ), b n ∈ ↑U.graph.toAddSubmonoidhb':Filter.Tendsto b Filter.atTop (nhds (ψ, φ))n:ℕ⊢ (fun n => (b n).1) n ∈ ↑U.domain.toAddSubmonoid H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h_cl:U.IsClosableψ:Hhψ:ψ ∈ U.closure.domainφ:H'hψφ:(ψ, φ) ∈ U.graph.topologicalClosureb:ℕ → H × H'hb':Filter.Tendsto b Filter.atTop (nhds (ψ, φ))n:ℕhb:∀ (n : ℕ), ∃ (x : (b n).1 ∈ U.domain), ↑U ⟨(b n).1, ⋯⟩ = (b n).2⊢ (fun n => (b n).1) n ∈ ↑U.domain.toAddSubmonoid All goals completed! 🐙 H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h_cl:¬U.IsClosable⊢ U.closure.domain ≤ ↑U.domain.closure All goals completed! 🐙lemma hasDenseDomain_iff_closure_hasDenseDomain : U.HasDenseDomain ↔ U.closure.HasDenseDomain := ⟨HasDenseDomain.closure, fun h ↦ dense_closure.mp (h.mono U.closure_domain_le_domain_closure)⟩lemma HasDenseDomain.neg (h : U.HasDenseDomain) : (-U).HasDenseDomain := hlemma HasDenseDomain.smul (h : U.HasDenseDomain) (c : ℂ) : (c • U).HasDenseDomain := hlemma HasDenseDomain.add_of_le (h₁ : U₁.HasDenseDomain) (h_le : U₁.domain ≤ U₂.domain) : (U₁ + U₂).HasDenseDomain := h₁.mono (H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁:U₁.HasDenseDomainh_le:U₁.domain ≤ U₂.domain⊢ ↑U₁.domain ⊆ ↑(U₁ + U₂).domain All goals completed! 🐙)lemma HasDenseDomain.sub_of_le (h₁ : U₁.HasDenseDomain) (h_le : U₁.domain ≤ U₂.domain) : (U₁ - U₂).HasDenseDomain := h₁.mono (H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁:U₁.HasDenseDomainh_le:U₁.domain ≤ U₂.domain⊢ ↑U₁.domain ⊆ ↑(U₁ - U₂).domain All goals completed! 🐙)lemma HasDenseDomain.sum_of_le {E : Submodule ℂ H} (hE : Dense (E : Set H)) (h : ∀ a, E ≤ (W a).domain) : (sum W).HasDenseDomain := hE.mono (H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'α:Type u_4inst✝:Fintype αW:α → H →ₗ.[ℂ] H'E:Submodule ℂ HhE:Dense ↑Eh:∀ (a : α), E ≤ (W a).domain⊢ ↑E ⊆ ↑(sum W).domain All goals completed! 🐙)lemma HasDenseDomain.pow (h : T.HasDenseDomain) (h_range : ∀ x : T.domain, T x ∈ T.domain) (n : ℕ) : (T ^ n).HasDenseDomain := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hh:T.HasDenseDomainh_range:∀ (x : ↥T.domain), ↑T x ∈ T.domainn:ℕ⊢ (T ^ n).HasDenseDomain H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hh:T.HasDenseDomainh_range:∀ (x : ↥T.domain), ↑T x ∈ T.domainn:ℕ⊢ ↑T.domain ⊆ ↑(T ^ n).domain induction n with H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hh:T.HasDenseDomainh_range:∀ (x : ↥T.domain), ↑T x ∈ T.domain⊢ ↑T.domain ⊆ ↑(T ^ 0).domain All goals completed! 🐙 H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hh:T.HasDenseDomainh_range:∀ (x : ↥T.domain), ↑T x ∈ T.domainn:ℕih:↑T.domain ⊆ ↑(T ^ n).domain⊢ ↑T.domain ⊆ ↑(T ^ (n + 1)).domain All goals completed! 🐙lemma pow_hasDenseDomain_of_le {n : ℕ} (h : (T ^ n).HasDenseDomain) {k : ℕ} (hle : k ≤ n) : (T ^ k).HasDenseDomain := h.mono <| pow_sub_mul_pow T hle ▸ compRestricted_domain_le _ _

U.rangeᗮ = U†.ker

c.f. LinearMap.orthogonal_range and ContinuousLinearMap.orthogonal_range

lemma HasDenseDomain.orthogonal_range [CompleteSpace H] (h : U.HasDenseDomain) : U.toFun.rangeᗮ = U†.toFun.ker.map U†.domain.subtype := H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh:U.HasDenseDomain⊢ U.toFun.rangeᗮ = map U†.domain.subtype U†.toFun.ker H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh:U.HasDenseDomainu:H'⊢ u ∈ U.toFun.rangeᗮ ↔ u ∈ map U†.domain.subtype U†.toFun.ker H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh:U.HasDenseDomainu:H'⊢ (∀ u_1 ∈ U.toFun.range, ⟪u, u_1⟫_ℂ = 0) ↔ ∃ (x : u ∈ U†.domain), ↑U† ⟨u, ⋯⟩ = 0 H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh:U.HasDenseDomainu:H'⊢ (∀ u_1 ∈ U.toFun.range, ⟪u, u_1⟫_ℂ = 0) → ∃ (x : u ∈ U†.domain), ↑U† ⟨u, ⋯⟩ = 0H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh:U.HasDenseDomainu:H'⊢ (∃ (x : u ∈ U†.domain), ↑U† ⟨u, ⋯⟩ = 0) → ∀ u_1 ∈ U.toFun.range, ⟪u, u_1⟫_ℂ = 0 H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh:U.HasDenseDomainu:H'⊢ (∀ u_1 ∈ U.toFun.range, ⟪u, u_1⟫_ℂ = 0) → ∃ (x : u ∈ U†.domain), ↑U† ⟨u, ⋯⟩ = 0 H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh:U.HasDenseDomainu:H'h':∀ u_1 ∈ U.toFun.range, ⟪u, u_1⟫_ℂ = 0⊢ ∃ (x : u ∈ U†.domain), ↑U† ⟨u, ⋯⟩ = 0 exact ⟨mem_adjoint_domain_of_exists u ⟨0, H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh:U.HasDenseDomainu:H'h':∀ u_1 ∈ U.toFun.range, ⟪u, u_1⟫_ℂ = 0⊢ ∀ (x : ↥U.domain), ⟪0, ↑x⟫_ℂ = ⟪u, ↑U x⟫_ℂ All goals completed! 🐙⟩, adjoint_apply_eq h _ (H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh:U.HasDenseDomainu:H'h':∀ u_1 ∈ U.toFun.range, ⟪u, u_1⟫_ℂ = 0⊢ ∀ (x : ↥U.domain), ⟪0, ↑x⟫_ℂ = ⟪↑⟨u, ⋯⟩, ↑U x⟫_ℂ All goals completed! 🐙)⟩ H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh:U.HasDenseDomainu:H'⊢ (∃ (x : u ∈ U†.domain), ↑U† ⟨u, ⋯⟩ = 0) → ∀ u_1 ∈ U.toFun.range, ⟪u, u_1⟫_ℂ = 0 H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh:U.HasDenseDomainu:H'hu:u ∈ U†.domainhu':↑U† ⟨u, ⋯⟩ = 0v:H'x:↥U.domainhxv:U.toFun x = v⊢ ⟪u, v⟫_ℂ = 0 All goals completed! 🐙

U†.kerᗮ = U.range.closure

lemma HasDenseDomain.orthogonal_adjoint_ker [CompleteSpace H] [CompleteSpace H'] (h : U.HasDenseDomain) : (U†.toFun.ker.map U†.domain.subtype)ᗮ = U.toFun.range.closure := h.orthogonal_range ▸ orthogonal_orthogonal_eq_closure _

B.2. Closability

lemma IsClosed.closure_eq (h : U.IsClosed) : U.closure = U := eq_of_eq_graph (h.isClosable.graph_closure_eq_closure_graph ▸ h.submodule_topologicalClosure_eq)lemma IsClosable.isClosed_iff (h : U.IsClosable) : U.IsClosed ↔ U.closure = U := ⟨IsClosed.closure_eq, fun h' ↦ h' ▸ h.closure_isClosed⟩

A LinearPMap with densely-defined formal adjoint is closable.

All goals completed! 🐙

A zero LinearPMap (any domain) is closable.

H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h_zero:↑U = 0x:H × H'hx:x ∈ U.graph.topologicalClosurehx₁:x.1 = 0b:ℕ → H × H'hb:∀ (n : ℕ), b n ∈ ↑U.graph.toAddSubmonoidhb':Filter.Tendsto (fun n => (b n).1) Filter.atTop (nhds x.1) ∧ Filter.Tendsto (fun n => (b n).2) Filter.atTop (nhds x.2)hbn:∀ (n : ℕ), (b n).2 = 0⊢ x.2 = 0 All goals completed! 🐙
H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h:U.IsClosablec:ℂhc:NeZero cx:H × H'hx:x ∈ (c • U).graph.topologicalClosurehx₁:x.1 = 0b:ℕ → H × H'hb:∀ (n : ℕ), b n ∈ ↑(c • U).graph.toAddSubmonoidhb':Filter.Tendsto (fun n => (b n).1) Filter.atTop (nhds x.1) ∧ Filter.Tendsto (fun n => (b n).2) Filter.atTop (nhds x.2)⊢ (∀ (n : ℕ), (fun n => ((b n).1, c⁻¹ • (b n).2)) n ∈ ↑U.graph.toAddSubmonoid) ∧ Filter.Tendsto (fun n => ((b n).1, c⁻¹ • (b n).2).1) Filter.atTop (nhds 0) ∧ Filter.Tendsto (fun n => ((b n).1, c⁻¹ • (b n).2).2) Filter.atTop (nhds (c⁻¹ • x.2)) H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h:U.IsClosablec:ℂhc:NeZero cx:H × H'hx:x ∈ (c • U).graph.topologicalClosurehx₁:x.1 = 0b:ℕ → H × H'hb:∀ (n : ℕ), b n ∈ ↑(c • U).graph.toAddSubmonoidhb':Filter.Tendsto (fun n => (b n).1) Filter.atTop (nhds x.1) ∧ Filter.Tendsto (fun n => (b n).2) Filter.atTop (nhds x.2)n:ℕ⊢ (fun n => ((b n).1, c⁻¹ • (b n).2)) n ∈ ↑U.graph.toAddSubmonoid H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h:U.IsClosablec:ℂhc:NeZero cx:H × H'hx:x ∈ (c • U).graph.topologicalClosurehx₁:x.1 = 0b:ℕ → H × H'hb:∀ (n : ℕ), b n ∈ ↑(c • U).graph.toAddSubmonoidhb':Filter.Tendsto (fun n => (b n).1) Filter.atTop (nhds x.1) ∧ Filter.Tendsto (fun n => (b n).2) Filter.atTop (nhds x.2)n:ℕu:↥(c • U).domain × H'hu:u ∈ ↑(c • U).toFun.graphhu':((c • U).domain.subtype.prodMap LinearMap.id) u = b n⊢ (fun n => ((b n).1, c⁻¹ • (b n).2)) n ∈ ↑U.graph.toAddSubmonoid H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h:U.IsClosablec:ℂhc:NeZero cx:H × H'hx:x ∈ (c • U).graph.topologicalClosurehx₁:x.1 = 0b:ℕ → H × H'hb:∀ (n : ℕ), b n ∈ ↑(c • U).graph.toAddSubmonoidhb':Filter.Tendsto (fun n => (b n).1) Filter.atTop (nhds x.1) ∧ Filter.Tendsto (fun n => (b n).2) Filter.atTop (nhds x.2)n:ℕu:↥(c • U).domain × H'hu:u ∈ ↑(c • U).toFun.graphhu':((c • U).domain.subtype.prodMap LinearMap.id) u = b n⊢ ∃ a, ∃ (h : a ∈ U.domain), a = (((c • U).domain.subtype.prodMap LinearMap.id) u).1 ∧ ↑U ⟨a, ⋯⟩ = c⁻¹ • (((c • U).domain.subtype.prodMap LinearMap.id) u).2 All goals completed! 🐙lemma IsClosable.smul_iff {c : ℂ} (hc : c ≠ 0) : (c • U).IsClosable ↔ U.IsClosable := ⟨fun h ↦ one_smul ℂ U ▸ inv_mul_cancel₀ hc ▸ smul_smul c⁻¹ c U ▸ h.smul c⁻¹, fun h ↦ h.smul c⟩lemma neg_eq_neg_one_smul (U : H →ₗ.[ℂ] H') : -U = (-1 : ℂ) • U := ext (H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'⊢ (-U).domain = (-1 • U).domain All goals completed! 🐙) (H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'⊢ ∀ ⦃x : H⦄ ⦃hf : x ∈ (-U).domain⦄ ⦃hg : x ∈ (-1 • U).domain⦄, ↑(-U) ⟨x, hf⟩ = ↑(-1 • U) ⟨x, hg⟩ All goals completed! 🐙)@[aesop safe apply] lemma IsClosable.neg (h : U.IsClosable) : (-U).IsClosable := neg_eq_neg_one_smul U ▸ h.smul _All goals completed! 🐙

B.3. Adjoints

@[simp] lemma adjoint_one [CompleteSpace H] : (1 : H →ₗ.[ℂ] H)† = 1 := H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace H⊢ 1† = 1 H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace Hx:H⊢ x ∈ 1†.domain ↔ x ∈ domain 1H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace Hx:Hhf✝:x ∈ 1†.domainhg✝:x ∈ domain 1⊢ ↑1† ⟨x, hf✝⟩ = ↑1 ⟨x, hg✝⟩ H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace Hx:H⊢ x ∈ 1†.domain ↔ x ∈ domain 1 H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace Hx:H⊢ x ∈ 1†.domain All goals completed! 🐙 H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hinst✝:CompleteSpace Hx:Hhf✝:x ∈ 1†.domainhg✝:x ∈ domain 1⊢ ↑1† ⟨x, hf✝⟩ = ↑1 ⟨x, hg✝⟩ All goals completed! 🐙

The adjoint of a zero LinearPMap (any domain) is zero (domain ⊤).

lemma adjoint_of_zero [CompleteSpace H] (h_zero : ⇑U = 0) : U† = 0 := H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh_zero:↑U = 0⊢ U† = 0 H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh_zero:↑U = 0⊢ U†.domain = domain 0H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh_zero:↑U = 0x:↥U†.domainy:↥(domain 0)hxy:↑x = ↑y⊢ ↑U† x = ↑0 y H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh_zero:↑U = 0⊢ U†.domain = domain 0 H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh_zero:↑U = 0x✝:H'⊢ x✝ ∈ U†.domain ↔ x✝ ∈ domain 0 H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh_zero:↑U = 0x✝:H'⊢ x✝ ∈ U†.domain exact (mem_adjoint_domain_iff _ _).mpr (continuous_of_const (H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh_zero:↑U = 0x✝:H'⊢ ∀ (x y : ↥U.domain), ((innerₛₗ ℂ) x✝ ∘ₗ U.toFun) x = ((innerₛₗ ℂ) x✝ ∘ₗ U.toFun) y All goals completed! 🐙)) H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh_zero:↑U = 0x:↥U†.domainy:↥(domain 0)hxy:↑x = ↑y⊢ ↑U† x = ↑0 y H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh_zero:↑U = 0x:↥U†.domainy:↥(domain 0)hxy:↑x = ↑yh:U.HasDenseDomain⊢ ↑U† x = ↑0 yH:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh_zero:↑U = 0x:↥U†.domainy:↥(domain 0)hxy:↑x = ↑yh:¬U.HasDenseDomain⊢ ↑U† x = ↑0 y H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh_zero:↑U = 0x:↥U†.domainy:↥(domain 0)hxy:↑x = ↑yh:U.HasDenseDomain⊢ ↑U† x = ↑0 y exact adjoint_apply_eq h x (H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh_zero:↑U = 0x:↥U†.domainy:↥(domain 0)hxy:↑x = ↑yh:U.HasDenseDomain⊢ ∀ (x_1 : ↥U.domain), ⟪↑0 y, ↑x_1⟫_ℂ = ⟪↑x, ↑U x_1⟫_ℂ All goals completed! 🐙) H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh_zero:↑U = 0x:↥U†.domainy:↥(domain 0)hxy:↑x = ↑yh:¬U.HasDenseDomain⊢ ↑U† x = ↑0 y All goals completed! 🐙
@[simp] lemma adjoint_zero [CompleteSpace H] : (0 : H →ₗ.[ℂ] H')† = 0 := adjoint_of_zero rfl@[simp] lemma adjoint_smul [CompleteSpace H] (U : H →ₗ.[ℂ] H') {c : ℂ} (hc : c ≠ 0) : (c • U)† = conj c • U† := H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU:H →ₗ.[ℂ] H'c:ℂhc:c ≠ 0⊢ (c • U)† = (starRingEnd ℂ) c • U† H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU:H →ₗ.[ℂ] H'c:ℂhc:c ≠ 0⊢ (c • U)†.domain = ((starRingEnd ℂ) c • U†).domainH:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU:H →ₗ.[ℂ] H'c:ℂhc:c ≠ 0x:↥(c • U)†.domainy:↥((starRingEnd ℂ) c • U†).domainhxy:↑x = ↑y⊢ ↑(c • U)† x = ↑((starRingEnd ℂ) c • U†) y H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU:H →ₗ.[ℂ] H'c:ℂhc:c ≠ 0⊢ (c • U)†.domain = ((starRingEnd ℂ) c • U†).domain H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU:H →ₗ.[ℂ] H'c:ℂhc:c ≠ 0x:H'⊢ x ∈ (c • U)†.domain ↔ x ∈ ((starRingEnd ℂ) c • U†).domain H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU:H →ₗ.[ℂ] H'c:ℂhc:c ≠ 0x:H'⊢ (Continuous fun w => ⟪x, c • ↑U w⟫_ℂ) ↔ Continuous fun w => ⟪x, ↑U w⟫_ℂ exact Iff.trans (H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU:H →ₗ.[ℂ] H'c:ℂhc:c ≠ 0x:H'⊢ (Continuous fun w => ⟪x, c • ↑U w⟫_ℂ) ↔ Continuous fun x_1 => c • ⟪x, ↑U x_1⟫_ℂ All goals completed! 🐙) (continuous_const_smul_iff₀ hc) H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU:H →ₗ.[ℂ] H'c:ℂhc:c ≠ 0x:↥(c • U)†.domainy:↥((starRingEnd ℂ) c • U†).domainhxy:↑x = ↑y⊢ ↑(c • U)† x = ↑((starRingEnd ℂ) c • U†) y H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU:H →ₗ.[ℂ] H'c:ℂhc:c ≠ 0x:↥(c • U)†.domainy:↥((starRingEnd ℂ) c • U†).domainhxy:↑x = ↑yh:U.HasDenseDomain⊢ ↑(c • U)† x = ↑((starRingEnd ℂ) c • U†) yH:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU:H →ₗ.[ℂ] H'c:ℂhc:c ≠ 0x:↥(c • U)†.domainy:↥((starRingEnd ℂ) c • U†).domainhxy:↑x = ↑yh:¬U.HasDenseDomain⊢ ↑(c • U)† x = ↑((starRingEnd ℂ) c • U†) y H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU:H →ₗ.[ℂ] H'c:ℂhc:c ≠ 0x:↥(c • U)†.domainy:↥((starRingEnd ℂ) c • U†).domainhxy:↑x = ↑yh:U.HasDenseDomain⊢ ↑(c • U)† x = ↑((starRingEnd ℂ) c • U†) y H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU:H →ₗ.[ℂ] H'c:ℂhc:c ≠ 0x:↥(c • U)†.domainy:↥((starRingEnd ℂ) c • U†).domainhxy:↑x = ↑yh:U.HasDenseDomainw:↥(c • U).domain⊢ ⟪↑((starRingEnd ℂ) c • U†) y, ↑w⟫_ℂ = ⟪↑x, ↑(c • U) w⟫_ℂ All goals completed! 🐙 H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU:H →ₗ.[ℂ] H'c:ℂhc:c ≠ 0x:↥(c • U)†.domainy:↥((starRingEnd ℂ) c • U†).domainhxy:↑x = ↑yh:¬U.HasDenseDomain⊢ ↑(c • U)† x = ↑((starRingEnd ℂ) c • U†) y All goals completed! 🐙@[simp] lemma adjoint_neg [CompleteSpace H] (U : H →ₗ.[ℂ] H') : (-U)† = -U† := H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU:H →ₗ.[ℂ] H'⊢ (-U)† = -U† All goals completed! 🐙All goals completed! 🐙lemma adjoint_add_le_add_adjoint [CompleteSpace H] (U₁ U₂ : H →ₗ.[ℂ] H') (h₁₂ : (U₁ + U₂).HasDenseDomain) : U₁† + U₂† ≤ (U₁ + U₂)† := H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁₂:(U₁ + U₂).HasDenseDomain⊢ U₁† + U₂† ≤ (U₁ + U₂)† H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁₂:(U₁ + U₂).HasDenseDomainh₁:U₁.HasDenseDomain⊢ U₁† + U₂† ≤ (U₁ + U₂)† H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁₂:(U₁ + U₂).HasDenseDomainh₁:U₁.HasDenseDomainh₂:U₂.HasDenseDomain⊢ U₁† + U₂† ≤ (U₁ + U₂)† H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁₂:(U₁ + U₂).HasDenseDomainh₁:U₁.HasDenseDomainh₂:U₂.HasDenseDomain⊢ (U₁† + U₂†).domain ≤ (U₁ + U₂)†.domainH:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁₂:(U₁ + U₂).HasDenseDomainh₁:U₁.HasDenseDomainh₂:U₂.HasDenseDomain⊢ ∀ ⦃x : ↥(U₁† + U₂†).domain⦄ ⦃y : ↥(U₁ + U₂)†.domain⦄, ↑x = ↑y → ↑(U₁† + U₂†) x = ↑(U₁ + U₂)† y H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁₂:(U₁ + U₂).HasDenseDomainh₁:U₁.HasDenseDomainh₂:U₂.HasDenseDomain⊢ (U₁† + U₂†).domain ≤ (U₁ + U₂)†.domain H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁₂:(U₁ + U₂).HasDenseDomainh₁:U₁.HasDenseDomainh₂:U₂.HasDenseDomainu:H'hu:u ∈ (U₁† + U₂†).domain⊢ u ∈ (U₁ + U₂)†.domain H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁₂:(U₁ + U₂).HasDenseDomainh₁:U₁.HasDenseDomainh₂:U₂.HasDenseDomainu:H'hu:u ∈ (U₁† + U₂†).domainx:↥(U₁ + U₂).domain⊢ ⟪↑U₁† ⟨u, ⋯⟩ + ↑U₂† ⟨u, ⋯⟩, ↑x⟫_ℂ = ⟪u, ↑(U₁ + U₂) x⟫_ℂ All goals completed! 🐙 H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁₂:(U₁ + U₂).HasDenseDomainh₁:U₁.HasDenseDomainh₂:U₂.HasDenseDomain⊢ ∀ ⦃x : ↥(U₁† + U₂†).domain⦄ ⦃y : ↥(U₁ + U₂)†.domain⦄, ↑x = ↑y → ↑(U₁† + U₂†) x = ↑(U₁ + U₂)† y H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁₂:(U₁ + U₂).HasDenseDomainh₁:U₁.HasDenseDomainh₂:U₂.HasDenseDomainu:↥(U₁† + U₂†).domainv:↥(U₁ + U₂)†.domainhuv:↑u = ↑v⊢ ↑(U₁† + U₂†) u = ↑(U₁ + U₂)† v H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁₂:(U₁ + U₂).HasDenseDomainh₁:U₁.HasDenseDomainh₂:U₂.HasDenseDomainu:↥(U₁† + U₂†).domainv:↥(U₁ + U₂)†.domainhuv:↑u = ↑vw:↥(U₁ + U₂).domain⊢ ⟪↑(U₁† + U₂†) u, ↑w⟫_ℂ = ⟪↑v, ↑(U₁ + U₂) w⟫_ℂ All goals completed! 🐙lemma adjoint_sub_le_sub_adjoint [CompleteSpace H] (U₁ U₂ : H →ₗ.[ℂ] H') (h₁₂ : (U₁ - U₂).HasDenseDomain) : U₁† - U₂† ≤ (U₁ - U₂)† := H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁₂:(U₁ - U₂).HasDenseDomain⊢ U₁† - U₂† ≤ (U₁ - U₂)† H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'inst✝:CompleteSpace HU₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁₂:(U₁ - U₂).HasDenseDomain⊢ U₁† + (-U₂)† ≤ (U₁ + -U₂)† All goals completed! 🐙H:Type u_1inst✝⁷:NormedAddCommGroup Hinst✝⁶:InnerProductSpace ℂ HH':Type u_2inst✝⁵:NormedAddCommGroup H'inst✝⁴:InnerProductSpace ℂ H'H'':Type u_3inst✝³:NormedAddCommGroup H''inst✝²:InnerProductSpace ℂ H''U:H →ₗ.[ℂ] H'V:H' →ₗ.[ℂ] H''inst✝¹:CompleteSpace Hinst✝:CompleteSpace H'hV:V.HasDenseDomainhVU:(V ∘ᵣ U).HasDenseDomainhU:U.HasDenseDomainh:(U† ∘ᵣ V†).IsFormalAdjoint (V ∘ᵣ U)⊢ U† ∘ᵣ V† ≤ (V ∘ᵣ U)† All goals completed! 🐙lemma adjoint_pow_le_pow_adjoint [CompleteSpace H] {n : ℕ} (h : (T ^ n).HasDenseDomain) : T† ^ n ≤ (T ^ n)† := H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hn:ℕh:(T ^ n).HasDenseDomain⊢ T† ^ n ≤ (T ^ n)† induction n with H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:(T ^ 0).HasDenseDomain⊢ T† ^ 0 ≤ (T ^ 0)† All goals completed! 🐙 H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hn:ℕih:(T ^ n).HasDenseDomain → T† ^ n ≤ (T ^ n)†h:(T ^ (n + 1)).HasDenseDomain⊢ T† ^ (n + 1) ≤ (T ^ (n + 1))† H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hn:ℕih:(T ^ n).HasDenseDomain → T† ^ n ≤ (T ^ n)†h:(T ^ (n + 1)).HasDenseDomainhTn:(T ^ n).HasDenseDomain⊢ T† ^ (n + 1) ≤ (T ^ (n + 1))† H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hn:ℕih:(T ^ n).HasDenseDomain → T† ^ n ≤ (T ^ n)†h:(T ^ (n + 1)).HasDenseDomainhTn:(T ^ n).HasDenseDomain⊢ T† ^ (n + 1) ≤ T† ∘ᵣ (npowRec n T)† All goals completed! 🐙

B.4. Continuity / boundedness

f : E →ₗ[𝕜] F is continuous iff there exists M > 0 s.t. ‖f x‖ ≤ M * ‖x‖ for all x : E.

This is a (convenient) immediate consequence of IsBoundedLinearMap.isLinearMap_and_continuous_iff_isBoundedLinearMap.

𝕜:Type u_5E:Type u_6F:Type u_7inst✝⁴:NontriviallyNormedField 𝕜inst✝³:SeminormedAddCommGroup Einst✝²:NormedSpace 𝕜 Einst✝¹:SeminormedAddCommGroup Finst✝:NormedSpace 𝕜 Ff:E →ₗ[𝕜] F⊢ IsLinearMap 𝕜 ⇑f ∧ Continuous ⇑f ↔ IsBoundedLinearMap 𝕜 ⇑f All goals completed! 🐙

Continuous operators are closable.

H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h:Continuous ↑Ux:H × H'hx:x ∈ U.graph.topologicalClosurehx₁:x.1 = 0b:ℕ → H × H'hb:∀ (n : ℕ), b n ∈ ↑U.graph.toAddSubmonoidhbx:Filter.Tendsto b Filter.atTop (nhds x.1 ×ˢ nhds x.2)⊢ x.2 = 0 H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h:Continuous ↑Ux:H × H'hx:x ∈ U.graph.topologicalClosurehx₁:x.1 = 0b:ℕ → H × H'hb:∀ (n : ℕ), b n ∈ ↑U.graph.toAddSubmonoidhbx:Filter.Tendsto b Filter.atTop (nhds x.1 ×ˢ nhds x.2)⊢ Filter.Tendsto (fun x => ‖(b x).2‖) Filter.atTop (nhds 0) H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h:Continuous ↑Ux:H × H'hx:x ∈ U.graph.topologicalClosurehx₁:x.1 = 0b:ℕ → H × H'hb:∀ (n : ℕ), b n ∈ ↑U.graph.toAddSubmonoidhbx:Filter.Tendsto b Filter.atTop (nhds x.1 ×ˢ nhds x.2)M:ℝhM:0 < Mh_bound:∀ (x : ↥U.domain), ‖U.toFun x‖ ≤ M * ‖x‖⊢ Filter.Tendsto (fun x => ‖(b x).2‖) Filter.atTop (nhds 0) H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h:Continuous ↑Ux:H × H'hx:x ∈ U.graph.topologicalClosurehx₁:x.1 = 0b:ℕ → H × H'hb:∀ (n : ℕ), b n ∈ ↑U.graph.toAddSubmonoidhbx:Filter.Tendsto b Filter.atTop (nhds x.1 ×ˢ nhds x.2)M:ℝhM:0 < Mh_bound:∀ (x : ↥U.domain), ‖U.toFun x‖ ≤ M * ‖x‖n:ℕ⊢ ‖(b n).2‖ ≤ M * ‖(b n).1‖H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h:Continuous ↑Ux:H × H'hx:x ∈ U.graph.topologicalClosurehx₁:x.1 = 0b:ℕ → H × H'hb:∀ (n : ℕ), b n ∈ ↑U.graph.toAddSubmonoidhbx:Filter.Tendsto b Filter.atTop (nhds x.1 ×ˢ nhds x.2)M:ℝhM:0 < Mh_bound:∀ (x : ↥U.domain), ‖U.toFun x‖ ≤ M * ‖x‖⊢ Filter.Tendsto (fun n => M * ‖(b n).1‖) Filter.atTop (nhds 0) H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h:Continuous ↑Ux:H × H'hx:x ∈ U.graph.topologicalClosurehx₁:x.1 = 0b:ℕ → H × H'hb:∀ (n : ℕ), b n ∈ ↑U.graph.toAddSubmonoidhbx:Filter.Tendsto b Filter.atTop (nhds x.1 ×ˢ nhds x.2)M:ℝhM:0 < Mh_bound:∀ (x : ↥U.domain), ‖U.toFun x‖ ≤ M * ‖x‖n:ℕ⊢ ‖(b n).2‖ ≤ M * ‖(b n).1‖ H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h:Continuous ↑Ux:H × H'hx:x ∈ U.graph.topologicalClosurehx₁:x.1 = 0b:ℕ → H × H'hb:∀ (n : ℕ), b n ∈ ↑U.graph.toAddSubmonoidhbx:Filter.Tendsto b Filter.atTop (nhds x.1 ×ˢ nhds x.2)M:ℝhM:0 < Mh_bound:∀ (x : ↥U.domain), ‖U.toFun x‖ ≤ M * ‖x‖n:ℕy:↥U.domainhy₁:↑y = (b n).1hy₂:↑U y = (b n).2⊢ ‖(b n).2‖ ≤ M * ‖(b n).1‖ H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h:Continuous ↑Ux:H × H'hx:x ∈ U.graph.topologicalClosurehx₁:x.1 = 0b:ℕ → H × H'hb:∀ (n : ℕ), b n ∈ ↑U.graph.toAddSubmonoidhbx:Filter.Tendsto b Filter.atTop (nhds x.1 ×ˢ nhds x.2)M:ℝhM:0 < Mh_bound:∀ (x : ↥U.domain), ‖U.toFun x‖ ≤ M * ‖x‖n:ℕy:↥U.domainhy₁:↑y = (b n).1hy₂:↑U y = (b n).2⊢ ‖↑U y‖ ≤ M * ‖↑y‖ All goals completed! 🐙 H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'h:Continuous ↑Ux:H × H'hx:x ∈ U.graph.topologicalClosurehx₁:x.1 = 0b:ℕ → H × H'hb:∀ (n : ℕ), b n ∈ ↑U.graph.toAddSubmonoidhbx:Filter.Tendsto b Filter.atTop (nhds x.1 ×ˢ nhds x.2)M:ℝhM:0 < Mh_bound:∀ (x : ↥U.domain), ‖U.toFun x‖ ≤ M * ‖x‖⊢ Filter.Tendsto (fun n => M * ‖(b n).1‖) Filter.atTop (nhds 0) All goals completed! 🐙

A strengthening of closure_domain_le_domain_closure for continuous operators.

H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace H'h:Continuous ↑Ux:Hhx:x ∈ ↑U.domain.closureM:ℝhM:0 < Mh_bound:∀ (x : ↥U.domain), ‖U.toFun x‖ ≤ M * ‖x‖b:ℕ → Hhb':Filter.Tendsto b Filter.atTop (nhds x)hb:∀ (n : ℕ), b n ∈ U.domainUb:ℕ → H' := fun n => ↑U ⟨b n, ⋯⟩hCS:CauchySeq Uby:H'hy:Filter.map Ub Filter.atTop ≤ nhds y⊢ Filter.Tendsto (fun n => (b n, Ub n)) Filter.atTop (nhds x ×ˢ nhds y) All goals completed! 🐙

A continuous operator is closed iff its domain is closed.

H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace H'h:Continuous ↑U⊢ U.closure = U ↔ _root_.IsClosed ↑U.domain H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace H'h:Continuous ↑Uh_domain:U.closure.domain = ↑U.domain.closure⊢ U.closure = U ↔ _root_.IsClosed ↑U.domain H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace H'h:Continuous ↑Uh_domain:U.closure.domain = ↑U.domain.closure⊢ U.closure = U → _root_.IsClosed ↑U.domainH:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace H'h:Continuous ↑Uh_domain:U.closure.domain = ↑U.domain.closure⊢ _root_.IsClosed ↑U.domain → U.closure = U H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace H'h:Continuous ↑Uh_domain:U.closure.domain = ↑U.domain.closure⊢ U.closure = U → _root_.IsClosed ↑U.domainH:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace H'h:Continuous ↑Uh_domain:U.closure.domain = ↑U.domain.closure⊢ _root_.IsClosed ↑U.domain → U.closure = U H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace H'h:Continuous ↑Uh_domain:U.closure.domain = ↑U.domain.closurehcl:_root_.IsClosed ↑U.domain⊢ U.closure = U H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace H'h:Continuous ↑Uh_domain:U.closure.domain = ↑U.domain.closurehcl:U.closure = U⊢ _root_.IsClosed ↑U.domain All goals completed! 🐙 H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace H'h:Continuous ↑Uh_domain:U.closure.domain = ↑U.domain.closurehcl:_root_.IsClosed ↑U.domain⊢ U.closure = U H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace H'h:Continuous ↑Uh_domain:U.closure.domain = ↑U.domain.closurehcl:_root_.IsClosed ↑U.domain⊢ U.domain = U.closure.domain All goals completed! 🐙
H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'hU:U.IsClosedx✝:↥U.domain × H'x₁:↥U.domainx₂:H'hx:(x₁, x₂) ∈ _root_.closure ↑U.toFun.graphb:ℕ → ↥U.domain × H'hb:∀ (n : ℕ), b n ∈ ↑U.toFun.graphhbx:Filter.Tendsto b Filter.atTop (nhds x₁ ×ˢ nhds x₂)⊢ ∃ x, (∀ (n : ℕ), x n ∈ ↑U.graph.toAddSubmonoid) ∧ Filter.Tendsto x Filter.atTop (nhds ↑x₁ ×ˢ nhds x₂) refine ⟨fun n ↦ (↑(b n).1, (b n).2), H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'hU:U.IsClosedx✝:↥U.domain × H'x₁:↥U.domainx₂:H'hx:(x₁, x₂) ∈ _root_.closure ↑U.toFun.graphb:ℕ → ↥U.domain × H'hb:∀ (n : ℕ), b n ∈ ↑U.toFun.graphhbx:Filter.Tendsto b Filter.atTop (nhds x₁ ×ˢ nhds x₂)⊢ ∀ (n : ℕ), (fun n => (↑(b n).1, (b n).2)) n ∈ ↑U.graph.toAddSubmonoid All goals completed! 🐙, Filter.Tendsto.prodMk (tendsto_subtype_rng.mp hbx.fst) hbx.snd⟩

The closed graph theorem for partial linear maps: a closed operator with closed domain is continuous.

This follows immediately from LinearMap.continuous_of_isClosed_graph and the completeness of H and H'.

lemma IsClosed.continuous_of_isClosed_domain [CompleteSpace H] [CompleteSpace H'] (hU : U.IsClosed) (h : _root_.IsClosed (U.domain : Set H)) : Continuous U := H:Type u_1inst✝⁵:NormedAddCommGroup Hinst✝⁴:InnerProductSpace ℂ HH':Type u_2inst✝³:NormedAddCommGroup H'inst✝²:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝¹:CompleteSpace Hinst✝:CompleteSpace H'hU:U.IsClosedh:_root_.IsClosed ↑U.domain⊢ Continuous ↑U H:Type u_1inst✝⁵:NormedAddCommGroup Hinst✝⁴:InnerProductSpace ℂ HH':Type u_2inst✝³:NormedAddCommGroup H'inst✝²:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝¹:CompleteSpace Hinst✝:CompleteSpace H'hU:U.IsClosedh:_root_.IsClosed ↑U.domainthis:CompleteSpace ↥U.domain⊢ Continuous ↑U All goals completed! 🐙

Closability is preserved upon adding a continuous operator.

H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁:U₁.IsClosableh₂:Continuous ↑U₂h:U₁.domain ≤ U₂.domainx✝:H × H'x₂:H'hx:(0, x₂) ∈ (U₁ + U₂).graph.topologicalClosure⊢ (0, (0, x₂).2) ∈ U₁.graph.topologicalClosure H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁:U₁.IsClosableh₂:Continuous ↑U₂h:U₁.domain ≤ U₂.domainx✝:H × H'x₂:H'hx:(0, x₂) ∈ (U₁ + U₂).graph.topologicalClosure⊢ ∃ x, (∀ (n : ℕ), x n ∈ ↑U₁.graph.toAddSubmonoid) ∧ Filter.Tendsto x Filter.atTop (nhds (0, (0, x₂).2)) H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁:U₁.IsClosableh₂:Continuous ↑U₂h:U₁.domain ≤ U₂.domainx✝:H × H'x₂:H'hx:(0, x₂) ∈ (U₁ + U₂).graph.topologicalClosureb:ℕ → H × H'hb:∀ (n : ℕ), b n ∈ ↑(U₁ + U₂).graph.toAddSubmonoidhbx:Filter.Tendsto b Filter.atTop (nhds (0, x₂))⊢ ∃ x, (∀ (n : ℕ), x n ∈ ↑U₁.graph.toAddSubmonoid) ∧ Filter.Tendsto x Filter.atTop (nhds (0, (0, x₂).2)) H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁:U₁.IsClosableh₂:Continuous ↑U₂h:U₁.domain ≤ U₂.domainx✝:H × H'x₂:H'hx:(0, x₂) ∈ (U₁ + U₂).graph.topologicalClosureb:ℕ → H × H'hb:∀ (n : ℕ), ∃ (x : (b n).1 ∈ U₁.domain ⊓ U₂.domain), ↑U₁ ⟨(b n).1, ⋯⟩ + ↑U₂ ⟨(b n).1, ⋯⟩ = (b n).2hbx:Filter.Tendsto b Filter.atTop (nhds 0 ×ˢ nhds x₂)⊢ ∃ x, (∀ (n : ℕ), ∃ (x_1 : (x n).1 ∈ U₁.domain), ↑U₁ ⟨(x n).1, ⋯⟩ = (x n).2) ∧ Filter.Tendsto x Filter.atTop (nhds 0 ×ˢ nhds x₂) H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁:U₁.IsClosableh₂:Continuous ↑U₂h:U₁.domain ≤ U₂.domainx✝:H × H'x₂:H'hx:(0, x₂) ∈ (U₁ + U₂).graph.topologicalClosureb:ℕ → H × H'hb:∀ (n : ℕ), ∃ (x : (b n).1 ∈ U₁.domain ⊓ U₂.domain), ↑U₁ ⟨(b n).1, ⋯⟩ + ↑U₂ ⟨(b n).1, ⋯⟩ = (b n).2hbx:Filter.Tendsto b Filter.atTop (nhds 0 ×ˢ nhds x₂)n:ℕ⊢ ∃ (x : ((fun n => ((b n).1, (b n).2 - ↑U₂ ⟨(b n).1, ⋯⟩)) n).1 ∈ U₁.domain), ↑U₁ ⟨((fun n => ((b n).1, (b n).2 - ↑U₂ ⟨(b n).1, ⋯⟩)) n).1, ⋯⟩ = ((fun n => ((b n).1, (b n).2 - ↑U₂ ⟨(b n).1, ⋯⟩)) n).2H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁:U₁.IsClosableh₂:Continuous ↑U₂h:U₁.domain ≤ U₂.domainx✝:H × H'x₂:H'hx:(0, x₂) ∈ (U₁ + U₂).graph.topologicalClosureb:ℕ → H × H'hb:∀ (n : ℕ), ∃ (x : (b n).1 ∈ U₁.domain ⊓ U₂.domain), ↑U₁ ⟨(b n).1, ⋯⟩ + ↑U₂ ⟨(b n).1, ⋯⟩ = (b n).2hbx:Filter.Tendsto b Filter.atTop (nhds 0 ×ˢ nhds x₂)⊢ Filter.Tendsto (fun n => ((b n).1, (b n).2 - ↑U₂ ⟨(b n).1, ⋯⟩)) Filter.atTop (nhds 0 ×ˢ nhds x₂) H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁:U₁.IsClosableh₂:Continuous ↑U₂h:U₁.domain ≤ U₂.domainx✝:H × H'x₂:H'hx:(0, x₂) ∈ (U₁ + U₂).graph.topologicalClosureb:ℕ → H × H'hb:∀ (n : ℕ), ∃ (x : (b n).1 ∈ U₁.domain ⊓ U₂.domain), ↑U₁ ⟨(b n).1, ⋯⟩ + ↑U₂ ⟨(b n).1, ⋯⟩ = (b n).2hbx:Filter.Tendsto b Filter.atTop (nhds 0 ×ˢ nhds x₂)n:ℕ⊢ ∃ (x : ((fun n => ((b n).1, (b n).2 - ↑U₂ ⟨(b n).1, ⋯⟩)) n).1 ∈ U₁.domain), ↑U₁ ⟨((fun n => ((b n).1, (b n).2 - ↑U₂ ⟨(b n).1, ⋯⟩)) n).1, ⋯⟩ = ((fun n => ((b n).1, (b n).2 - ↑U₂ ⟨(b n).1, ⋯⟩)) n).2 All goals completed! 🐙 H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁:U₁.IsClosableh₂:Continuous ↑U₂h:U₁.domain ≤ U₂.domainx✝:H × H'x₂:H'hx:(0, x₂) ∈ (U₁ + U₂).graph.topologicalClosureb:ℕ → H × H'hb:∀ (n : ℕ), ∃ (x : (b n).1 ∈ U₁.domain ⊓ U₂.domain), ↑U₁ ⟨(b n).1, ⋯⟩ + ↑U₂ ⟨(b n).1, ⋯⟩ = (b n).2hbx:Filter.Tendsto b Filter.atTop (nhds 0 ×ˢ nhds x₂)⊢ Filter.Tendsto (fun n => ((b n).1, (b n).2 - ↑U₂ ⟨(b n).1, ⋯⟩)) Filter.atTop (nhds 0 ×ˢ nhds x₂) H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁:U₁.IsClosableh₂:Continuous ↑U₂h:U₁.domain ≤ U₂.domainx✝:H × H'x₂:H'hx:(0, x₂) ∈ (U₁ + U₂).graph.topologicalClosureb:ℕ → H × H'hb:∀ (n : ℕ), ∃ (x : (b n).1 ∈ U₁.domain ⊓ U₂.domain), ↑U₁ ⟨(b n).1, ⋯⟩ + ↑U₂ ⟨(b n).1, ⋯⟩ = (b n).2hbx:Filter.Tendsto b Filter.atTop (nhds 0 ×ˢ nhds x₂)⊢ Filter.Tendsto (fun n => (b n).2 - ↑U₂ ⟨(b n).1, ⋯⟩) Filter.atTop (nhds x₂) H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'U₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'h₁:U₁.IsClosableh₂:Continuous ↑U₂h:U₁.domain ≤ U₂.domainx✝:H × H'x₂:H'hx:(0, x₂) ∈ (U₁ + U₂).graph.topologicalClosureb:ℕ → H × H'hb:∀ (n : ℕ), ∃ (x : (b n).1 ∈ U₁.domain ⊓ U₂.domain), ↑U₁ ⟨(b n).1, ⋯⟩ + ↑U₂ ⟨(b n).1, ⋯⟩ = (b n).2hbx:Filter.Tendsto b Filter.atTop (nhds 0 ×ˢ nhds x₂)⊢ Filter.Tendsto (fun n => ↑U₂ ⟨(b n).1, ⋯⟩) Filter.atTop (nhds 0) All goals completed! 🐙

Closability is preserved upon subtracting a continuous operator.

lemma IsClosable.sub_continuous (h₁ : U₁.IsClosable) (h₂ : Continuous U₂) (h : U₁.domain ≤ U₂.domain) : (U₁ - U₂).IsClosable := sub_eq_add_neg U₁ U₂ ▸ h₁.add_continuous h₂.neg h

Closedness is preserved upon adding a continuous operator.

H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U₁:H →ₗ.[ℂ] H'U₂:H →ₗ.[ℂ] H'inst✝:CompleteSpace H'h₁:U₁.IsClosedh₂:Continuous ↑U₂h:U₁.domain ≤ U₂.domainhcl:(U₁ + U₂).IsClosablex₁:Hx₂:H'hx:(x₁, x₂) ∈ (U₁ + U₂).graph.topologicalClosureb:ℕ → H × H'hbx:Filter.Tendsto b Filter.atTop (nhds x₁ ×ˢ nhds x₂)hb:∀ (n : ℕ), ∃ (x : (b n).1 ∈ U₁.domain), ↑(U₁ + U₂) ⟨(b n).1, ⋯⟩ = (b n).2hb₁U₂:∀ (n : ℕ), (b n).1 ∈ U₂.domainhCS:CauchySeq fun n => ↑U₂ ⟨(b n).1, ⋯⟩y:H'hy:Filter.map (fun n => ↑U₂ ⟨(b n).1, ⋯⟩) Filter.atTop ≤ nhds yhU₁:(x₁, x₂ - y) ∈ U₁.graphhx₁:x₁ ∈ U₁.domainhU₂y:↑U₂ ⟨x₁, ⋯⟩ = y⊢ (x₁, x₂) ∈ (U₁ + U₂).graph All goals completed! 🐙

Closedness is preserved upon subtracting a continuous operator.

lemma IsClosed.sub_continuous [CompleteSpace H'] (h₁ : U₁.IsClosed) (h₂ : Continuous U₂) (h : U₁.domain ≤ U₂.domain) : (U₁ - U₂).IsClosed := sub_eq_add_neg U₁ U₂ ▸ h₁.add_continuous h₂.neg h
lemma adjoint_domain_of_continuous [CompleteSpace H] (h : Continuous U) : U†.domain = ⊤ := H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh:Continuous ↑U⊢ U†.domain = ⊤ H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh:Continuous ↑Ux✝:H'⊢ x✝ ∈ U†.domain ↔ x✝ ∈ ⊤ H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh:Continuous ↑Ux✝:H'⊢ Continuous ((fun w => ⟪x✝, w⟫_ℂ) ∘ ⇑U.toFun) exact Continuous.comp (H:Type u_1inst✝⁴:NormedAddCommGroup Hinst✝³:InnerProductSpace ℂ HH':Type u_2inst✝²:NormedAddCommGroup H'inst✝¹:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝:CompleteSpace Hh:Continuous ↑Ux✝:H'⊢ Continuous fun w => ⟪x✝, w⟫_ℂ All goals completed! 🐙) hH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domainh₂':T₂†.domain = ⊤h₁₂:(T₁ + T₂).HasDenseDomain⊢ (T₁ + T₂)† = T₁† + T₂† H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domainh₂':T₂†.domain = ⊤h₁₂:(T₁ + T₂).HasDenseDomain⊢ T₁† + T₂† ≤ (T₁ + T₂)†H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domainh₂':T₂†.domain = ⊤h₁₂:(T₁ + T₂).HasDenseDomain⊢ (T₁† + T₂†).domain = (T₁ + T₂)†.domain H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domainh₂':T₂†.domain = ⊤h₁₂:(T₁ + T₂).HasDenseDomain⊢ T₁† + T₂† ≤ (T₁ + T₂)† All goals completed! 🐙 H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domainh₂':T₂†.domain = ⊤h₁₂:(T₁ + T₂).HasDenseDomain⊢ (T₁† + T₂†).domain = (T₁ + T₂)†.domain H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domainh₂':T₂†.domain = ⊤h₁₂:(T₁ + T₂).HasDenseDomainx:H⊢ x ∈ (T₁† + T₂†).domain ↔ x ∈ (T₁ + T₂)†.domain H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domainh₂':T₂†.domain = ⊤h₁₂:(T₁ + T₂).HasDenseDomainx:H⊢ x ∈ T₁†.domain ↔ x ∈ (T₁ + T₂)†.domain H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domainh₂':T₂†.domain = ⊤h₁₂:(T₁ + T₂).HasDenseDomainx:H⊢ x ∈ T₁†.domain → x ∈ (T₁ + T₂)†.domainH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domainh₂':T₂†.domain = ⊤h₁₂:(T₁ + T₂).HasDenseDomainx:H⊢ x ∈ (T₁ + T₂)†.domain → x ∈ T₁†.domain H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domainh₂':T₂†.domain = ⊤h₁₂:(T₁ + T₂).HasDenseDomainx:H⊢ x ∈ T₁†.domain → x ∈ (T₁ + T₂)†.domainH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domainh₂':T₂†.domain = ⊤h₁₂:(T₁ + T₂).HasDenseDomainx:H⊢ x ∈ (T₁ + T₂)†.domain → x ∈ T₁†.domain H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domainh₂':T₂†.domain = ⊤h₁₂:(T₁ + T₂).HasDenseDomainx:Hh':x ∈ (T₁ + T₂)†.domain⊢ x ∈ T₁†.domain H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domainh₂':T₂†.domain = ⊤h₁₂:(T₁ + T₂).HasDenseDomainx:Hh':x ∈ T₁†.domain⊢ x ∈ (T₁ + T₂)†.domain H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domainh₂':T₂†.domain = ⊤h₁₂:(T₁ + T₂).HasDenseDomainx:Hh':x ∈ T₁†.domain⊢ ∃ w, ∀ (x_1 : ↥(T₁ + T₂).domain), ⟪w, ↑x_1⟫_ℂ = ⟪x, ↑(T₁ + T₂) x_1⟫_ℂ H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domainh₂':T₂†.domain = ⊤h₁₂:(T₁ + T₂).HasDenseDomainx:Hh':x ∈ T₁†.domain⊢ ∀ (x_1 : ↥(T₁ + T₂).domain), ⟪↑T₁† ⟨x, h'⟩ + ↑T₂† ⟨x, ⋯⟩, ↑x_1⟫_ℂ = ⟪x, ↑(T₁ + T₂) x_1⟫_ℂ H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domainh₂':T₂†.domain = ⊤h₁₂:(T₁ + T₂).HasDenseDomainx:Hh':x ∈ T₁†.domainy:↥(T₁ + T₂).domain⊢ ⟪↑T₁† ⟨x, h'⟩ + ↑T₂† ⟨x, ⋯⟩, ↑y⟫_ℂ = ⟪x, ↑(T₁ + T₂) y⟫_ℂ All goals completed! 🐙 H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domainh₂':T₂†.domain = ⊤h₁₂:(T₁ + T₂).HasDenseDomainx:Hh':x ∈ (T₁ + T₂)†.domain⊢ x ∈ T₁†.domain H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domainh₂':T₂†.domain = ⊤h₁₂:(T₁ + T₂).HasDenseDomainx:Hh':x ∈ (T₁ + T₂)†.domain⊢ ∃ w, ∀ (x_1 : ↥T₁.domain), ⟪w, ↑x_1⟫_ℂ = ⟪x, ↑T₁ x_1⟫_ℂ H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domainh₂':T₂†.domain = ⊤h₁₂:(T₁ + T₂).HasDenseDomainx:Hh':x ∈ (T₁ + T₂)†.domain⊢ ∀ (x_1 : ↥T₁.domain), ⟪↑(T₁ + T₂)† ⟨x, h'⟩ - ↑T₂† ⟨x, ⋯⟩, ↑x_1⟫_ℂ = ⟪x, ↑T₁ x_1⟫_ℂ H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domainh₂':T₂†.domain = ⊤h₁₂:(T₁ + T₂).HasDenseDomainx:Hh':x ∈ (T₁ + T₂)†.domainy:↥T₁.domain⊢ ⟪↑(T₁ + T₂)† ⟨x, h'⟩ - ↑T₂† ⟨x, ⋯⟩, ↑y⟫_ℂ = ⟪x, ↑T₁ y⟫_ℂ All goals completed! 🐙lemma HasDenseDomain.adjoint_sub_continuous [CompleteSpace H] (h₁ : T₁.HasDenseDomain) (h₂ : Continuous T₂) (h : T₁.domain ≤ T₂.domain) : (T₁ - T₂)† = T₁† - T₂† := H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domain⊢ (T₁ - T₂)† = T₁† - T₂† H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh₁:T₁.HasDenseDomainh₂:Continuous ↑T₂h:T₁.domain ≤ T₂.domain⊢ (T₁ + -T₂)† = T₁† + (-T₂)† All goals completed! 🐙

B.5. Unitary conjugation

The conjugation u A u⁻¹ of a partially-defined operator A : H →ₗ.[ℂ] H by a unitary u : H ≃ₗᵢ[ℂ] H', with domain u (A.domain) = u⁻¹ ⁻¹' (A.domain) and action y ↦ u (A (u⁻¹ y)). Since u and u⁻¹ are ℂ-linear, the result is again ℂ-linear.

def unitaryConj : H' →ₗ.[ℂ] H' where domain := A.domain.comap (u.symm.toLinearEquiv : H' →ₗ[ℂ] H) toFun := u.toLinearEquiv.toLinearMap.comp <| A.toFun.comp (((u.symm.toLinearEquiv : H' →ₗ[ℂ] H).comp (A.domain.comap (u.symm.toLinearEquiv : H' →ₗ[ℂ] H)).subtype).codRestrict A.domain fun x => x.2)

Membership in the conjugated domain: x ∈ D(u A u⁻¹) ↔ u⁻¹ x ∈ D(A).

lemma mem_unitaryConj_domain_iff {x : H'} : x ∈ (unitaryConj u A).domain ↔ u.symm x ∈ A.domain := Iff.rfl

The defining formula (u A u⁻¹) x = u (A (u⁻¹ x)).

lemma unitaryConj_apply (x : (unitaryConj u A).domain) : unitaryConj u A x = u (A ⟨u.symm (x : H'), (mem_unitaryConj_domain_iff u A).mp x.2⟩) := rfl

u maps D(A) into D(u A u⁻¹).

lemma map_mem_unitaryConj_domain (y : A.domain) : u (y : H) ∈ (unitaryConj u A).domain := H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'u:H ≃ₗᵢ[ℂ] H'A:H →ₗ.[ℂ] Hy:↥A.domain⊢ u ↑y ∈ (unitaryConj u A).domain All goals completed! 🐙

The action on the image domain: (u A u⁻¹)(u y) = u (A y) for y ∈ D(A).

lemma unitaryConj_apply_map (y : A.domain) : unitaryConj u A ⟨u (y : H), map_mem_unitaryConj_domain u A y⟩ = u (A y) := H:Type u_1inst✝³:NormedAddCommGroup Hinst✝²:InnerProductSpace ℂ HH':Type u_2inst✝¹:NormedAddCommGroup H'inst✝:InnerProductSpace ℂ H'u:H ≃ₗᵢ[ℂ] H'A:H →ₗ.[ℂ] Hy:↥A.domain⊢ ↑(unitaryConj u A) ⟨u ↑y, ⋯⟩ = u (↑A y) All goals completed! 🐙

If A has dense domain, then so does u A u⁻¹: the domain u⁻¹ ⁻¹' (A.domain) is the preimage of a dense set under a homeomorphism.

lemma HasDenseDomain.unitaryConj_dense_domain (hdense : A.HasDenseDomain) : (unitaryConj u A).HasDenseDomain := hdense.preimage u.symm.toHomeomorph.isOpenMap

If A - z is surjective for a scalar z : ℂ, then so is u A u⁻¹ - z.

All goals completed! 🐙

C. Classes of operators

C.1. Unbounded operators

lemma IsUnbounded.hasDenseDomain (h : U.IsUnbounded) : U.HasDenseDomain := h.1lemma IsUnbounded.isClosable (h : U.IsUnbounded) : U.IsClosable := h.2H:Type u_1inst✝⁵:NormedAddCommGroup Hinst✝⁴:InnerProductSpace ℂ HH':Type u_2inst✝³:NormedAddCommGroup H'inst✝²:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝¹:CompleteSpace Hinst✝:CompleteSpace H'h:U.IsUnboundedh_adj:¬U†.HasDenseDomainy:H'hy:y ∉ _root_.closure ↑U†.domainh_ne_bot:U†.domainᗮ = ⊥ → Falsex:H'hx:x ∈ U†.domainᗮhx':x ≠ 0⊢ WithLp.toLp 2 ((0, x).2, -(0, x).1) ∈ (submoduleToLp U†.graph)ᗮ H:Type u_1inst✝⁵:NormedAddCommGroup Hinst✝⁴:InnerProductSpace ℂ HH':Type u_2inst✝³:NormedAddCommGroup H'inst✝²:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝¹:CompleteSpace Hinst✝:CompleteSpace H'h:U.IsUnboundedh_adj:¬U†.HasDenseDomainy✝:H'hy✝:y ∉ _root_.closure ↑U†.domainh_ne_bot:U†.domainᗮ = ⊥ → Falsex:H'hx:x ∈ U†.domainᗮhx':x ≠ 0y:H'Uy:Hhy:WithLp.toLp 2 (y, Uy) ∈ submoduleToLp U†.graph⊢ ⟪WithLp.toLp 2 (y, Uy), WithLp.toLp 2 ((0, x).2, -(0, x).1)⟫_ℂ = 0 H:Type u_1inst✝⁵:NormedAddCommGroup Hinst✝⁴:InnerProductSpace ℂ HH':Type u_2inst✝³:NormedAddCommGroup H'inst✝²:InnerProductSpace ℂ H'U:H →ₗ.[ℂ] H'inst✝¹:CompleteSpace Hinst✝:CompleteSpace H'h:U.IsUnboundedh_adj:¬U†.HasDenseDomainy✝:H'hy✝:y ∉ _root_.closure ↑U†.domainh_ne_bot:U†.domainᗮ = ⊥ → Falsex:H'hx:x ∈ U†.domainᗮhx':x ≠ 0y:H'Uy:Hhy:WithLp.toLp 2 (y, Uy) ∈ submoduleToLp U†.graph⊢ ⟪y, x⟫_ℂ = 0 All goals completed! 🐙lemma IsUnbounded.closure (h : U.IsUnbounded) : U.closure.IsUnbounded := ⟨h.1.closure, h.2.closureIsClosable⟩All goals completed! 🐙All goals completed! 🐙lemma IsUnbounded.le_adjoint_adjoint [CompleteSpace H] [CompleteSpace H'] (h : U.IsUnbounded) : U ≤ U†† := h.adjoint_adjoint_eq_closure ▸ U.le_closurelemma IsUnbounded.isClosed_iff [CompleteSpace H] [CompleteSpace H'] (h : U.IsUnbounded) : U.IsClosed ↔ U†† = U := h.adjoint_adjoint_eq_closure ▸ h.2.isClosed_iff

U†.rangeᗮ = U.closure.ker

lemma IsUnbounded.orthogonal_adjoint_range [CompleteSpace H] [CompleteSpace H'] (h : U.IsUnbounded) : U†.toFun.rangeᗮ = U.closure.toFun.ker.map U.closure.domain.subtype := h.adjoint_adjoint_eq_closure ▸ h.adjoint.hasDenseDomain.orthogonal_range

U.closure.kerᗮ = U†.range

lemma IsUnbounded.orthogonal_closure_ker [CompleteSpace H] [CompleteSpace H'] (h : U.IsUnbounded) : (U.closure.toFun.ker.map U.closure.domain.subtype)ᗮ = U†.toFun.range.closure := h.adjoint_adjoint_eq_closure ▸ h.adjoint.hasDenseDomain.orthogonal_adjoint_ker

C.2. Symmetric operators

The analogue of inner_map_polarization for LinearPMap.

lemma inner_map_polarization (x y : T.domain) : ⟪T y, x⟫_ℂ = (⟪T (x + y), ↑(x + y)⟫_ℂ - ⟪T (x - y), ↑(x - y)⟫_ℂ + I * ⟪T (x + I • y), ↑(x + I • y)⟫_ℂ - I * ⟪T (x - I • y), ↑(x - I • y)⟫_ℂ) / 4 := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hx:↥T.domainy:↥T.domain⊢ ⟪↑T y, ↑x⟫_ℂ = (⟪↑T (x + y), ↑(x + y)⟫_ℂ - ⟪↑T (x - y), ↑(x - y)⟫_ℂ + I * ⟪↑T (x + I • y), ↑(x + I • y)⟫_ℂ - I * ⟪↑T (x - I • y), ↑(x - I • y)⟫_ℂ) / 4 H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hx:↥T.domainy:↥T.domain⊢ ⟪↑T y, ↑x⟫_ℂ = (⟪↑T x, ↑x⟫_ℂ + ⟪↑T y, ↑x⟫_ℂ + (⟪↑T x, ↑y⟫_ℂ + ⟪↑T y, ↑y⟫_ℂ) - (⟪↑T x, ↑x⟫_ℂ - (⟪↑T y, ↑x⟫_ℂ + (⟪↑T x, ↑y⟫_ℂ - ⟪↑T y, ↑y⟫_ℂ))) + (I * ⟪↑T x, ↑x⟫_ℂ + ⟪↑T y, ↑x⟫_ℂ + (-⟪↑T x, ↑y⟫_ℂ + I * ⟪↑T y, ↑y⟫_ℂ)) - (I * ⟪↑T x, ↑x⟫_ℂ + -⟪↑T y, ↑x⟫_ℂ - (-⟪↑T x, ↑y⟫_ℂ + -(I * ⟪↑T y, ↑y⟫_ℂ)))) / 4 All goals completed! 🐙

The analogue of inner_map_polarization' for LinearPMap.

theorem inner_map_polarization' (x y : T.domain) : ⟪T x, y⟫_ℂ = (⟪T (x + y), ↑(x + y)⟫_ℂ - ⟪T (x - y), ↑(x - y)⟫_ℂ - I * ⟪T (x + I • y), ↑(x + I • y)⟫_ℂ + I * ⟪T (x - I • y), ↑(x - I • y)⟫_ℂ) / 4 := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hx:↥T.domainy:↥T.domain⊢ ⟪↑T x, ↑y⟫_ℂ = (⟪↑T (x + y), ↑(x + y)⟫_ℂ - ⟪↑T (x - y), ↑(x - y)⟫_ℂ - I * ⟪↑T (x + I • y), ↑(x + I • y)⟫_ℂ + I * ⟪↑T (x - I • y), ↑(x - I • y)⟫_ℂ) / 4 H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hx:↥T.domainy:↥T.domain⊢ ⟪↑T x, ↑y⟫_ℂ = (⟪↑T x, ↑x⟫_ℂ + ⟪↑T y, ↑x⟫_ℂ + (⟪↑T x, ↑y⟫_ℂ + ⟪↑T y, ↑y⟫_ℂ) - (⟪↑T x, ↑x⟫_ℂ - (⟪↑T y, ↑x⟫_ℂ + (⟪↑T x, ↑y⟫_ℂ - ⟪↑T y, ↑y⟫_ℂ)) + (I * ⟪↑T x, ↑x⟫_ℂ + ⟪↑T y, ↑x⟫_ℂ + (-⟪↑T x, ↑y⟫_ℂ + I * ⟪↑T y, ↑y⟫_ℂ))) + (I * ⟪↑T x, ↑x⟫_ℂ + -⟪↑T y, ↑x⟫_ℂ - (-⟪↑T x, ↑y⟫_ℂ + -(I * ⟪↑T y, ↑y⟫_ℂ)))) / 4 All goals completed! 🐙
H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hh_re:∀ (x : ↥T.domain), (starRingEnd ℂ) ⟪↑T x, ↑x⟫_ℂ = ⟪↑T x, ↑x⟫_ℂx:↥T.domainy:↥T.domain⊢ (⟪↑T (x + y), ↑(x + y)⟫_ℂ - ⟪↑T (x - y), ↑(x - y)⟫_ℂ - I * ⟪↑T (x + I • y), ↑(x + I • y)⟫_ℂ + I * ⟪↑T (x - I • y), ↑(x - I • y)⟫_ℂ) / 4 = (⟪↑T (x + y), ↑(x + y)⟫_ℂ - ⟪↑T (x - y), ↑(x - y)⟫_ℂ + -(I * ⟪↑T (x + I • y), ↑(x + I • y)⟫_ℂ) - -(I * ⟪↑T (x - I • y), ↑(x - I • y)⟫_ℂ)) / 4 All goals completed! 🐙lemma IsSymmetric.isClosable [CompleteSpace H] (h : T.IsSymmetric) (h' : T.HasDenseDomain) : T.IsClosable := isClosable_iff_exists_closed_extension.mpr ⟨T†, adjoint_isClosed h', h.le_adjoint h'⟩lemma IsSymmetric.isUnbounded_iff_hasDenseDomain [CompleteSpace H] (h : T.IsSymmetric) : T.IsUnbounded ↔ T.HasDenseDomain := and_iff_left_of_imp h.isClosablelemma isSymmetric_iff_le_adjoint [CompleteSpace H] (h : T.HasDenseDomain) : T.IsSymmetric ↔ T ≤ T† := H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.HasDenseDomain⊢ T.IsSymmetric ↔ T ≤ T† H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.HasDenseDomainh_le:T ≤ T†x:↥T.domainy:↥T.domain⊢ ⟪↑T x, ↑y⟫_ℂ = ⟪↑x, ↑T y⟫_ℂ H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.HasDenseDomainh_le:T ≤ T†x:↥T.domainy:↥T.domainh_eq:↑T x = ↑T† ⟨↑x, ⋯⟩⊢ ⟪↑T x, ↑y⟫_ℂ = ⟪↑x, ↑T y⟫_ℂ All goals completed! 🐙lemma IsSymmetric.closure_le_adjoint [CompleteSpace H] (h : T.IsSymmetric) (h' : T.HasDenseDomain) : T.closure ≤ T† := H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsSymmetrich':T.HasDenseDomain⊢ T.closure ≤ T† H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsSymmetrich':T.HasDenseDomainh_adj:T†.IsClosed⊢ T.closure ≤ T† All goals completed! 🐙H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsSymmetrich':T.HasDenseDomain⊢ T† = T.closure ↔ T†.domain = T.closure.domain H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsSymmetrich':T.HasDenseDomain⊢ T† = T.closure → T†.domain = T.closure.domainH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsSymmetrich':T.HasDenseDomain⊢ T†.domain = T.closure.domain → T† = T.closure H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsSymmetrich':T.HasDenseDomain⊢ T† = T.closure → T†.domain = T.closure.domainH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsSymmetrich':T.HasDenseDomain⊢ T†.domain = T.closure.domain → T† = T.closure H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsSymmetrich':T.HasDenseDomainh'':T†.domain = T.closure.domain⊢ T† = T.closure H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsSymmetrich':T.HasDenseDomainh'':T† = T.closure⊢ T†.domain = T.closure.domain All goals completed! 🐙 H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsSymmetrich':T.HasDenseDomainh'':T†.domain = T.closure.domain⊢ T† = T.closure All goals completed! 🐙lemma IsSymmetric.isSelfAdjoint_iff [CompleteSpace H] (h : T.IsSymmetric) (h' : T.HasDenseDomain) : IsSelfAdjoint T ↔ T†.domain = T.domain := H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsSymmetrich':T.HasDenseDomain⊢ IsSelfAdjoint T ↔ T†.domain = T.domain H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsSymmetrich':T.HasDenseDomain⊢ IsSelfAdjoint T → T†.domain = T.domainH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsSymmetrich':T.HasDenseDomain⊢ T†.domain = T.domain → IsSelfAdjoint T H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsSymmetrich':T.HasDenseDomain⊢ IsSelfAdjoint T → T†.domain = T.domainH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsSymmetrich':T.HasDenseDomain⊢ T†.domain = T.domain → IsSelfAdjoint T H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsSymmetrich':T.HasDenseDomainh'':T†.domain = T.domain⊢ IsSelfAdjoint T H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsSymmetrich':T.HasDenseDomainh'':IsSelfAdjoint T⊢ T†.domain = T.domain All goals completed! 🐙 H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsSymmetrich':T.HasDenseDomainh'':T†.domain = T.domain⊢ IsSelfAdjoint T All goals completed! 🐙lemma add_adjoint_isSymmetric [CompleteSpace H] (h : T.HasDenseDomain) : (T + T.adjoint).IsSymmetric := H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.HasDenseDomain⊢ (T + T†).IsSymmetric H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.HasDenseDomainx:↥(T + T†).domainy:↥(T + T†).domain⊢ ⟪↑(T + T†) x, ↑y⟫_ℂ = ⟪↑x, ↑(T + T†) y⟫_ℂ H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.HasDenseDomainx:↥(T + T†).domainy:↥(T + T†).domainh₁:⟪↑T† ⟨↑x, ⋯⟩, ↑⟨↑y, ⋯⟩⟫_ℂ = ⟪↑⟨↑x, ⋯⟩, ↑T ⟨↑y, ⋯⟩⟫_ℂ⊢ ⟪↑(T + T†) x, ↑y⟫_ℂ = ⟪↑x, ↑(T + T†) y⟫_ℂ H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.HasDenseDomainx:↥(T + T†).domainy:↥(T + T†).domainh₁:⟪↑T† ⟨↑x, ⋯⟩, ↑⟨↑y, ⋯⟩⟫_ℂ = ⟪↑⟨↑x, ⋯⟩, ↑T ⟨↑y, ⋯⟩⟫_ℂh₂:(starRingEnd ℂ) ⟪↑T† ⟨↑y, ⋯⟩, ↑⟨↑x, ⋯⟩⟫_ℂ = (starRingEnd ℂ) ⟪↑⟨↑y, ⋯⟩, ↑T ⟨↑x, ⋯⟩⟫_ℂ⊢ ⟪↑(T + T†) x, ↑y⟫_ℂ = ⟪↑x, ↑(T + T†) y⟫_ℂ H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.HasDenseDomainx:↥(T + T†).domainy:↥(T + T†).domainh₁:⟪↑T† ⟨↑x, ⋯⟩, ↑⟨↑y, ⋯⟩⟫_ℂ = ⟪↑⟨↑x, ⋯⟩, ↑T ⟨↑y, ⋯⟩⟫_ℂh₂:⟪↑x, ↑T† ⟨↑y, ⋯⟩⟫_ℂ = ⟪↑T ⟨↑x, ⋯⟩, ↑y⟫_ℂ⊢ ⟪↑(T + T†) x, ↑y⟫_ℂ = ⟪↑x, ↑(T + T†) y⟫_ℂ H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.HasDenseDomainx:↥(T + T†).domainy:↥(T + T†).domainh₁:⟪↑T† ⟨↑x, ⋯⟩, ↑⟨↑y, ⋯⟩⟫_ℂ = ⟪↑⟨↑x, ⋯⟩, ↑T ⟨↑y, ⋯⟩⟫_ℂh₂:⟪↑x, ↑T† ⟨↑y, ⋯⟩⟫_ℂ = ⟪↑T ⟨↑x, ⋯⟩, ↑y⟫_ℂ⊢ ⟪↑T ⟨↑x, ⋯⟩, ↑y⟫_ℂ + ⟪↑x, ↑T ⟨↑y, ⋯⟩⟫_ℂ = ⟪↑x, ↑T ⟨↑y, ⋯⟩⟫_ℂ + ⟪↑T ⟨↑x, ⋯⟩, ↑y⟫_ℂ All goals completed! 🐙H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hh:T.IsSymmetricn:ℕih:(T ^ n).IsSymmetricx:↥(T ^ (n + 1)).domainy:↥(T ^ (n + 1)).domainy':↥(T * T ^ n).domain := ⟨↑y, ⋯⟩Tx:↥(T ^ n).domain := ⟨↑T ⟨↑x, ⋯⟩, ⋯⟩Tny:↥T.domain := ⟨↑(T ^ n) ⟨↑y', ⋯⟩, ⋯⟩h_eq:↑T Tny = ↑(T ^ (n + 1)) y⊢ ⟪↑(T ^ (n + 1)) x, ↑y⟫_ℂ = ⟪↑x, ↑(T ^ (n + 1)) y⟫_ℂ All goals completed! 🐙@[aesop safe apply] lemma IsSymmetric.neg (h : T.IsSymmetric) : (-T).IsSymmetric := fun x y ↦ H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hh:T.IsSymmetricx:↥(-T).domainy:↥(-T).domain⊢ ⟪↑(-T) x, ↑y⟫_ℂ = ⟪↑x, ↑(-T) y⟫_ℂ All goals completed! 🐙@[aesop safe apply] lemma IsSymmetric.add (h₁ : T₁.IsSymmetric) (h₂ : T₂.IsSymmetric) : (T₁ + T₂).IsSymmetric := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hh₁:T₁.IsSymmetrich₂:T₂.IsSymmetric⊢ (T₁ + T₂).IsSymmetric H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hh₁:T₁.IsSymmetrich₂:T₂.IsSymmetricx:↥(T₁ + T₂).domainy:↥(T₁ + T₂).domain⊢ ⟪↑(T₁ + T₂) x, ↑y⟫_ℂ = ⟪↑x, ↑(T₁ + T₂) y⟫_ℂ All goals completed! 🐙@[aesop safe apply] lemma IsSymmetric.sub (h₁ : T₁.IsSymmetric) (h₂ : T₂.IsSymmetric) : (T₁ - T₂).IsSymmetric := sub_eq_add_neg T₁ T₂ ▸ h₁.add h₂.neg@[aesop safe apply] lemma IsSymmetric.smul (h : T.IsSymmetric) {c : ℂ} (hc : conj c = c) : (c • T).IsSymmetric := fun x y ↦ H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hh:T.IsSymmetricc:ℂhc:(starRingEnd ℂ) c = cx:↥(c • T).domainy:↥(c • T).domain⊢ ⟪↑(c • T) x, ↑y⟫_ℂ = ⟪↑x, ↑(c • T) y⟫_ℂ All goals completed! 🐙@[aesop safe apply] lemma IsSymmetric.real_smul (h : T.IsSymmetric) (r : ℝ) : (r • T).IsSymmetric := h.smul (conj_ofReal r)@[aesop safe apply] lemma IsSymmetric.sum (h : ∀ a, (S a).IsSymmetric) : (sum S).IsSymmetric := H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hα:Type u_4inst✝:Fintype αS:α → H →ₗ.[ℂ] Hh:∀ (a : α), (S a).IsSymmetric⊢ (LinearPMap.sum S).IsSymmetric H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ Hα:Type u_4inst✝:Fintype αS:α → H →ₗ.[ℂ] Hh:∀ (a : α), (S a).IsSymmetricx:↥(LinearPMap.sum S).domainy:↥(LinearPMap.sum S).domain⊢ ⟪↑(LinearPMap.sum S) x, ↑y⟫_ℂ = ⟪↑x, ↑(LinearPMap.sum S) y⟫_ℂ All goals completed! 🐙lemma IsSymmetric.of_le (h₁ : T₁.IsSymmetric) (h_le : T₂ ≤ T₁) : T₂.IsSymmetric := H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hh₁:T₁.IsSymmetrich_le:T₂ ≤ T₁⊢ T₂.IsSymmetric H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hh₁:T₁.IsSymmetrich_le:T₂ ≤ T₁x:↥T₂.domainy:↥T₂.domain⊢ ⟪↑T₂ x, ↑y⟫_ℂ = ⟪↑x, ↑T₂ y⟫_ℂ H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hh₁:T₁.IsSymmetrich_le:T₂ ≤ T₁x:↥T₂.domainy:↥T₂.domainhx:↑T₂ x = ↑T₁ ⟨↑x, ⋯⟩⊢ ⟪↑T₂ x, ↑y⟫_ℂ = ⟪↑x, ↑T₂ y⟫_ℂ H:Type u_1inst✝¹:NormedAddCommGroup Hinst✝:InnerProductSpace ℂ HT₁:H →ₗ.[ℂ] HT₂:H →ₗ.[ℂ] Hh₁:T₁.IsSymmetrich_le:T₂ ≤ T₁x:↥T₂.domainy:↥T₂.domainhx:↑T₂ x = ↑T₁ ⟨↑x, ⋯⟩hy:↑T₂ y = ↑T₁ ⟨↑y, ⋯⟩⊢ ⟪↑T₂ x, ↑y⟫_ℂ = ⟪↑x, ↑T₂ y⟫_ℂ All goals completed! 🐙

The closure of a symmetric densely-defined operator is symmetric: T†† is a symmetric closed extension of T, so it extends T.closure, whose symmetry then descends.

lemma IsSymmetric.closure [CompleteSpace H] (hsym : T.IsSymmetric) (hdense : T.HasDenseDomain) : T.closure.IsSymmetric := H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hhsym:T.IsSymmetrichdense:T.HasDenseDomain⊢ T.closure.IsSymmetric H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hhsym:T.IsSymmetrichdense:T.HasDenseDomainhle:T ≤ T†⊢ T.closure.IsSymmetric H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hhsym:T.IsSymmetrichdense:T.HasDenseDomainhle:T ≤ T†hadj_dense:T†.HasDenseDomain⊢ T.closure.IsSymmetric H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hhsym:T.IsSymmetrichdense:T.HasDenseDomainhle:T ≤ T†hadj_dense:T†.HasDenseDomainhT_le:T ≤ T††⊢ T.closure.IsSymmetric H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hhsym:T.IsSymmetrichdense:T.HasDenseDomainhle:T ≤ T†hadj_dense:T†.HasDenseDomainhT_le:T ≤ T††hc:T††.IsClosed⊢ T.closure.IsSymmetric H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hhsym:T.IsSymmetrichdense:T.HasDenseDomainhle:T ≤ T†hadj_dense:T†.HasDenseDomainhT_le:T ≤ T††hc:T††.IsClosedh1:T††.IsSymmetric⊢ T.closure.IsSymmetric All goals completed! 🐙

A LinearPMap constructed from a symmetric LinearMap with dense domain is an unbounded operator.

lemma isUnbounded_of_dense_of_isSymmetric [CompleteSpace H] {E : Submodule ℂ H} (hE : Dense (E : Set H)) {f : E →ₗ[ℂ] H} (h : ∀ x y : E, ⟪f x, ↑y⟫_ℂ = ⟪↑x, f y⟫_ℂ) : (mk E f).IsUnbounded := ⟨hE, IsSymmetric.isClosable h hE⟩

Variant of of_dense_of_isSymmetric for an endomorphism satisfying LinearMap.IsSymmetric.

lemma isUnbounded_of_dense_of_isSymmetric' [CompleteSpace H] {E : Submodule ℂ H} (hE : Dense (E : Set H)) {f : E →ₗ[ℂ] E} (h : f.IsSymmetric) : (mk E (E.subtype ∘ₗ f)).IsUnbounded := ⟨hE, IsSymmetric.isClosable h hE⟩

C.3. Self-adjoint operators

H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:IsSelfAdjoint T⊢ T.IsFormalAdjoint T nth_rw 1 [H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:IsSelfAdjoint T⊢ (star T).IsFormalAdjoint TH:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:IsSelfAdjoint T⊢ (star T).IsFormalAdjoint T All goals completed! 🐙lemma IsSelfAdjoint.isClosed [CompleteSpace H] (h : IsSelfAdjoint T) : T.IsClosed := h ▸ adjoint_isClosed h.dense_domainlemma IsSelfAdjoint.isClosable [CompleteSpace H] (h : IsSelfAdjoint T) : T.IsClosable := (isClosed h).isClosablelemma IsSelfAdjoint.isUnbounded [CompleteSpace H] (h : IsSelfAdjoint T) : T.IsUnbounded := ⟨h.dense_domain, isClosable h⟩lemma IsSelfAdjoint.isEssentiallySelfAdjoint [CompleteSpace H] (h : IsSelfAdjoint T) : T.IsEssentiallySelfAdjoint := isEssentiallySelfAdjoint_def.mpr (h.isClosed.closure_eq.symm ▸ h)@[aesop safe apply] lemma IsSelfAdjoint.adjoint [CompleteSpace H] (h : IsSelfAdjoint T) : IsSelfAdjoint T† := H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:IsSelfAdjoint T⊢ IsSelfAdjoint T† H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T† = T⊢ IsSelfAdjoint T† All goals completed! 🐙All goals completed! 🐙@[aesop safe apply] lemma IsSelfAdjoint.real_smul [CompleteSpace H] (h : IsSelfAdjoint T) {r : ℝ} (hr : r ≠ 0) : IsSelfAdjoint (r • T) := smul h (ofReal_ne_zero.mpr hr) (conj_ofReal r)@[aesop safe apply] lemma IsSelfAdjoint.neg [CompleteSpace H] (h : IsSelfAdjoint T) : IsSelfAdjoint (-T) := neg_eq_neg_one_smul T ▸ smul h (H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:IsSelfAdjoint T⊢ -1 ≠ 0 All goals completed! 🐙) (H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:IsSelfAdjoint T⊢ (starRingEnd ℂ) (-1) = -1 All goals completed! 🐙)

Self-adjointness from surjectivity of T ± i: a symmetric, densely-defined operator T for which T + I • 1 and T - I • 1 both have full range is self-adjoint.

H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hhsym:T.IsSymmetrichdense:T.HasDenseDomainhadd:(T + I • 1).toFun.range = ⊤hsub:(T - I • 1).toFun.range = ⊤hplus:∀ (φ : H), ∃ ψ, ↑T ψ + I • ↑ψ = φhminus:∀ (φ : H), ∃ ψ, ↑T ψ - I • ↑ψ = φhle:T ≤ T†w:Hhw:w ∈ T†.domainW:↥T†.domain := ⟨w, hw⟩x:↥T.domainhx:↑T x - I • ↑x = ↑T† W - I • ↑WX:↥T†.domain := ⟨↑x, ⋯⟩hX:X = ⟨↑x, ⋯⟩hxeq:↑T† X = ↑T xhdiff:↑T† (W - X) = I • (↑W - ↑X)hker:∀ (w : ↥T†.domain), ↑T† w = I • ↑w → ↑w = 0⊢ w ∈ T†.eqLocus T H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hhsym:T.IsSymmetrichdense:T.HasDenseDomainhadd:(T + I • 1).toFun.range = ⊤hsub:(T - I • 1).toFun.range = ⊤hplus:∀ (φ : H), ∃ ψ, ↑T ψ + I • ↑ψ = φhminus:∀ (φ : H), ∃ ψ, ↑T ψ - I • ↑ψ = φhle:T ≤ T†x:↥T.domainX:↥T†.domain := ⟨↑x, ⋯⟩hX:X = ⟨↑x, ⋯⟩hxeq:↑T† X = ↑T xhker:∀ (w : ↥T†.domain), ↑T† w = I • ↑w → ↑w = 0hw:↑x ∈ T†.domainW:↥T†.domain := ⟨↑x, hw⟩hx:↑T x - I • ↑x = ↑T† W - I • ↑Whdiff:↑T† (W - X) = I • (↑W - ↑X)⊢ ↑x ∈ T†.eqLocus T All goals completed! 🐙

C.4. Essentially self-adjoint operators

lemma IsEssentiallySelfAdjoint.hasDenseDomain [CompleteSpace H] (h : T.IsEssentiallySelfAdjoint) : T.HasDenseDomain := hasDenseDomain_iff_closure_hasDenseDomain.mpr h.dense_domainlemma IsEssentiallySelfAdjoint.isSymmetric [CompleteSpace H] (h : T.IsEssentiallySelfAdjoint) : T.IsSymmetric := (IsSelfAdjoint.isSymmetric h).of_le T.le_closurelemma IsEssentiallySelfAdjoint.isClosable [CompleteSpace H] (h : T.IsEssentiallySelfAdjoint) : T.IsClosable := h.isSymmetric.isClosable h.hasDenseDomainlemma IsEssentiallySelfAdjoint.isUnbounded [CompleteSpace H] (h : T.IsEssentiallySelfAdjoint) : T.IsUnbounded := h.isSymmetric.isUnbounded_iff_hasDenseDomain.mpr h.hasDenseDomain

The closure is the unique self-adjoint extension of an essentially self-adjoint operator.

lemma IsEssentiallySelfAdjoint.unique_self_adjoint_extension [CompleteSpace H] (h : T.IsEssentiallySelfAdjoint) {T₂ : H →ₗ.[ℂ] H} (h_le : T ≤ T₂) (h₂ : IsSelfAdjoint T₂) : T₂ = T.closure := H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsEssentiallySelfAdjointT₂:H →ₗ.[ℂ] Hh_le:T ≤ T₂h₂:IsSelfAdjoint T₂⊢ T₂ = T.closure H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsEssentiallySelfAdjointT₂:H →ₗ.[ℂ] Hh_le:T ≤ T₂h₂:IsSelfAdjoint T₂h_cl:T₂.IsClosed⊢ T₂ = T.closure H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsEssentiallySelfAdjointT₂:H →ₗ.[ℂ] Hh_le:T ≤ T₂h₂:IsSelfAdjoint T₂h_cl:T₂.IsClosedh_le':T.closure ≤ T₂⊢ T₂ = T.closure All goals completed! 🐙
@[aesop safe apply] lemma IsEssentiallySelfAdjoint.smul [CompleteSpace H] (h : T.IsEssentiallySelfAdjoint) {c : ℂ} (hc : c ≠ 0) (hc' : conj c = c) : (c • T).IsEssentiallySelfAdjoint := H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsEssentiallySelfAdjointc:ℂhc:c ≠ 0hc':(starRingEnd ℂ) c = c⊢ (c • T).IsEssentiallySelfAdjoint All goals completed! 🐙@[aesop safe apply] lemma IsEssentiallySelfAdjoint.real_smul [CompleteSpace H] (h : T.IsEssentiallySelfAdjoint) {r : ℝ} (hr : r ≠ 0) : (r • T).IsEssentiallySelfAdjoint := h.smul (ofReal_ne_zero.mpr hr) (conj_ofReal r)@[aesop safe apply] lemma IsEssentiallySelfAdjoint.neg [CompleteSpace H] (h : T.IsEssentiallySelfAdjoint) : (-T).IsEssentiallySelfAdjoint := neg_eq_neg_one_smul T ▸ h.smul (H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsEssentiallySelfAdjoint⊢ -1 ≠ 0 All goals completed! 🐙) (H:Type u_1inst✝²:NormedAddCommGroup Hinst✝¹:InnerProductSpace ℂ HT:H →ₗ.[ℂ] Hinst✝:CompleteSpace Hh:T.IsEssentiallySelfAdjoint⊢ (starRingEnd ℂ) (-1) = -1 All goals completed! 🐙)