FiniteTraceSlowdown.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Trace transition matrices under an exact holding slowdown

def OAI.ContingencyTables.FiniteChainSlowdown.slowKilled line 16
lemma OAI.ContingencyTables.FiniteChainSlowdown.slowKilled_apply line 31
lemma OAI.ContingencyTables.FiniteChainSlowdown.inner line 42
theorem OAI.ContingencyTables.FiniteChainSlowdown.dual_bound line 48
Source documentation
The observable dual estimate is also stable under the holding factor. This is the estimate used by trajectory concentration; a full spectral gap for unrelated observables is not needed.
```
theorem dual_bound (C : FiniteChain X) (a : ℝ) (ha0 : 0 ≤ a) (ha1 : a ≤ 1)
    (ha : 1/2 ≤ a) (K : ℝ) (hK : 0 ≤ K) (g H : X → ℝ)
    (h : (C.inner g H)^2 ≤ K*C.inner g g*C.energy H) :
    ((slow C a ha0 ha1).inner g H)^2 ≤
      (2*K)*(slow C a ha0 ha1).inner g g*(slow C a ha0 ha1).energy H := by
…
```
Mentions: OAI.ContingencyTables.FiniteChainSlowdown.slow, OAI.ContingencyTables.FiniteChainSlowdown.inner, OAI.ContingencyTables.FiniteChainSlowdown.energy

theorem OAI.ContingencyTables.FiniteChainSlowdown.warm_moment_bound line 66

Source documentation

Thus all accepted warm-start trajectory moment estimates transfer to the implemented holding chain with a factor of at most two.

theorem warm_moment_bound (C : FiniteChain X) (a : ℝ) (ha0 : 0 ≤ a) (ha1 : a ≤ 1)
    (ha : 1/2 ≤ a) (K U : ℝ) (hK : 0 ≤ K) (hU : 0 ≤ U) (g : X → ℝ)
    (hdual : ∀ H,(C.inner g H)^2 ≤ K*C.inner g g*C.energy H)
    (nu : X → ℝ) (hwarm : ∀ x,nu x ≤ U*C.π x) (N : ℕ) (hN : 0 < N) :
    (∑ x,nu x*(slow C a ha0 ha1).squareMoment g N x)/(N:ℝ)^2 ≤
      4*U*K*C.inner g g/N := by
…

Mentions: OAI.ContingencyTables.FiniteChainSlowdown.slow

lemma OAI.ContingencyTables.FiniteChainSlowdown.slow_apply line 77
lemma OAI.ContingencyTables.FiniteChainSlowdown.slowKilled_matches line 86
theorem OAI.ContingencyTables.FiniteChainSlowdown.hitKernel line 104
Source documentation
A holding step changes when the chain hits the selected set, but not where it first hits. The equality follows from the Green residual identity, without manipulating an infinite series term by term.
```
theorem hitKernel (C : FiniteChain X) (A : X → Prop)
    (Q : KilledKernel (FiniteChain.Outside A))
    (a : ℝ) (ha0 : 0 < a) (ha1 : a ≤ 1)
    (x : FiniteChain.Outside A) (y : FiniteChain.Inside A) :
    (slow C a ha0.le ha1).hitKernel A (slowKilled Q a ha0 ha1) x y=C.hitKernel A Q x y := by
…
```
Mentions: OAI.ContingencyTables.FiniteChainSlowdown.slow, OAI.ContingencyTables.FiniteChainSlowdown.slowKilled

theorem OAI.ContingencyTables.FiniteChainSlowdown.traceMatrix line 123

Source documentation

The trace itself acquires exactly the same holding factor.

theorem traceMatrix (C : FiniteChain X) (A : X → Prop)
    (Q : KilledKernel (FiniteChain.Outside A))
    (a : ℝ) (ha0 : 0 < a) (ha1 : a ≤ 1)
    (x y : FiniteChain.Inside A) :
    (slow C a ha0.le ha1).traceMatrix A (slowKilled Q a ha0 ha1) x y=
      a*C.traceMatrix A Q x y+if x=y then 1-a else 0 := by
…

Mentions: OAI.ContingencyTables.FiniteChainSlowdown.slow, OAI.ContingencyTables.FiniteChainSlowdown.slowKilled

theorem OAI.ContingencyTables.FiniteChainSlowdown.trace_energy line 142

theorem OAI.ContingencyTables.FiniteChainSlowdown.trace_variance_bound line 169

Source documentation

This transfers the accepted trace Poincaré estimate to the actual dyadic holding chain, rather than merely to a separately defined trace.

theorem trace_variance_bound (C : FiniteChain X) (A : X → Prop)
    [Nonempty (FiniteChain.Inside A)] (Q : KilledKernel (FiniteChain.Outside A))
    (hQ : ∀ x y : FiniteChain.Outside A,Q.Q x y=C.P x.val y.val)
    (a : ℝ) (ha0 : 0 < a) (ha1 : a ≤ 1) (ha : 1/2 ≤ a)
    (K : ℝ) (hK : 0 ≤ K) (f : FiniteChain.Inside A → ℝ)
    (h : (C.traceChain A Q hQ).variance f ≤ K*(C.traceChain A Q hQ).energy f) :
    ((slow C a ha0.le ha1).traceChain A (slowKilled Q a ha0 ha1)
      (slowKilled_matches C A Q hQ a ha0 ha1)).variance f ≤
        (2*K)*((slow C a ha0.le ha1).traceChain A (slowKilled Q a ha0 ha1)
          (slowKilled_matches C A Q hQ a ha0 ha1)).energy f := by
…

Mentions: OAI.ContingencyTables.FiniteChainSlowdown.variance, OAI.ContingencyTables.FiniteChainSlowdown.energy, OAI.ContingencyTables.FiniteChainSlowdown.slow, OAI.ContingencyTables.FiniteChainSlowdown.slowKilled, OAI.ContingencyTables.FiniteChainSlowdown.slowKilled_matches