Noncrossing.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.CouplingParameters.crossingPartner line 12
Source documentation
The interval in which the unconditioned partner crosses an eligible threshold.
```
def crossingPartner (right : Bool) (u : ℝ) : Set ℝ :=
…
```
theorem OAI.FiniteFactor.CouplingParameters.crossingPartner_measurable line 15
theorem OAI.FiniteFactor.CouplingParameters.posterior_noncrossing_le_exp line 20

theorem OAI.FiniteFactor.CouplingParameters.vectorPosterior_noncrossing_le_exp line 36

Source documentation

Simultaneous noncrossing of any fixed eligible coordinates, conditional on the entire endpoint vector. The exponent is the sum of their actual biases.

theorem vectorPosterior_noncrossing_le_exp {ι : Type*}
    (p : ι → CouplingParameters) (right : ι → Bool) (w : ι → Fin 2)
    (x u : ι → ℝ) (I : Finset ι)
    (hx : ∀ i ∈ I, x i ∈ Set.Ico 0 1)
    (hu : ∀ i ∈ I, (p i).width (w i) ≤ u i ∧ u i ≤ 1-(p i).width (w i))
    (heligible : ∀ i ∈ I, if right i then u i ≤ x i else x i < u i) :
    vectorPosterior p right x (Set.pi (I : Set ι) (fun i => (crossingPartner (right i) (u i))ᶜ)) ≤
      ENNReal.ofReal (Real.exp (-(∑ i ∈ I, (p i).rho (w i) / 10))) := by
…

Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.vectorPosterior, OAI.FiniteFactor.CouplingParameters.crossingPartner, OAI.FiniteFactor.CouplingParameters.rho

theorem OAI.FiniteFactor.CouplingParameters.vectorPosterior_noncrossing_source_bound line 54