OAI/NumberTheory/PrimePackets/ObservationSigmaAlgebra.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The sigma algebra and conditional expectations of finite observations

  1. def OAI.PrimeDegreePackets.observationSigma line 15
  2. lemma OAI.PrimeDegreePackets.observationSigma_le line 18
  3. lemma OAI.PrimeDegreePackets.stronglyMeasurable_observation_values line 30
  4. lemma OAI.PrimeDegreePackets.setIntegral_eq_of_observation_atoms line 37

    Source documentation

    Equality on the finitely many observation atoms determines all set integrals over the sigma algebra generated by that observation.

    lemma setIntegral_eq_of_observation_atoms
    (μ : Measure Y) (Q : Y → β) (hQ : ∀ b, MeasurableSet {y | Q y = b})
    {f g : Y → ℝ} (hf : Integrable f μ) (hg : Integrable g μ)
    (hatom : ∀ b, ∫ y in {y | Q y = b}, f y ∂μ = ∫ y in {y | Q y = b}, g y ∂μ)
    {s : Set Y} (hs : MeasurableSet[observationSigma Q] s) :
    ∫ y in s, f y ∂μ = ∫ y in s, g y ∂μ := by
…

    Mentions: OAI.PrimeDegreePackets.observationSigma

  5. lemma OAI.PrimeDegreePackets.observation_values_ae_eq_condExp line 59