The Keneral Associated with a Process

def StieltjesFunction.restrict {ι : Type u_1} [TopologicalSpace ι] [LinearOrder ι] (f : StieltjesFunction ι) (s : Set ι) : StieltjesFunction ↑s

Restrict domain of a Stieltjes function f to a set s.

Equations

• f.restrict s = { toFun := fun (x : ↑s) => ↑f ↑x, mono' := ⋯, right_continuous' := ⋯ }

theorem StieltjesFunction.bddAbove_restrict_Ioc {ι : Type u_1} [TopologicalSpace ι] [LinearOrder ι] {a b : ι} (f : StieltjesFunction ι) : BddAbove (Set.range ↑(f.restrict (Set.Ioc a b)))

theorem StieltjesFunction.bddBelow_restrict_Ioc {ι : Type u_1} [TopologicalSpace ι] [LinearOrder ι] {a b : ι} (f : StieltjesFunction ι) : BddBelow (Set.range ↑(f.restrict (Set.Ioc a b)))

theorem StieltjesFunction.iSup_restrict_Ioc {ι : Type u_1} [TopologicalSpace ι] [LinearOrder ι] {a b : ι} (f : StieltjesFunction ι) (hab : a < b) : ⨆ (i : ↑(Set.Ioc a b)), ↑(f.restrict (Set.Ioc a b)) i = ↑f b

theorem StieltjesFunction.iInf_restrict_Ioc {ι : Type u_1} [TopologicalSpace ι] [LinearOrder ι] {a b : ι} [OrderTopology ι] [DenselyOrdered ι] (f : StieltjesFunction ι) (hab : a < b) : ⨅ (i : ↑(Set.Ioc a b)), ↑(f.restrict (Set.Ioc a b)) i = ↑f a

instance instCompactIccSpaceElemIoc_brownianMotion {X : Type u_4} [TopologicalSpace X] [Preorder X] [CompactIccSpace X] {a b : X} : CompactIccSpace ↑(Set.Ioc a b)

theorem StieltjesFunction.measure_restrict_Ioc {ι : Type u_1} [TopologicalSpace ι] [LinearOrder ι] {a b : ι} [OrderTopology ι] [DenselyOrdered ι] [MeasurableSpace ι] [BorelSpace ι] [CompactIccSpace ι] [SecondCountableTopology ι] (f : StieltjesFunction ι) (hab : a < b) : (f.restrict (Set.Ioc a b)).measure Set.univ = ENNReal.ofReal (↑f b - ↑f a)

instance StieltjesFunction.isFiniteMeasure_restrict_Ioc {ι : Type u_1} [TopologicalSpace ι] [LinearOrder ι] {a b : ι} [OrderTopology ι] [DenselyOrdered ι] [MeasurableSpace ι] [BorelSpace ι] [CompactIccSpace ι] [SecondCountableTopology ι] {f : StieltjesFunction ι} : MeasureTheory.IsFiniteMeasure (f.restrict (Set.Ioc a b)).measure

theorem StieltjesFunction.measure_restrict_eq_comap {ι : Type u_1} [TopologicalSpace ι] [LinearOrder ι] [OrderTopology ι] [DenselyOrdered ι] [MeasurableSpace ι] [BorelSpace ι] [CompactIccSpace ι] [SecondCountableTopology ι] (f : StieltjesFunction ι) (a b : ι) : (f.restrict (Set.Ioc a b)).measure = MeasureTheory.Measure.comap Subtype.val f.measure

theorem StieltjesFunction.measurable_measure' {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] {mΩ : MeasurableSpace Ω} [OrderTopology ι] [DenselyOrdered ι] [MeasurableSpace ι] [BorelSpace ι] [CompactIccSpace ι] [SecondCountableTopology ι] {f : Ω → StieltjesFunction ι} (hf : ∀ (i : ι), Measurable fun (x : Ω) => ↑(f x) i) : Measurable fun (ω : Ω) => (f ω).measure

def StieltjesFunction.rightContMono {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] {X : ι → Ω → ℝ} (hcont : ∀ (ω : Ω), Function.IsRightContinuous fun (x : ι) => X x ω) (hmono : ∀ (ω : Ω), Monotone fun (x : ι) => X x ω) : Ω → StieltjesFunction ι

If X : ι → Ω → ℝ is a right continuous and monotone process, then for each ω : Ω, X · ω is a StieltjesFunction defined on ι.

Equations

• StieltjesFunction.rightContMono hcont hmono ω = { toFun := fun (x : ι) => X x ω, mono' := ⋯, right_continuous' := ⋯ }

noncomputable def StieltjesFunction.kernel {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] {mΩ : MeasurableSpace Ω} [OrderTopology ι] [DenselyOrdered ι] [MeasurableSpace ι] [BorelSpace ι] [CompactIccSpace ι] [SecondCountableTopology ι] {f : Ω → StieltjesFunction ι} (hf : ∀ (i : ι), Measurable fun (x : Ω) => ↑(f x) i) : ProbabilityTheory.Kernel Ω ι

If f : Ω → StieltjesFunction ι satisfies for each i, f · i is measurable, then f defines a kernel.

Equations

• StieltjesFunction.kernel hf = { toFun := fun (ω : Ω) => (f ω).measure, measurable' := ⋯ }

noncomputable def StieltjesFunction.kernelOfRightContAdaptedMono {ι : Type u_1} {Ω : Type u_2} [TopologicalSpace ι] [LinearOrder ι] {mΩ : MeasurableSpace Ω} {ℱ : MeasureTheory.Filtration ι mΩ} {X : ι → Ω → ℝ} [OrderTopology ι] [DenselyOrdered ι] [MeasurableSpace ι] [BorelSpace ι] [CompactIccSpace ι] [SecondCountableTopology ι] (ha : MeasureTheory.Adapted ℱ X) (hcont : ∀ (ω : Ω), Function.IsRightContinuous fun (x : ι) => X x ω) (hmono : ∀ (ω : Ω), Monotone fun (x : ι) => X x ω) : ProbabilityTheory.Kernel Ω ι

If X : ι → Ω → ℝ is a right continuous, adapted, and monotone process, then X defines a kernel that maps each ω to (X · ω).measure.

Equations

• StieltjesFunction.kernelOfRightContAdaptedMono ha hcont hmono = { toFun := fun (ω : Ω) => (StieltjesFunction.rightContMono hcont hmono ω).measure, measurable' := ⋯ }

@[implicit_reducible]

instance MeasureTheory.VectorMeasure.instMeasurableSpace_brownianMotion {E : Type u_3} {ι : Type u_4} [MeasurableSpace ι] [AddCommMonoid E] [TopologicalSpace E] : MeasurableSpace (VectorMeasure ι E)

Measurability structure on VectorMeasure.

Equations

• MeasureTheory.VectorMeasure.instMeasurableSpace_brownianMotion = ⨆ (s : Set ι), ⨆ (_ : MeasurableSet s), MeasurableSpace.comap (fun (μ : MeasureTheory.VectorMeasure ι E) => ↑μ s) (borel E)

theorem MeasureTheory.VectorMeasure.measurable_coe {E : Type u_3} {ι : Type u_4} [MeasurableSpace ι] [AddCommMonoid E] [TopologicalSpace E] [MeasurableSpace E] [BorelSpace E] {s : Set ι} (hs : MeasurableSet s) : Measurable fun (μ : VectorMeasure ι E) => ↑μ s

theorem MeasureTheory.VectorMeasure.measurable_of_measurable_coe {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {ι : Type u_4} [MeasurableSpace ι] [AddCommMonoid E] [TopologicalSpace E] [MeasurableSpace E] [BorelSpace E] {f : Ω → VectorMeasure ι E} (h : ∀ (s : Set ι), MeasurableSet s → Measurable fun (ω : Ω) => ↑(f ω) s) : Measurable f

theorem stronglyMeasurable_limUnder_atTop {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [LinearOrder ι] {mΩ : MeasurableSpace Ω} {Y : ι → Ω → E} [OrderTopology ι] [SecondCountableTopology ι] [NormedAddCommGroup E] [CompleteSpace E] [Nonempty ι] (hY : ∀ (i : ι), MeasureTheory.StronglyMeasurable (Y i)) (hvar : ∀ (ω : Ω), BoundedVariationOn (fun (x : ι) => Y x ω) Set.univ) : MeasureTheory.StronglyMeasurable fun (ω : Ω) => Filter.atTop.limUnder fun (x : ι) => Y x ω

theorem stronglyMeasurable_limUnder_atBot {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [LinearOrder ι] {mΩ : MeasurableSpace Ω} {Y : ι → Ω → E} [OrderTopology ι] [SecondCountableTopology ι] [NormedAddCommGroup E] [CompleteSpace E] [Nonempty ι] (hY : ∀ (i : ι), MeasureTheory.StronglyMeasurable (Y i)) (hvar : ∀ (ω : Ω), BoundedVariationOn (fun (x : ι) => Y x ω) Set.univ) : MeasureTheory.StronglyMeasurable fun (ω : Ω) => Filter.atBot.limUnder fun (x : ι) => Y x ω

theorem stronglyMeasurable_rightLim {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [LinearOrder ι] {mΩ : MeasurableSpace Ω} {Y : ι → Ω → E} [OrderTopology ι] [SecondCountableTopology ι] [NormedAddCommGroup E] [CompleteSpace E] [DenselyOrdered ι] (hY : ∀ (i : ι), MeasureTheory.StronglyMeasurable (Y i)) (hvar : ∀ (ω : Ω), BoundedVariationOn (fun (x : ι) => Y x ω) Set.univ) (x : ι) : MeasureTheory.StronglyMeasurable fun (ω : Ω) => Function.rightLim (fun (x : ι) => Y x ω) x

theorem stronglyMeasurable_vectorMeasure_Ioc {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [LinearOrder ι] {mΩ : MeasurableSpace Ω} {Y : ι → Ω → E} [OrderTopology ι] [SecondCountableTopology ι] [NormedAddCommGroup E] [CompleteSpace E] [DenselyOrdered ι] [MeasurableSpace ι] [BorelSpace ι] [CompactIccSpace ι] (hY : ∀ (i : ι), MeasureTheory.StronglyMeasurable (Y i)) (hvar : ∀ (ω : Ω), BoundedVariationOn (fun (x : ι) => Y x ω) Set.univ) {a b : ι} (hab : a ≤ b) : MeasureTheory.StronglyMeasurable fun (ω : Ω) => ↑⋯.vectorMeasure (Set.Ioc a b)

theorem stronglyMeasurable_vectorMeasure_univ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [LinearOrder ι] {mΩ : MeasurableSpace Ω} {Y : ι → Ω → E} [OrderTopology ι] [SecondCountableTopology ι] [NormedAddCommGroup E] [CompleteSpace E] [DenselyOrdered ι] [MeasurableSpace ι] [BorelSpace ι] [CompactIccSpace ι] (hY : ∀ (i : ι), MeasureTheory.StronglyMeasurable (Y i)) (hvar : ∀ (ω : Ω), BoundedVariationOn (fun (x : ι) => Y x ω) Set.univ) : MeasureTheory.StronglyMeasurable fun (ω : Ω) => ↑⋯.vectorMeasure Set.univ

theorem BoundedVariationOn.measurable_vectorMeasure_of_stronglyMeasurable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [LinearOrder ι] {mΩ : MeasurableSpace Ω} {Y : ι → Ω → E} [OrderTopology ι] [DenselyOrdered ι] [MeasurableSpace ι] [BorelSpace ι] [CompactIccSpace ι] [SecondCountableTopology ι] [NormedAddCommGroup E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] (hY : ∀ (i : ι), MeasureTheory.StronglyMeasurable (Y i)) (hvar : ∀ (ω : Ω), BoundedVariationOn (fun (x : ι) => Y x ω) Set.univ) : Measurable fun (ω : Ω) => ⋯.vectorMeasure

theorem BoundedVariationOn.measurable_vectorMeasure_of_measurable {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [LinearOrder ι] {mΩ : MeasurableSpace Ω} {Y : ι → Ω → E} [OrderTopology ι] [DenselyOrdered ι] [MeasurableSpace ι] [BorelSpace ι] [CompactIccSpace ι] [SecondCountableTopology ι] [NormedAddCommGroup E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (hY : ∀ (i : ι), Measurable (Y i)) (hvar : ∀ (ω : Ω), BoundedVariationOn (fun (x : ι) => Y x ω) Set.univ) : Measurable fun (ω : Ω) => ⋯.vectorMeasure

theorem BoundedVariationOn.measurable_vectorMeasure_of_adapted {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [LinearOrder ι] {mΩ : MeasurableSpace Ω} {ℱ : MeasureTheory.Filtration ι mΩ} {Y : ι → Ω → E} [OrderTopology ι] [DenselyOrdered ι] [MeasurableSpace ι] [BorelSpace ι] [CompactIccSpace ι] [SecondCountableTopology ι] [NormedAddCommGroup E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] (ha : MeasureTheory.Adapted ℱ Y) (hvar : ∀ (ω : Ω), BoundedVariationOn (fun (x : ι) => Y x ω) Set.univ) : Measurable fun (ω : Ω) => ⋯.vectorMeasure

theorem BoundedVariationOn.measurable_vectorMeasure_of_stronglyAdapted {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} [TopologicalSpace ι] [LinearOrder ι] {mΩ : MeasurableSpace Ω} {ℱ : MeasureTheory.Filtration ι mΩ} {Y : ι → Ω → E} [OrderTopology ι] [DenselyOrdered ι] [MeasurableSpace ι] [BorelSpace ι] [CompactIccSpace ι] [SecondCountableTopology ι] [NormedAddCommGroup E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E] (ha : MeasureTheory.StronglyAdapted ℱ Y) (hvar : ∀ (ω : Ω), BoundedVariationOn (fun (x : ι) => Y x ω) Set.univ) : Measurable fun (ω : Ω) => ⋯.vectorMeasure