OAI.Rokhlin.local_moving_cancellation: intermediate lemma from OpenAI, Rokhlin's multiple-mixing problem for one transformation

import Mathlib
import Definitions.Def_OAIQ3Ro002

section

set_option linter.all false
set_option linter.unusedVariables false
set_option linter.unusedTactic false
set_option linter.unreachableTactic false

namespace OAI

noncomputable section

namespace Rokhlin

section
open MeasureTheory ProbabilityTheory Set Filter
open scoped Topology BigOperators ComplexConjugate
variable {U Y X A C : Type*} [MeasurableSpace U] [MeasurableSpace Y]
    [MeasurableSpace.CountablyGenerated Y] [MeasurableSpace X]
    [Fintype A] [MeasurableSpace A] [MeasurableSingletonClass A]
    [MeasurableSpace C] [MeasurableSingletonClass C]
    (κ : Kernel U Y) [IsMarkovKernel κ] (S : Set (U × HilbertCode κ))
    (E : BorelFibreEnumeration S) (ψ : U × HilbertCode κ → C) (hψ : Measurable ψ)
    (D : C ≃ C) (a₀ a : U) (b : C)
    (hb : {g : localProjectiveGroup κ S a₀ | localGroupBlock κ S ψ a₀ g = b}.Finite)
    (G : localProjectiveGroup κ S a₀ ≃* localProjectiveGroup κ S a₀)
    (hG : ∀ g, localGroupBlock κ S ψ a₀ (G g) = D.symm (localGroupBlock κ S ψ a₀ g))
    (J : localProjectiveGroup κ S a₀ ≃* localProjectiveGroup κ S a)
    (hJ : ∀ g, localGroupBlock κ S ψ a (J g) = localGroupBlock κ S ψ a₀ g)
    (e : {q // (a,q) ∈ S} ≃ localProjectiveGroup κ S a)
    (he : ∀ q, (e q).val = HilbertCode.projective a q.val)
    (hχ : ProjectiveCharacters (κ a)
      (fun g : Additive (localProjectiveGroup κ S a) => projectiveCharacter (κ a) g.toMul.val))
    {μ : Measure X} [IsProbabilityMeasure μ]
    (x : Y → X) (hx : MeasurePreserving x (κ a) μ)
    (t : ℕ → X → X) (ht : ∀ m, MeasurePreserving (t m) μ μ)
    (htadd : ∀ c d z, t (c+d) z = t d (t c z))
    (hmix : ∀ A B : Set X, MeasurableSet A → MeasurableSet B →
      Tendsto (fun m => μ (A ∩ t m ⁻¹' B)) atTop (𝓝 (μ A * μ B)))
    (α : X → A) (hα : Measurable α) (v : A → ℂ)
    (hcenter : ∫ z, v (α z) ∂μ = 0)
    (hH : Tendsto (fun n : ℕ => wordEntropy (η := μ) (fun m z => α (t m z)) n / n)
      atTop (𝓝 0))
    (R : Y → Y) (f : Y → ℂ) (hf : ∀ n y, f ((R^[n]) y) = v (α (t n (x y))))
include hb hG hJ he hχ hx ht htadd hmix hα hcenter hH hf in
lemma local_moving_cancellation :
    Tendsto (fun N : ℕ => (N : ℝ)⁻¹ * ∑ n ∈ Finset.range N,
      (E.restrictLevel ψ hψ ((D.symm^[n]) b)).fibreSum
        (absoluteCoefficient κ (f ∘ R^[n])) a) atTop (𝓝 0) := by
  sorry
end

end Rokhlin

end

end OAI
end