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 := ⋯ }
Instances For
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)
:
The local functor is monotone.
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
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)
:
The Stable properties form a monad with the local functor.
Equations
- One or more equations did not get rendered due to their size.