OAI/Dynamics/SmoothObstruction/StandardProbability.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothObstruction.unitQuantile line 15
2. lemma OAI.SmoothObstruction.monotone_unitQuantile line 18
3. lemma OAI.SmoothObstruction.measurable_unitQuantile line 24
4. lemma OAI.SmoothObstruction.map_unitQuantile line 27
5. lemma OAI.SmoothObstruction.strictMono_unitQuantile line 65
6. lemma OAI.SmoothObstruction.embedding_unitQuantile line 81
7. def OAI.SmoothObstruction.ConullIsomorphic line 87

   Source documentation

   Measure-space isomorphism after removing measurable null sets.

   Also declared: ComparatorChallenges/SmoothObstruction.lean:30 (same declaration text).

   def ConullIsomorphic {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
       (μ : Measure X) (ν : Measure Y) : Prop :=
   …

8. def OAI.SmoothObstruction.StandardNonatomic line 96

   Source documentation

   Standard nonatomic in the source's explicit modulo-null-set sense.

   Also declared: ComparatorChallenges/SmoothObstruction.lean:39 (same declaration text).

   def StandardNonatomic {X : Type*} [MeasurableSpace X] (μ : Measure X) : Prop :=
   …

9. lemma OAI.SmoothObstruction.equivImage_preserving line 100
10. def OAI.SmoothObstruction.setEqEquiv line 113
11. lemma OAI.SmoothObstruction.setEqEquiv_preserving line 118
12. lemma OAI.SmoothObstruction.conullIsomorphic_of_common_embedding line 127

    Source documentation

    Two measurable embeddings having the same image law give an actual measurable isomorphism on conull sets, not merely two factors.

    lemma conullIsomorphic_of_common_embedding {X Y Z : Type*}
        [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z]
        {f : X → Z} {g : Y → Z} (hf : MeasurableEmbedding f) (hg : MeasurableEmbedding g)
        (μ : Measure X) (ν : Measure Y) (heq : μ.map f = ν.map g) :
        ConullIsomorphic μ ν := by
    …

    Mentions: OAI.SmoothObstruction.ConullIsomorphic

13. lemma OAI.SmoothObstruction.nullSingleton_map_embedding line 157
14. theorem OAI.SmoothObstruction.standardNonatomic_of_standardBorel line 167

    Source documentation

    The nonatomic standard-Borel classification needed by prop:system, with the same closed-unit-interval reference as the frozen main target.

    theorem standardNonatomic_of_standardBorel {X : Type*} [MeasurableSpace X]
        [StandardBorelSpace X] (μ : Measure X) [IsProbabilityMeasure μ]
        [NullSingletonClass μ] : StandardNonatomic μ := by
    …

    Mentions: OAI.SmoothObstruction.StandardNonatomic