AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicGlobalHorizon

- Index in the original integer-horizon ladder corresponding to horizon `2^k`.

def dyadicGlobalIndex (k : ℕ) : ℕ := 2 ^ k - 1

/-- The corresponding positive dyadic horizon. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicGlobalHorizon.lean:35published source at 7bcd37294df1

- The corresponding positive dyadic horizon.

def dyadicHorizon (k : ℕ) : ℝ≥0 := (2 ^ k : ℕ)

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicGlobalHorizon.lean:38published source at 7bcd37294df1

No declaration docstring.

@[simp] theorem dyadicGlobalIndex_add_one (k : ℕ) :
    dyadicGlobalIndex k + 1 = 2 ^ k := by
  have hpos : 0 < 2 ^ k := by positivity
  simp only [dyadicGlobalIndex]
  omega

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicGlobalHorizon.lean:40published source at 7bcd37294df1

No declaration docstring.

@[simp] theorem integerHorizon_dyadicGlobalIndex (k : ℕ) :
    integerHorizon (dyadicGlobalIndex k) = dyadicHorizon k := by
  simp [integerHorizon, dyadicHorizon, dyadicGlobalIndex_add_one]

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicGlobalHorizon.lean:46published source at 7bcd37294df1

No declaration docstring.

@[simp] theorem dyadicHorizon_pos (k : ℕ) : 0 < dyadicHorizon k := by
  simp [dyadicHorizon]

/-- The dyadic subsequence indices are monotone. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicGlobalHorizon.lean:50published source at 7bcd37294df1

- The dyadic subsequence indices are monotone.

theorem dyadicGlobalIndex_mono : Monotone dyadicGlobalIndex := by
  intro k l hkl
  have hp : 2 ^ k ≤ 2 ^ l := Nat.pow_le_pow_right (by decide) hkl
  exact Nat.sub_le_sub_right hp 1

/-- The dyadic subsequence is cofinal in the natural-number index set. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicGlobalHorizon.lean:54published source at 7bcd37294df1

- The dyadic subsequence is cofinal in the natural-number index set.

theorem dyadicGlobalIndex_ge_self (k : ℕ) : k ≤ dyadicGlobalIndex k := by
  have hpow : k < 2 ^ k := Nat.lt_two_pow_self
  simp only [dyadicGlobalIndex]
  omega

/-- Topological cofinality of `k ↦ 2^k - 1`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicGlobalHorizon.lean:60published source at 7bcd37294df1

- Topological cofinality of `k ↦ 2^k - 1`.

theorem tendsto_dyadicGlobalIndex_atTop :
    Tendsto dyadicGlobalIndex atTop atTop := by
  apply tendsto_atTop.2
  intro N
  filter_upwards [eventually_ge_atTop N] with k hk
  exact hk.trans (dyadicGlobalIndex_ge_self k)

/-- The global canonical localizer restricted to dyadic horizons. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicGlobalHorizon.lean:66published source at 7bcd37294df1

- The global canonical localizer restricted to dyadic horizons.

noncomputable def dyadicGlobalLocalizingTime
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2Integrand filtration mu)
    (k : ℕ) (omega : Omega) : ℝ≥0 :=
  globalLocalizingTime hUsual eta (dyadicGlobalIndex k) omega

/-- Every member of the dyadic subsequence remains a Chewi stopping time. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicGlobalHorizon.lean:74published source at 7bcd37294df1

- Every member of the dyadic subsequence remains a Chewi stopping time.

theorem dyadicGlobalLocalizingTime_isChewiStoppingTime
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2Integrand filtration mu) (k : ℕ) :
    IsChewiStoppingTime filtration
      (fun omega =>
        (dyadicGlobalLocalizingTime hUsual eta k omega : WithTop ℝ≥0)) := by
  exact globalLocalizingTime_isChewiStoppingTime hUsual eta (dyadicGlobalIndex k)

/-- The dyadic global localizers are pointwise increasing. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicGlobalHorizon.lean:81published source at 7bcd37294df1

- The dyadic global localizers are pointwise increasing.

theorem dyadicGlobalLocalizingTime_mono
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2Integrand filtration mu) :
    Monotone (fun k => dyadicGlobalLocalizingTime hUsual eta k) := by
  intro k l hkl
  exact globalLocalizingTime_mono hUsual eta (dyadicGlobalIndex_mono hkl)

/-- The `k`-th dyadic global localizer is bounded by the matching horizon
`2^k`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicGlobalHorizon.lean:90published source at 7bcd37294df1

- The `k`-th dyadic global localizer is bounded by the matching horizon `2^k`.

theorem dyadicGlobalLocalizingTime_le_horizon
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2Integrand filtration mu)
    (k : ℕ) (omega : Omega) :
    dyadicGlobalLocalizingTime hUsual eta k omega ≤ dyadicHorizon k := by
  simpa only [dyadicGlobalLocalizingTime, integerHorizon_dyadicGlobalIndex] using
    globalLocalizingTime_le_horizon hUsual eta (dyadicGlobalIndex k) omega

/-- The cofinal dyadic subsequence still tends to infinity almost surely. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicGlobalHorizon.lean:99published source at 7bcd37294df1

- The cofinal dyadic subsequence still tends to infinity almost surely.

theorem dyadicGlobalLocalizingTime_tendsto_top_ae
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2Integrand filtration mu) :
    ∀ᵐ omega ∂mu,
      Tendsto
        (fun k =>
          (dyadicGlobalLocalizingTime hUsual eta k omega : WithTop ℝ≥0))
        atTop (𝓝 (⊤ : WithTop ℝ≥0)) := by
  filter_upwards [globalLocalizingTime_tendsto_top_ae hUsual eta]
    with omega homega
  exact homega.comp tendsto_dyadicGlobalIndex_atTop

end DyadicGlobalHorizon
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicGlobalHorizon.lean:108published source at 7bcd37294df1