feat(QM): AddZeroClass for UnboundedOperator

[gloges]

• Defines zero as the zero map with full domain.

• Defines addition of unbounded operators, using two junk values:

  • When D(U1) ∩ D(U2) is not dense, use the zero with full domain.
  • When D(U1) ∩ D(U2) is dense but U1 + U2 is not closable, use the zero map on D(U1) ∩ D(U2).

  This second junk value will be needed so that smul distributes over addition in all cases. It ensures that c • (U1 + U2) = c • U1 + c • U2 holds for (c : ℂ) = 0 when D(U1) ∩ D(U2) is dense, since the RHS is the zero map on D(U1) ∩ D(U2) regardless of whether U1 + U2 is closable or not.

• add_assoc proves associativity holds when no junk values are encountered

(cf. #957, #978)

[gloges]

t-quantum-mechanics

[gloges]

RFC

[jstoobysmith]

Looks mainly good to me. Couple of comments

[jstoobysmith]

awaiting-author

[gloges]

I realized that add_assoc could be generalized slightly; addition is associative when neither of the intermediate additions U1 + U2 and U2 + U3 is a junk value. The hypotheses should now be easier to supply, as they concern the two pairs separately.

[gloges]

-awaiting-author

[jstoobysmith]

Approved - many thanks. Will merge shortly
ready-to-merge

[jstoobysmith]

ready-to-merge