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