Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 8 research declarations. Search 10,000 more complete Mathlib declarations.
8 results
Clear filtersQuantumMechanics.SpaceDHilbertSpace.mulOperator_add_eq
Plain-language statement
(𝓜 μ g).domain = ⊤ is a sufficient condition to ensure equality in mulOperator_add_ge.
Source project: Physlib
Person-level attribution pending.
QuantumMechanics.SpaceDHilbertSpace.mulOperator_add_ge
Plain-language statement
𝓜 μ (f + g) extends 𝓜 μ f + 𝓜 μ g. In general the domains do not match: ψ ∈ (𝓜 μ f + 𝓜 μ g).domain amounts to MemHS (f • ψ) μ and MemHS (g • ψ) μ whereas ψ ∈ (𝓜 μ (f + g)).domain is equivalent to the weaker condition MemHS ((f + g) • ψ) μ. See mulOperator_add_eq for a sufficient condition to ensure equality.
Source project: Physlib
Person-level attribution pending.
QuantumMechanics.SpaceDHilbertSpace.mulOperator_adjoint_eq_conj
Plain-language statement
The adjoint of a multiplication operator is again a multiplication operator.
Source project: Physlib
Person-level attribution pending.
QuantumMechanics.SpaceDHilbertSpace.mulOperator_compRestricted_eq
Plain-language statement
(𝓜 μ g).domain = ⊤ is a sufficient condition to ensure equality in mulOperator_compRestricted_ge.
Source project: Physlib
Person-level attribution pending.
QuantumMechanics.SpaceDHilbertSpace.mulOperator_compRestricted_le
Plain-language statement
𝓜 μ (f • g) extends 𝓜 μ f * 𝓜 μ g. In general the domains do not match: ψ ∈ (𝓜 μ f * 𝓜 μ g).domain amounts to MemHS (g • ψ) μ and MemHS (f • g • ψ) μ whereas ψ ∈ (𝓜 μ (f • g)).domain only requires MemHS (f • g • ψ) μ. See mulOperator_compRestricted_eq for a sufficient condition to ensure equality.
Source project: Physlib
Person-level attribution pending.
QuantumMechanics.SpaceDHilbertSpace.mulOperator_domain_ge_of_hasTemperateGrowth
Plain-language statement
The multiplication operator corresponding to a function of temperate growth contains all Schwartz maps in its domain.
Source project: Physlib
Person-level attribution pending.