FinitePosteriorAC.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FiniteFactor.CouplingParameters.diagonalHaarReference line 13
Source documentation
A normalized reference law allowing either a diagonal or a Haar draw.
```
def diagonalHaarReference (t : ℝ) : Measure ℝ :=
…
```
instance OAI.FiniteFactor.CouplingParameters.diagonalHaarReference_probability line 16
theorem OAI.FiniteFactor.CouplingParameters.posteriorKernel_ac_diagonalHaar line 23
Source documentation
Every coordinate posterior has an absolutely continuous off-diagonal part. The diagonal atom is retained explicitly in the reference measure.
```
theorem posteriorKernel_ac_diagonalHaar (p : CouplingParameters) (right : Bool) (t : ℝ) :
    p.posteriorKernel right t ≪ diagonalHaarReference t := by
…
```
Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.diagonalHaarReference
theorem OAI.FiniteFactor.CouplingParameters.vectorPosterior_finite_map line 37
Source documentation
Full conditional law with only F resampled, given the entire original endpoint vector. The coordinates outside F are exactly fixed.
```
theorem vectorPosterior_finite_map {ι : Type*} [DecidableEq ι]
    (p : ι → CouplingParameters) (F : Finset ι) (x : ι → ℝ) :
    (vectorPosterior p (fun _ => false) x).map
      (fun y i => if i ∈ F then y i else x i) =
      Measure.infinitePi (fun i => if i ∈ F then (p i).posteriorKernel false (x i)
        else Measure.dirac (x i)) := by
…
```
Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.vectorPosterior, OAI.FiniteFactor.CouplingParameters.posteriorKernel
theorem OAI.FiniteFactor.CouplingParameters.vectorPosterior_finite_ac line 54
Source documentation
Absolute continuity of the actual full-vector conditional law after a finite replacement. This uses finitely many coordinate changes only.
```
theorem vectorPosterior_finite_ac {ι : Type*} [DecidableEq ι]
    (p : ι → CouplingParameters) (F : Finset ι) (x : ι → ℝ) :
    (vectorPosterior p (fun _ => false) x).map
      (fun y i => if i ∈ F then y i else x i) ≪
      Measure.infinitePi (fun i => if i ∈ F then diagonalHaarReference (x i)
        else Measure.dirac (x i)) := by
…
```
Mentions: OAI.FiniteFactor.CouplingParameters, OAI.FiniteFactor.CouplingParameters.vectorPosterior, OAI.FiniteFactor.CouplingParameters.diagonalHaarReference