MeasureTheory.Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part
theorem MeasureTheory.Submartingale.mul_integral_upcrossingsBefore_le_integral_pos_part :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ℕ → Ω → ℝ}
{ℱ : MeasureTheory.Filtration ℕ m0} [inst : MeasureTheory.IsFiniteMeasure μ] (a b : ℝ),
MeasureTheory.Submartingale f ℱ μ →
∀ (N : ℕ),
(b - a) * ∫ (x : Ω), ↑(MeasureTheory.upcrossingsBefore a b f N x) ∂μ ≤
∫ (x : Ω), (fun ω => (f N ω - a)⁺) x ∂μ
Doob's upcrossing estimate is a theorem in measure theory and martingale theory. Given a real valued discrete submartingale `f` and real values `a` and `b`, it states that the expected value of the number of times the process `f` crosses from below `a` to above `b` before the time `N`, multiplied by `(b - a)`, is less than or equal to the expected value of the positive part of `(f N - a)`. Here, the upcrossings are being counted using the function `upcrossingsBefore`. So, mathematically we can denote the theorem as: `(b - a) * 𝔼[upcrossingsBefore a b f N] ≤ 𝔼[(f N - a)⁺]`. This theorem is an important result in the theory of martingales and has applications in areas like probability theory and financial mathematics.
More concisely: The expected value of the number of upcrossings of a discrete submartingale from below a to above b before time N, multiplied by the difference between b and a, is less than or equal to the expected value of the positive part of the difference between the submartingale value at time N and a.
|
MeasureTheory.upperCrossingTime_le
theorem MeasureTheory.upperCrossingTime_le :
∀ {Ω : Type u_1} {ι : Type u_2} [inst : ConditionallyCompleteLinearOrderBot ι] {a b : ℝ} {f : ι → Ω → ℝ} {N : ι}
{n : ℕ} {ω : Ω}, MeasureTheory.upperCrossingTime a b f N n ω ≤ N
This theorem states that for any types Ω and ι, where ι is a conditionally complete linear order with a minimum element, given any two real numbers `a` and `b`, a function `f` mapping from ι × Ω to ℝ, a specific value `N` of type ι, a natural number `n`, and a specific value `ω` of type Ω, the upper crossing time of `f` at heights `a` and `b` with respect to `N`, `n`, and `ω` is always less than or equal to `N`. The upper crossing time is a concept from measure theory, indicating how much time a stochastic process spends above a certain level.
More concisely: For any type Ω with a minimum element, any conditionally complete linear order ι, any real-valued function f on ι × Ω, any value N ∈ ι, natural number n, and value ω ∈ Ω, the upper crossing time of f at heights a and b with respect to N, n, and ω is always less than or equal to N.
|
MeasureTheory.stoppedValue_upperCrossingTime
theorem MeasureTheory.stoppedValue_upperCrossingTime :
∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω},
MeasureTheory.upperCrossingTime a b f N (n + 1) ω ≠ N →
b ≤ MeasureTheory.stoppedValue f (MeasureTheory.upperCrossingTime a b f N (n + 1)) ω
The theorem `MeasureTheory.stoppedValue_upperCrossingTime` states that for any types `Ω`, real numbers `a` and `b`, a function `f` from natural numbers to a function from `Ω` to real numbers, natural numbers `N` and `n`, and an element `ω` of `Ω`, if the upper crossing time of `f` with respect to `a` and `b` at `N` and `n + 1` for `ω` is not equal to `N`, then `b` is less than or equal to the stopped value of `f` with respect to the upper crossing time of `f` with respect to `a` and `b` at `N` and `n + 1` for `ω`. In simpler terms, if `f` crosses the upper limit `b` after time `N`, the stopped value at the crossing time will be at least `b`.
More concisely: If the upper crossing time of function `f` with respect to `a` and `b` at `N` and `n+1` for `ω` is not equal to `N`, then the stopped value of `f` with respect to `a` and `b` at `N` and `n+1` for `ω` is greater than or equal to `b`.
|
MeasureTheory.upperCrossingTime_succ
theorem MeasureTheory.upperCrossingTime_succ :
∀ {Ω : Type u_1} {ι : Type u_2} [inst : Preorder ι] [inst_1 : OrderBot ι] [inst_2 : InfSet ι] {a b : ℝ}
{f : ι → Ω → ℝ} {N : ι} {n : ℕ} {ω : Ω},
MeasureTheory.upperCrossingTime a b f N (n + 1) ω =
MeasureTheory.hitting f (Set.Ici b)
(MeasureTheory.lowerCrossingTimeAux a f (MeasureTheory.upperCrossingTime a b f N n ω) N ω) N ω
The theorem `MeasureTheory.upperCrossingTime_succ` states that for any set of real numbers Ω, an ordered type ι with a least element (OrderBot) and an InfSet structure, a pair of real numbers `a` and `b`, a function `f` from ι and Ω to ℝ, a value `N` of type ι, a natural number `n` and an element `ω` of Ω, the upper crossing time of `f` at level `b` after time `N` and `n + 1` times at the point `ω` is equal to the first time `f` reaches or exceeds `b` after the first time `f` drops below `a` after the `n`-th upper crossing time of `f` at level `b` after time `N` at the point `ω` but before time `N`.
More concisely: For any function `f` from an ordered type `ι` and a set of real numbers `Ω` to ℝ, the `(n+1)`-th upper crossing time of `f` at level `b` after time `N` at point `ω` is the first time after the last upper crossing before `N` that `f(x) ≥ b` for some `x > N` such that `f(x) < a`, where `a ≤ b` and `N, ω ∈ Ω`.
|
MeasureTheory.upperCrossingTime_mono
theorem MeasureTheory.upperCrossingTime_mono :
∀ {Ω : Type u_1} {ι : Type u_2} [inst : ConditionallyCompleteLinearOrderBot ι] {a b : ℝ} {f : ι → Ω → ℝ} {N : ι}
{n m : ℕ} {ω : Ω},
n ≤ m → MeasureTheory.upperCrossingTime a b f N n ω ≤ MeasureTheory.upperCrossingTime a b f N m ω
This theorem states that for any types `Ω` and `ι`, with `ι` equipped with a conditionally complete linear order bot structure, any two real numbers `a` and `b`, any function `f` from `ι` and `Ω` to real numbers, any value `N` of type `ι`, any natural numbers `n` and `m`, and any value `ω` of type `Ω`, if `n` is less than or equal to `m`, then the upper crossing time of `f` with respect to `a`, `b`, `N`, and `n` at `ω` is less than or equal to the upper crossing time of `f` with respect to `a`, `b`, `N`, and `m` at `ω`. In mathematical terms, this says that the upper crossing time is monotonic with respect to the natural numbers `n` and `m`.
More concisely: For any function `f` from a conditionally complete linear order `(ι, ≤)` to the real numbers, and any `a`, `b` in the real numbers, `N` in `ι`, `n` and `m` natural numbers with `n ≤ m`, and `ω` in the domain of `f`, the upper crossing time of `f` with respect to `a`, `b`, `N`, and `n` at `ω` is less than or equal to the upper crossing time of `f` with respect to `a`, `b`, `N`, and `m` at `ω`.
|
MeasureTheory.stoppedValue_lowerCrossingTime
theorem MeasureTheory.stoppedValue_lowerCrossingTime :
∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω},
MeasureTheory.lowerCrossingTime a b f N n ω ≠ N →
MeasureTheory.stoppedValue f (MeasureTheory.lowerCrossingTime a b f N n) ω ≤ a
The theorem `MeasureTheory.stoppedValue_lowerCrossingTime` states that for any types `Ω`, real numbers `a` and `b`, a function `f` from natural numbers to a function from `Ω` to real numbers, and natural numbers `N` and `n`, and an element `ω` of `Ω`, if the `n`-th lower crossing time of `f` with respect to `a` and `b` before time `N` is not equal to `N`, then the stopped value of `f` at the `n`-th lower crossing time for `ω` is less than or equal to `a`. In simpler terms, it is saying that if a function crosses a certain high value and then dips below a certain low value before a specified time, the value of the function at the time it first dips below the low value (provided this time is not the end time) will indeed be less than or equal to the low value.
More concisely: If the function `f` from natural numbers to real functions on type `Ω` does not have its `n`-th lower crossing time equal to `N` before time `N`, then for all `ω` in `Ω`, the stopped value of `f` at the `n`-th lower crossing time for `ω` is less than or equal to `a`.
|
MeasureTheory.lowerCrossingTime_le_upperCrossingTime_succ
theorem MeasureTheory.lowerCrossingTime_le_upperCrossingTime_succ :
∀ {Ω : Type u_1} {ι : Type u_2} [inst : ConditionallyCompleteLinearOrderBot ι] {a b : ℝ} {f : ι → Ω → ℝ} {N : ι}
{n : ℕ} {ω : Ω},
MeasureTheory.lowerCrossingTime a b f N n ω ≤ MeasureTheory.upperCrossingTime a b f N (n + 1) ω
The theorem `MeasureTheory.lowerCrossingTime_le_upperCrossingTime_succ` states that for all possible types `'Ω` and `'ι`, given a conditionally complete linear order with a least element on type `'ι`, real numbers `a` and `b`, a function `f` mapping from type `'ι` to `'Ω` to real numbers, a value `N` of type `'ι`, a natural number `n` and a value `ω` of type `'Ω`, the lower crossing time of `f` at `N` for the `n`-th time is less than or equal to the upper crossing time of `f` at `N` for the `n+1`-th time. In plain English, this theorem asserts that the first time before `N` when `f` reaches below `a` after reaching above `b` for the `n`-th time is always less than or equal to the time when `f` reaches above `b` for the `n+1`-th time.
More concisely: For all types 'Ω and 'ι, given a conditionally complete linear order with a least element on type 'ι, real numbers a < b, a function f : 'ι -> 'Ω -> Real, value N : 'ι, natural number n, and value ω : 'Ω, the n-th lower crossing time of f at N is less than or equal to the (n+1)-th upper crossing time of f at N.
|
MeasureTheory.upperCrossingTime_stabilize
theorem MeasureTheory.upperCrossingTime_stabilize :
∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n m : ℕ} {ω : Ω},
n ≤ m → MeasureTheory.upperCrossingTime a b f N n ω = N → MeasureTheory.upperCrossingTime a b f N m ω = N
This theorem states that for any types `Ω` and real numbers `a` and `b`, any function `f` from natural numbers to `Ω` to real numbers, any natural numbers `N`, `n`, and `m`, and any `ω` of type `Ω`, if `n` is less than or equal to `m` and the upper crossing time of `a`, `b`, `f`, `N`, `n` at `ω` equals `N`, then the upper crossing time of `a`, `b`, `f`, `N`, `m` at `ω` also equals `N`.
In mathematical terms, an upper crossing time is a concept used in measure theory that represents the least time that a given stochastic process crosses a certain upper level.
More concisely: For any types `Ω`, real numbers `a` and `b`, function `f` from natural numbers to `Ω` to real numbers, natural numbers `N`, `n`, `m`, and `ω` of type `Ω`, if `n ≤ m` and the upper crossing time of `a`, `b`, `f`, `N` at `ω` equals `N`, then the upper crossing time of `a`, `b`, `f`, `N`, `m` at `ω` also equals `N`.
|
MeasureTheory.lowerCrossingTime_le
theorem MeasureTheory.lowerCrossingTime_le :
∀ {Ω : Type u_1} {ι : Type u_2} [inst : ConditionallyCompleteLinearOrderBot ι] {a b : ℝ} {f : ι → Ω → ℝ} {N : ι}
{n : ℕ} {ω : Ω}, MeasureTheory.lowerCrossingTime a b f N n ω ≤ N
The theorem `MeasureTheory.lowerCrossingTime_le` states that, for any given sets Ω and ι (with ι having a conditionally complete linear order with a least element), real numbers `a` and `b`, function `f` mapping from Ω×ι to real numbers, a specific element `N` from ι, a natural number `n`, and an element `ω` from Ω, the "lower crossing time" of `f` (the first time before `N` that `f` reaches below `a` after reaching above `b` for the `n`-th time) is always less than or equal to `N`. In simpler terms, the time when the function dips below a certain level after reaching above another level a specific number of times will never exceed a prescribed time limit.
More concisely: For any sets Ω and ι, real numbers a ≤ b, function f : Ω × ι → ℝ, element N ∈ ι, natural number n, and ω ∈ Ω, the lower crossing time of f at (ω, N), defined as the infimum time t < N such that f(ω, t) < a after reaching above b for the n-th time, is less than or equal to N.
|
MeasureTheory.upperCrossingTime_lt_of_le_upcrossingsBefore
theorem MeasureTheory.upperCrossingTime_lt_of_le_upcrossingsBefore :
∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω},
0 < N → a < b → n ≤ MeasureTheory.upcrossingsBefore a b f N ω → MeasureTheory.upperCrossingTime a b f N n ω < N
This theorem states that for any types `Ω` representing a set of outcomes, real numbers `a` and `b` with `a` less than `b`, a function `f` mapping natural numbers and outcomes to real numbers, and natural numbers `N` and `n` with `N` greater than zero and `n` less than or equal to the number of upcrossings before time `N`, the upper crossing time of `f` at values `a` and `b` before time `N` for any outcome `ω` is less than `N`. In other words, it says that if the number of times the function `f` upcrosses between `a` and `b` before time `N` is greater than or equal to a certain number `n`, then the `n`-th upper crossing time of `f` between `a` and `b` occurs before time `N`.
More concisely: For any function `f` mapping natural numbers and outcomes to real numbers, if there exist types `Ω`, real numbers `a` < `b`, natural numbers `N` > 0, and `n` <= number of upcrossings before `N` of `f(x, ω)` between `a` and `b`, then the `n`-th upper crossing time of `f(x, ω)` between `a` and `b` occurs before time `N`.
|
MeasureTheory.upperCrossingTime_le_lowerCrossingTime
theorem MeasureTheory.upperCrossingTime_le_lowerCrossingTime :
∀ {Ω : Type u_1} {ι : Type u_2} [inst : ConditionallyCompleteLinearOrderBot ι] {a b : ℝ} {f : ι → Ω → ℝ} {N : ι}
{n : ℕ} {ω : Ω}, MeasureTheory.upperCrossingTime a b f N n ω ≤ MeasureTheory.lowerCrossingTime a b f N n ω
The theorem `MeasureTheory.upperCrossingTime_le_lowerCrossingTime` asserts that for any types `Ω` and `ι`, the latter of which has the structure of a conditionally complete linear order bot, and any real numbers `a` and `b`, function `f` mapping from `ι` and `Ω` to the real numbers, any element `N` of `ι`, any natural number `n`, and any element `ω` of `Ω`, the "upper crossing time" of `f` is less than or equal to its "lower crossing time".
In other words, it's saying that the first time `f` reaches above level `b` for the `n`-th time and then dips below level `a` before time `N`, happens on or after the first time `f` reaches above level `b` for the `n`-th time.
More concisely: For any conditionally complete linear order bot ι, real numbers a < b, function f : ι × Ω → ℝ, natural number n, element N ∈ ι, and ω ∈ Ω, the n-th upper crossing time of f is less than or equal to the n-th lower crossing time.
|
MeasureTheory.Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part
theorem MeasureTheory.Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part :
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ℕ → Ω → ℝ}
{ℱ : MeasureTheory.Filtration ℕ m0} [inst : MeasureTheory.IsFiniteMeasure μ] (a b : ℝ),
MeasureTheory.Submartingale f ℱ μ →
ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), MeasureTheory.upcrossings a b f ω ∂μ ≤
⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ
This theorem, named "MeasureTheory.Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_part", is a variant of Doob's upcrossing lemma in probability theory. It states that for any measure space `Ω` with a measurable space `m0` and a measure `μ`, a filtration `ℱ` on `m0`, a sequence `f` of real-valued functions on `Ω`, and two real numbers `a` and `b`, if `f` is a submartingale with respect to `ℱ` and `μ`, then the product of the non-negative part of the difference between `b` and `a` and the expectation of the number of upcrossings of the sequence `f` from `a` to `b` is less than or equal to the supremum of the expectations of the positive part of the difference between `f N ω` and `a` for all `N`. Mathematically, this can be represented as:
\[ \text{ENNReal.ofReal} (b - a) \times \int_{\Omega} \text{MeasureTheory.upcrossings}~ a~ b~ f~(\omega)~d\mu \leq \sup_N \int_{\Omega} \text{ENNReal.ofReal} (f(N, \omega) - a)^+~d\mu \]
More concisely: For any measurable space, filtration, submartingale, and real numbers, the product of the non-negative difference between the numbers and the expected number of upcrossings is less than or equal to the supremum of the expectations of the positive difference. Mathematically, $\text{ENNReal.ofReal}(b-a) \times \int_{\Omega} \text{MeasureTheory.upcrossings}~ a~ b~ f~(\omega)~d\mu \leq \sup\_N \int_{\Omega} \text{ENNReal.ofReal}(f(N, \omega) - a)^+~d\mu$.
|
MeasureTheory.upperCrossingTime_lt_bddAbove
theorem MeasureTheory.upperCrossingTime_lt_bddAbove :
∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ} {ω : Ω},
a < b → BddAbove {n | MeasureTheory.upperCrossingTime a b f N n ω < N}
The theorem `MeasureTheory.upperCrossingTime_lt_bddAbove` states that for any types `Ω` and real numbers `a` and `b`, any function `f` from natural numbers to a function from `Ω` to real numbers, any natural number `N`, and any value `ω` of type `Ω`, if `a` is less than `b`, then the set of natural numbers `n` for which the upper crossing time of `a` and `b` for the function `f` at `N` and `n` and `ω` is less than `N`, is bounded above. This essentially means that there is an upper limit to the "upper crossing time" values that are less than `N`.
More concisely: For any types Ω, real numbers a < b, function f from natural numbers to Ω -> real numbers, natural number N, and value ω of type Ω, the set of natural numbers n with upper crossing time of a and b for f at N and n and ω less than N, is bounded above.
|