StationaryCuts.lean`

58 declarations, 0 contain sorry, 0 declared as axioms

def OAI.FKCRT.CutOutput.firstIndex line 11
Source documentation
Totalized first index; on nonempty predicates this is the ordinary least index.
```
def firstIndex (p : ℕ → Prop) : ℕ := by
…
```
lemma OAI.FKCRT.CutOutput.firstIndex_spec line 17
lemma OAI.FKCRT.CutOutput.firstIndex_le line 21
lemma OAI.FKCRT.CutOutput.firstIndex_measurable line 24
structure OAI.FKCRT.CutOutput.Data line 34
def OAI.FKCRT.CutOutput.left line 42
def OAI.FKCRT.CutOutput.right line 43
def OAI.FKCRT.CutOutput.output line 44
lemma OAI.FKCRT.CutOutput.Data.output_eq_get line 47
lemma OAI.FKCRT.CutOutput.Data.output_segment line 94
lemma OAI.FKCRT.CutOutput.output_translate line 104
lemma OAI.FKCRT.CutOutput.output_measurable line 123

def OAI.FKCRT.Stationary.maxSum line 147

Source documentation

The nonnegative running maximum of the partial sums of a stationary observable.

def maxSum (T : Ω → Ω) (f : Ω → ℝ) : ℕ → Ω → ℝ
  | 0, _ => 0
  | n+1,x => max 0 (f x+maxSum T f n (T x))

omit [MeasurableSpace Ω] in

lemma OAI.FKCRT.Stationary.maxSum_nonneg line 152
lemma OAI.FKCRT.Stationary.maxSum_mono line 157
lemma OAI.FKCRT.Stationary.measurable_maxSum line 163
lemma OAI.FKCRT.Stationary.integrable_maxSum line 169
lemma OAI.FKCRT.Stationary.maxSum_bound_sum line 176
lemma OAI.FKCRT.Stationary.integral_on_maxSum_nonneg line 193
Source documentation
Finite maximal ergodic inequality. In particular no independence of the observations is used in the maximal step.
```
lemma integral_on_maxSum_nonneg {T : Ω → Ω} {f : Ω → ℝ}
    (hT : MeasurePreserving T μ μ) (hf : Integrable f μ) (hm : Measurable f) (n : ℕ) :
    0 ≤ ∫ x in {x | 0 < maxSum T f n x},f x ∂μ := by
…
```
Mentions: OAI.FKCRT.Stationary.maxSum
lemma OAI.FKCRT.Stationary.finite_maximal_bound line 227

lemma OAI.FKCRT.Stationary.maximal_bound line 244

Source documentation

Hopf's stationary maximal bound, for a nonnegative integrable observable.

lemma maximal_bound {T : Ω → Ω} {U : Ω → ℝ}
    (hT : MeasurePreserving T μ μ) (hU : Integrable U μ) (hm : Measurable U)
    (hpos : ∀ x,0 ≤ U x) (η : ℝ) (hη : 0 < η) :
    μ {x | ∃ n : ℕ,(n:ℝ)*η < ∑ i∈Finset.range n,U (T^[i] x)} ≤
      ENNReal.ofReal ((∫ x,U x ∂μ)/η) := by
…

def OAI.FKCRT.Stationary.average line 270
lemma OAI.FKCRT.Stationary.measurable_average line 273
lemma OAI.FKCRT.Stationary.average_sub line 278
lemma OAI.FKCRT.Stationary.maximal_abs_average_bound line 282

theorem OAI.FKCRT.Stationary.ae_average_limit_of_L1_approx line 311

Source documentation

The stationary maximal inequality makes almost-sure convergence of averages stable under L¹ approximation.

theorem ae_average_limit_of_L1_approx {T : Ω → Ω} {f : Ω → ℝ} {g : ℕ → Ω → ℝ}
    {m : ℝ} {a : ℕ → ℝ} (hT : MeasurePreserving T μ μ)
    (hf : Integrable f μ) (hmf : Measurable f)
    (hg : ∀ k,Integrable (g k) μ) (hmg : ∀ k,Measurable (g k))
    (happrox : Tendsto (fun k => ∫ x,|f x-g k x| ∂μ) atTop (𝓝 0))
    (ha : Tendsto a atTop (𝓝 m))
    (hgood : ∀ k,∀ᵐ x ∂μ,Tendsto (fun n => average T (g k) n x) atTop (𝓝 (a k))) :
    ∀ᵐ x ∂μ,Tendsto (fun n => average T f n x) atTop (𝓝 m) := by
…

Mentions: OAI.FKCRT.Stationary.average

lemma OAI.FKCRT.Stationary.linear_remainder_of_ratio line 369
lemma OAI.FKCRT.Stationary.ratio_limit_of_linear_remainder line 384

lemma OAI.FKCRT.Stationary.ratio_limit_of_multiples line 400

Source documentation

Monotonicity fills the bounded gaps between a fixed arithmetic subsequence.

lemma ratio_limit_of_multiples {S : ℕ → ℝ} (hS : Monotone S) (r : ℕ) (hr : 0 < r)
    (m : ℝ) (ht : Tendsto (fun q => S (r*q)/(q:ℝ)) atTop (𝓝 ((r:ℝ)*m))) :
    Tendsto (fun n => S n/(n:ℝ)) atTop (𝓝 m) := by
…

lemma OAI.FKCRT.Stationary.sum_range_blocks line 442
lemma OAI.FKCRT.Stationary.interlaced_nonneg_limit line 455
def OAI.FKCRT.Stationary.seqLaw line 476
instance OAI.FKCRT.Stationary.seqLaw_probability line 478
def OAI.FKCRT.Stationary.shift line 482
lemma OAI.FKCRT.Stationary.measurable_shift line 484
lemma OAI.FKCRT.Stationary.shift_preserving line 487
lemma OAI.FKCRT.Stationary.shift_add line 493
lemma OAI.FKCRT.Stationary.shift_iterate line 497
def OAI.FKCRT.Stationary.coords line 502
lemma OAI.FKCRT.Stationary.coords_mono line 505
lemma OAI.FKCRT.Stationary.coords_le line 512
lemma OAI.FKCRT.Stationary.measurable_shift_coords line 515
lemma OAI.FKCRT.Stationary.indep_coords line 527
def OAI.FKCRT.Stationary.window line 532
lemma OAI.FKCRT.Stationary.window_mono line 534
lemma OAI.FKCRT.Stationary.window_disjoint line 539
lemma OAI.FKCRT.Stationary.finite_window_progression_indep line 554
lemma OAI.FKCRT.Stationary.finite_window_progression_limit line 564
lemma OAI.FKCRT.Stationary.finite_window_nonneg_limit line 582
lemma OAI.FKCRT.Stationary.finite_window_limit line 594
def OAI.FKCRT.Stationary.windowFiltration line 618
lemma OAI.FKCRT.Stationary.windowFiltration_sup line 623

theorem OAI.FKCRT.Stationary.iid_shift_strong_law line 644

Source documentation

Stationary averages of any integrable observation of a two-sided iid sequence, not just cylinder observations.

theorem iid_shift_strong_law (ν : Measure α) [IsProbabilityMeasure ν]
    {f : (ℤ → α) → ℝ} (hf : Measurable f) (hint : Integrable f (seqLaw ν)) :
    ∀ᵐ x ∂seqLaw ν,Tendsto (fun n => average (shift 1) f n x) atTop
      (𝓝 (∫ x,f x ∂seqLaw ν)) := by
…

Mentions: OAI.FKCRT.Stationary.seqLaw, OAI.FKCRT.Stationary.average, OAI.FKCRT.Stationary.shift

def OAI.FKCRT.Stationary.reflect line 672
lemma OAI.FKCRT.Stationary.measurable_reflect line 673
lemma OAI.FKCRT.Stationary.reflect_preserving line 675
lemma OAI.FKCRT.Stationary.reflected_shift_iterate line 679
theorem OAI.FKCRT.Stationary.iid_reverse_shift_strong_law line 689