feat: Dieudonné measure on a well-order

[vihdzp]

Given a well-order of uncountable cofinality, we can define a measurable space, consisting of sets which either contain or entirely omit a club set. On this space, the indicator function of stationary sets is a measure, known as the Dieudonné measure. It is a zero-one measure, which is nevertheless not a Dirac measure; it in fact has empty support.

---

• depends on: [Merged by Bors] - feat: stationary sets #39727
• depends on: feat: intervals Ici/Ioi are cofinal/closed under directed suprema #39747
• depends on: [Merged by Bors] - chore: coe_mk lemma for OuterMeasure #40167

[github-actions]

PR summary 64caf25786

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.MeasureTheory.Constructions.Dieudonne (new file)	1624

---

Declarations diff

+ DirSupClosed.Ici
+ DirSupClosed.Iic
+ DirSupClosed.Ioi
+ DirSupClosedOn.Ici
+ DirSupClosedOn.Iic
+ DirSupClosedOn.Ioi
+ DirSupInacc.Iic
+ DirSupInacc.Ioi
+ DirSupInaccOn.Iic
+ DirSupInaccOn.Ioi
+ Ici_inter
+ Ioi_inter
+ IsClub.isStationary
+ IsCofinal.Ici
+ IsCofinal.Ioi
+ IsCofinal.inter_of_isUpperSet_left
+ IsCofinal.inter_of_isUpperSet_right
+ IsCofinal.nonempty
+ IsStationary
+ IsStationary.isCofinal
+ IsStationary.mono
+ IsStationary.nonempty
+ IsStationary.of_not_isCofinal_compl
+ IsStationary.singleton_top
+ IsStationary.univ
+ IsUpperSet.isCofinal
+ _root_.IsMax.isClub_singleton
+ _root_.isClub_Ici
+ _root_.isClub_Ioi
+ _root_.isClub_empty_iff
+ _root_.isUpperSet_Ici
+ _root_.isUpperSet_Ioi
+ coe_mk
+ exists_isClub_subset
+ iInter_of_countable
+ instance : IsZeroOneMeasure (α := α) measure
+ instance : MeasurableSingletonClass α
+ instance [NoMaxOrder α] : NoAtoms (α := α) measure
+ instance [Nonempty α] : IsProbabilityMeasure (α := α) measure
+ inter_Ici
+ inter_Ioi
+ isStationary_iUnion_iff
+ isStationary_iUnion_iff_of_cof_le_one
+ isStationary_iUnion_iff_of_countable
+ isStationary_iUnion_iff_of_orderTop
+ isStationary_iff_top_mem
+ isStationary_sUnion_iff
+ isStationary_sUnion_iff_of_cof_le_one
+ isStationary_sUnion_iff_of_countable
+ isStationary_sUnion_iff_of_orderTop
+ isStationary_singleton_iff
+ isStationary_union_iff
+ isStationary_univ_iff
+ measurableSet_def
+ measurableSet_of_isClub
+ measurableSet_of_not_isStationary
+ measurableSet_of_orderTop
+ measure
+ measure_eq_dirac
+ measure_eq_one_iff
+ measure_eq_zero_iff
+ measure_of_isClub
+ measure_of_isStationary
+ measure_of_not_isCofinal
+ measure_of_not_isStationary
+ nonempty
+ not_isCofinal_Iio
+ not_isStationary_empty
+ not_isStationary_iff
+ not_isStationary_of_isEmpty
+ not_isStationary_singleton
+ sInter_of_countable
+ singleton_top
+ support_measure
- isUpperSet_Ici
- isUpperSet_Ioi

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

[mathlib-dependent-issues]

This PR/issue depends on:

• [Merged by Bors] - feat: stationary sets #39727
• feat: intervals Ici/Ioi are cofinal/closed under directed suprema #39747
• [Merged by Bors] - chore: coe_mk lemma for OuterMeasure #40167
  By Dependent Issues (🤖). Happy coding!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.