almost surely quantifier

Stream: Is there code for X?

[Quinn]

do i have a quantifier (in the sense of (A->Prop)->Prop) for "almost surely"?

something along the lines of:

-- there exists a set N of measure zero such that when ω is in Ω-N, Pω → μω > 0
def AlmostSurely {Ω} [ΩMeasurable : MeasurableSpace Ω] (μ : Measure Ω) (P : Ω -> Prop) : Prop :=
   ∃ N ∈ ΩMeasurable.MeasurableSet', ∀ ω ∈ Ω.compl N, P ω → μ ω > 0

the signature of the formazliation is right, but the definition is not.

[Quinn]

import Mathlib.MeasureTheory.MeasurableSpace.Basic
import Mathlib.MeasureTheory.Measure.MeasureSpaceDef

open MeasureTheory

-- there exists a set N of measure zero such that when ω is in Ω-N, Pω → μω > 0
def AlmostSurely {Ω} [MeasurableSpace Ω] (μ : Measure Ω) (P : Ω -> Prop) : Prop :=
   ∃ N ∈ {X : Set Ω | μ X = 0}, ∀ ω ∈ {ω : Set Ω | ¬ ω ⊆ N}, ∀ ω', ω ω' → P ω' → μ ω > 0

i think this is right

[Ruben Van de Velde]

Is that Filter.Frequently?

[Quinn]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Filter/Basic.html#Filter.Frequently hm? I don't see a correspondence

[Quinn]

Filter.Frequently is certainly a quantifier, but i don't see how it's the same quantifier--- unless there's some gal-brain'd metaphor between order and measure i'm not thinking of

[Kexing Ying]

Almost surely is described using Filter.eventually and the ae filter. See MeasureTheory.ae_iff

[Quinn]

ah thanks!

[Quinn]

yeah i think i just don't know enough measure theory to have fluently deduced that almost everywhere is the foundation of almost surely. haha

[Quinn]

this is really cool!

[Quinn]

import Mathlib.MeasureTheory.MeasurableSpace.Basic
import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
import Mathlib.MeasureTheory.OuterMeasure.AE

open MeasureTheory
def AS {Ω} [MeasurableSpace Ω] (μ : ProbabilityMeasure Ω) (p : Ω -> Prop) : Prop := ∀ᵐ x ∂μ, p x -- Filter.Eventually p (ae μ)

why is this getting

failed to synthesize
  FunLike (ProbabilityMeasure Ω) (Set Ω) ENNReal
Additional diagnostic information may be available using the `set_option diagnostics true` command.

??

there's a coercion that should be getting triggered:

/-- Probability measures are defined as the subtype of measures that have the property of being
probability measures (i.e., their total mass is one). -/
def ProbabilityMeasure (Ω : Type*) [MeasurableSpace Ω] : Type _ :=
  { μ : Measure Ω // IsProbabilityMeasure μ }

namespace ProbabilityMeasure

variable {Ω : Type*} [MeasurableSpace Ω]

instance [Inhabited Ω] : Inhabited (ProbabilityMeasure Ω) :=
  ⟨⟨Measure.dirac default, Measure.dirac.isProbabilityMeasure⟩⟩

-- Porting note: as with other subtype synonyms (e.g., `ℝ≥0`), we need a new function for the
-- coercion instead of relying on `Subtype.val`.
/-- Coercion from `MeasureTheory.ProbabilityMeasure Ω` to `MeasureTheory.Measure Ω`. -/
@[coe]
def toMeasure : ProbabilityMeasure Ω → Measure Ω := Subtype.val

/-- A probability measure can be interpreted as a measure. -/
instance : Coe (ProbabilityMeasure Ω) (MeasureTheory.Measure Ω) := { coe := toMeasure }

instance (μ : ProbabilityMeasure Ω) : IsProbabilityMeasure (μ : Measure Ω) :=
  μ.prop

[Jireh Loreaux]

∀ᵐ x ∂(μ : Measure Ω), p x works, but I think the issue is that ∂ is also notation for docs#frontier ? That should likely be scoped.

[Quinn]

well it works when I say mu is a Measure \Omega, just not when i say it's ProbabiltiyMeasure \Omega

[Yaël Dillies]

Isn't that #13740 ?

[Jireh Loreaux]

@Quinn I mean this works:

import Mathlib.MeasureTheory.MeasurableSpace.Basic
import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
import Mathlib.MeasureTheory.OuterMeasure.AE

open MeasureTheory
def AS {Ω} [MeasurableSpace Ω] (μ : ProbabilityMeasure Ω) (p : Ω -> Prop) : Prop := ∀ᵐ x ∂(μ : Measure Ω), p x -- Filter.Eventually p (ae μ)

[Yaël Dillies]

Jireh, this is due to Yury's generalisation of docs#MeasureTheory.ae

[Yaël Dillies]

See #13740 for a fix

[Jireh Loreaux]

yeah, that's it.

[Quinn]

ok cool

[Quinn]

thanks Jireh!

[Yaël Dillies]

I am working on it, but I didn't quite manage to get the elaborator right yet. Help welcome!