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 : ι × ι →₀ Ω → E and a value at ⊥: valueBot : Ω → E. 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 E 𝓕 may produce the same function (⇑X : ι → Ω → E) = (⇑Y : ι → Ω → E).

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

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

• le_of_mem_I (p : ι × ι) : p ∈ self.I → p.1 ≤ p.2
• 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

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

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

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

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

• le_of_mem_support_value (p : ι × ι) : p ∈ self.value.support → p.1 ≤ p.2

  The intervals in the support of value are ordered.

• 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} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess E 𝓕) : ℝ

A bound on the value at ⊥.

Equations

• V.valueBotBound = max 0 ⋯.choose

@[simp]

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

The value at ⊥ is bounded by valueBotBound.

@[simp]

theorem ProbabilityTheory.SimpleProcess.valueBotBound_nonneg {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess E 𝓕) : 0 ≤ V.valueBotBound

theorem ProbabilityTheory.SimpleProcess.measurable_value {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess E 𝓕) (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} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess E 𝓕) : ℝ

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} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess E 𝓕) (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.

@[simp]

theorem ProbabilityTheory.SimpleProcess.valueBound_nonneg {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess E 𝓕) : 0 ≤ V.valueBound

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

Equations

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

@[simp]

theorem ProbabilityTheory.SimpleProcess.zero_valueBot {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (a✝ : Ω) : valueBot 0 a✝ = 0 a✝

@[simp]

theorem ProbabilityTheory.SimpleProcess.zero_value {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} : value 0 = 0

instance ProbabilityTheory.SimpleProcess.instNeg {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} : Neg (SimpleProcess E 𝓕)

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} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess E 𝓕) : (-V).value = -V.value

@[simp]

theorem ProbabilityTheory.SimpleProcess.neg_valueBot {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess E 𝓕) (a✝ : Ω) : (-V).valueBot a✝ = (-V.valueBot) a✝

instance ProbabilityTheory.SimpleProcess.instAdd {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} : Add (SimpleProcess E 𝓕)

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} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (V W : SimpleProcess E 𝓕) (a✝ : Ω) : (V + W).valueBot a✝ = (V.valueBot + W.valueBot) a✝

@[simp]

theorem ProbabilityTheory.SimpleProcess.add_value {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (V W : SimpleProcess E 𝓕) : (V + W).value = V.value + W.value

instance ProbabilityTheory.SimpleProcess.instSub {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} : Sub (SimpleProcess E 𝓕)

Equations

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

@[simp]

theorem ProbabilityTheory.SimpleProcess.sub_valueBot {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (V W : SimpleProcess E 𝓕) (a✝ : Ω) : (V - W).valueBot a✝ = (V.valueBot - W.valueBot) a✝

@[simp]

theorem ProbabilityTheory.SimpleProcess.sub_value {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (V W : SimpleProcess E 𝓕) : (V - W).value = V.value - W.value

instance ProbabilityTheory.SimpleProcess.instSMul {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} : SMul ℝ (SimpleProcess E 𝓕)

Equations

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

@[simp]

theorem ProbabilityTheory.SimpleProcess.smul_value {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (c : ℝ) (V : SimpleProcess E 𝓕) : (c • V).value = c • V.value

@[simp]

theorem ProbabilityTheory.SimpleProcess.smul_valueBot {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (c : ℝ) (V : SimpleProcess E 𝓕) (a✝ : Ω) : (c • V).valueBot a✝ = (c • V.valueBot) a✝

instance ProbabilityTheory.SimpleProcess.instAddCommGroup {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} : AddCommGroup (SimpleProcess E 𝓕)

Equations

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

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

Equations

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

theorem ProbabilityTheory.SimpleProcess.Finset.measurable_prod' {M : Type u_4} {ι : Type u_5} {α : Type u_6} [CommMonoid M] [MeasurableSpace M] [MeasurableMul₂ M] {m : MeasurableSpace α} {f : ι → α → M} (s : Finset ι) (hf : ∀ i ∈ s, Measurable (f i)) : Measurable (∏ i ∈ s, f i)

theorem ProbabilityTheory.SimpleProcess.Finset.measurable_sum' {M : Type u_4} {ι : Type u_5} {α : Type u_6} [AddCommMonoid M] [MeasurableSpace M] [MeasurableAdd₂ M] {m : MeasurableSpace α} {f : ι → α → M} (s : Finset ι) (hf : ∀ i ∈ s, Measurable (f i)) : Measurable (∑ i ∈ s, f i)

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

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 : Ω → E) => (Set.Ioc p.1 p.2).indicator (fun (x : ι) => v ω) i

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

Equations

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

theorem ProbabilityTheory.SimpleProcess.apply_eq {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess E 𝓕) (i : ι) (ω : Ω) : ↑V i ω = {⊥}.indicator (fun (x : ι) => V.valueBot ω) i + V.value.sum fun (p : ι × ι) (v : Ω → E) => (Set.Ioc p.1 p.2).indicator (fun (x : ι) => v ω) i

@[simp]

theorem ProbabilityTheory.SimpleProcess.coe_zero {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} : ↑0 = 0

@[simp]

theorem ProbabilityTheory.SimpleProcess.coe_neg {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess E 𝓕) : ↑(-V) = -↑V

@[simp]

theorem ProbabilityTheory.SimpleProcess.coe_add {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (V W : SimpleProcess E 𝓕) : ↑(V + W) = ↑V + ↑W

@[simp]

theorem ProbabilityTheory.SimpleProcess.coe_sub {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (V W : SimpleProcess E 𝓕) : ↑(V - W) = ↑V - ↑W

@[simp]

theorem ProbabilityTheory.SimpleProcess.coe_smul {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (c : ℝ) (V : SimpleProcess E 𝓕) : ↑(c • V) = c • ↑V

theorem ProbabilityTheory.SimpleProcess.coe_bounded {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess E 𝓕) : ∃ (C : ℝ), ∀ (i : ι) (ω : Ω), ‖↑V i ω‖ ≤ C

def ProbabilityTheory.SimpleProcess.integral {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] (B : E →L[ℝ] F →L[ℝ] G) (V : SimpleProcess E 𝓕) (X : ι → Ω → F) : WithTop ι → Ω → G

The elementary stochastic integral with respect to a continuous bilinear map B.

Equations

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

@[reducible, inline]

abbrev ProbabilityTheory.SimpleProcess.integralEval {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] [SecondCountableTopology (E →L[ℝ] F)] (V : SimpleProcess (E →L[ℝ] F) 𝓕) (X : ι → Ω → E) : WithTop ι → Ω → F

The linear elementary stochastic integral where the simple process takes values in E →L[ℝ] F, as a special case of integral with B the evaluation map.

Equations

• V.integralEval X = ProbabilityTheory.SimpleProcess.integral (ContinuousLinearMap.id ℝ (E →L[ℝ] F)) V X

@[simp]

theorem ProbabilityTheory.SimpleProcess.integral_const_right {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (c : Ω → F) (V : SimpleProcess E 𝓕) : (integral B V fun (x : ι) => c) = fun (x : WithTop ι) => 0

@[simp]

theorem ProbabilityTheory.SimpleProcess.integral_neg_right {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (V : SimpleProcess E 𝓕) (X : ι → Ω → F) : integral B V (-X) = -integral B V X

@[simp]

theorem ProbabilityTheory.SimpleProcess.integral_add_right {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (V : SimpleProcess E 𝓕) (X Y : ι → Ω → F) : integral B V (X + Y) = integral B V X + integral B V Y

@[simp]

theorem ProbabilityTheory.SimpleProcess.integral_sub_right {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (V : SimpleProcess E 𝓕) (X Y : ι → Ω → F) : integral B V (X - Y) = integral B V X - integral B V Y

@[simp]

theorem ProbabilityTheory.SimpleProcess.integral_smul_right {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (c : ℝ) (V : SimpleProcess E 𝓕) (X : ι → Ω → F) : integral B V (c • X) = c • integral B V X

@[simp]

theorem ProbabilityTheory.SimpleProcess.integral_zero_left {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (X : ι → Ω → F) : integral B 0 X = fun (x : WithTop ι) => 0

@[simp]

theorem ProbabilityTheory.SimpleProcess.integral_neg_left {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (V : SimpleProcess E 𝓕) (X : ι → Ω → F) : integral B (-V) X = -integral B V X

@[simp]

theorem ProbabilityTheory.SimpleProcess.integral_add_left {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (V W : SimpleProcess E 𝓕) (X : ι → Ω → F) : integral B (V + W) X = integral B V X + integral B W X

@[simp]

theorem ProbabilityTheory.SimpleProcess.integral_sub_left {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (V W : SimpleProcess E 𝓕) (X : ι → Ω → F) : integral B (V - W) X = integral B V X - integral B W X

@[simp]

theorem ProbabilityTheory.SimpleProcess.integral_smul_left {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (c : ℝ) (V : SimpleProcess E 𝓕) (X : ι → Ω → F) : integral B (c • V) X = c • integral B V X

@[simp]

theorem ProbabilityTheory.SimpleProcess.integral_bot {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (V : SimpleProcess E 𝓕) (X : ι → Ω → F) : integral B V X ⊥ = fun (x : Ω) => 0

@[simp]

theorem ProbabilityTheory.SimpleProcess.integral_top {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (V : SimpleProcess E 𝓕) (X : ι → Ω → F) (ω : Ω) : integral B V X ⊤ ω = V.value.sum fun (p : ι × ι) (v : Ω → E) => (B (v ω)) (X p.2 ω - X p.1 ω)

theorem ProbabilityTheory.SimpleProcess.stoppedProcess_integral {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G} (V : SimpleProcess E 𝓕) (X : ι → Ω → F) (τ : Ω → WithTop ι) : MeasureTheory.stoppedProcess (integral B V X ∘ WithTop.some) τ = integral B V (MeasureTheory.stoppedProcess X τ) ∘ WithTop.some

def ProbabilityTheory.SimpleProcess.map₂ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] [MeasurableSpace F] [BorelSpace F] [SecondCountableTopology F] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (B : E →L[ℝ] F →L[ℝ] G) (V : SimpleProcess E 𝓕) (W : SimpleProcess F 𝓕) : SimpleProcess G 𝓕

Application of a bounded bilinear map pointwise to two simple processes.

Equations

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

@[simp]

theorem ProbabilityTheory.SimpleProcess.map₂_value {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] [MeasurableSpace F] [BorelSpace F] [SecondCountableTopology F] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (B : E →L[ℝ] F →L[ℝ] G) (V : SimpleProcess E 𝓕) (W : SimpleProcess F 𝓕) : (map₂ B V W).value = V.value.sum fun (p : ι × ι) (v : Ω → E) => W.value.sum fun (q : ι × ι) (w : Ω → F) => Finsupp.single (max p.1 q.1, min p.2 q.2) (if q.1 ≤ p.2 ∧ p.1 ≤ q.2 then fun (ω : Ω) => (B (v ω)) (w ω) else 0)

@[simp]

theorem ProbabilityTheory.SimpleProcess.map₂_valueBot {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] [MeasurableSpace F] [BorelSpace F] [SecondCountableTopology F] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (B : E →L[ℝ] F →L[ℝ] G) (V : SimpleProcess E 𝓕) (W : SimpleProcess F 𝓕) (ω : Ω) : (map₂ B V W).valueBot ω = (B (V.valueBot ω)) (W.valueBot ω)

theorem ProbabilityTheory.SimpleProcess.map₂_swap {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] [MeasurableSpace F] [BorelSpace F] [SecondCountableTopology F] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (B : E →L[ℝ] F →L[ℝ] G) (V : SimpleProcess E 𝓕) (W : SimpleProcess F 𝓕) : map₂ B V W = map₂ B.flip W V

@[simp]

theorem ContinuousLinearMap.finsuppSum_apply {R₁ : Type u_6} {R₂ : Type u_7} [Semiring R₁] [Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_8} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_9} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₂ M₂] [ContinuousAdd M₂] {ι : Type u_10} {A : Type u_11} [Zero A] (g : ι →₀ A) (f : ι → A → M₁ →SL[σ₁₂] M₂) (b : M₁) : (g.sum f) b = g.sum fun (i : ι) (a : A) => (f i a) b

@[simp]

theorem ProbabilityTheory.SimpleProcess.coe_map₂ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] [MeasurableSpace F] [BorelSpace F] [SecondCountableTopology F] [MeasurableSpace G] [BorelSpace G] [SecondCountableTopology G] (B : E →L[ℝ] F →L[ℝ] G) (V : SimpleProcess E 𝓕) (W : SimpleProcess F 𝓕) : ↑(map₂ B V W) = fun (i : ι) (ω : Ω) => (B (↑V i ω)) (↑W i ω)

Interpreted as functions, map₂ is just applying B pointwise.

theorem ProbabilityTheory.SimpleProcess.integral_assoc {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] [MeasurableSpace F] [BorelSpace F] [SecondCountableTopology F] {H : Type u_6} [NormedAddCommGroup H] [NormedSpace ℝ H] {I : Type u_7} [NormedAddCommGroup I] [NormedSpace ℝ I] {J : Type u_8} [NormedAddCommGroup J] [NormedSpace ℝ J] [MeasurableSpace J] [BorelSpace J] [SecondCountableTopology J] {B₁ : E →L[ℝ] H →L[ℝ] I} {B₂ : F →L[ℝ] G →L[ℝ] H} {B₃ : E →L[ℝ] F →L[ℝ] J} {B₄ : J →L[ℝ] G →L[ℝ] I} (hB : ∀ (x : E) (y : F) (z : G), (B₁ x) ((B₂ y) z) = (B₄ ((B₃ x) y)) z) (V : SimpleProcess E 𝓕) (W : SimpleProcess F 𝓕) (X : ι → Ω → G) : integral B₁ V (integral B₂ W X ∘ WithTop.some) = integral B₄ (map₂ B₃ V W) X

The most general case of associativity of the elementary stochastic integral.

def ProbabilityTheory.SimpleProcess.comp {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] [SecondCountableTopology (F →L[ℝ] G)] [SecondCountableTopology (E →L[ℝ] F)] [SecondCountableTopology (E →L[ℝ] G)] (V : SimpleProcess (F →L[ℝ] G) 𝓕) (W : SimpleProcess (E →L[ℝ] F) 𝓕) : SimpleProcess (E →L[ℝ] G) 𝓕

Composition of simple processes taking values in continuous linear maps.

Equations

• V.comp W = ProbabilityTheory.SimpleProcess.map₂ (ContinuousLinearMap.compL ℝ E F G) V W

@[simp]

theorem ProbabilityTheory.SimpleProcess.comp_valueBot_apply {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] [SecondCountableTopology (F →L[ℝ] G)] [SecondCountableTopology (E →L[ℝ] F)] [SecondCountableTopology (E →L[ℝ] G)] (V : SimpleProcess (F →L[ℝ] G) 𝓕) (W : SimpleProcess (E →L[ℝ] F) 𝓕) (ω : Ω) (a✝ : E) : ((V.comp W).valueBot ω) a✝ = (V.valueBot ω) ((W.valueBot ω) a✝)

@[simp]

theorem ProbabilityTheory.SimpleProcess.comp_value {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] [SecondCountableTopology (F →L[ℝ] G)] [SecondCountableTopology (E →L[ℝ] F)] [SecondCountableTopology (E →L[ℝ] G)] (V : SimpleProcess (F →L[ℝ] G) 𝓕) (W : SimpleProcess (E →L[ℝ] F) 𝓕) : (V.comp W).value = V.value.sum fun (p : ι × ι) (v : Ω → F →L[ℝ] G) => W.value.sum fun (q : ι × ι) (w : Ω → E →L[ℝ] F) => Finsupp.single (max p.1 q.1, min p.2 q.2) (if q.1 ≤ p.2 ∧ p.1 ≤ q.2 then fun (ω : Ω) => (v ω).comp (w ω) else 0)

@[simp]

theorem ProbabilityTheory.SimpleProcess.coe_comp {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] [SecondCountableTopology (F →L[ℝ] G)] [SecondCountableTopology (E →L[ℝ] F)] [SecondCountableTopology (E →L[ℝ] G)] (V : SimpleProcess (F →L[ℝ] G) 𝓕) (W : SimpleProcess (E →L[ℝ] F) 𝓕) : ↑(V.comp W) = fun (i : ι) (ω : Ω) => (↑V i ω).comp (↑W i ω)

theorem ProbabilityTheory.SimpleProcess.integralEval_assoc {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] [SecondCountableTopology (F →L[ℝ] G)] [SecondCountableTopology (E →L[ℝ] F)] [SecondCountableTopology (E →L[ℝ] G)] (X : ι → Ω → E) (V : SimpleProcess (F →L[ℝ] G) 𝓕) (W : SimpleProcess (E →L[ℝ] F) 𝓕) : V.integralEval (W.integralEval X ∘ WithTop.some) = (V.comp W).integralEval X

def ProbabilityTheory.ElementaryPredictableSet.indicator {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (S : ElementaryPredictableSet 𝓕) (e : E) : SimpleProcess E 𝓕

The indicator function of an elementary predictable set as a simple process. This takes value 0 at time not in S, and e at time S.

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} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (S : ElementaryPredictableSet 𝓕) (e : E) : ↑(S.indicator e) = Function.curry ((↑S).indicator fun (x : ι × Ω) => e)

theorem ProbabilityTheory.ElementaryPredictableSet.integral_indicator_apply {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_5} [NormedAddCommGroup G] [NormedSpace ℝ G] (S : ElementaryPredictableSet 𝓕) (e : E) (B : E →L[ℝ] F →L[ℝ] G) (X : ι → Ω → F) (i : ι) (ω : Ω) : SimpleProcess.integral B (S.indicator e) X (↑i) ω = ∑ p ∈ S.I, (S.set p).indicator (fun (ω : Ω) => (B e) (MeasureTheory.stoppedProcess X (fun (x : Ω) => ↑i) p.2 ω - MeasureTheory.stoppedProcess X (fun (x : Ω) => ↑i) p.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} {E : Type u_3} [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] {𝓕 : MeasureTheory.Filtration ι mΩ} (V : SimpleProcess E 𝓕) : MeasureTheory.IsPredictable 𝓕 ↑V

theorem ProbabilityTheory.SimpleProcess.iSup_comap_eq_predictable {ι : Type u_1} {Ω : Type u_2} (E : Type u_3) [LinearOrder ι] [OrderBot ι] {mΩ : MeasurableSpace Ω} [NormedAddCommGroup E] [mE : MeasurableSpace E] [NormedSpace ℝ E] [BorelSpace E] [SecondCountableTopology E] (𝓕 : MeasureTheory.Filtration ι mΩ) [Filter.atTop.IsCountablyGenerated] [MeasurableSingletonClass E] [Nontrivial E] : ⨆ (V : SimpleProcess E 𝓕), MeasurableSpace.comap (Function.uncurry ↑V) mE = 𝓕.predictable