SmallCommutingCorrections.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Small corrections commuting with the averaging dynamics

The correcting element may change with the sample and the averaging length may grow arbitrarily fast. Commutation transports the correction outside the entire window. The compact-observable estimate then controls it uniformly over all starting points, without an ergodic-element premise.

lemma OAI.DukePrimeDegree.orbitWindowProbability_commuting_smul line 30

Source documentation

Exact transport of the correction through a finite orbit window.

lemma orbitWindowProbability_commuting_smul
    (ν : ProbabilityMeasure X) (T : X → X) (hT : Measurable T)
    (a : G) (hcomm : Function.Commute T (fun x => a • x)) (N : ℕ) :
    orbitWindowProbability (ν.map (fun x => a • x)) T hT N =
      (orbitWindowProbability ν T hT N).map (fun x => a • x) := by
…

Mentions: OAI.DukePrimeDegree.orbitWindowProbability

theorem OAI.DukePrimeDegree.commuting_corrections_window_integral_tendsto_zero line 43

Source documentation

This estimate is independent of the rate of growth of the window length, because compact observables have a global translation modulus.

theorem commuting_corrections_window_integral_tendsto_zero
    (ν : I → ProbabilityMeasure X) (T : X → X) (hT : Measurable T)
    (a : I → G) (ha : Tendsto a l (𝓝 1))
    (hcomm : ∀ i, Function.Commute T (fun x => a i • x))
    (N : I → ℕ) (f : CompactlySupportedContinuousMap X ℝ) :
    Tendsto (fun i =>
      (∫ x, f x ∂(orbitWindowProbability ((ν i).map (fun y => a i • y)) T hT (N i) : Measure X)) -
      ∫ x, f x ∂(orbitWindowProbability (ν i) T hT (N i) : Measure X))
      l (𝓝 0) := by
…

Mentions: OAI.DukePrimeDegree.orbitWindowProbability

theorem OAI.DukePrimeDegree.commuting_corrections_preserve_window_integral_limit line 67

Source documentation

If the original window has the desired compact-observable limit, the corrected initial law has the same limit.

theorem commuting_corrections_preserve_window_integral_limit
    (ν : I → ProbabilityMeasure X) (T : X → X) (hT : Measurable T)
    (a : I → G) (ha : Tendsto a l (𝓝 1))
    (hcomm : ∀ i, Function.Commute T (fun x => a i • x))
    (N : I → ℕ) (f : CompactlySupportedContinuousMap X ℝ) (c : ℝ)
    (hlim : Tendsto (fun i =>
      ∫ x, f x ∂(orbitWindowProbability (ν i) T hT (N i) : Measure X)) l (𝓝 c)) :
    Tendsto (fun i =>
      ∫ x, f x ∂(orbitWindowProbability ((ν i).map (fun y => a i • y)) T hT (N i) : Measure X))
      l (𝓝 c) := by
…

Mentions: OAI.DukePrimeDegree.orbitWindowProbability