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 pushforward measure π*μprep, not μFS directly. This is cleaner than the spec's μFS-relative formulation: via the measure bridge, the two agree, but this form lets weights_sum_eq_one be proved without dragging μFS through.

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.

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.