A measurable unit section of the ray map

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

The ray map mk : {v // v ≠ 0} → ℙ 𝕜 (EuclideanSpace 𝕜 ι) has no continuous section (the tautological bundle is non-trivial), but it has a measurable one, and a canonical one: send a ray to its unit-norm representative whose first non-zero coordinate is real and positive.

• firstIndex — the first non-zero coordinate of a non-zero vector (ι linearly ordered);
• unitScalar, unitRep — the normalising scalar conj(vᵢ)/|vᵢ| · ‖v‖⁻¹ and the representative it produces; unitRep_smul is scale-invariance, so unitRep descends to the quotient;
• unitSection — the section ℙ 𝕜 (EuclideanSpace 𝕜 ι) → EuclideanSpace 𝕜 ι, with norm_unitSection : ‖unitSection p‖ = 1 and mk_unitSection : mk (unitSection p) = p;
• ★ measurable_unitSection — it is Borel measurable: unitRep is the finite sum over i of the candidate i (a measurable function of v) restricted to the measurable set "first index = i" (measurableSet_firstIndex_eq), and Projectivization.lift_measurable descends it.

This discharges the hypothesis every preparation-level construction of the corpus takes (a unit-norm measurable rep with mk (rep p) = p): Projectivization.unitSection is such a rep, for every finite-dimensional EuclideanSpace over ℝ or ℂ.

References: CsdLean4/Mathlib/LinearAlgebra/Projectivization/MeasureSpace.lean (lift_measurable); CsdLean4/LF2/FlowChannel.lean (isUnitaryLift_unitSection, the consumer); specs/qit-chain-scoping.md (W6″).

The first non-zero coordinate

def Projectivization.coordSupport {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] (v : EuclideanSpace 𝕜 ι) : Finset ι

The support of a vector, as a finset of coordinates.

Equations

• Projectivization.coordSupport v = {i : ι | v.ofLp i ≠ 0}

theorem Projectivization.mem_coordSupport {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] {v : EuclideanSpace 𝕜 ι} {i : ι} : i ∈ coordSupport v ↔ v.ofLp i ≠ 0

theorem Projectivization.coordSupport_nonempty {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] {v : EuclideanSpace 𝕜 ι} (hv : v ≠ 0) : (coordSupport v).Nonempty

theorem Projectivization.coordSupport_smul {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] {v : EuclideanSpace 𝕜 ι} {t : 𝕜} (ht : t ≠ 0) : coordSupport (t • v) = coordSupport v

noncomputable def Projectivization.firstIndex {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (v : { v : EuclideanSpace 𝕜 ι // v ≠ 0 }) : ι

The first non-zero coordinate of a non-zero vector.

Equations

• Projectivization.firstIndex v = (Projectivization.coordSupport ↑v).min' ⋯

theorem Projectivization.apply_firstIndex_ne_zero {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (v : { v : EuclideanSpace 𝕜 ι // v ≠ 0 }) : (↑v).ofLp (firstIndex v) ≠ 0

theorem Projectivization.firstIndex_le {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (v : { v : EuclideanSpace 𝕜 ι // v ≠ 0 }) {i : ι} (hi : (↑v).ofLp i ≠ 0) : firstIndex v ≤ i

theorem Projectivization.apply_eq_zero_of_lt_firstIndex {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (v : { v : EuclideanSpace 𝕜 ι // v ≠ 0 }) {j : ι} (hj : j < firstIndex v) : (↑v).ofLp j = 0

theorem Projectivization.firstIndex_eq_iff {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (v : { v : EuclideanSpace 𝕜 ι // v ≠ 0 }) (i : ι) : firstIndex v = i ↔ (↑v).ofLp i ≠ 0 ∧ ∀ j < i, (↑v).ofLp j = 0

theorem Projectivization.firstIndex_smul {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (v : { v : EuclideanSpace 𝕜 ι // v ≠ 0 }) {t : 𝕜} (ht : t ≠ 0) : firstIndex ⟨t • ↑v, ⋯⟩ = firstIndex v

The unit section

noncomputable def Projectivization.unitScalar {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (v : { v : EuclideanSpace 𝕜 ι // v ≠ 0 }) : 𝕜

The normalising scalar of a non-zero vector: the conjugate phase of its first non-zero coordinate, over the norm.

Equations

• Projectivization.unitScalar v = (starRingEnd 𝕜) ((↑v).ofLp (Projectivization.firstIndex v)) / ↑‖(↑v).ofLp (Projectivization.firstIndex v)‖ * ↑‖↑v‖⁻¹

theorem Projectivization.norm_unitScalar {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (v : { v : EuclideanSpace 𝕜 ι // v ≠ 0 }) : ‖unitScalar v‖ * ‖↑v‖ = 1

theorem Projectivization.unitScalar_ne_zero {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (v : { v : EuclideanSpace 𝕜 ι // v ≠ 0 }) : unitScalar v ≠ 0

noncomputable def Projectivization.unitRep {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (v : { v : EuclideanSpace 𝕜 ι // v ≠ 0 }) : EuclideanSpace 𝕜 ι

The unit representative of a non-zero vector: normalised, with its first non-zero coordinate real and positive.

Equations

• Projectivization.unitRep v = Projectivization.unitScalar v • ↑v

theorem Projectivization.norm_unitRep {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (v : { v : EuclideanSpace 𝕜 ι // v ≠ 0 }) : ‖unitRep v‖ = 1

theorem Projectivization.unitRep_ne_zero {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (v : { v : EuclideanSpace 𝕜 ι // v ≠ 0 }) : unitRep v ≠ 0

theorem Projectivization.unitRep_smul {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (v : { v : EuclideanSpace 𝕜 ι // v ≠ 0 }) {t : 𝕜} (ht : t ≠ 0) : unitRep ⟨t • ↑v, ⋯⟩ = unitRep v

The unit representative is scale-invariant.

theorem Projectivization.unitRep_scale_invariant {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (a b : { v : EuclideanSpace 𝕜 ι // v ≠ 0 }) (t : 𝕜) (h : ↑a = t • ↑b) : unitRep a = unitRep b

noncomputable def Projectivization.unitSection {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] : Projectivization 𝕜 (EuclideanSpace 𝕜 ι) → EuclideanSpace 𝕜 ι

The unit section of the ray map: a unit-norm representative of every ray, chosen so that the first non-zero coordinate is real and positive.

Equations

• Projectivization.unitSection = Projectivization.lift Projectivization.unitRep ⋯

theorem Projectivization.unitSection_mk {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (v : EuclideanSpace 𝕜 ι) (hv : v ≠ 0) : (mk 𝕜 v hv).unitSection = unitRep ⟨v, hv⟩

theorem Projectivization.norm_unitSection {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (p : Projectivization 𝕜 (EuclideanSpace 𝕜 ι)) : ‖p.unitSection‖ = 1

theorem Projectivization.unitSection_ne_zero {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (p : Projectivization 𝕜 (EuclideanSpace 𝕜 ι)) : p.unitSection ≠ 0

theorem Projectivization.mk_unitSection {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (p : Projectivization 𝕜 (EuclideanSpace 𝕜 ι)) : mk 𝕜 p.unitSection ⋯ = p

The unit section is a section: mk (unitSection p) = p.

Measurability

theorem Projectivization.measurable_coord {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} (i : ι) : Measurable fun (v : EuclideanSpace 𝕜 ι) => v.ofLp i

theorem Projectivization.measurableSet_firstIndex_eq {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (i : ι) : MeasurableSet {v : { v : EuclideanSpace 𝕜 ι // v ≠ 0 } | firstIndex v = i}

The set of vectors whose first non-zero coordinate is i is measurable.

noncomputable def Projectivization.candidateRep {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] (i : ι) (v : EuclideanSpace 𝕜 ι) : EuclideanSpace 𝕜 ι

The candidate representative for a given first index, as a function on all vectors.

Equations

• Projectivization.candidateRep i v = ((starRingEnd 𝕜) (v.ofLp i) / ↑‖v.ofLp i‖ * ↑‖v‖⁻¹) • v

theorem Projectivization.measurable_candidateRep {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] (i : ι) : Measurable (candidateRep i)

theorem Projectivization.unitRep_eq_sum {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] (v : { v : EuclideanSpace 𝕜 ι // v ≠ 0 }) : unitRep v = ∑ i : ι, {w : { v : EuclideanSpace 𝕜 ι // v ≠ 0 } | firstIndex w = i}.indicator (fun (w : { v : EuclideanSpace 𝕜 ι // v ≠ 0 }) => candidateRep i ↑w) v

theorem Projectivization.measurable_unitRep {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] : Measurable unitRep

theorem Projectivization.measurable_unitSection {𝕜 : Type u_1} [RCLike 𝕜] {ι : Type u_2} [Fintype ι] [LinearOrder ι] : Measurable unitSection

★ The unit section is measurable.