BilateralConditionalSupport.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Actual conditional measures on bilateral itinerary fibers

theorem OAI.DukePrimeDegree.ae_graph_condKernel_fiber line 16

Source documentation

Disintegration of the graph of a measurable map is concentrated on the corresponding fibers.

theorem ae_graph_condKernel_fiber
    {S Y : Type*} [MeasurableSpace S] [MeasurableEq S]
    [MeasurableSpace Y] [StandardBorelSpace Y] [Nonempty Y]
    (μ : Measure Y) [IsProbabilityMeasure μ]
    (f : Y → S) (hf : Measurable f) :
    let ρ := μ.map (fun y => (f y,y))
…

theorem OAI.DukePrimeDegree.ae_condDistrib_self_fiber line 32
def OAI.DukePrimeDegree.bilateralNameObservation line 46
theorem OAI.DukePrimeDegree.measurable_bilateralNameObservation line 52
theorem OAI.DukePrimeDegree.bilateralNameObservation_eq_iff line 62
theorem OAI.DukePrimeDegree.ae_bilateral_condKernel_fiber line 72
Source documentation
Almost every conditional measure for the actual bilateral itinerary law is supported on the geometric fiber of any representative.
```
theorem ae_bilateral_condKernel_fiber {n : ℕ}
    (ell : Fin n → ℝ) (hell : ∑ i, ell i=0)
    (Q : X n → ℕ) (hQ : Measurable Q)
    (μ : Measure (X n)) [IsProbabilityMeasure μ] :
    let F := bilateralNameObservation ell hell Q
…
```
Mentions: OAI.DukePrimeDegree.bilateralNameObservation