8.ex · Book p. 230 · PDF p. 242

Exercises

The exercises test the chapter's definitions, proof calculations, edge cases, and extensions without changing the chapter's formalization status.

Open this section in the canonical August 9 source ↗

Place in the proof route

The chapter uses this material in the route toward The augmentation preserves the desired target as a marginal. The declaration-level source map is intentionally left inside the formalization layer until exact theorem anchors have been audited.

Why is this valid?

Chapter-level validity conditions

Both conditional distributions require finite, measurable normalizing constants.
Marginal preservation follows from Tonelli/Fubini only after nonnegativity and measurability are established.
An oracle specification must state whether samples are exact or approximate.

View Lean formalization

No declaration-level mapping has been accepted for this section. This is a route status, not a failed Lean declaration.