LF1 Preparation

Category: 3-Local (LF1 conditional preparation measure on Ω0).

Glossary: https://glossary.constraintsurfacedynamics.com/preparation-region/ Plain-language, CSD-role and formal statements of the preparation region, with this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh.

noncomputable def CSD.LF1.OnticSetup.prepFiniteMeasure {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] (S : OnticSetup SigmaSpace) : MeasureTheory.FiniteMeasure SigmaSpace

The finite measure obtained by restricting μL to the preparation region Ω0.

Equations

• S.prepFiniteMeasure = ⟨(↑S.μL).restrict S.Ω0, ⋯⟩

noncomputable def CSD.LF1.OnticSetup.prepMeasure {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] (S : OnticSetup SigmaSpace) : MeasureTheory.ProbabilityMeasure SigmaSpace

The preparation probability measure, obtained by normalizing the restricted measure.

Equations

• S.prepMeasure = S.prepFiniteMeasure.normalize

@[simp]

theorem CSD.LF1.OnticSetup.prepFiniteMeasure_toMeasure {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] (S : OnticSetup SigmaSpace) : ↑S.prepFiniteMeasure = (↑S.μL).restrict S.Ω0

theorem CSD.LF1.OnticSetup.prepFiniteMeasure_ne_zero {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] (S : OnticSetup SigmaSpace) : ↑S.prepFiniteMeasure ≠ 0

The restricted preparation measure is nonzero because μL Ω0 ≠ 0 — the structure field hΩ0_nonzero, transferred across the restriction by Measure.restrict_eq_zero.

theorem CSD.LF1.OnticSetup.prepMeasure_toMeasure_eq {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] (S : OnticSetup SigmaSpace) : ↑S.prepMeasure = ↑S.prepFiniteMeasure.normalize

The preparation law unfolds to the normalisation of the restricted measure. This equation is definitional (rfl) and assumes nothing.

⚠️ Corrected 2026-08-11. This docstring previously read "Since the restricted measure is nonzero, normalization gives back the usual conditional preparation law" — attributing to this lemma a content it does not have. Nonzeroness is what makes the normalisation the genuine conditional law rather than a fallback, but it plays no part in the equation proved here; compare prepFiniteMeasure_ne_zero, which is where that fact lives.

theorem CSD.LF1.OnticSetup.prepFiniteMeasure_mass_eq {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] (S : OnticSetup SigmaSpace) : ↑S.prepFiniteMeasure.mass = ↑S.μL S.Ω0

The mass of prepFiniteMeasure, coerced to ENNReal, equals µL(Ω0). Isolated so a Mathlib refactor of FiniteMeasure.ennreal_mass or Measure.restrict_apply lands in one place.

theorem CSD.LF1.OnticSetup.prepFiniteMeasure_ne_zero_pair {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] (S : OnticSetup SigmaSpace) : S.prepFiniteMeasure ≠ 0 ∧ S.prepFiniteMeasure.mass ≠ 0

prepFiniteMeasure is nonzero as a finite measure, and its mass is nonzero as an ℝ≥0. Both facts are needed by prepMeasure_apply; bundling them isolates the dependency on FiniteMeasure.mass_nonzero_iff.

theorem CSD.LF1.OnticSetup.prepMeasure_apply {SigmaSpace : Type u_1} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] (S : OnticSetup SigmaSpace) (A : Set SigmaSpace) (hA : MeasurableSet A) : ↑S.prepMeasure A = ↑S.μL (A ∩ S.Ω0) / ↑S.μL S.Ω0

The preparation probability measure applied to a measurable set A equals the Liouville measure of A ∩ Ω0 divided by µL(Ω0). Explicit form of the conditional preparation measure (Paper A §4.2).

The proof routes through three named intermediate facts (prepMeasure_toMeasure_eq, prepFiniteMeasure_toMeasure, prepFiniteMeasure_mass_eq) plus three Mathlib lemmas (toMeasure_normalize_eq_of_nonzero, Measure.smul_apply, Measure.restrict_apply), so a future Mathlib rename of any one is localised to this proof.