No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
46structure QuantumState (n : ℕ) where
47 amplitudes : Fin n → ℂ
48 normalized : (Finset.univ.sum fun i => Complex.normSq (amplitudes i)) = 1
49
50/-- A unitary operator preserves inner products. -/
used by (24)
From the project-wide theorem graph. These declarations reference this one in their body.
-
born_rule_jcost_connection
in IndisputableMonolith.Foundation.QuantumLedger
decl_use
-
expectedCost
in IndisputableMonolith.Foundation.QuantumLedger
decl_use
-
probability
in IndisputableMonolith.Foundation.QuantumLedger
decl_use
-
prob_nonneg
in IndisputableMonolith.Foundation.QuantumLedger
decl_use
-
prob_sum_one
in IndisputableMonolith.Foundation.QuantumLedger
decl_use
-
QuantumState
in IndisputableMonolith.Foundation.QuantumLedger
decl_use
-
CloningMachine
in IndisputableMonolith.Information.NoCloning
decl_use
-
innerProduct
in IndisputableMonolith.Information.NoCloning
decl_use
-
inner_product_self
in IndisputableMonolith.Information.NoCloning
decl_use
-
QuantumState
in IndisputableMonolith.Information.NoCloning
decl_use
-
QuantumState
in IndisputableMonolith.QFT.PauliExclusion
decl_use
-
unitary_preserves_norm
in IndisputableMonolith.QFT.Unitarity
decl_use
-
born_rule_nonneg
in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse
decl_use
-
born_rule_normalized
in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse
decl_use
-
cost_probability_relation
in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse
decl_use
-
filter_map_weight_sum
in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse
decl_use
-
isDefinite
in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse
decl_use
-
isSuperposition
in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse
decl_use
-
measurement_postulate_derived
in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse
decl_use
-
measurementProbability
in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse
decl_use
-
outcomeCost
in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse
decl_use
-
probability_equals_weight
in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse
decl_use
-
QuantumState
in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse
decl_use
-
stateToLedger
in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse
decl_use
depends on (8)
Lean names referenced from this declaration's body.
-
A
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
QuantumState
in IndisputableMonolith.Foundation.QuantumLedger
decl_use
-
QuantumState
in IndisputableMonolith.Information.NoCloning
decl_use
-
A
in IndisputableMonolith.Masses.Anchor
decl_use
-
A
in IndisputableMonolith.Modal.Actualization
decl_use
-
normalized
in IndisputableMonolith.NavierStokes.RunningMaxNormalization
decl_use
-
QuantumState
in IndisputableMonolith.QFT.PauliExclusion
decl_use
-
QuantumState
in IndisputableMonolith.Quantum.Measurement.WavefunctionCollapse
decl_use