Crossing.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.CouplingParameters.crossingLabel line 13
Source documentation
Conditioning on y uses a bottom label; conditioning on x uses a top label.
```
def crossingLabel (right : Bool) (w : Fin 2) : Fin 5 :=
…
```
theorem OAI.FiniteFactor.CouplingParameters.crossingLabel_mass line 16
theorem OAI.FiniteFactor.CouplingParameters.crossingLabel_length line 20
theorem OAI.FiniteFactor.CouplingParameters.crossingLabel_interval line 25
theorem OAI.FiniteFactor.CouplingParameters.crossingLabel_opposite_interval line 31
def OAI.FiniteFactor.CouplingParameters.posteriorMass line 38
Source documentation
This is the conditional label weight from conditional-kernel.
```
def posteriorMass (right : Bool) (t : ℝ) (i : Fin 5) : ℝ :=
…
```
theorem OAI.FiniteFactor.CouplingParameters.posteriorMass_nonneg line 41
theorem OAI.FiniteFactor.CouplingParameters.posteriorMass_sum line 48
theorem OAI.FiniteFactor.CouplingParameters.crossing_component_density_ge_one line 55
theorem OAI.FiniteFactor.CouplingParameters.crossing_posterior_lower line 70

theorem OAI.FiniteFactor.CouplingParameters.crossing_partner_interval line 85

Source documentation

The opposite endpoint of the selected label crosses the threshold surely.

theorem crossing_partner_interval (right : Bool) (w : Fin 2) {u : ℝ}
    (hu : p.width w ≤ u ∧ u ≤ 1-p.width w) :
    p.endpointInterval (!right) (crossingLabel right w) ⊆
      if right then Set.Iio u else Set.Ici u := by
…

Mentions: OAI.FiniteFactor.CouplingParameters.crossingLabel

def OAI.FiniteFactor.CouplingParameters.posteriorLaw line 99
Source documentation
The actual probability measure in the displayed conditional-kernel formula. The disintegration identities are proved separately.
```
def posteriorLaw (right : Bool) (t : ℝ) : Measure ℝ :=
…
```
instance OAI.FiniteFactor.CouplingParameters.posteriorLaw_probability line 103
theorem OAI.FiniteFactor.CouplingParameters.posteriorLaw_component_le line 115

theorem OAI.FiniteFactor.CouplingParameters.posteriorLaw_crossing_lower line 126

Source documentation

Both orientations of the actual posterior crossing estimate, with the source constant 1/10 and no assumptions on a candidate projection.

theorem posteriorLaw_crossing_lower (right : Bool) (w : Fin 2)
    {t u : ℝ} (ht : t ∈ Set.Ico 0 1) (hu : p.width w ≤ u ∧ u ≤ 1-p.width w)
    (heligible : if right then u ≤ t else t < u) :
    ENNReal.ofReal (p.rho w / 10) ≤
      p.posteriorLaw right t (if right then Set.Iio u else Set.Ici u) := by
…