`BookProof.ChapterSelectingEvents.selecting_events_not_rewriting_history` {α : Type*} [MeasurableSpace α] [StandardBorelSpace α] (μ : Measure α) [IsProbabilityMeasure μ] [NullSingl

Proved

BookProof.ChapterSelectingEvents.selecting_events_not_rewriting_history

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterSelectingEvents.

BookProof.ChapterSelectingEvents.selecting_events_not_rewriting_history {α : Type*} [MeasurableSpace α] [StandardBorelSpace α] (μ : Measure α) [IsProbabilityMeasure μ] [NullSingletonClass μ] (E F : Set α) (_hE : MeasurableSet E) (hF : MeasurableSet F) (_hEpos : μ E > 0) (_hFpos : μ F > 0) : μ[F | E] = μ (E ∩ F) / μ E

Formalization note: Lean 4 identifier BookProof.ChapterSelectingEvents.selecting_events_not_rewriting_history.

Preamble

-- Generated from ChapterSelectingEvents.lean — theorem BookProof.ChapterSelectingEvents.selecting_events_not_rewriting_history
import Mathlib
import Definitions.Def_ChapterSelectingEvents
open BookProof.ChapterSelectingEvents


open scoped BigOperators
open MeasureTheory ProbabilityTheory


variable (H : Type*) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]

variable {Ω Data : Type*} [MeasurableSpace Ω]
variable {X : Type*} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ]
variable {Seed Model : Type*} [Fintype Seed] [Fintype Model] [DecidableEq Model]

Formal statement

theorem BookProof.ChapterSelectingEvents.selecting_events_not_rewriting_history
    {α : Type*} [MeasurableSpace α] [StandardBorelSpace α]
    (μ : Measure α) [IsProbabilityMeasure μ] [NullSingletonClass μ]
    (E F : Set α) (_hE : MeasurableSet E) (hF : MeasurableSet F)
    (_hEpos : μ E > 0) (_hFpos : μ F > 0) :
    μ[F | E] = μ (E ∩ F) / μ E := by sorry

View graph