RealPathApproximation.lean`

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Keeping an entire finite history during real-kernel comparison

def OAI.ContingencyTables.RealKernelApproximation.mapKernel line 14
lemma OAI.ContingencyTables.RealKernelApproximation.rational_map_push line 19
def OAI.ContingencyTables.RealKernelApproximation.liftKernel line 27
Source documentation
a can contain the entire past. Only read a is used for the next random transition; put a retains every coordinate needed afterward.
```
def liftKernel (K : FiniteKernel X Y) (read : A → X) (put : A → Y → B) : FiniteKernel A B where
…
```
def OAI.ContingencyTables.RealKernelApproximation.liftRational line 33
theorem OAI.ContingencyTables.RealKernelApproximation.lifted_row_distance line 38
Source documentation
Recording extra coordinates never increases one transition's error.
```
theorem lifted_row_distance [DecidableEq B] (Q : X → RationalLaw Y)
    (K : FiniteKernel X Y) (read : A → X) (put : A → Y → B) (a : A) :
    distance ((rationalKernel (liftRational Q read put)).P a)
      ((liftKernel K read put).P a) ≤ distance ((rationalKernel Q).P (read a)) (K.P (read a)) := by
…
```
Mentions: OAI.ContingencyTables.RealKernelApproximation.distance, OAI.ContingencyTables.RealKernelApproximation.rationalKernel, OAI.ContingencyTables.RealKernelApproximation.liftRational, OAI.ContingencyTables.RealKernelApproximation.liftKernel
theorem OAI.ContingencyTables.RealKernelApproximation.lifted_walk_distance line 49
Source documentation
The joint-history version of the accumulated transition bound. The recorded state may be a fixed-length vector of every visited state.
```
theorem lifted_walk_distance [DecidableEq A] (Q : X → RationalLaw X)
    (K : FiniteKernel X X) (read : A → X) (put : A → X → A)
    (η : ℝ) (hη : ∀ x,distance ((rationalKernel Q).P x) (K.P x) ≤ η)
    (a : A) (n : ℕ) :
    distance (fun b => ((walkLaw (liftRational Q read put) a n).mass b:ℝ))
      (((liftKernel K read put).power n).P a) ≤ n*η := by
…
```
Mentions: OAI.ContingencyTables.RealKernelApproximation.distance, OAI.ContingencyTables.RealKernelApproximation.rationalKernel, OAI.ContingencyTables.RealKernelApproximation.liftRational, OAI.ContingencyTables.RealKernelApproximation.liftKernel
abbrev OAI.ContingencyTables.RealKernelApproximation.PathState line 61
Source documentation
The first coordinate records which entries of the vector have been written. Saturation keeps the state space finite even after the horizon.
```
abbrev PathState (X : Type*) (N : ℕ) := Fin (N+1) × (Fin (N+1) → X)
```
def OAI.ContingencyTables.RealKernelApproximation.nextPosition line 63
def OAI.ContingencyTables.RealKernelApproximation.pathRead line 66
def OAI.ContingencyTables.RealKernelApproximation.pathPut line 68
def OAI.ContingencyTables.RealKernelApproximation.pathInitial line 71
theorem OAI.ContingencyTables.RealKernelApproximation.path_distance line 75
Source documentation
Error for the entire recorded path, hence also for any event defined from all the empirical observations, is at most one row error per step.
```
theorem path_distance (Q : X → RationalLaw X) (K : FiniteKernel X X)
    (η : ℝ) (hη : ∀ x,distance ((rationalKernel Q).P x) (K.P x) ≤ η)
    (N n : ℕ) (x : X) :
    distance (fun a => ((walkLaw (liftRational Q pathRead pathPut) (pathInitial N x) n).mass a:ℝ))
      (((liftKernel K pathRead pathPut).power n).P (pathInitial N x)) ≤ n*η :=
…
```
Mentions: OAI.ContingencyTables.RealKernelApproximation.distance, OAI.ContingencyTables.RealKernelApproximation.rationalKernel, OAI.ContingencyTables.RealKernelApproximation.liftRational, OAI.ContingencyTables.RealKernelApproximation.pathRead, OAI.ContingencyTables.RealKernelApproximation.pathPut, OAI.ContingencyTables.RealKernelApproximation.pathInitial, OAI.ContingencyTables.RealKernelApproximation.liftKernel