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.

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

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

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 }

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 := ⋯ }

@[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₀

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 := ⋯ }

@[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

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.

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

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

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

@[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.

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.

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

@[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.

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 := ⋯ } }

@[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

@[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✝

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.

@[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

@[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✝

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.

@[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✝

@[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

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.

@[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

@[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✝

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.

@[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✝

@[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

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.

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 := ⋯ }

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

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 }

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

@[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

@[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

@[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

@[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

@[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

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

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.

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

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.

@[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)

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.

theorem ProbabilityTheory.ElementaryPredictableSet.measurableSet_predictable {ι : Type u_1} {Ω : Type u_2} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ι mΩ} (S : ElementaryPredictableSet 𝓕) : MeasurableSet ↑S

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].

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

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