LF2 Projective Weights

Category: 3-Local (LF2 measurable partitions on the projective target and their weight normalisation).

Spec §4:

• MeasurablePartition — measurable partition of P up to null sets (spec §4.1).
• projectiveWeight — the weight of an outcome region under the pushforward of a preparation measure (spec §4.2).
• weights_sum_eq_one — normalisation (spec §4.3).

The partition is stated relative to the preparation's pushforward measure π*μprep. The measure bridges concern the sector's reference measure μL; they do not identify π*μprep with μFS for an arbitrary preparation measure. A μFS-relative partition would also suffice if π*μprep ≪ μFS, since absolute continuity transfers its null overlaps and null uncovered set to π*μprep. No such relationship is assumed here. See specs/LF2-plan.md §2.3 for the partition interface.

weights_sum_eq_one uses measurability of π, the probability preparation measure and the partition hypotheses. It does not use a Fubini–Study measure or the sector's symmetry and measure-bridge properties.

structure CSD.LF2.MeasurablePartition (P : Type u_1) [MeasurableSpace P] (μ : MeasureTheory.Measure P) (n : ℕ) : Type u_1

A finite measurable partition of P up to μ-null sets: measurable parts, pairwise intersections of μ-measure zero, and complement of the union of μ-measure zero.

• parts : Fin n → Set P

  The parts, indexed by Fin n.

• measurable (i : Fin n) : MeasurableSet (self.parts i)

  Each part is measurable.

• pairwise_null (i j : Fin n) : i ≠ j → μ (self.parts i ∩ self.parts j) = 0

  Pairwise intersections are null.

• cover_null : μ (⋃ (i : Fin n), self.parts i)ᶜ = 0

  The complement of the union is null.

noncomputable def CSD.LF2.projectiveWeight {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] (D : SectorData SigmaSpace P G) (μprep : MeasureTheory.Measure SigmaSpace) (O : Set P) : ENNReal

Projective weight of an outcome region O ⊆ P under the pushforward of a preparation measure. This definition allows arbitrary measures and sets; probability normalisation and measurable parts are assumed in weights_sum_eq_one.

Equations

• CSD.LF2.projectiveWeight D μprep O = (MeasureTheory.Measure.map D.π μprep) O

theorem CSD.LF2.projectiveWeight_def {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] (D : SectorData SigmaSpace P G) (μprep : MeasureTheory.Measure SigmaSpace) (O : Set P) : projectiveWeight D μprep O = (MeasureTheory.Measure.map D.π μprep) O

Unfolding lemma: projectiveWeight is the pushforward measure of the region. Not @[simp] — leaving projectiveWeight as a named abstraction makes downstream proofs and theorem statements readable; callers unfold projectiveWeight (or rewrite with this lemma explicitly) when they need to expose the underlying pushforward.

theorem CSD.LF2.weights_sum_eq_one {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] (D : SectorData SigmaSpace P G) {n : ℕ} (μprep : MeasureTheory.Measure SigmaSpace) [MeasureTheory.IsProbabilityMeasure μprep] (π_part : MeasurablePartition P (MeasureTheory.Measure.map D.π μprep) n) : ∑ i : Fin n, projectiveWeight D μprep (π_part.parts i) = 1

Spec §4.3 normalisation. For a probability preparation measure and a measurable partition of P up to π*μprep-null sets, the weights sum to one.