Documentation

CsdLean4.LF2.EffectFn

Projective effect function (the quadratic-form representation layer) #

Category: 3-Local (pre-LF4 plan Phase 2 — the representation-layer object: given a unit-vector representative map rep : P → EuclideanSpace ℂ (Fin N) from an abstract projective space P and a finite-dimensional Effect, effectProjFn rep E p returns the real number that, integrated against π_*μprep, gives the probability of outcome E under a preparation pushing forward to a measure on P.

Honest scope (F-02, external review 2026-08-06) #

effectProjFn is the Born quadratic form by definition: it is Re(v† E v) at the representative v = rep p, and for rank-1 effects it evaluates pointwise to ‖⟨rep p, φ⟩‖² (effectProjFn_rankOne). So the LF2 theorems that integrate it are representation/consistency statements — they exhibit the operational probability as an integral of an already-quadratic integrand, and (vs the Busch route) they avoid the trace-form characterisation step, not the quadratic form itself. The genuine Born-from-volume content — computing the Fubini–Study measure of a separately specified region and finding the Born weight — lives in LF4 (MomentBornN, BornRegionUncond, born_frequency_convergence_N_uncond); do not cite this layer for it. The trace-form / density-operator description is a reformulation, available via traceForm + born_quadratic.

source
noncomputable def CSD.LF2.effectProjFn {N : ℕ} {P : Type u_1} (rep : P → EuclideanSpace ℂ (Fin N)) (E : Effect N) :
P → ℝ

Projective effect function (quadratic form). Given a unit-vector representative map rep : P → EuclideanSpace ℂ (Fin N) and a finite-dimensional Effect E, returns the real number RCLike.re (star v ⬝ᵥ E.M *ᵥ v) where v = (rep p).ofLp is the underlying function. The probability assignment from a preparation measure μprep is then ∫ p, effectProjFn rep E p ∂(π_*μprep).

Equations
Instances For
    source
    theorem CSD.LF2.effectProjFn_rankOne {N : ℕ} {P : Type u_1} (rep : P → EuclideanSpace ℂ (Fin N)) (φ : EuclideanSpace ℂ (Fin N)) (hφ : ‖φ‖ = 1) (p : P) :
    effectProjFn rep (rankOneEffect φ hφ) p = ‖inner ℂ (rep p) φ‖ ^ 2

    For the rank-1 effect |φ⟩⟨φ|, the projective effect function evaluates pointwise to ‖⟨rep p, φ⟩‖². This is the standard Born quadratic form at the representative vector.

    source
    @[simp]
    theorem CSD.LF2.effectProjFn_zero {N : ℕ} {P : Type u_1} (rep : P → EuclideanSpace ℂ (Fin N)) :
    effectProjFn rep Effect.zero = 0

    The zero effect's projective effect function is identically zero.

    source
    theorem CSD.LF2.effectProjFn_one {N : ℕ} {P : Type u_1} (rep : P → EuclideanSpace ℂ (Fin N)) (p : P) :
    effectProjFn rep Effect.one p = ‖rep p‖ ^ 2

    The identity effect's projective effect function is ‖rep p‖² pointwise. For unit-norm rep p this is 1.

    source
    theorem CSD.LF2.effectProjFn_add {N : ℕ} {P : Type u_1} (rep : P → EuclideanSpace ℂ (Fin N)) (E F : Effect N) (hLe : (1 - (E.M + F.M)).PosSemidef) (p : P) :
    effectProjFn rep (E.add F hLe) p = effectProjFn rep E p + effectProjFn rep F p

    The projective effect function is additive in the effect argument (when the sum is itself an effect).

    Bounds #

    The projective effect function is non-negative (from E.nonneg) and bounded by 1 for unit-norm rep p (from E.le_one).

    source
    theorem CSD.LF2.effectProjFn_nonneg {N : ℕ} {P : Type u_1} (rep : P → EuclideanSpace ℂ (Fin N)) (E : Effect N) (p : P) :
    0 ≤ effectProjFn rep E p

    The projective effect function is pointwise non-negative. Routes through Matrix.PosSemidef.re_dotProduct_nonneg applied to E.M's PSD content.

    source
    theorem CSD.LF2.effectProjFn_le_norm_sq {N : ℕ} {P : Type u_1} (rep : P → EuclideanSpace ℂ (Fin N)) (E : Effect N) (p : P) :
    effectProjFn rep E p ≤ ‖rep p‖ ^ 2

    The projective effect function is pointwise bounded by ‖rep p‖². For unit-norm rep p this is 1. Routes through E.le_one applied via the same re_dotProduct_nonneg mechanism on 1 - E.M.

    source
    theorem CSD.LF2.effectProjFn_le_one {N : ℕ} {P : Type u_1} (rep : P → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : P), ‖rep p‖ = 1) (E : Effect N) (p : P) :
    effectProjFn rep E p ≤ 1

    Specialisation of effectProjFn_le_norm_sq to unit-norm rep p.

    Measurability #

    effectProjFn rep E is measurable when rep is measurable. The function decomposes as rep composed with a continuous map EuclideanSpace ℂ (Fin N) → ℝ (a real quadratic form). On finite-dim normed spaces all polynomial expressions are continuous.

    source
    theorem CSD.LF2.effectProjFn_measurable {N : ℕ} {Q : Type u_2} [MeasurableSpace Q] (rep : Q → EuclideanSpace ℂ (Fin N)) (hrep_meas : Measurable rep) (E : Effect N) :
    Measurable (effectProjFn rep E)

    The projective effect function is measurable in its argument when rep is measurable.

    source
    theorem CSD.LF2.effectProjFn_integrable {N : ℕ} {Q : Type u_2} [MeasurableSpace Q] (rep : Q → EuclideanSpace ℂ (Fin N)) (hrep_unit : ∀ (p : Q), ‖rep p‖ = 1) (hrep_meas : Measurable rep) (E : Effect N) (μ : MeasureTheory.Measure Q) [MeasureTheory.IsFiniteMeasure μ] :
    MeasureTheory.Integrable (effectProjFn rep E) μ

    The projective effect function is integrable against any finite measure when rep is measurable and unit-norm. Routes via Integrable.of_bound: measurable + pointwise bounded by 1 (via effectProjFn_le_one) + finite measure ⟹ integrable.