OAI/Combinatorics/UniformKServer/ConditionalLaw.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Finite posterior calculus for the finite-law construction. All conditional laws are computed from fiber weights, including the zero-probability fibers. This supplies, rather than assumes, the all-step filtering identities.

  1. def OAI.UniformKServer.ConditionalLaw.mass line 18
  2. def OAI.UniformKServer.ConditionalLaw.kernel line 21
  3. def OAI.UniformKServer.ConditionalLaw.posterior line 24
  4. def OAI.UniformKServer.ConditionalLaw.measurable line 27
  5. theorem OAI.UniformKServer.ConditionalLaw.mass_nonneg line 30
  6. theorem OAI.UniformKServer.ConditionalLaw.weight_le_mass line 36
  7. theorem OAI.UniformKServer.ConditionalLaw.mass_eq line 42
  8. theorem OAI.UniformKServer.ConditionalLaw.kernel_nonneg line 49
  9. theorem OAI.UniformKServer.ConditionalLaw.kernel_sum line 56
  10. theorem OAI.UniformKServer.ConditionalLaw.balance line 67
  11. theorem OAI.UniformKServer.ConditionalLaw.weighted_kernel_sum line 75
  12. theorem OAI.UniformKServer.ConditionalLaw.posterior_measurable line 84
  13. theorem OAI.UniformKServer.ConditionalLaw.test_identity line 94

    Source documentation

    The finite conditional-expectation identity. The test function is old history measurable; no restriction to a later selected event is made.

    theorem test_identity {w : Ω → ℝ} (hw : ∀ ω, 0 ≤ w ω) (F : Setoid Ω)
    (a X : Ω → ℝ) (ha : measurable F a) :
    (∑ ω, w ω*a ω*posterior w F X ω) = ∑ ω, w ω*a ω*X ω := by
…

    Mentions: OAI.UniformKServer.ConditionalLaw.measurable, OAI.UniformKServer.ConditionalLaw.posterior

  14. theorem OAI.UniformKServer.ConditionalLaw.filtering line 110
  15. theorem OAI.UniformKServer.ConditionalLaw.posterior_nonneg line 116
  16. theorem OAI.UniformKServer.ConditionalLaw.posterior_le_one line 120
  17. theorem OAI.UniformKServer.ConditionalLaw.posterior_sub line 128
  18. theorem OAI.UniformKServer.ConditionalLaw.posterior_abs line 132
  19. theorem OAI.UniformKServer.ConditionalLaw.expected_contraction line 140