Documentation

TauCeti.Probability.Process.DisjointWindow

Expanding a product of averages over disjoint windows #

Writing window N i j = (i + 1) * N + j for the i-th block of N consecutive indices, a product of block averages over these windows expands as an average of products over tuples:

โˆ i, blockAverage (Y i) (window N i) = ๐”ผ js, โˆ i, Y i (window N i (js i))

Two facts make this the right shape for the block factorization.

The expansion is exact. It is Fintype.prod_sum together with the normalisation (N ^ m)โปยน = โˆ i, (N : โ„)โปยน, so no error term appears.

Every tuple is an injective selection. The windows are pairwise disjoint โ€” window N i j < window N i' j' whenever i < i' and j < N โ€” so distinct coordinates of a tuple, whose entries are indices in Fin N, always carry distinct indices (window_selection_injective). This is what removes the diagonal terms that an expansion over a single window would produce, and it is why the factorization can apply a contractability argument to every term of the average without exception.

The moving selection #

The same windows also appear as a moving selection, in the shape the Lยฒ convergence theorems quantify over: disjointWindow c is the family n โ†ฆ (j โ†ฆ window (n + 1) c j), so at each length factor c reads [(c + 1)(n + 1), (c + 2)(n + 1)). Two facts make it usable there โ€” disjointWindow_injective at each length, with disjointWindow_eventually_injective the eventual form those theorems take, and disjointWindow_ne for disjointness across factors.

That combination is what fixed starts cannot supply: windows from two distinct fixed starts overlap once the common length exceeds the gap between the starts, whereas these move outward as the length grows. The generic fixed-start selection is fixedStart in Process/BlockAverage.lean.

References #

Nothing here involves a measure or the Lยฒ theory: the module is index arithmetic plus block-average algebra, which is why it sits with the process API rather than under Exchangeability/L2/.

References #

source
def TauCeti.Probability.window (N i j : โ„•) :
โ„•

The i-th window of N consecutive indices, starting after the first (i + 1) * N of them. Shifting past (i + 1) * N rather than i * N keeps the windows disjoint from each other and from the first N indices.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.Probability.window_def (N i j : โ„•) :
    window N i j = (i + 1) * N + j
    source
    theorem TauCeti.Probability.lt_window {N i j j' : โ„•} (hj : j < N) :
    j < window N i j'

    The windows sit above the initial block. Every window index exceeds every index of the first N coordinates, so an initial selection and a window selection never collide.

    source
    theorem TauCeti.Probability.window_lt_window {N i i' j j' : โ„•} (hj : j < N) (hi : i < i') :
    window N i j < window N i' j'

    The windows are ordered. An index inside window i precedes every index of any later window i', provided the offset j stays inside the window.

    source
    theorem TauCeti.Probability.window_selection_strictMono {m N : โ„•} (js : Fin m โ†’ Fin N) :
    StrictMono fun (i : Fin m) => window N โ†‘i โ†‘(js i)

    A tuple reads the windows in order. Reading factor i at position js i of its own window gives a strictly monotone selection: the windows are ordered, so the factor index alone decides the order, whatever position each factor reads.

    source
    theorem TauCeti.Probability.window_selection_injective {m N : โ„•} (js : Fin m โ†’ Fin N) :
    Function.Injective fun (i : Fin m) => window N โ†‘i โ†‘(js i)

    Distinct coordinates of a tuple land in distinct windows. Since the windows are pairwise disjoint, the selection i โ†ฆ window N i (js i) is injective for every tuple js โ€” immediate from window_selection_strictMono.

    source
    theorem TauCeti.Probability.prod_blockAverage_window_eq_expect {ฮฉ : Type u_1} {m N : โ„•} (Y : Fin m โ†’ โ„• โ†’ ฮฉ โ†’ โ„) (ฯ‰ : ฮฉ) :
    โˆ i : Fin m, blockAverage (Y i) (fun (j : Fin N) => window N โ†‘i โ†‘j) ฯ‰ = Finset.univ.expect fun (js : Fin m โ†’ Fin N) => โˆ i : Fin m, Y i (window N โ†‘i โ†‘(js i)) ฯ‰

    The disjoint-window instance. This specialises prod_blockAverage_eq_expect, imported from Process/BlockAverage.lean, to the windows window N i, where every tuple is an injective selection by window_selection_injective.

    The disjoint-window selection #

    The moving selection a block factorization needs: at each length, distinct factors read disjoint windows. The generic fixed-start selection lives with blockAverage in Probability/Process/BlockAverage.lean.

    source
    def TauCeti.Probability.disjointWindow (c n : โ„•) :
    Fin (n + 1) โ†’ โ„•

    The disjoint-window selection: at length n + 1, factor c reads the window window (n + 1) c, occupying [(c + 1)(n + 1), (c + 2)(n + 1)).

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.Probability.disjointWindow_apply (c n : โ„•) (j : Fin (n + 1)) :
      disjointWindow c n j = window (n + 1) c โ†‘j
      source
      theorem TauCeti.Probability.disjointWindow_injective (c n : โ„•) :
      Function.Injective (disjointWindow c n)

      Each disjoint window is an injective selection at each length.

      source
      theorem TauCeti.Probability.disjointWindow_eventually_injective (c : โ„•) :
      โˆ€แถ  (n : โ„•) in Filter.atTop, Function.Injective (disjointWindow c n)

      The eventual form, as the moving-selection theorems take it.

      source
      theorem TauCeti.Probability.disjointWindow_ne {c c' : โ„•} (h : c โ‰  c') (n : โ„•) (j j' : Fin (n + 1)) :
      disjointWindow c n j โ‰  disjointWindow c' n j'

      Distinct factors never collide. The windows of two different factors are disjoint at every length, which is exactly what fixed starts cannot provide.