# Simple processes and elementary stochastic integral #

## Main definitions #

- `ElementaryPredictableSet`: the type of elementary predictable sets
- `SimpleProcess`: the type of simple processes, as a Module over ℝ
- `SimpleProcess.toFun`: simple process interpreted as a stochastic process, with a CoeFun instance
- `SimpleProcess.integral`: elementary stochastic integral
- `SimpleProcess.isPredictable`: simple processes are predictable

## Implementation notes #

`SimpleProcess` consists of a value function as a `Finsupp`: `value : ι × ι →₀ Ω → F` and a value at ⊥: `valueBot : Ω → F`. This allows the definition of operations like addition to be defined naturally.

However, this makes the function `SimpleProcess.toFun` non-injective, so `SimpleProcess` is not `FunLike`. In other words, two distinct elements `X Y : SimpleProcess F 𝓕` may produce the same function `(⇑X : ι → Ω → F) = (⇑Y : ι → Ω → F)`.

There are subtleties that are caused by this: for example, by a nonnegative simple process, we mean `X : SimpleProcess F 𝓕` with `0 ≤ X.valueBot` and `0 ≤ X.value`, which is not the same as `0 ≤ (⇑X : ι → Ω → F)`.

Similarly, `ElementaryPredictableSet` is a data type that has a coercion to `Set (ι × Ω)`, but this coercion is not injective, so it is not `SetLike`. This makes it easy to define the indicator function of an elementary predictable set as a simple process by mapping respective datas (which is why it also requires disjoint unions).

## TODO #

- Generalize instance variables.

source
structure ProbabilityTheory.ElementaryPredictableSet {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} (𝓕 : MeasureTheory.Filtration ι mΩ) :
Type (max u_1 u_2)

An elementary predictable set is a finite disjoint union of sets of the form `{⊥} × B` for `B ∈ 𝓕 ⊥` and of the form `(s, t] × B` for `s < t` in `ι` and `B ∈ 𝓕 s`.

Note that we require the union to be disjoint. This is not necessary, but makes it easier to define the indicator function of an elementary predictable set as a `SimpleProcess`.

- setBot : Set Ω

  The set over `⊥`.

- I : Finset (ι × ι)

  The finite index for sets over `(s, t]`.

- set : ι × ι → Set Ω

  The sets over `(s, t]`.

- measurableSet_setBot : MeasurableSet self.setBot
- measurableSet_set (p : ι × ι) : p ∈ self.I → MeasurableSet (self.set p)
- pairwiseDisjoint : (↑self.I).PairwiseDisjoint fun (p : ι × ι) => Set.Ioc p.1 p.2 ×ˢ self.set p

Instances For

source
def ProbabilityTheory.ElementaryPredictableSet.toSet {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} (S : ElementaryPredictableSet 𝓕) :
Set (ι × Ω)

Coercion from an `ElementaryPredictableSet 𝓕` to a `Set (ι × Ω)`.

Equations

- ↑S = {⊥} ×ˢ S.setBot ∪ ⋃ p ∈ S.I, Set.Ioc p.1 p.2 ×ˢ S.set p

Instances For

source
instance ProbabilityTheory.ElementaryPredictableSet.instCoeOutSetProd {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} :
CoeOut (ElementaryPredictableSet 𝓕) (Set (ι × Ω))
Equations

- ProbabilityTheory.ElementaryPredictableSet.instCoeOutSetProd = { coe := ProbabilityTheory.ElementaryPredictableSet.toSet }

source
def ProbabilityTheory.ElementaryPredictableSet.singletonBotProd {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {B₀ : Set Ω} (hB₀ : MeasurableSet B₀) :
ElementaryPredictableSet 𝓕

The set `{⊥} × B₀` as an `ElementaryPredictableSet`.

Equations

- ProbabilityTheory.ElementaryPredictableSet.singletonBotProd hB₀ = { setBot := B₀, I := ∅, set := default, measurableSet_setBot := hB₀, measurableSet_set := ⋯, pairwiseDisjoint := ⋯ }

Instances For

source
@[simp]
theorem ProbabilityTheory.ElementaryPredictableSet.coe_singletonBotProd {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} {B₀ : Set Ω} (hB₀ : MeasurableSet B₀) :
↑(singletonBotProd hB₀) = {⊥} ×ˢ B₀
source
def ProbabilityTheory.ElementaryPredictableSet.IocProd {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} (i j : ι) {B : Set Ω} (hB : MeasurableSet B) :
ElementaryPredictableSet 𝓕

The set `(i, j] × B` as an `ElementaryPredictableSet`.

Equations

- ProbabilityTheory.ElementaryPredictableSet.IocProd i j hB = { setBot := ∅, I := {(i, j)}, set := fun (p : ι × ι) => B, measurableSet_setBot := ⋯, measurableSet_set := ⋯, pairwiseDisjoint := ⋯ }

Instances For

source
@[simp]
theorem ProbabilityTheory.ElementaryPredictableSet.coe_IocProd {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} (i j : ι) {B : Set Ω} (hB : MeasurableSet B) :
↑(IocProd i j hB) = Set.Ioc i j ×ˢ B
source
structure ProbabilityTheory.SimpleProcess {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} (F : Type u_4) [NormedAddCommGroup F] [MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] (𝓕 : MeasureTheory.Filtration ι mΩ) :
Type (max (max u_1 u_2) u_4)

A simple process is defined as a finite sum of indicator functions of intervals `(s, t]`, each assigned to a bounded `𝓕 s`-measurable random variable `value`, plus a `valueBot` at ⊥.

- valueBot : Ω → F

  The value at ⊥.

- value : ι × ι →₀ Ω → F

  The value on each interval. Note that intervals are not necessarily disjoint.

- measurable_valueBot : Measurable self.valueBot

  The value at ⊥ is measurable with respect to the filtration at ⊥.

- measurable_value' (p : ι × ι) : p ∈ self.value.support → Measurable (self.value p)

  The value on each interval is measurable with respect to the filtration at the left endpoint.

  Do not use this lemma directly. Use `SimpleProcess.measurable_value` instead.

- bounded_valueBot : ∃ (C : ℝ), ∀ (ω : Ω), ‖self.valueBot ω‖ ≤ C

  The value at ⊥ is bounded.

- bounded_value : ∃ (C : ℝ), ∀ p ∈ self.value.support, ∀ (ω : Ω), ‖self.value p ω‖ ≤ C

  The value on each interval is bounded.

Instances For

source
theorem ProbabilityTheory.SimpleProcess.ext {ι : Type u_1} {Ω : Type u_2} {inst✝ : LinearOrder ι} {inst✝¹ : OrderBot ι} {mΩ : MeasurableSpace Ω} {F : Type u_4} {inst✝² : NormedAddCommGroup F} {inst✝³ : MeasurableSpace F} {inst✝⁴ : NormedSpace ℝ F} {inst✝⁵ : BorelSpace F} {inst✝⁶ : SecondCountableTopology F} {𝓕 : MeasureTheory.Filtration ι mΩ} {x y : SimpleProcess F 𝓕} (valueBot : x.valueBot = y.valueBot) (value : x.value = y.value) :
x = y
source
theorem ProbabilityTheory.SimpleProcess.ext_iff {ι : Type u_1} {Ω : Type u_2} {inst✝ : LinearOrder ι} {inst✝¹ : OrderBot ι} {mΩ : MeasurableSpace Ω} {F : Type u_4} {inst✝² : NormedAddCommGroup F} {inst✝³ : MeasurableSpace F} {inst✝⁴ : NormedSpace ℝ F} {inst✝⁵ : BorelSpace F} {inst✝⁶ : SecondCountableTopology F} {𝓕 : MeasureTheory.Filtration ι mΩ} {x y : SimpleProcess F 𝓕} :
x = y ↔ x.valueBot = y.valueBot ∧ x.value = y.value
source
noncomputable def ProbabilityTheory.SimpleProcess.valueBotBound {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess F 𝓕) :
ℝ

A bound on the value at ⊥.

Equations

- V.valueBotBound = ⋯.choose

Instances For

source
@[simp]
theorem ProbabilityTheory.SimpleProcess.valueBot_le_valueBotBound {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess F 𝓕) (ω : Ω) :
‖V.valueBot ω‖ ≤ V.valueBotBound

The value at ⊥ is bounded by `valueBotBound`.

source
theorem ProbabilityTheory.SimpleProcess.measurable_value {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess F 𝓕) (p : ι × ι) :
Measurable (V.value p)

The value of the simple process at the left endpoint of an interval is measurable with respect to the filtration at the left endpoint.

Note that we do not require `p ∈ V.value.support`, because the value is 0 otherwise, which is measurable.

source
noncomputable def ProbabilityTheory.SimpleProcess.valueBound {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess F 𝓕) :
ℝ

A nonnegative bound on the value on each interval.

Equations

- V.valueBound = max 0 ⋯.choose

Instances For

source
@[simp]
theorem ProbabilityTheory.SimpleProcess.value_le_valueBound {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess F 𝓕) (p : ι × ι) (ω : Ω) :
‖V.value p ω‖ ≤ V.valueBound

The value on each interval is bounded by `valueBound`. Note that we do not require `p ∈ V.value.support`.

source
instance ProbabilityTheory.SimpleProcess.instZero {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} :
Zero (SimpleProcess F 𝓕)
Equations

- ProbabilityTheory.SimpleProcess.instZero = { zero := { valueBot := 0, value := 0, measurable_valueBot := ⋯, measurable_value' := ⋯, bounded_valueBot := ⋯, bounded_value := ⋯ } }

source
@[simp]
theorem ProbabilityTheory.SimpleProcess.zero_value {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} :
value 0 = 0
source
@[simp]
theorem ProbabilityTheory.SimpleProcess.zero_valueBot {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (a✝ : Ω) :
valueBot 0 a✝ = 0 a✝
source
instance ProbabilityTheory.SimpleProcess.instNeg {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} :
Neg (SimpleProcess F 𝓕)
Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem ProbabilityTheory.SimpleProcess.neg_value {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess F 𝓕) :
(-V).value = -V.value
source
@[simp]
theorem ProbabilityTheory.SimpleProcess.neg_valueBot {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess F 𝓕) (a✝ : Ω) :
(-V).valueBot a✝ = (-V.valueBot) a✝
source
instance ProbabilityTheory.SimpleProcess.instAdd {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} :
Add (SimpleProcess F 𝓕)
Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem ProbabilityTheory.SimpleProcess.add_valueBot {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (V W : SimpleProcess F 𝓕) (a✝ : Ω) :
(V + W).valueBot a✝ = (V.valueBot + W.valueBot) a✝
source
@[simp]
theorem ProbabilityTheory.SimpleProcess.add_value {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (V W : SimpleProcess F 𝓕) :
(V + W).value = V.value + W.value
source
instance ProbabilityTheory.SimpleProcess.instSub {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} :
Sub (SimpleProcess F 𝓕)
Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem ProbabilityTheory.SimpleProcess.sub_value {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (V W : SimpleProcess F 𝓕) :
(V - W).value = V.value - W.value
source
@[simp]
theorem ProbabilityTheory.SimpleProcess.sub_valueBot {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (V W : SimpleProcess F 𝓕) (a✝ : Ω) :
(V - W).valueBot a✝ = (V.valueBot - W.valueBot) a✝
source
instance ProbabilityTheory.SimpleProcess.instSMul {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} :
SMul ℝ (SimpleProcess F 𝓕)
Equations

- One or more equations did not get rendered due to their size.

source
@[simp]
theorem ProbabilityTheory.SimpleProcess.smul_valueBot {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (c : ℝ) (V : SimpleProcess F 𝓕) (a✝ : Ω) :
(c • V).valueBot a✝ = (c • V.valueBot) a✝
source
@[simp]
theorem ProbabilityTheory.SimpleProcess.smul_value {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (c : ℝ) (V : SimpleProcess F 𝓕) :
(c • V).value = c • V.value
source
instance ProbabilityTheory.SimpleProcess.instAddCommGroup {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} :
AddCommGroup (SimpleProcess F 𝓕)
Equations

- One or more equations did not get rendered due to their size.

source
instance ProbabilityTheory.SimpleProcess.instModule {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} :
Module ℝ (SimpleProcess F 𝓕)
Equations

- ProbabilityTheory.SimpleProcess.instModule = { toSMul := ProbabilityTheory.SimpleProcess.instSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

source
def ProbabilityTheory.SimpleProcess.toFun {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess F 𝓕) (i : ι) (ω : Ω) :
F

Coercion from a simple process to a function. Note that this is not injective.

Equations

- ↑V i ω = {⊥}.indicator (fun (x : ι) => V.valueBot ω) i + V.value.sum fun (p : ι × ι) (v : Ω → F) => (Set.Ioc p.1 p.2).indicator (fun (x : ι) => v ω) i

Instances For

source
instance ProbabilityTheory.SimpleProcess.instCoeFun {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} :
CoeFun (SimpleProcess F 𝓕) fun (x : SimpleProcess F 𝓕) => ι → Ω → F
Equations

- ProbabilityTheory.SimpleProcess.instCoeFun = { coe := ProbabilityTheory.SimpleProcess.toFun }

source
theorem ProbabilityTheory.SimpleProcess.apply_eq {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess F 𝓕) (i : ι) (ω : Ω) :
↑V i ω = {⊥}.indicator (fun (x : ι) => V.valueBot ω) i + V.value.sum fun (p : ι × ι) (v : Ω → F) => (Set.Ioc p.1 p.2).indicator (fun (x : ι) => v ω) i
source
@[simp]
theorem ProbabilityTheory.SimpleProcess.coe_zero {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} :
↑0 = 0
source
@[simp]
theorem ProbabilityTheory.SimpleProcess.coe_neg {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess F 𝓕) :
↑(-V) = -↑V
source
@[simp]
theorem ProbabilityTheory.SimpleProcess.coe_add {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (V W : SimpleProcess F 𝓕) :
↑(V + W) = ↑V + ↑W
source
@[simp]
theorem ProbabilityTheory.SimpleProcess.coe_sub {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (V W : SimpleProcess F 𝓕) :
↑(V - W) = ↑V - ↑W
source
@[simp]
theorem ProbabilityTheory.SimpleProcess.coe_smul {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (c : ℝ) (V : SimpleProcess F 𝓕) :
↑(c • V) = c • ↑V
source
theorem ProbabilityTheory.SimpleProcess.coe_bounded {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess F 𝓕) :
∃ (C : ℝ), ∀ (i : ι) (ω : Ω), ‖↑V i ω‖ ≤ C
source
def ProbabilityTheory.SimpleProcess.integral {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} {E : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] (B : E →L[ℝ] F →L[ℝ] G) (X : ι → Ω → E) (V : SimpleProcess F 𝓕) :
WithTop ι → Ω → G

The elementary stochastic integral.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem ProbabilityTheory.SimpleProcess.integral_zero_left {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} {E : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (V : SimpleProcess F 𝓕) :
integral B (fun (x : ι) => 0) V = fun (x : WithTop ι) => 0
source
@[simp]
theorem ProbabilityTheory.SimpleProcess.integral_neg_left {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} {E : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (X : ι → Ω → E) (V : SimpleProcess F 𝓕) :
integral B (-X) V = -integral B X V
source
@[simp]
theorem ProbabilityTheory.SimpleProcess.integral_add_left {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} {E : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (X Y : ι → Ω → E) (V : SimpleProcess F 𝓕) :
integral B (X + Y) V = integral B X V + integral B Y V
source
@[simp]
theorem ProbabilityTheory.SimpleProcess.integral_sub_left {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} {E : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (X Y : ι → Ω → E) (V : SimpleProcess F 𝓕) :
integral B (X - Y) V = integral B X V - integral B Y V
source
@[simp]
theorem ProbabilityTheory.SimpleProcess.integral_smul_left {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} {E : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (c : ℝ) (X : ι → Ω → E) (V : SimpleProcess F 𝓕) :
integral B (c • X) V = c • integral B X V
source
@[simp]
theorem ProbabilityTheory.SimpleProcess.integral_zero_right {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} {E : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (X : ι → Ω → E) :
integral B X 0 = fun (x : WithTop ι) => 0
source
@[simp]
theorem ProbabilityTheory.SimpleProcess.integral_neg_right {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} {E : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (X : ι → Ω → E) (V : SimpleProcess F 𝓕) :
integral B X (-V) = -integral B X V
source
@[simp]
theorem ProbabilityTheory.SimpleProcess.integral_add_right {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} {E : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (X : ι → Ω → E) (V W : SimpleProcess F 𝓕) :
integral B X (V + W) = integral B X V + integral B X W
source
@[simp]
theorem ProbabilityTheory.SimpleProcess.integral_sub_right {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} {E : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (X : ι → Ω → E) (V W : SimpleProcess F 𝓕) :
integral B X (V - W) = integral B X V - integral B X W
source
@[simp]
theorem ProbabilityTheory.SimpleProcess.integral_smul_right {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} {E : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (c : ℝ) (X : ι → Ω → E) (V : SimpleProcess F 𝓕) :
integral B X (c • V) = c • integral B X V
source
def ProbabilityTheory.ElementaryPredictableSet.indicator {ι : Type u_1} {Ω : Type u_2} (F : Type u_3) [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} [One F] (S : ElementaryPredictableSet 𝓕) :
SimpleProcess F 𝓕

The indicator function of an elementary predictable set as a simple process.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem ProbabilityTheory.ElementaryPredictableSet.coe_indicator {ι : Type u_1} {Ω : Type u_2} (F : Type u_3) [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} [One F] (S : ElementaryPredictableSet 𝓕) :
↑(indicator F S) = Function.curry ((↑S).indicator 1)
source
theorem ProbabilityTheory.ElementaryPredictableSet.integral_indicator {ι : Type u_1} {Ω : Type u_2} (F : Type u_3) [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} {E : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup G] [NormedSpace ℝ G] [One F] (S : ElementaryPredictableSet 𝓕) (B : E →L[ℝ] F →L[ℝ] G) (X : ι → Ω → E) :
SimpleProcess.integral B X (indicator F S) = fun (i : WithTop ι) (ω : Ω) => ∑ p ∈ S.I, (B (MeasureTheory.stoppedProcess X (fun (x : Ω) => i) p.2 ω - MeasureTheory.stoppedProcess X (fun (x : Ω) => i) p.1 ω)) ((S.set p).indicator 1 ω)

Explicit formula for `1_S ● X` where `S` is an elementary predictable set.

source
theorem ProbabilityTheory.ElementaryPredictableSet.measurableSet_predictable {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} (S : ElementaryPredictableSet 𝓕) :
MeasurableSet ↑S
source
theorem ProbabilityTheory.ElementaryPredictableSet.generateFrom_eq_predictable (ι : Type u_1) (Ω : Type u_2) [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} [Filter.atTop.IsCountablyGenerated] :
MeasurableSpace.generateFrom {x : Set (ι × Ω) | ∃ (S : ElementaryPredictableSet 𝓕), ↑S = x} = 𝓕.predictable

The elementary predictable sets generate the predictable σ-algebra. Note that we require the time domain to have countably generated `atTop` so that each `(t, ∞]` can be written as a countable union of intervals `(t, s]`.

source
theorem ProbabilityTheory.SimpleProcess.isPredictable {ι : Type u_1} {Ω : Type u_2} {F : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess F 𝓕) :
MeasureTheory.IsPredictable 𝓕 ↑V
source
theorem ProbabilityTheory.SimpleProcess.iSup_comap_eq_predictable {ι : Type u_1} {Ω : Type u_2} (F : Type u_3) [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup F] [mF : MeasurableSpace F] [NormedSpace ℝ F] [BorelSpace F] [SecondCountableTopology F] (𝓕 : MeasureTheory.Filtration ι mΩ) [Filter.atTop.IsCountablyGenerated] [One F] [NeZero 1] :
⨆ (V : SimpleProcess F 𝓕), MeasurableSpace.comap (Function.uncurry ↑V) mF = 𝓕.predictable