Adapted and progressively measurable processes #
This file defines the related notions of a process u being Adapted, StronglyAdapted
or StronglyProgressive (progressively measurable) with respect to a filter f, and proves
some basic facts about them.
Main definitions #
MeasureTheory.Adapted: a sequence of functionsuis said to be adapted to a filtrationfif at each point in timei,u iisf i-measurableMeasureTheory.StronglyAdapted: a sequence of functionsuis said to be strongly adapted to a filtrationfif at each point in timei,u iisf i-strongly measurableMeasureTheory.IsStronglyProgressive: a sequence of functionsuis said to be strongly progressive with respect to a filtrationfif at each point in timei,urestricted toSet.Iic i × Ωis strongly measurable with respect to the productMeasurableSpacestructure where the σ-algebra used forΩisf i.
Main results #
StronglyAdapted.isStronglyProgressive_of_continuous: a continuous strongly adapted process is strongly progressive.
Tags #
adapted, progressively measurable
def
MeasureTheory.Adapted
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{β : ι → Type u_3}
[(i : ι) → MeasurableSpace (β i)]
(f : Filtration ι m)
(u : (i : ι) → Ω → β i)
:
A sequence of functions u is adapted to a filtration f if for all i,
u i is f i-measurable.
The definition known as Adapted before 2026-01-13 is now StronglyAdapted.
Equations
- MeasureTheory.Adapted f u = ∀ (i : ι), Measurable (u i)
Instances For
theorem
MeasureTheory.Adapted.mul
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → MeasurableSpace (β i)]
{u v : (i : ι) → Ω → β i}
[(i : ι) → Mul (β i)]
[∀ (i : ι), MeasurableMul₂ (β i)]
(hu : Adapted f u)
(hv : Adapted f v)
:
theorem
MeasureTheory.Adapted.add
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → MeasurableSpace (β i)]
{u v : (i : ι) → Ω → β i}
[(i : ι) → Add (β i)]
[∀ (i : ι), MeasurableAdd₂ (β i)]
(hu : Adapted f u)
(hv : Adapted f v)
:
theorem
MeasureTheory.Adapted.div
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → MeasurableSpace (β i)]
{u v : (i : ι) → Ω → β i}
[(i : ι) → Div (β i)]
[∀ (i : ι), MeasurableDiv₂ (β i)]
(hu : Adapted f u)
(hv : Adapted f v)
:
theorem
MeasureTheory.Adapted.sub
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → MeasurableSpace (β i)]
{u v : (i : ι) → Ω → β i}
[(i : ι) → Sub (β i)]
[∀ (i : ι), MeasurableSub₂ (β i)]
(hu : Adapted f u)
(hv : Adapted f v)
:
theorem
MeasureTheory.Adapted.inv
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → MeasurableSpace (β i)]
{u : (i : ι) → Ω → β i}
[(i : ι) → Group (β i)]
[∀ (i : ι), MeasurableInv (β i)]
(hu : Adapted f u)
:
theorem
MeasureTheory.Adapted.neg
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → MeasurableSpace (β i)]
{u : (i : ι) → Ω → β i}
[(i : ι) → AddGroup (β i)]
[∀ (i : ι), MeasurableNeg (β i)]
(hu : Adapted f u)
:
theorem
MeasureTheory.Adapted.smul
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → MeasurableSpace (β i)]
{u : (i : ι) → Ω → β i}
{𝕂 : Type u_4}
[MeasurableSpace 𝕂]
[(i : ι) → SMul 𝕂 (β i)]
[∀ (i : ι), MeasurableSMul 𝕂 (β i)]
(c : 𝕂)
(hu : Adapted f u)
:
theorem
MeasureTheory.Adapted.measurable
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → MeasurableSpace (β i)]
{u : (i : ι) → Ω → β i}
{i : ι}
(hf : Adapted f u)
:
Measurable (u i)
theorem
MeasureTheory.Adapted.measurable_le
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → MeasurableSpace (β i)]
{u : (i : ι) → Ω → β i}
{i j : ι}
(hf : Adapted f u)
(hij : i ≤ j)
:
Measurable (u i)
theorem
MeasureTheory.adapted_const'
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{β : ι → Type u_3}
[(i : ι) → MeasurableSpace (β i)]
(f : Filtration ι m)
(x : (i : ι) → β i)
:
Adapted f fun (i : ι) (x_1 : Ω) => x i
theorem
MeasureTheory.adapted_const
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{β : Type u_4}
[MeasurableSpace β]
(f : Filtration ι m)
(x : β)
:
Adapted f fun (x_1 : ι) (x_2 : Ω) => x
def
MeasureTheory.StronglyAdapted
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
(f : Filtration ι m)
(u : (i : ι) → Ω → β i)
:
A sequence of functions u is strongly adapted to a filtration f if for all i,
u i is f i-strongly measurable.
Equations
- MeasureTheory.StronglyAdapted f u = ∀ (i : ι), MeasureTheory.StronglyMeasurable (u i)
Instances For
theorem
MeasureTheory.StronglyAdapted.mul
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u v : (i : ι) → Ω → β i}
[(i : ι) → Mul (β i)]
[∀ (i : ι), ContinuousMul (β i)]
(hu : StronglyAdapted f u)
(hv : StronglyAdapted f v)
:
StronglyAdapted f (u * v)
theorem
MeasureTheory.StronglyAdapted.add
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u v : (i : ι) → Ω → β i}
[(i : ι) → Add (β i)]
[∀ (i : ι), ContinuousAdd (β i)]
(hu : StronglyAdapted f u)
(hv : StronglyAdapted f v)
:
StronglyAdapted f (u + v)
theorem
MeasureTheory.StronglyAdapted.div'
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u v : (i : ι) → Ω → β i}
[(i : ι) → Div (β i)]
[∀ (i : ι), ContinuousDiv (β i)]
(hu : StronglyAdapted f u)
(hv : StronglyAdapted f v)
:
StronglyAdapted f (u / v)
theorem
MeasureTheory.StronglyAdapted.sub
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u v : (i : ι) → Ω → β i}
[(i : ι) → Sub (β i)]
[∀ (i : ι), ContinuousSub (β i)]
(hu : StronglyAdapted f u)
(hv : StronglyAdapted f v)
:
StronglyAdapted f (u - v)
theorem
MeasureTheory.StronglyAdapted.inv
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u : (i : ι) → Ω → β i}
[(i : ι) → Group (β i)]
[∀ (i : ι), ContinuousInv (β i)]
(hu : StronglyAdapted f u)
:
theorem
MeasureTheory.StronglyAdapted.neg
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u : (i : ι) → Ω → β i}
[(i : ι) → AddGroup (β i)]
[∀ (i : ι), ContinuousNeg (β i)]
(hu : StronglyAdapted f u)
:
StronglyAdapted f (-u)
theorem
MeasureTheory.StronglyAdapted.smul
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u : (i : ι) → Ω → β i}
[(i : ι) → SMul ℝ (β i)]
[∀ (i : ι), ContinuousConstSMul ℝ (β i)]
(c : ℝ)
(hu : StronglyAdapted f u)
:
StronglyAdapted f (c • u)
theorem
MeasureTheory.StronglyAdapted.norm
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_4}
{u : (i : ι) → Ω → β i}
[(i : ι) → SeminormedAddCommGroup (β i)]
(hu : StronglyAdapted f u)
:
StronglyAdapted f fun (t : ι) (ω : Ω) => ‖u t ω‖
The norm of a strongly adapted process is strongly adapted.
theorem
MeasureTheory.StronglyAdapted.stronglyMeasurable
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u : (i : ι) → Ω → β i}
{i : ι}
(hf : StronglyAdapted f u)
:
StronglyMeasurable (u i)
theorem
MeasureTheory.StronglyAdapted.stronglyMeasurable_le
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u : (i : ι) → Ω → β i}
{i j : ι}
(hf : StronglyAdapted f u)
(hij : i ≤ j)
:
StronglyMeasurable (u i)
theorem
MeasureTheory.StronglyAdapted.adapted
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u : (i : ι) → Ω → β i}
[mΒ : (i : ι) → MeasurableSpace (β i)]
[∀ (i : ι), BorelSpace (β i)]
[∀ (i : ι), TopologicalSpace.PseudoMetrizableSpace (β i)]
(hf : StronglyAdapted f u)
:
Adapted f u
theorem
MeasureTheory.Adapted.stronglyAdapted
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u : (i : ι) → Ω → β i}
[mΒ : (i : ι) → MeasurableSpace (β i)]
[∀ (i : ι), OpensMeasurableSpace (β i)]
[∀ (i : ι), TopologicalSpace.PseudoMetrizableSpace (β i)]
[∀ (i : ι), SecondCountableTopology (β i)]
(hf : Adapted f u)
:
StronglyAdapted f u
theorem
MeasureTheory.stronglyAdapted_iff_adapted
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u : (i : ι) → Ω → β i}
[mΒ : (i : ι) → MeasurableSpace (β i)]
[∀ (i : ι), BorelSpace (β i)]
[∀ (i : ι), TopologicalSpace.PseudoMetrizableSpace (β i)]
[∀ (i : ι), SecondCountableTopology (β i)]
:
theorem
MeasureTheory.stronglyAdapted_const'
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
(f : Filtration ι m)
(x : (i : ι) → β i)
:
StronglyAdapted f fun (i : ι) (x_1 : Ω) => x i
theorem
MeasureTheory.stronglyAdapted_const
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{β : Type u_4}
[TopologicalSpace β]
(f : Filtration ι m)
(x : β)
:
StronglyAdapted f fun (x_1 : ι) (x_2 : Ω) => x
theorem
MeasureTheory.stronglyAdapted_zero'
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
(β : ι → Type u_3)
[(i : ι) → TopologicalSpace (β i)]
[(i : ι) → Zero (β i)]
(f : Filtration ι m)
:
StronglyAdapted f 0
theorem
MeasureTheory.stronglyAdapted_zero
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
(β : Type u_4)
[TopologicalSpace β]
[Zero β]
(f : Filtration ι m)
:
StronglyAdapted f 0
theorem
MeasureTheory.Filtration.stronglyAdapted_natural
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{β : ι → Type u_3}
[(i : ι) → TopologicalSpace (β i)]
{u : (i : ι) → Ω → β i}
[∀ (i : ι), TopologicalSpace.MetrizableSpace (β i)]
[mβ : (i : ι) → MeasurableSpace (β i)]
[∀ (i : ι), BorelSpace (β i)]
(hum : ∀ (i : ι), StronglyMeasurable (u i))
:
StronglyAdapted (natural u hum) u
def
MeasureTheory.IsStronglyProgressive
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
(f : Filtration ι m)
(u : ι → Ω → β)
:
Strongly progressive process. A sequence of functions u is said to be strongly
progressive with respect to a filtration f if at each point in time i, u restricted to
Set.Iic i × Ω is strongly measurable with respect to the product MeasurableSpace structure
where the σ-algebra used for Ω is f i.
The usual definition uses the interval [0,i], which we replace by Set.Iic i. We recover the
usual definition for index types ℝ≥0 or ℕ.
Equations
- MeasureTheory.IsStronglyProgressive f u = ∀ (i : ι), MeasureTheory.StronglyMeasurable fun (p : ↑(Set.Iic i) × Ω) => u (↑p.1) p.2
Instances For
theorem
MeasureTheory.isStronglyProgressive_const
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
(f : Filtration ι m)
(b : β)
:
IsStronglyProgressive f fun (x : ι) (x_1 : Ω) => b
theorem
MeasureTheory.IsStronglyProgressive.stronglyAdapted
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[MeasurableSpace ι]
(h : IsStronglyProgressive f u)
:
StronglyAdapted f u
theorem
MeasureTheory.IsStronglyProgressive.comp
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[MeasurableSpace ι]
{t : ι → Ω → ι}
[TopologicalSpace ι]
[BorelSpace ι]
[TopologicalSpace.PseudoMetrizableSpace ι]
(h : IsStronglyProgressive f u)
(ht : IsStronglyProgressive f t)
(ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i)
:
IsStronglyProgressive f fun (i : ι) (ω : Ω) => u (t i ω) ω
theorem
MeasureTheory.IsStronglyProgressive.mul
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u v : ι → Ω → β}
[MeasurableSpace ι]
[Mul β]
[ContinuousMul β]
(hu : IsStronglyProgressive f u)
(hv : IsStronglyProgressive f v)
:
IsStronglyProgressive f fun (i : ι) (ω : Ω) => u i ω * v i ω
theorem
MeasureTheory.IsStronglyProgressive.add
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u v : ι → Ω → β}
[MeasurableSpace ι]
[Add β]
[ContinuousAdd β]
(hu : IsStronglyProgressive f u)
(hv : IsStronglyProgressive f v)
:
IsStronglyProgressive f fun (i : ι) (ω : Ω) => u i ω + v i ω
theorem
MeasureTheory.IsStronglyProgressive.finsetProd'
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
{γ : Type u_4}
[CommMonoid β]
[ContinuousMul β]
{U : γ → ι → Ω → β}
{s : Finset γ}
(h : ∀ c ∈ s, IsStronglyProgressive f (U c))
:
IsStronglyProgressive f (∏ c ∈ s, U c)
theorem
MeasureTheory.IsStronglyProgressive.finsetSum'
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
{γ : Type u_4}
[AddCommMonoid β]
[ContinuousAdd β]
{U : γ → ι → Ω → β}
{s : Finset γ}
(h : ∀ c ∈ s, IsStronglyProgressive f (U c))
:
IsStronglyProgressive f (∑ c ∈ s, U c)
@[deprecated MeasureTheory.IsStronglyProgressive.finsetSum' (since := "2026-04-08")]
theorem
MeasureTheory.IsStronglyProgressive.finset_sum'
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
{γ : Type u_4}
[AddCommMonoid β]
[ContinuousAdd β]
{U : γ → ι → Ω → β}
{s : Finset γ}
(h : ∀ c ∈ s, IsStronglyProgressive f (U c))
:
IsStronglyProgressive f (∑ c ∈ s, U c)
@[deprecated MeasureTheory.IsStronglyProgressive.finsetProd' (since := "2026-04-08")]
theorem
MeasureTheory.IsStronglyProgressive.finset_prod'
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
{γ : Type u_4}
[CommMonoid β]
[ContinuousMul β]
{U : γ → ι → Ω → β}
{s : Finset γ}
(h : ∀ c ∈ s, IsStronglyProgressive f (U c))
:
IsStronglyProgressive f (∏ c ∈ s, U c)
theorem
MeasureTheory.IsStronglyProgressive.finsetProd
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
{γ : Type u_4}
[CommMonoid β]
[ContinuousMul β]
{U : γ → ι → Ω → β}
{s : Finset γ}
(h : ∀ c ∈ s, IsStronglyProgressive f (U c))
:
IsStronglyProgressive f fun (i : ι) (a : Ω) => ∏ c ∈ s, U c i a
theorem
MeasureTheory.IsStronglyProgressive.finsetSum
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
{γ : Type u_4}
[AddCommMonoid β]
[ContinuousAdd β]
{U : γ → ι → Ω → β}
{s : Finset γ}
(h : ∀ c ∈ s, IsStronglyProgressive f (U c))
:
IsStronglyProgressive f fun (i : ι) (a : Ω) => ∑ c ∈ s, U c i a
@[deprecated MeasureTheory.IsStronglyProgressive.finsetSum (since := "2026-04-08")]
theorem
MeasureTheory.IsStronglyProgressive.finset_sum
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
{γ : Type u_4}
[AddCommMonoid β]
[ContinuousAdd β]
{U : γ → ι → Ω → β}
{s : Finset γ}
(h : ∀ c ∈ s, IsStronglyProgressive f (U c))
:
IsStronglyProgressive f fun (i : ι) (a : Ω) => ∑ c ∈ s, U c i a
@[deprecated MeasureTheory.IsStronglyProgressive.finsetProd (since := "2026-04-08")]
theorem
MeasureTheory.IsStronglyProgressive.finset_prod
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
{γ : Type u_4}
[CommMonoid β]
[ContinuousMul β]
{U : γ → ι → Ω → β}
{s : Finset γ}
(h : ∀ c ∈ s, IsStronglyProgressive f (U c))
:
IsStronglyProgressive f fun (i : ι) (a : Ω) => ∏ c ∈ s, U c i a
theorem
MeasureTheory.IsStronglyProgressive.inv
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[MeasurableSpace ι]
[Group β]
[ContinuousInv β]
(hu : IsStronglyProgressive f u)
:
IsStronglyProgressive f fun (i : ι) (ω : Ω) => (u i ω)⁻¹
theorem
MeasureTheory.IsStronglyProgressive.neg
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[MeasurableSpace ι]
[AddGroup β]
[ContinuousNeg β]
(hu : IsStronglyProgressive f u)
:
IsStronglyProgressive f fun (i : ι) (ω : Ω) => -u i ω
theorem
MeasureTheory.IsStronglyProgressive.div'
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u v : ι → Ω → β}
[MeasurableSpace ι]
[Group β]
[ContinuousDiv β]
(hu : IsStronglyProgressive f u)
(hv : IsStronglyProgressive f v)
:
IsStronglyProgressive f fun (i : ι) (ω : Ω) => u i ω / v i ω
theorem
MeasureTheory.IsStronglyProgressive.sub
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u v : ι → Ω → β}
[MeasurableSpace ι]
[AddGroup β]
[ContinuousSub β]
(hu : IsStronglyProgressive f u)
(hv : IsStronglyProgressive f v)
:
IsStronglyProgressive f fun (i : ι) (ω : Ω) => u i ω - v i ω
theorem
MeasureTheory.IsStronglyProgressive.norm
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
[MeasurableSpace ι]
{β : Type u_4}
{u : ι → Ω → β}
[SeminormedAddCommGroup β]
(hu : IsStronglyProgressive f u)
:
IsStronglyProgressive f fun (t : ι) (ω : Ω) => ‖u t ω‖
The norm of a strongly progressive process is strongly progressive.
theorem
MeasureTheory.isStronglyProgressive_of_tendsto'
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
{γ : Type u_4}
[MeasurableSpace ι]
[TopologicalSpace.PseudoMetrizableSpace β]
(fltr : Filter γ)
[fltr.NeBot]
[fltr.IsCountablyGenerated]
{U : γ → ι → Ω → β}
(h : ∀ (l : γ), IsStronglyProgressive f (U l))
(h_tendsto : Filter.Tendsto U fltr (nhds u))
:
theorem
MeasureTheory.isStronglyProgressive_of_tendsto
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[MeasurableSpace ι]
[TopologicalSpace.PseudoMetrizableSpace β]
{U : ℕ → ι → Ω → β}
(h : ∀ (l : ℕ), IsStronglyProgressive f (U l))
(h_tendsto : Filter.Tendsto U Filter.atTop (nhds u))
:
theorem
MeasureTheory.StronglyAdapted.isStronglyProgressive_of_continuous
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[TopologicalSpace ι]
[TopologicalSpace.MetrizableSpace ι]
[SecondCountableTopology ι]
[MeasurableSpace ι]
[OpensMeasurableSpace ι]
[TopologicalSpace.PseudoMetrizableSpace β]
(h : StronglyAdapted f u)
(hu_cont : ∀ (ω : Ω), Continuous fun (i : ι) => u i ω)
:
A continuous and strongly adapted process is strongly progressive.
theorem
MeasureTheory.StronglyAdapted.isStronglyProgressive_of_discrete
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[TopologicalSpace ι]
[DiscreteTopology ι]
[SecondCountableTopology ι]
[MeasurableSpace ι]
[OpensMeasurableSpace ι]
[TopologicalSpace.PseudoMetrizableSpace β]
(h : StronglyAdapted f u)
:
For filtrations indexed by a discrete order, StronglyAdapted and IsStronglyProgressive are
equivalent. This lemma provides StronglyAdapted f u → IsStronglyProgressive f u.
See IsStronglyProgressive.stronglyAdapted for the reverse direction, which is true more generally.
@[deprecated MeasureTheory.IsStronglyProgressive (since := "2026-04-24")]
def
MeasureTheory.ProgMeasurable
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
(f : Filtration ι m)
(u : ι → Ω → β)
:
Alias of MeasureTheory.IsStronglyProgressive.
Strongly progressive process. A sequence of functions u is said to be strongly
progressive with respect to a filtration f if at each point in time i, u restricted to
Set.Iic i × Ω is strongly measurable with respect to the product MeasurableSpace structure
where the σ-algebra used for Ω is f i.
The usual definition uses the interval [0,i], which we replace by Set.Iic i. We recover the
usual definition for index types ℝ≥0 or ℕ.
Instances For
@[deprecated MeasureTheory.isStronglyProgressive_const (since := "2026-04-24")]
theorem
MeasureTheory.progMeasurable_const
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
(f : Filtration ι m)
(b : β)
:
IsStronglyProgressive f fun (x : ι) (x_1 : Ω) => b
@[deprecated MeasureTheory.IsStronglyProgressive.stronglyAdapted (since := "2026-04-24")]
theorem
MeasureTheory.ProgMeasurable.stronglyAdapted
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[MeasurableSpace ι]
(h : IsStronglyProgressive f u)
:
StronglyAdapted f u
Alias of MeasureTheory.IsStronglyProgressive.stronglyAdapted.
@[deprecated MeasureTheory.IsStronglyProgressive.comp (since := "2026-04-24")]
theorem
MeasureTheory.ProgMeasurable.comp
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[MeasurableSpace ι]
{t : ι → Ω → ι}
[TopologicalSpace ι]
[BorelSpace ι]
[TopologicalSpace.PseudoMetrizableSpace ι]
(h : IsStronglyProgressive f u)
(ht : IsStronglyProgressive f t)
(ht_le : ∀ (i : ι) (ω : Ω), t i ω ≤ i)
:
IsStronglyProgressive f fun (i : ι) (ω : Ω) => u (t i ω) ω
Alias of MeasureTheory.IsStronglyProgressive.comp.
@[deprecated MeasureTheory.IsStronglyProgressive.add (since := "2026-04-24")]
theorem
MeasureTheory.ProgMeasurable.add
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u v : ι → Ω → β}
[MeasurableSpace ι]
[Add β]
[ContinuousAdd β]
(hu : IsStronglyProgressive f u)
(hv : IsStronglyProgressive f v)
:
IsStronglyProgressive f fun (i : ι) (ω : Ω) => u i ω + v i ω
Alias of MeasureTheory.IsStronglyProgressive.add.
@[deprecated MeasureTheory.IsStronglyProgressive.mul (since := "2026-04-24")]
theorem
MeasureTheory.ProgMeasurable.mul
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u v : ι → Ω → β}
[MeasurableSpace ι]
[Mul β]
[ContinuousMul β]
(hu : IsStronglyProgressive f u)
(hv : IsStronglyProgressive f v)
:
IsStronglyProgressive f fun (i : ι) (ω : Ω) => u i ω * v i ω
Alias of MeasureTheory.IsStronglyProgressive.mul.
@[deprecated MeasureTheory.IsStronglyProgressive.finsetSum' (since := "2026-04-24")]
theorem
MeasureTheory.ProgMeasurable.finset_sum'
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
{γ : Type u_4}
[AddCommMonoid β]
[ContinuousAdd β]
{U : γ → ι → Ω → β}
{s : Finset γ}
(h : ∀ c ∈ s, IsStronglyProgressive f (U c))
:
IsStronglyProgressive f (∑ c ∈ s, U c)
@[deprecated MeasureTheory.IsStronglyProgressive.finsetProd' (since := "2026-04-24")]
theorem
MeasureTheory.ProgMeasurable.finset_prod'
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
{γ : Type u_4}
[CommMonoid β]
[ContinuousMul β]
{U : γ → ι → Ω → β}
{s : Finset γ}
(h : ∀ c ∈ s, IsStronglyProgressive f (U c))
:
IsStronglyProgressive f (∏ c ∈ s, U c)
@[deprecated MeasureTheory.IsStronglyProgressive.finsetSum (since := "2026-04-24")]
theorem
MeasureTheory.ProgMeasurable.finset_sum
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
{γ : Type u_4}
[AddCommMonoid β]
[ContinuousAdd β]
{U : γ → ι → Ω → β}
{s : Finset γ}
(h : ∀ c ∈ s, IsStronglyProgressive f (U c))
:
IsStronglyProgressive f fun (i : ι) (a : Ω) => ∑ c ∈ s, U c i a
@[deprecated MeasureTheory.IsStronglyProgressive.finsetProd (since := "2026-04-24")]
theorem
MeasureTheory.ProgMeasurable.finset_prod
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
[MeasurableSpace ι]
{γ : Type u_4}
[CommMonoid β]
[ContinuousMul β]
{U : γ → ι → Ω → β}
{s : Finset γ}
(h : ∀ c ∈ s, IsStronglyProgressive f (U c))
:
IsStronglyProgressive f fun (i : ι) (a : Ω) => ∏ c ∈ s, U c i a
@[deprecated MeasureTheory.IsStronglyProgressive.neg (since := "2026-04-24")]
theorem
MeasureTheory.ProgMeasurable.neg
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[MeasurableSpace ι]
[AddGroup β]
[ContinuousNeg β]
(hu : IsStronglyProgressive f u)
:
IsStronglyProgressive f fun (i : ι) (ω : Ω) => -u i ω
Alias of MeasureTheory.IsStronglyProgressive.neg.
@[deprecated MeasureTheory.IsStronglyProgressive.inv (since := "2026-04-24")]
theorem
MeasureTheory.ProgMeasurable.inv
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[MeasurableSpace ι]
[Group β]
[ContinuousInv β]
(hu : IsStronglyProgressive f u)
:
IsStronglyProgressive f fun (i : ι) (ω : Ω) => (u i ω)⁻¹
Alias of MeasureTheory.IsStronglyProgressive.inv.
@[deprecated MeasureTheory.IsStronglyProgressive.sub (since := "2026-04-24")]
theorem
MeasureTheory.ProgMeasurable.sub
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u v : ι → Ω → β}
[MeasurableSpace ι]
[AddGroup β]
[ContinuousSub β]
(hu : IsStronglyProgressive f u)
(hv : IsStronglyProgressive f v)
:
IsStronglyProgressive f fun (i : ι) (ω : Ω) => u i ω - v i ω
Alias of MeasureTheory.IsStronglyProgressive.sub.
@[deprecated MeasureTheory.IsStronglyProgressive.div' (since := "2026-04-24")]
theorem
MeasureTheory.ProgMeasurable.div'
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u v : ι → Ω → β}
[MeasurableSpace ι]
[Group β]
[ContinuousDiv β]
(hu : IsStronglyProgressive f u)
(hv : IsStronglyProgressive f v)
:
IsStronglyProgressive f fun (i : ι) (ω : Ω) => u i ω / v i ω
Alias of MeasureTheory.IsStronglyProgressive.div'.
@[deprecated MeasureTheory.IsStronglyProgressive.norm (since := "2026-04-24")]
theorem
MeasureTheory.ProgMeasurable.norm
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
[MeasurableSpace ι]
{β : Type u_4}
{u : ι → Ω → β}
[SeminormedAddCommGroup β]
(hu : IsStronglyProgressive f u)
:
IsStronglyProgressive f fun (t : ι) (ω : Ω) => ‖u t ω‖
Alias of MeasureTheory.IsStronglyProgressive.norm.
The norm of a strongly progressive process is strongly progressive.
@[deprecated MeasureTheory.isStronglyProgressive_of_tendsto (since := "2026-04-24")]
theorem
MeasureTheory.progMeasurable_of_tendsto
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[MeasurableSpace ι]
[TopologicalSpace.PseudoMetrizableSpace β]
{U : ℕ → ι → Ω → β}
(h : ∀ (l : ℕ), IsStronglyProgressive f (U l))
(h_tendsto : Filter.Tendsto U Filter.atTop (nhds u))
:
@[deprecated MeasureTheory.isStronglyProgressive_of_tendsto' (since := "2026-04-24")]
theorem
MeasureTheory.progMeasurable_of_tendsto'
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
{γ : Type u_4}
[MeasurableSpace ι]
[TopologicalSpace.PseudoMetrizableSpace β]
(fltr : Filter γ)
[fltr.NeBot]
[fltr.IsCountablyGenerated]
{U : γ → ι → Ω → β}
(h : ∀ (l : γ), IsStronglyProgressive f (U l))
(h_tendsto : Filter.Tendsto U fltr (nhds u))
:
@[deprecated MeasureTheory.StronglyAdapted.isStronglyProgressive_of_continuous (since := "2026-04-24")]
theorem
MeasureTheory.StronglyAdapted.progMeasurable_of_continuous
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[TopologicalSpace ι]
[TopologicalSpace.MetrizableSpace ι]
[SecondCountableTopology ι]
[MeasurableSpace ι]
[OpensMeasurableSpace ι]
[TopologicalSpace.PseudoMetrizableSpace β]
(h : StronglyAdapted f u)
(hu_cont : ∀ (ω : Ω), Continuous fun (i : ι) => u i ω)
:
Alias of MeasureTheory.StronglyAdapted.isStronglyProgressive_of_continuous.
A continuous and strongly adapted process is strongly progressive.
@[deprecated MeasureTheory.StronglyAdapted.isStronglyProgressive_of_discrete (since := "2026-04-24")]
theorem
MeasureTheory.StronglyAdapted.progMeasurable_of_discrete
{Ω : Type u_1}
{ι : Type u_2}
{m : MeasurableSpace Ω}
[Preorder ι]
{f : Filtration ι m}
{β : Type u_3}
[TopologicalSpace β]
{u : ι → Ω → β}
[TopologicalSpace ι]
[DiscreteTopology ι]
[SecondCountableTopology ι]
[MeasurableSpace ι]
[OpensMeasurableSpace ι]
[TopologicalSpace.PseudoMetrizableSpace β]
(h : StronglyAdapted f u)
:
Alias of MeasureTheory.StronglyAdapted.isStronglyProgressive_of_discrete.
For filtrations indexed by a discrete order, StronglyAdapted and IsStronglyProgressive are
equivalent. This lemma provides StronglyAdapted f u → IsStronglyProgressive f u.
See IsStronglyProgressive.stronglyAdapted for the reverse direction, which is true more generally.