WholeFutureProbabilityKernel.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

A probability kernel on the entire subordinate future

The intrinsic product has an s-finite measurable version. Restricting it on the jointly measurable future relation and normalizing gives an actual probability kernel. On the exceptional zero/infinite-mass set we use a point mass; the intrinsic formula holds almost everywhere whenever the proved positive finite future-mass condition applies.

def OAI.DukePrimeDegree.EliminationChain.futureRestrictedKernel line 25
def OAI.DukePrimeDegree.EliminationChain.futureNormalizedKernel line 37
def OAI.DukePrimeDegree.EliminationChain.wholeFutureProbabilityKernel line 53
Source documentation
Normalize where the full-future mass is positive finite, using a fixed point mass on the remaining measurable exceptional set.
```
def wholeFutureProbabilityKernel (c : EliminationChain P D)
    (hf : c.finalEntries = allPositiveRoots n)
    (κ : Kernel (X n) c.Time) [IsSFiniteKernel κ]
    (ell : Fin n → ℝ) (hell : ∑ k, ell k=0) (Q : X n → ℕ)
    (hQ : Measurable Q) (m : ℕ) : Kernel (X n) c.Time :=
…
```
Mentions: OAI.DukePrimeDegree.EliminationChain, OAI.DukePrimeDegree.allPositiveRoots
instance OAI.DukePrimeDegree.EliminationChain.wholeFutureProbabilityKernel_markov line 66
lemma OAI.DukePrimeDegree.EliminationChain.wholeFutureProbabilityKernel_apply line 83
theorem OAI.DukePrimeDegree.EliminationChain.exists_wholeFutureProbabilityKernel line 104
def OAI.DukePrimeDegree.EliminationChain.futureAmbientKernel line 130
Source documentation
Push a time-coordinate kernel to the actual right root orbits.
```
def futureAmbientKernel (c : EliminationChain P D)
    (hf : c.finalEntries = allPositiveRoots n)
    (κ : Kernel (X n) c.Time) [IsSFiniteKernel κ] : Kernel (X n) (X n) where
…
```
Mentions: OAI.DukePrimeDegree.EliminationChain, OAI.DukePrimeDegree.allPositiveRoots
instance OAI.DukePrimeDegree.EliminationChain.futureAmbientKernel_markov line 147
lemma OAI.DukePrimeDegree.EliminationChain.ae_wholeFutureKernel_same_names line 158

theorem OAI.DukePrimeDegree.exists_low_entropy_wholeFutureProbabilityKernel line 191

Source documentation

The constructed low-height-entropy observation has a measurable probability-kernel version of its normalized whole-future root measures. Stationarity with respect to the ambient measure is a separate assertion.

theorem exists_low_entropy_wholeFutureProbabilityKernel (d : ℕ)
    (ell : Fin (d+1) → ℝ) (hell : ∑ i, ell i=0)
    (hgap : ∀ p : allPositiveRoots (d+1), Real.log 4 ≤ ell p.val.2-ell p.val.1)
    (μ : Measure (X (d+1))) [IsProbabilityMeasure μ]
    [ErgodicSMul (Multiplicative (LogCoordinates d)) (X (d+1)) μ]
    {ε : ℝ} (hε : 0 < ε) :
    ∃ (H Q : X (d+1) → ℕ) (κ : Kernel (X (d+1)) (UpperRootTime (d+1))),
      Measurable H ∧ Measurable Q ∧ IsMarkovKernel κ ∧
      (∀ m, IsCompact {x | H x ≤ m}) ∧
      (∀ m, (Q '' {x | H x ≤ m}).Finite) ∧
      (∀ N, observationEntropyRate μ
        (fun x => rightAction x (diagonalOneParameter ell hell (-1))) (heightClip H N) < ε) ∧
…

Mentions: OAI.DukePrimeDegree.allPositiveRoots, OAI.DukePrimeDegree.UpperRootTime, OAI.DukePrimeDegree.heightClip