SigmaLayer/BasisMeasurement: the record layer for an arbitrary observable (MD-1)

Category: 7-SigmaLayer (the record layer — arbitrary measurement context).

The record layer of SigmaLayer/Measurement.lean is stated in the computational basis (bornRate ψ i = ‖ψ i‖²). This file generalises it to an arbitrary observable — any orthonormal basis b : OrthonormalBasis (Fin n) ℂ E of a complex inner-product space E — with the outcome probability the standard Born weight ‖⟨bᵢ, ψ⟩‖². The generalisation is a change of basis: measuring ψ in context b is measuring the coordinate representation b.repr ψ in the computational basis, so every record-layer theorem transports along the isometry b.repr.

• bornRateBasis / bornRateBasis_eq_inner_sq — the Born rate of outcome i in context b is ‖⟨bᵢ, ψ⟩‖²;
• sum_bornRateBasis_unit — the rates form a probability vector on a unit state;
• bornMeasurementBasis / bornMeasurementBasis_prob — the record-layer measurement in context b, with outcome probability ‖⟨bᵢ, ψ⟩‖².

Foundational-triple, no sorry.

References

SigmaLayer/Measurement.lean (the computational-basis record layer, bornMeasurement); Mathlib OrthonormalBasis.repr (the isometry to EuclideanSpace).

noncomputable def CSD.RecordLayer.bornRateBasis {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (b : OrthonormalBasis (Fin n) ℂ E) (ψ : E) (i : Fin n) : ℝ

The Born rate for a general observable (orthonormal basis b): the squared overlap ‖⟨bᵢ, ψ⟩‖², realised as the computational-basis rate of the coordinate representation b.repr ψ.

Equations

• CSD.RecordLayer.bornRateBasis b ψ i = CSD.RecordLayer.bornRate (b.repr ψ) i

theorem CSD.RecordLayer.bornRateBasis_eq_inner_sq {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (b : OrthonormalBasis (Fin n) ℂ E) (ψ : E) (i : Fin n) : bornRateBasis b ψ i = ‖inner ℂ (b i) ψ‖ ^ 2

The general Born rate is the standard squared overlap ‖⟨bᵢ, ψ⟩‖².

theorem CSD.RecordLayer.norm_repr_eq {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (b : OrthonormalBasis (Fin n) ℂ E) (ψ : E) : ‖b.repr ψ‖ = ‖ψ‖

The coordinate representation is norm-preserving (b.repr is an isometry).

theorem CSD.RecordLayer.sum_bornRateBasis_unit {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (b : OrthonormalBasis (Fin n) ℂ E) (ψ : E) (hψ : ‖ψ‖ = 1) : ∑ i : Fin n, bornRateBasis b ψ i = 1

The general Born rates form a probability vector on a unit state.

noncomputable def CSD.RecordLayer.bornMeasurementBasis {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (b : OrthonormalBasis (Fin n) ℂ E) (ψ : E) (t : SigmaLayer.OnticTime) : Measurement n

The record-layer measurement in a general observable context b: the computational-basis Born measurement of the coordinate representation b.repr ψ.

Equations

• CSD.RecordLayer.bornMeasurementBasis b ψ t = CSD.RecordLayer.Measurement.bornMeasurement (b.repr ψ) t

theorem CSD.RecordLayer.bornMeasurementBasis_prob {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (b : OrthonormalBasis (Fin n) ℂ E) (ψ : E) (hψ : ‖ψ‖ = 1) (i : Fin n) (t : SigmaLayer.OnticTime) : (bornMeasurementBasis b ψ t).prob i = ENNReal.ofReal (‖inner ℂ (b i) ψ‖ ^ 2)

The basins set the probabilities = Born, in any observable context. The outcome-i probability of the measurement in context b is exactly ‖⟨bᵢ, ψ⟩‖².