LeanPool.PointwiseBirkhoff.Main

def LeanPool.PointwiseBirkhoff.birkhoffMax {α : Type u_1} (f : α → α) (φ : α → ℝ) : ℕ →o α → ℝ

The maximum of birkhoffSum f φ i for i ranging from 1 to n + 1.

Equations

• LeanPool.PointwiseBirkhoff.birkhoffMax f φ = partialSups (birkhoffSum f φ ∘ Nat.succ)

theorem LeanPool.PointwiseBirkhoff.birkhoffMax_succ {ι✝ : Type u_2} {f : ι✝ → ι✝} {φ : ι✝ → ℝ} {x : ι✝} {n : ℕ} : (birkhoffMax f φ) n.succ x = φ x + max 0 ((birkhoffMax f φ) n (f x))

@[reducible, inline]

abbrev LeanPool.PointwiseBirkhoff.birkhoffMaxDiff {α : Type u_1} (f : α → α) (φ : α → ℝ) (n : ℕ) (x : α) : ℝ

The one-step difference between consecutive Birkhoff maxima along the orbit.

Equations

• LeanPool.PointwiseBirkhoff.birkhoffMaxDiff f φ n x = (LeanPool.PointwiseBirkhoff.birkhoffMax f φ) (n + 1) x - (LeanPool.PointwiseBirkhoff.birkhoffMax f φ) n (f x)

theorem LeanPool.PointwiseBirkhoff.birkhoffMaxDiff_aux {α✝ : Type u_2} {f : α✝ → α✝} {φ : α✝ → ℝ} {n : ℕ} {x : α✝} : birkhoffMaxDiff f φ n x = φ x - min 0 ((birkhoffMax f φ) n (f x))

theorem LeanPool.PointwiseBirkhoff.birkhoffMaxDiff_antitone {ι✝ : Type u_2} {f : ι✝ → ι✝} {φ : ι✝ → ℝ} : Antitone (birkhoffMaxDiff f φ)

theorem LeanPool.PointwiseBirkhoff.birkhoffSum_measurable {α : Type u_1} {n : ℕ} [MeasurableSpace α] {f : α → α} (hf : Measurable f) {φ : α → ℝ} (hφ : Measurable φ) : Measurable (birkhoffSum f φ n)

theorem LeanPool.PointwiseBirkhoff.birkhoffMax_measurable {α : Type u_1} {n : ℕ} [MeasurableSpace α] {f : α → α} (hf : Measurable f) {φ : α → ℝ} (hφ : Measurable φ) : Measurable ((birkhoffMax f φ) n)

noncomputable def LeanPool.PointwiseBirkhoff.birkhoffSup {α : Type u_2} (f : α → α) (φ : α → ℝ) (x : α) : EReal

The supremum of birkhoffSum f φ (n + 1) x over n : ℕ.

Equations

• LeanPool.PointwiseBirkhoff.birkhoffSup f φ x = ⨆ (n : ℕ), ↑(birkhoffSum f φ (n + 1) x)

theorem LeanPool.PointwiseBirkhoff.birkhoffSup_measurable {α : Type u_2} [msα : MeasurableSpace α] {f : α → α} (hf : Measurable f) {φ : α → ℝ} (hφ : Measurable φ) : Measurable (birkhoffSup f φ)

def LeanPool.PointwiseBirkhoff.divergentSet {α : Type u_2} (f : α → α) (φ : α → ℝ) : Set α

The set of points x for which birkhoffSup f φ x = ⊤.

Equations

• LeanPool.PointwiseBirkhoff.divergentSet f φ = LeanPool.PointwiseBirkhoff.birkhoffSup f φ ⁻¹' {⊤}

theorem LeanPool.PointwiseBirkhoff.divergentSet_invariant {α✝ : Type u_3} {f : α✝ → α✝} {φ : α✝ → ℝ} {x : α✝} : f x ∈ divergentSet f φ ↔ x ∈ divergentSet f φ

theorem LeanPool.PointwiseBirkhoff.divergentSet_measurable {α : Type u_2} [msα : MeasurableSpace α] {f : α → α} (hf : Measurable f) {φ : α → ℝ} (hφ : Measurable φ) : MeasurableSet (divergentSet f φ)

theorem LeanPool.PointwiseBirkhoff.divergentSet_mem_invalg {α : Type u_2} [msα : MeasurableSpace α] {f : α → α} (hf : Measurable f) {φ : α → ℝ} (hφ : Measurable φ) : MeasurableSet (divergentSet f φ)

theorem LeanPool.PointwiseBirkhoff.birkhoffMax_tendsto_top_mem_divergentSet {α✝ : Type u_3} {f : α✝ → α✝} {φ : α✝ → ℝ} {x : α✝} (hx : x ∈ divergentSet f φ) : Filter.Tendsto (fun (x_1 : ℕ) => (birkhoffMax f φ) x_1 x) Filter.atTop Filter.atTop

theorem LeanPool.PointwiseBirkhoff.birkhoffMaxDiff_tendsto_of_mem_divergentSet {α✝ : Type u_3} {f : α✝ → α✝} {φ : α✝ → ℝ} {x : α✝} (hx : x ∈ divergentSet f φ) : Filter.Tendsto (fun (x_1 : ℕ) => birkhoffMaxDiff f φ x_1 x) Filter.atTop (nhds (φ x))

@[reducible, inline]

abbrev LeanPool.PointwiseBirkhoff.nonneg : Filter ℝ

The filter on real numbers approaching the non-positive half-line from above.

Equations

• LeanPool.PointwiseBirkhoff.nonneg = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal (Set.Iio ε)

theorem LeanPool.PointwiseBirkhoff.birkhoffAverage_tendsto_nonpos_of_not_mem_divergentSet {α✝ : Type u_3} {f : α✝ → α✝} {φ : α✝ → ℝ} {x : α✝} (hx : x ∉ divergentSet f φ) : Filter.Tendsto (fun (x_1 : ℕ) => birkhoffAverage ℝ f φ x_1 x) Filter.atTop nonneg

theorem LeanPool.PointwiseBirkhoff.iterates_integrable {α : Type u_2} [msα : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → α} {φ : α → ℝ} {i : ℕ} (hf : MeasureTheory.MeasurePreserving f μ μ) (hφ : MeasureTheory.Integrable φ μ) : MeasureTheory.Integrable (φ ∘ f^[i]) μ

theorem LeanPool.PointwiseBirkhoff.birkhoffSum_integrable {α : Type u_2} [msα : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → α} {φ : α → ℝ} {n : ℕ} (hf : MeasureTheory.MeasurePreserving f μ μ) (hφ : MeasureTheory.Integrable φ μ) : MeasureTheory.Integrable (birkhoffSum f φ n) μ

theorem LeanPool.PointwiseBirkhoff.birkhoffMax_integrable {α : Type u_2} [msα : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → α} {φ : α → ℝ} {n : ℕ} (hf : MeasureTheory.MeasurePreserving f μ μ) (hφ : MeasureTheory.Integrable φ μ) : MeasureTheory.Integrable ((birkhoffMax f φ) n) μ

theorem LeanPool.PointwiseBirkhoff.birkhoffMaxDiff_integrable {α : Type u_2} [msα : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → α} {φ : α → ℝ} {n : ℕ} (hf : MeasureTheory.MeasurePreserving f μ μ) (hφ : MeasureTheory.Integrable φ μ) : MeasureTheory.Integrable (birkhoffMaxDiff f φ n) μ

theorem LeanPool.PointwiseBirkhoff.int_birkhoffMaxDiff_in_divergentSet_tendsto {α : Type u_2} [msα : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → α} {φ : α → ℝ} (hf : MeasureTheory.MeasurePreserving f μ μ) (hφ : MeasureTheory.Integrable φ μ) (hφ' : Measurable φ) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α) in divergentSet f φ, birkhoffMaxDiff f φ n x ∂μ) Filter.atTop (nhds (∫ (x : α) in divergentSet f φ, φ x ∂μ))

theorem LeanPool.PointwiseBirkhoff.int_birkhoffMaxDiff_in_divergentSet_nonneg {α : Type u_2} [msα : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → α} {φ : α → ℝ} {n : ℕ} (hf : MeasureTheory.MeasurePreserving f μ μ) (hφ : MeasureTheory.Integrable φ μ) (hφ' : Measurable φ) : 0 ≤ ∫ (x : α) in divergentSet f φ, birkhoffMaxDiff f φ n x ∂μ

theorem LeanPool.PointwiseBirkhoff.int_in_divergentSet_nonneg {α : Type u_2} [msα : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → α} {φ : α → ℝ} (hf : MeasureTheory.MeasurePreserving f μ μ) (hφ : MeasureTheory.Integrable φ μ) (hφ' : Measurable φ) : 0 ≤ ∫ (x : α) in divergentSet f φ, φ x ∂μ

theorem LeanPool.PointwiseBirkhoff.nullMeasurableSpace_le {α : Type u_2} [msα : MeasurableSpace α] {μ : MeasureTheory.Measure α} : msα ≤ MeasureTheory.NullMeasurableSpace.instMeasurableSpace

theorem LeanPool.PointwiseBirkhoff.divergentSet_zero_meas_of_condexp_neg {α : Type u_2} [msα : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → α} {φ : α → ℝ} [hμ : MeasureTheory.IsProbabilityMeasure μ] (h : ∀ᵐ (x : α) ∂μ, μ[φ | MeasurableSpace.invariants f] x < 0) (hf : MeasureTheory.MeasurePreserving f μ μ) (hφ : MeasureTheory.Integrable φ μ) (hφ' : Measurable φ) : μ (divergentSet f φ) = 0

theorem LeanPool.PointwiseBirkhoff.limsup_birkhoffAverage_nonpos_of_condexp_neg {α : Type u_2} [msα : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → α} {φ : α → ℝ} [hμ : MeasureTheory.IsProbabilityMeasure μ] (hf : MeasureTheory.MeasurePreserving f μ μ) (hφ : MeasureTheory.Integrable φ μ) (hφ' : Measurable φ) (h : ∀ᵐ (x : α) ∂μ, μ[φ | MeasurableSpace.invariants f] x < 0) : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (x_1 : ℕ) => birkhoffAverage ℝ f φ x_1 x) Filter.atTop nonneg

noncomputable def LeanPool.PointwiseBirkhoff.invCondexp {α : Type u_2} [msα : MeasurableSpace α] (μ : MeasureTheory.Measure α) (f : α → α) (φ : α → ℝ) : α → ℝ

Conditional expectation of an observable onto the invariant measurable space of f.

Equations

• LeanPool.PointwiseBirkhoff.invCondexp μ f φ = μ[φ | MeasurableSpace.invariants f]

theorem LeanPool.PointwiseBirkhoff.birkhoffErgodicTheorem_aux {α : Type u_2} [msα : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → α} {φ : α → ℝ} [hμ : MeasureTheory.IsProbabilityMeasure μ] {ε : ℝ} (hε : 0 < ε) (hf : MeasureTheory.MeasurePreserving f μ μ) (hφ : MeasureTheory.Integrable φ μ) (hφ' : Measurable φ) : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (x_1 : ℕ) => birkhoffAverage ℝ f φ x_1 x - (invCondexp μ f φ x + ε)) Filter.atTop nonneg

theorem LeanPool.PointwiseBirkhoff.birkhoffErgodicTheorem {α : Type u_2} [msα : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → α} {φ : α → ℝ} [hμ : MeasureTheory.IsProbabilityMeasure μ] (hf : MeasureTheory.MeasurePreserving f μ μ) (hφ : MeasureTheory.Integrable φ μ) (hφ' : Measurable φ) : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (x_1 : ℕ) => birkhoffAverage ℝ f φ x_1 x) Filter.atTop (nhds (invCondexp μ f φ x))

This is the main result but assuming Measurable φ.

theorem LeanPool.PointwiseBirkhoff.birkhoffErgodicTheorem' {α : Type u_2} [msα : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → α} [hμ : MeasureTheory.IsProbabilityMeasure μ] {Φ : α → ℝ} (hf : MeasureTheory.MeasurePreserving f μ μ) (hΦ : MeasureTheory.Integrable Φ μ) : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (x_1 : ℕ) => birkhoffAverage ℝ f Φ x_1 x) Filter.atTop (nhds (invCondexp μ f Φ x))

Here we drop the assumption that the observable is Measurable.