@[simp]

theorem MeasureTheory.hittingBtwn_self {ι : Type u_1} {Ω : Type u_2} {β : Type u_3} [ConditionallyCompletePartialOrderInf ι] (f : ι → Ω → β) (s : Set β) (n : ι) (ω : Ω) : hittingBtwn f s n n ω = n

theorem MeasureTheory.hittingBtwn_congr {Ω : Type u_2} {f g : ℕ → Ω → ℝ} {s : Set ℝ} (h : ∀ (i : ℕ) (ω : Ω), f i ω ∈ s ↔ g i ω ∈ s) (n m : ℕ) : hittingBtwn f s n m = hittingBtwn g s n m

hittingBtwn only depends on the hitting predicate.

theorem MeasureTheory.upperCrossingTime_congr {Ω : Type u_2} {f g : ℕ → Ω → ℝ} {a b : ℝ} {N : ℕ} (hIic : ∀ (i : ℕ) (ω : Ω), f i ω ≤ a ↔ g i ω ≤ a) (hIci : ∀ (i : ℕ) (ω : Ω), b ≤ f i ω ↔ b ≤ g i ω) (n : ℕ) : upperCrossingTime a b f N n = upperCrossingTime a b g N n

Upper crossing times only depend on the position of the process relative to a and b.

theorem MeasureTheory.lowerCrossingTime_congr {Ω : Type u_2} {f g : ℕ → Ω → ℝ} {a b : ℝ} {N : ℕ} (hIic : ∀ (i : ℕ) (ω : Ω), f i ω ≤ a ↔ g i ω ≤ a) (hIci : ∀ (i : ℕ) (ω : Ω), b ≤ f i ω ↔ b ≤ g i ω) (n : ℕ) : lowerCrossingTime a b f N n = lowerCrossingTime a b g N n

Lower crossing times only depend on the position of the process relative to a and b.

theorem MeasureTheory.upcrossingStrat_congr {Ω : Type u_2} {f g : ℕ → Ω → ℝ} {a b : ℝ} {N : ℕ} (hIic : ∀ (i : ℕ) (ω : Ω), f i ω ≤ a ↔ g i ω ≤ a) (hIci : ∀ (i : ℕ) (ω : Ω), b ≤ f i ω ↔ b ≤ g i ω) (n : ℕ) : upcrossingStrat a b f N n = upcrossingStrat a b g N n

theorem MeasureTheory.upcrossingsBefore_congr {Ω : Type u_2} {f g : ℕ → Ω → ℝ} {a b : ℝ} {N : ℕ} {ω : Ω} (hIic : ∀ (i : ℕ) (ω : Ω), f i ω ≤ a ↔ g i ω ≤ a) (hIci : ∀ (i : ℕ) (ω : Ω), b ≤ f i ω ↔ b ≤ g i ω) : upcrossingsBefore a b f N ω = upcrossingsBefore a b g N ω

theorem MeasureTheory.upcrossingStrat_eq_zero_or_one {Ω : Type u_2} (a b : ℝ) (f : ℕ → Ω → ℝ) (N n : ℕ) (ω : Ω) : upcrossingStrat a b f N n ω = 0 ∨ upcrossingStrat a b f N n ω = 1

upcrossingStrat takes only the values 0 and 1.

theorem MeasureTheory.mul_upcrossingsBefore_le_sum_add_posPart {Ω : Type u_2} {f : ℕ → Ω → ℝ} {a b : ℝ} {N : ℕ} {ω : Ω} (hab : a < b) : (b - a) * ↑(upcrossingsBefore a b f N ω) ≤ ∑ k ∈ Finset.range N, upcrossingStrat a b f N k ω * (f (k + 1) - f k) ω + (a - f N ω)⁺

Pathwise upcrossing inequality with correction term: unlike MeasureTheory.mul_upcrossingsBefore_le, this requires no assumption a ≤ f N ω, at the price of the extra term max (a - f N ω) 0.

theorem MeasureTheory.upcrossingsBefore_lt_of_exists_upcrossing' {Ω : Type u_2} {f : ℕ → Ω → ℝ} {a b : ℝ} {N : ℕ} {ω : Ω} (hab : a < b) {N₁ N₂ : ℕ} (hN₁ : N ≤ N₁) (hN₁' : f N₁ ω ≤ a) (hN₂ : N₁ ≤ N₂) (hN₂' : b ≤ f N₂ ω) : upcrossingsBefore a b f N ω < upcrossingsBefore a b f (N₂ + 1) ω

Non-strict variant of MeasureTheory.upcrossingsBefore_lt_of_exists_upcrossing: since the lower crossing hits Set.Iic a and the upper crossing hits Set.Ici b, it suffices that the levels are reached (f N₁ ω ≤ a and b ≤ f N₂ ω) rather than strictly crossed. The Mathlib proof already only uses the non-strict forms internally.

theorem MeasureTheory.le_upcrossingsBefore_of_alternating {Ω : Type u_2} {f : ℕ → Ω → ℝ} {a b : ℝ} {N : ℕ} {ω : Ω} (hab : a < b) {m : ℕ} {c : ℕ → ℕ} (hmono : ∀ (i : ℕ), i + 1 < 2 * m → c i < c (i + 1)) (hN : ∀ i < 2 * m, c i < N) (ha : ∀ i < m, f (c (2 * i)) ω ≤ a) (hb : ∀ i < m, b ≤ f (c (2 * i + 1)) ω) : m ≤ upcrossingsBefore a b f N ω

Alternations force upcrossings: if there are m pairs of (strictly increasing) times below N at which f is alternately at most a and at least b, then f has at least m upcrossings of [a, b] before N.

theorem MeasureTheory.exists_alternating_of_le_upcrossingsBefore {Ω : Type u_2} {f : ℕ → Ω → ℝ} {a b : ℝ} {N : ℕ} {ω : Ω} (hab : a < b) {m : ℕ} (hm : m ≤ upcrossingsBefore a b f N ω) : ∃ (c : ℕ → ℕ), (∀ (i : ℕ), i + 1 < 2 * m → c i < c (i + 1)) ∧ (∀ i < 2 * m, c i < N) ∧ (∀ i < m, f (c (2 * i)) ω ≤ a) ∧ ∀ i < m, b ≤ f (c (2 * i + 1)) ω

Converse of le_upcrossingsBefore_of_alternating: if f has at least m upcrossings of [a, b] before N, then there is a strictly increasing sequence of 2 * m times below N at which f is alternately at most a (at even positions) and at least b (at odd positions). The times are the lower/upper crossing times.