OAI/Analysis/FiniteFactor/Coupling/VectorBayes.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.CouplingParameters.orientPair line 14

   Source documentation

   The orientation records the conditioning endpoint first.

   def orientPair (right : Bool) (z : ℝ × ℝ) : ℝ × ℝ :=
   …

2. theorem OAI.FiniteFactor.CouplingParameters.orientPair_measurable line 17
3. theorem OAI.FiniteFactor.CouplingParameters.posterior_compProd line 20
4. def OAI.FiniteFactor.CouplingParameters.vectorCoupling line 35
5. instance OAI.FiniteFactor.CouplingParameters.vectorCoupling_probability line 38
6. def OAI.FiniteFactor.CouplingParameters.vectorEndpoint line 41
7. theorem OAI.FiniteFactor.CouplingParameters.vectorEndpoint_measurable line 44
8. theorem OAI.FiniteFactor.CouplingParameters.vectorEndpoint_law line 48
9. def OAI.FiniteFactor.CouplingParameters.vectorPosterior line 58
10. instance OAI.FiniteFactor.CouplingParameters.vectorPosterior_markov line 61
11. theorem OAI.FiniteFactor.CouplingParameters.vectorPosterior_disintegration line 66

    Source documentation

    The product posterior is the conditional law given the entire selected endpoint vector. This identity holds for the actual augmented product law.

    theorem vectorPosterior_disintegration {ι : Type*} (p : ι → CouplingParameters) (right : ι → Bool) :
        ((vectorCoupling p).map (vectorEndpoint right)) ⊗ₘ (vectorPosterior p right) =
          (vectorCoupling p).map (fun ω => (vectorEndpoint right ω, vectorEndpoint (fun i => !right i) ω)) := by
    …

    Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.vectorCoupling, OAI.FiniteFactor.CouplingParameters.vectorEndpoint, OAI.FiniteFactor.CouplingParameters.vectorPosterior

12. theorem OAI.FiniteFactor.CouplingParameters.vectorPosterior_independence line 104

    Source documentation

    Full-vector conditional independence, including both endpoint orientations. Together with vectorPosterior_disintegration this is independence under the actual conditional law, not a statement about a separately chosen product.

    theorem vectorPosterior_independence {ι : Type*} (p : ι → CouplingParameters) (right : ι → Bool)
        (x : ι → ℝ) (I : Finset ι) (S : ι → Set ℝ) (hS : ∀ i ∈ I, MeasurableSet (S i)) :
        vectorPosterior p right x (Set.pi (I : Set ι) S) =
          ∏ i ∈ I, (p i).posteriorKernel (right i) (x i) (S i) :=
    …

    Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.vectorPosterior, OAI.FiniteFactor.CouplingParameters.posteriorKernel

13. theorem OAI.FiniteFactor.CouplingParameters.vectorPosterior_rectangle line 111

    Source documentation

    Defining conditional identity for every measurable pair of full-vector events.

    theorem vectorPosterior_rectangle {ι : Type*} (p : ι → CouplingParameters) (right : ι → Bool)
        {A B : Set (ι → ℝ)} (hA : MeasurableSet A) (hB : MeasurableSet B) :
        (∫⁻ x in A, vectorPosterior p right x B ∂((vectorCoupling p).map (vectorEndpoint right))) =
          vectorCoupling p {ω | vectorEndpoint right ω ∈ A ∧ vectorEndpoint (fun i => !right i) ω ∈ B} := by
    …

    Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.vectorPosterior, OAI.FiniteFactor.CouplingParameters.vectorCoupling, OAI.FiniteFactor.CouplingParameters.vectorEndpoint