Conditioning.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.CouplingParameters.vectorPosterior_eq_condDistrib line 14
Source documentation
Identification with mathlib's regular conditional distribution.
```
theorem vectorPosterior_eq_condDistrib {ι : Type*} [Countable ι]
    (p : ι → CouplingParameters) (right : ι → Bool) :
    condDistrib (vectorEndpoint (fun i => !right i)) (vectorEndpoint right) (vectorCoupling p)
      =ᵐ[(vectorCoupling p).map (vectorEndpoint right)] vectorPosterior p right :=
…
```
Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.vectorEndpoint, OAI.FiniteFactor.CouplingParameters.vectorCoupling, OAI.FiniteFactor.CouplingParameters.vectorPosterior

theorem OAI.FiniteFactor.CouplingParameters.vector_condExp_event_le line 24

Source documentation

A bound on the proved full-vector posterior is a conditional-expectation bound on the original augmented probability space.

theorem vector_condExp_event_le {ι : Type*} [Countable ι]
    (p : ι → CouplingParameters) (right : ι → Bool)
    {B : Set ((ι → ℝ) × (ι → ℝ))} (hB : MeasurableSet B) {δ : ℝ}
    (hb : ∀ᵐ x ∂(vectorCoupling p).map (vectorEndpoint right),
      (vectorPosterior p right x).real (Prod.mk x ⁻¹' B) ≤ δ) :
    ∀ᵐ ω ∂vectorCoupling p,
      (vectorCoupling p)[
        (fun ω => B.indicator (fun _ => (1 : ℝ))
          (vectorEndpoint right ω, vectorEndpoint (fun i => !right i) ω)) |
        (inferInstance : MeasurableSpace (ι → ℝ)).comap (vectorEndpoint right)] ω ≤ δ := by
…

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

theorem OAI.FiniteFactor.CouplingParameters.vector_mask_tsum_integral_le line 53

Source documentation

The countably infinite masked estimate, instantiated on the actual augmented coupling using the verified posterior. No conditional probability hypothesis remains to be supplied independently of the kernel.

theorem vector_mask_tsum_integral_le {ι V : Type*} [Countable ι] [Countable V]
    (p : ι → CouplingParameters) (right : ι → Bool)
    (B : V → Set ((ι → ℝ) × (ι → ℝ))) (hB : ∀ v, MeasurableSet (B v))
    (f : V → (ι → Fin 6 × (ℝ × ℝ)) → ℝ) (δ : ℝ)
    (hf : ∀ v, Integrable (f v) (vectorCoupling p))
    (hfm : ∀ v, StronglyMeasurable[(inferInstance : MeasurableSpace (ι → ℝ)).comap (vectorEndpoint right)] (f v))
    (hf0 : ∀ v ω, 0 ≤ f v ω)
    (hsum : ∀ᵐ ω ∂vectorCoupling p, Summable (fun v => f v ω))
    (hint : Integrable (fun ω => ∑' v, f v ω) (vectorCoupling p))
    (hb : ∀ v, ∀ᵐ x ∂(vectorCoupling p).map (vectorEndpoint right),
      (vectorPosterior p right x).real (Prod.mk x ⁻¹' B v) ≤ δ) :
    (∫ ω, (∑' v, ((fun ω => (vectorEndpoint right ω,
…