# The Local Monad on Stable Properties #

source
@[reducible, inline]
abbrev ProbabilityTheory.StableCat {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [ConditionallyCompleteLinearOrderBot ι] (E : Type u_4) [Zero E] (𝓕 : MeasureTheory.Filtration ι mΩ) :
Type (max (max u_1 u_2) u_4)

The category of stable properties.

Equations

- ProbabilityTheory.StableCat E 𝓕 = CategoryTheory.ObjectProperty.FullSubcategory fun (p : (ι → Ω → E) → Prop) => ProbabilityTheory.IsStable 𝓕 p

Instances For

source
def ProbabilityTheory.Local {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [Zero E] [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} (P : MeasureTheory.Measure Ω) (p : StableCat E 𝓕) :
StableCat E 𝓕

Local is a functor from Stable to Stable.

Equations

- ProbabilityTheory.Local P p = { obj := fun (x : ι → Ω → E) => ProbabilityTheory.Locally p.obj 𝓕 x P, property := ⋯ }

Instances For

source
theorem ProbabilityTheory.LocalMono {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [Zero E] [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} (P : MeasureTheory.Measure Ω) {p q : StableCat E 𝓕} (h : p ⟶ q) (u : ι → Ω → E) :
(Local P p).obj u ≤ (Local P q).obj u

The local functor is monotone.

source
noncomputable def ProbabilityTheory.LocalFunctor {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [Zero E] [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} (P : MeasureTheory.Measure Ω) :
CategoryTheory.Functor (StableCat E 𝓕) (StableCat E 𝓕)

The local functor.

Equations

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

Instances For

source
noncomputable def ProbabilityTheory.StableMonad {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [Zero E] [ConditionallyCompleteLinearOrderBot ι] [TopologicalSpace ι] [OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} [MeasureTheory.IsFiniteMeasure P] [DenselyOrdered ι] [NoMaxOrder ι] [SecondCountableTopology ι] (h𝓕 : 𝓕.IsRightContinuous) :
CategoryTheory.Monad (StableCat E 𝓕)

The Stable properties form a monad with the local functor.

Equations

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

Instances For