The Local Monad on Stable Properties

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

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

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.

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.

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] [NoMaxOrder ι] [SecondCountableTopology ι] [𝓕.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.