Exchangeability and de Finetti

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremJointly exchangeable arrays are exactly the Aldous--Hoover codings in law#

An array process with a.e.-measurable entries in a standard Borel space, on a probability space, is jointly exchangeable if and only if its law is the law of a measurable joint Aldous--Hoover coding X i j = F(U, U_i, U_j, U_{i,j}) under independent uniform noise.

TauCeti.Probability.jointlyExchangeable_iff_exists_map_jointArray_eq.{u_1, u_2} {α : Type u_1}
  [MeasurableSpace α] [StandardBorelSpace α] {Ω : Type u_2} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ × ℕ → Ω → α}
  (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) :
  TauCeti.Probability.JointlyExchangeable μ X ↔
    ∃ F,
      Measurable F ∧
        MeasureTheory.Measure.map (fun u p => TauCeti.Probability.AldousHoover.jointArray F p u)
            (TauCeti.Probability.AldousHoover.noiseMeasure Unit (Sym2 ℕ)) =
          MeasureTheory.Measure.map (fun ω p => X p ω) μ

Lean

Formalized in Tau Ceti as TauCeti.Probability.jointlyExchangeable_iff_exists_map_jointArray_eq.

Sources

• Tau Ceti documentation: TauCeti.Probability.jointlyExchangeable_iff_exists_map_jointArray_eq
• Source of TauCeti.Probability.jointlyExchangeable_iff_exists_map_jointArray_eq in TauCeti/Probability/Exchangeability/Arrays/AldousHoover/Joint/Representation.lean
• Tau Ceti roadmap status: Exchangeability and de Finetti

LeanTauCeti.Probability.jointlyExchangeable_iff_exists_map_jointArray_eq

Uses 1

Proof usesDe Finetti's theorem

TheoremThe Diaconis--Freedman theorem#

A recurrent process is Markov exchangeable if and only if it is a mixture of Markov chains.

TauCeti.Probability.markovExchangeable_iff_mixedMarkovChain.{u_1, u_2} {Ω : Type u_1} {α : Type u_2}
  [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α}
  [MeasureTheory.IsFiniteMeasure μ] [NeZero μ] (hrec : TauCeti.Probability.Recurrent μ X) :
  TauCeti.Probability.MarkovExchangeable μ X ↔ TauCeti.Probability.MixedMarkovChain μ X

Lean

Formalized in Tau Ceti as TauCeti.Probability.markovExchangeable_iff_mixedMarkovChain.

Other forms

The Diaconis--Freedman representation theorem. Formalized in Tau Ceti as TauCeti.Probability.MarkovExchangeable.mixedMarkovChain.

TauCeti.Probability.MarkovExchangeable.mixedMarkovChain.{u_1, u_2} {Ω : Type u_1} {α : Type u_2}
  [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α}
  [MeasureTheory.IsFiniteMeasure μ] [NeZero μ] (h : TauCeti.Probability.MarkovExchangeable μ X)
  (hrec : TauCeti.Probability.Recurrent μ X) : TauCeti.Probability.MixedMarkovChain μ X

The Diaconis--Freedman representation theorem at a fixed start. Formalized in Tau Ceti as TauCeti.Probability.MarkovExchangeable.mixedMarkovChain_of_ae_initial_eq.

TauCeti.Probability.MarkovExchangeable.mixedMarkovChain_of_ae_initial_eq.{u_1, u_2} {Ω : Type u_1}
  {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω}
  {X : ℕ → Ω → α} [MeasureTheory.IsProbabilityMeasure μ] {a₀ : α}
  (h : TauCeti.Probability.MarkovExchangeable μ X) (hrec : TauCeti.Probability.Recurrent μ X)
  (h0 : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = a₀) : TauCeti.Probability.MixedMarkovChain μ X

Sources

• Tau Ceti documentation: TauCeti.Probability.markovExchangeable_iff_mixedMarkovChain
• Source of TauCeti.Probability.markovExchangeable_iff_mixedMarkovChain in TauCeti/Probability/Exchangeability/Recurrence/InitialState.lean
• Tau Ceti roadmap status: Exchangeability and de Finetti

LeanTauCeti.Probability.markovExchangeable_iff_mixedMarkovChain · TauCeti.Probability.MarkovExchangeable.mixedMarkovChain · TauCeti.Probability.MarkovExchangeable.mixedMarkovChain_of_ae_initial_eq

Uses 1

Proof usesDe Finetti's theorem

TheoremThe de Finetti–Ryll-Nardzewski equivalence#

A process with a.e. measurable coordinates, valued in a nonempty standard Borel space, is contractable iff it is both exchangeable and conditionally i.i.d. Derived from the two-way contractable_iff_conditionallyIID, with the exchangeability conjunct supplied by ConditionallyIID.exchangeable (the conjunct is redundant given conditional i.i.d.-ness).

TauCeti.Probability.deFinetti_RyllNardzewski_equivalence.{u_1, u_2} {Ω : Type u_1} {α : Type u_2}
  {mΩ : MeasurableSpace Ω} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α}
  (hX_meas : ∀ (n : ℕ), AEMeasurable (X n) μ) :
  TauCeti.Probability.Contractable μ X ↔
    TauCeti.Probability.Exchangeable μ X ∧ TauCeti.Probability.ConditionallyIID μ X

Lean

Formalized in Tau Ceti as TauCeti.Probability.deFinetti_RyllNardzewski_equivalence.

Other forms

The de Finetti–Ryll-Nardzewski equivalence, mixture form (Kallenberg, Theorem 1.1), in conjunction form. Formalized in Tau Ceti as TauCeti.Probability.contractable_iff_exchangeable_and_mixedIID.

TauCeti.Probability.contractable_iff_exchangeable_and_mixedIID.{u_1, u_2} {Ω : Type u_1}
  {α : Type u_2} {mΩ : MeasurableSpace Ω} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α}
  (hX_meas : ∀ (n : ℕ), AEMeasurable (X n) μ) :
  TauCeti.Probability.Contractable μ X ↔
    TauCeti.Probability.Exchangeable μ X ∧ TauCeti.Probability.MixedIID μ X

Sources

• Tau Ceti documentation: TauCeti.Probability.deFinetti_RyllNardzewski_equivalence
• Source of TauCeti.Probability.deFinetti_RyllNardzewski_equivalence in TauCeti/Probability/DeFinetti/Theorem.lean
• Tau Ceti roadmap status: Exchangeability and de Finetti

LeanTauCeti.Probability.deFinetti_RyllNardzewski_equivalence · TauCeti.Probability.contractable_iff_exchangeable_and_mixedIID

Uses 1

Proof usesDe Finetti–Ryll-Nardzewski, two-way mixture form

TheoremFinite de Finetti theorem, total-variation form#

If the first n coordinates of a process are exchangeable and m ≤ n, then the total variation distance between the m-prefix law and the with-replacement sample of the n-prefix law (for n > 0, the empirical-product mixture) is at most 2 * choose m 2 / n.

The normalization is Mathlib's: etvDist P Q is the signed-measure norm ‖P - Q‖, twice the distance sup_A |P A - Q A|, so in terms of that distance the bound is choose m 2 / n (etvDist_le_two_mul_iff).

TauCeti.Probability.ExchangeableAt.etvDist_prefixLaw_sampleWithReplacement_le.{u_1, u_2}
  {α : Type u_1} [MeasurableSpace α] {Ω : Type u_2} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} {m n : ℕ}
  (h : TauCeti.Probability.ExchangeableAt μ X n) (hmn : m ≤ n)
  (hX : ∀ (i : Fin n), AEMeasurable (X ↑i) μ) :
  MeasureTheory.etvDist (TauCeti.Probability.prefixLaw μ X m)
      (TauCeti.Probability.sampleWithReplacement (TauCeti.Probability.prefixLaw μ X n)) ≤
    2 * (↑(m.choose 2) / ↑n)

Lean

Formalized in Tau Ceti as TauCeti.Probability.ExchangeableAt.etvDist_prefixLaw_sampleWithReplacement_le.

Other forms

Finite de Finetti theorem. Formalized in Tau Ceti as TauCeti.Probability.ExchangeableAt.finiteDeFinetti.

TauCeti.Probability.ExchangeableAt.finiteDeFinetti.{u_1, u_2} {α : Type u_1} [MeasurableSpace α]
  {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} {m n : ℕ}
  (h : TauCeti.Probability.ExchangeableAt μ X n) (hmn : m ≤ n)
  (hX : ∀ (i : Fin n), AEMeasurable (X ↑i) μ) {A : Set (Fin m → α)} (hA : MeasurableSet A) :
  (TauCeti.Probability.prefixLaw μ X m) A ≤
      (TauCeti.Probability.sampleWithReplacement (TauCeti.Probability.prefixLaw μ X n)) A +
        ↑(m.choose 2) / ↑n ∧
    (TauCeti.Probability.sampleWithReplacement (TauCeti.Probability.prefixLaw μ X n)) A ≤
      (TauCeti.Probability.prefixLaw μ X m) A + ↑(m.choose 2) / ↑n

Sources

• Tau Ceti documentation: TauCeti.Probability.ExchangeableAt.etvDist_prefixLaw_sampleWithReplacement_le
• Source of TauCeti.Probability.ExchangeableAt.etvDist_prefixLaw_sampleWithReplacement_le in TauCeti/Probability/Exchangeability/FiniteDeFinetti.lean
• Tau Ceti roadmap status: Exchangeability and de Finetti

LeanTauCeti.Probability.ExchangeableAt.etvDist_prefixLaw_sampleWithReplacement_le · TauCeti.Probability.ExchangeableAt.finiteDeFinetti

Uses 1

Proof usesQuantitative finite de Finetti bound, exchangeable law to empirical mixture

TheoremHewitt–Savage in ergodic form#

The finitely supported permutations of the time index act ergodically on an i.i.d. product law P^{⊗ℕ}.

This is the zero-one law exchangeableSigma_trivial_of_infinitePi read through exchangeableSigma_trivial_iff_ergodicSMul. It is the permutation-action counterpart of the shift ergodicity recorded by MeasureTheory.Measure.ergodic_shift_infinitePi_const.

TauCeti.Probability.ergodicSMul_infinitePi_const.{u_1} {α : Type u_1} [MeasurableSpace α]
  (P : MeasureTheory.ProbabilityMeasure α) :
  ErgodicSMul TauCeti.FinitaryPerm (ℕ → α) (MeasureTheory.Measure.infinitePi fun x => ↑P)

Lean

Formalized in Tau Ceti as TauCeti.Probability.ergodicSMul_infinitePi_const.

Sources

• Tau Ceti documentation: TauCeti.Probability.ergodicSMul_infinitePi_const
• Source of TauCeti.Probability.ergodicSMul_infinitePi_const in TauCeti/Probability/Exchangeability/PathSpace/Exchangeable/Ergodic.lean
• Tau Ceti roadmap status: Exchangeability and de Finetti

LeanTauCeti.Probability.ergodicSMul_infinitePi_const

TheoremConditional independence as a functional representation#

If X and Y are conditionally independent given Z, then their joint law with Z is obtained by keeping Z and applying two measurable coding functions to separate uniform coordinates. When μ is a probability measure, the noises are independent both of one another and of the original sample carrying Z.

ProbabilityTheory.CondIndepFun.exists_independent_coding.{u_1, u_2, u_3, u_4} {Ω : Type u_1}
  {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [MeasurableSpace Ω] [StandardBorelSpace Ω]
  [MeasurableSpace β] [MeasurableSpace γ] [MeasurableSpace δ] [StandardBorelSpace β] [Nonempty β]
  [StandardBorelSpace γ] [Nonempty γ] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ] {X : Ω → β} {Y : Ω → γ} {Z : Ω → δ} {hZ : Measurable Z}
  (h : ProbabilityTheory.CondIndepFun (MeasurableSpace.comap Z inferInstance) ⋯ X Y μ)
  (hX : Measurable X) (hY : Measurable Y) :
  ∃ f g,
    Measurable (Function.uncurry f) ∧
      Measurable (Function.uncurry g) ∧
        MeasureTheory.Measure.map (fun p => (Z p.1, f (Z p.1) p.2.1, g (Z p.1) p.2.2))
            (μ.prod (MeasureTheory.volume.prod MeasureTheory.volume)) =
          MeasureTheory.Measure.map (fun ω => (Z ω, X ω, Y ω)) μ

Lean

Formalized in Tau Ceti as ProbabilityTheory.CondIndepFun.exists_independent_coding.

Sources

• Tau Ceti documentation: ProbabilityTheory.CondIndepFun.exists_independent_coding
• Source of ProbabilityTheory.CondIndepFun.exists_independent_coding in TauCeti/Probability/Kernel/ConditionalRandomization.lean
• Tau Ceti roadmap status: Exchangeability and de Finetti

LeanProbabilityTheory.CondIndepFun.exists_independent_coding

DefinitionMeasureTheory.Measure.deFinettiBarycenter#

The de Finetti barycenter of a mixing law π on ProbabilityMeasure α: the measure ∫ P^{⊗ℕ} dπ(P) on ℕ → α mixing the countable powers against π. For π a probability measure this is the law of a sequence drawn i.i.d. from a π-random probability measure.

MeasureTheory.Measure.deFinettiBarycenter.{u_1} {α : Type u_1} [MeasurableSpace α]
  (π : MeasureTheory.Measure (MeasureTheory.ProbabilityMeasure α)) : MeasureTheory.Measure (ℕ → α)

Lean

Formalized in Tau Ceti as MeasureTheory.Measure.deFinettiBarycenter.

Sources

• Tau Ceti documentation: MeasureTheory.Measure.deFinettiBarycenter
• Source of MeasureTheory.Measure.deFinettiBarycenter in TauCeti/Probability/Process/PathLaw/Mixture.lean
• Tau Ceti roadmap status: Exchangeability and de Finetti

LeanMeasureTheory.Measure.deFinettiBarycenter

Used by 1

Used byThe de Finetti correspondence

DefinitionThe de Finetti correspondence#

Over a standard Borel state space, the de Finetti barycenter is a bijection from mixing laws — probability measures on ProbabilityMeasure α — onto exchangeable probability measures on ℕ → α.

The forward map is Measure.deFinettiBarycenter; the inverse sends an exchangeable law to its mixing law. Injectivity is uniqueness of the mixing law and surjectivity is de Finetti's theorem, so the equivalence is exactly the content of ExchangeableLaw.existsUnique_mixingLaw in bijective form.

TauCeti.Probability.deFinettiEquiv.{u_1} {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] :
  MeasureTheory.ProbabilityMeasure (MeasureTheory.ProbabilityMeasure α) ≃
    { ρ // TauCeti.Probability.ExchangeableLaw ↑ρ }

Lean

Formalized in Tau Ceti as TauCeti.Probability.deFinettiEquiv.

Sources

• Tau Ceti documentation: TauCeti.Probability.deFinettiEquiv
• Source of TauCeti.Probability.deFinettiEquiv in TauCeti/Probability/DeFinetti/Correspondence.lean
• Tau Ceti roadmap status: Exchangeability and de Finetti

LeanTauCeti.Probability.deFinettiEquiv

Uses 2

Statement usesMeasureTheory.Measure.deFinettiBarycenter

Proof usesDe Finetti's theorem

TheoremThe path law of a recurrent process started at a₀ is the image of its excursion law#

Only the base state's singleton needs to be measurable.

TauCeti.Probability.Recurrent.pathLaw_eq_map_pathOfExcursions.{u_1, u_2} {Ω : Type u_1}
  {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω}
  {X : ℕ → Ω → α} {a₀ : α} (hrec : TauCeti.Probability.Recurrent μ X)
  (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (ha₀ : MeasurableSet {a₀})
  (h0 : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = a₀) :
  TauCeti.Probability.pathLaw μ X =
    MeasureTheory.Measure.map (TauCeti.pathOfExcursions a₀)
      (TauCeti.Probability.pathLaw μ (TauCeti.Probability.excursionProcess X a₀))

Lean

Formalized in Tau Ceti as TauCeti.Probability.Recurrent.pathLaw_eq_map_pathOfExcursions.

Sources

• Tau Ceti documentation: TauCeti.Probability.Recurrent.pathLaw_eq_map_pathOfExcursions
• Source of TauCeti.Probability.Recurrent.pathLaw_eq_map_pathOfExcursions in TauCeti/Probability/Recurrent/Excursion.lean
• Tau Ceti roadmap status: Exchangeability and de Finetti

LeanTauCeti.Probability.Recurrent.pathLaw_eq_map_pathOfExcursions

TheoremDe Finetti's theorem#

An exchangeable process valued in a nonempty standard Borel space is conditionally i.i.d. This is the conventional theorem-name handle for conditionallyIID_of_exchangeable.

TauCeti.Probability.deFinetti.{u_1, u_2} {Ω : Type u_1} {α : Type u_2} {mΩ : MeasurableSpace Ω}
  [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX_meas : ∀ (n : ℕ), AEMeasurable (X n) μ)
  (hX : TauCeti.Probability.Exchangeable μ X) : TauCeti.Probability.ConditionallyIID μ X

Lean

Formalized in Tau Ceti as TauCeti.Probability.deFinetti.

Other forms

De Finetti's theorem as an equivalence. Formalized in Tau Ceti as TauCeti.Probability.deFinetti_equivalence.

TauCeti.Probability.deFinetti_equivalence.{u_1, u_2} {Ω : Type u_1} {α : Type u_2}
  {mΩ : MeasurableSpace Ω} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α}
  (hX_meas : ∀ (n : ℕ), AEMeasurable (X n) μ) :
  TauCeti.Probability.Exchangeable μ X ↔ TauCeti.Probability.ConditionallyIID μ X

De Finetti's theorem for countably infinite index types. Formalized in Tau Ceti as TauCeti.Probability.conditionallyIID_of_exchangeableFamily.

TauCeti.Probability.conditionallyIID_of_exchangeableFamily.{u_1, u_2, u_3} {Ω : Type u_1}
  {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [Countable ι] [Infinite ι]
  [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → α}
  (hX : TauCeti.Probability.ExchangeableFamily μ X) (hX_meas : ∀ (i : ι), Measurable (X i)) :
  TauCeti.Probability.ConditionallyIID μ X

De Finetti's theorem in empirical-frequency form. Formalized in Tau Ceti as TauCeti.Probability.deFinetti_tendsto_empiricalMeasure_apply.

TauCeti.Probability.deFinetti_tendsto_empiricalMeasure_apply.{u_1, u_2} {Ω : Type u_1}
  {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω}
  {X : ℕ → Ω → α} [StandardBorelSpace α] [Nonempty α] [MeasureTheory.IsFiniteMeasure μ]
  (hX : TauCeti.Probability.Exchangeable μ X) (hX_meas : ∀ (n : ℕ), AEMeasurable (X n) μ) :
  ∃ ν,
    TauCeti.Probability.ConditionallyIIDWith μ X ν ∧
      ∀ (B : Set α),
        MeasurableSet B →
          ∀ᵐ (ω : Ω) ∂μ,
            Filter.Tendsto
              (fun n => (↑(TauCeti.Probability.empiricalMeasure (fun i => X i ω) n) B).toReal)
              Filter.atTop (nhds (↑(ν ω) B).toReal)

De Finetti's theorem in empirical-measure form. Formalized in Tau Ceti as TauCeti.Probability.deFinetti_empiricalMeasure.

TauCeti.Probability.deFinetti_empiricalMeasure.{u_1, u_2} {Ω : Type u_1} {α : Type u_2}
  [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α}
  [TopologicalSpace α] [PolishSpace α] [BorelSpace α] [Nonempty α] [MeasureTheory.IsFiniteMeasure μ]
  (hX : TauCeti.Probability.Exchangeable μ X) (hX_meas : ∀ (n : ℕ), AEMeasurable (X n) μ) :
  ∃ ν,
    TauCeti.Probability.ConditionallyIIDWith μ X ν ∧
      ∀ᵐ (ω : Ω) ∂μ,
        Filter.Tendsto (fun n => TauCeti.Probability.empiricalMeasure (fun i => X i ω) n)
          Filter.atTop (nhds (ν ω))

De Finetti's theorem via L² averaging. Formalized in Tau Ceti as TauCeti.Probability.deFinetti_viaL2.

TauCeti.Probability.deFinetti_viaL2.{u_1, u_2} {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω]
  [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX_meas : ∀ (n : ℕ), Measurable (X n))
  (hX : TauCeti.Probability.Exchangeable μ X) : TauCeti.Probability.ConditionallyIID μ X

de Finetti's theorem via Koopman operators. Formalized in Tau Ceti as TauCeti.Probability.deFinetti_viaKoopman.

TauCeti.Probability.deFinetti_viaKoopman.{u_1, u_2} {Ω : Type u_1} {α : Type u_2}
  [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α}
  (hX_meas : ∀ (n : ℕ), Measurable (X n)) (hX : TauCeti.Probability.Exchangeable μ X) :
  TauCeti.Probability.ConditionallyIID μ X

De Finetti's theorem, conditional form. Formalized in Tau Ceti as TauCeti.Probability.conditionallyIID_of_exchangeable.

TauCeti.Probability.conditionallyIID_of_exchangeable.{u_1, u_2} {Ω : Type u_1} {α : Type u_2}
  {mΩ : MeasurableSpace Ω} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α}
  (hX : TauCeti.Probability.Exchangeable μ X) (hX_meas : ∀ (n : ℕ), AEMeasurable (X n) μ) :
  TauCeti.Probability.ConditionallyIID μ X

de Finetti's theorem, directed form. Formalized in Tau Ceti as TauCeti.Probability.mixedIIDWith_of_contractable.

TauCeti.Probability.mixedIIDWith_of_contractable.{u_1, u_2} {Ω : Type u_1} {α : Type u_2}
  {mΩ : MeasurableSpace Ω} [MeasurableSpace α] [StandardBorelSpace Ω] [StandardBorelSpace α]
  [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α}
  (hX : TauCeti.Probability.Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) :
  TauCeti.Probability.MixedIIDWith μ X (TauCeti.Probability.tailConditionalProbabilityMeasure μ X)

De Finetti's theorem, mixture equivalence form (Kallenberg, Theorem 1.1). Formalized in Tau Ceti as TauCeti.Probability.exchangeable_iff_mixedIID.

TauCeti.Probability.exchangeable_iff_mixedIID.{u_1, u_2} {Ω : Type u_1} {α : Type u_2}
  {mΩ : MeasurableSpace Ω} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α}
  (hX_meas : ∀ (n : ℕ), AEMeasurable (X n) μ) :
  TauCeti.Probability.Exchangeable μ X ↔ TauCeti.Probability.MixedIID μ X

de Finetti's theorem, mixture form: contractable ⇒ mixed i.i.d. Formalized in Tau Ceti as TauCeti.Probability.mixedIID_of_contractable.

TauCeti.Probability.mixedIID_of_contractable.{u_3, u_4} {Ω : Type u_3} {α : Type u_4}
  [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α}
  (hX : TauCeti.Probability.Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) :
  TauCeti.Probability.MixedIID μ X

de Finetti's theorem, mixture form: exchangeable ⇒ mixed i.i.d. Formalized in Tau Ceti as TauCeti.Probability.mixedIID_of_exchangeable.

TauCeti.Probability.mixedIID_of_exchangeable.{u_3, u_4} {Ω : Type u_3} {α : Type u_4}
  [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α}
  (hX : TauCeti.Probability.Exchangeable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) :
  TauCeti.Probability.MixedIID μ X

De Finetti's theorem, unique mixture form. Formalized in Tau Ceti as TauCeti.Probability.deFinetti_mixture.

TauCeti.Probability.deFinetti_mixture.{u_1, u_2} {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω]
  [MeasurableSpace α] [StandardBorelSpace α] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} (hX : TauCeti.Probability.Exchangeable μ X)
  (hX_meas : ∀ (n : ℕ), AEMeasurable (X n) μ) :
  ∃! π,
    TauCeti.Probability.pathLaw μ X =
      (↑π).bind fun P => MeasureTheory.Measure.infinitePi fun x => ↑P

Sources

• Tau Ceti documentation: TauCeti.Probability.deFinetti
• Source of TauCeti.Probability.deFinetti in TauCeti/Probability/DeFinetti/Theorem.lean

LeanTauCeti.Probability.deFinetti · TauCeti.Probability.deFinetti_equivalence · TauCeti.Probability.conditionallyIID_of_exchangeableFamily · TauCeti.Probability.deFinetti_tendsto_empiricalMeasure_apply · TauCeti.Probability.deFinetti_empiricalMeasure · TauCeti.Probability.deFinetti_viaL2 · TauCeti.Probability.deFinetti_viaKoopman · TauCeti.Probability.conditionallyIID_of_exchangeable · TauCeti.Probability.mixedIIDWith_of_contractable · TauCeti.Probability.exchangeable_iff_mixedIID · TauCeti.Probability.mixedIID_of_contractable · TauCeti.Probability.mixedIID_of_exchangeable · TauCeti.Probability.deFinetti_mixture

Uses 3 · Used by 5

Proof usesThe contractable form of de Finetti's theorem via L² averaging · De Finetti's theorem transported along an explicit enumeration · The mean ergodic theorem for conditional expectations

Used byDe Finetti–Ryll-Nardzewski, two-way mixture form · Jointly exchangeable arrays are exactly the Aldous--Hoover codings in law · The de Finetti correspondence · The Diaconis--Freedman theorem · De Finetti's theorem for the rows of a block of pairs

TheoremDe Finetti–Ryll-Nardzewski, two-way mixture form#

A process with a.e. measurable coordinates, valued in a nonempty standard Borel space, under a finite measure, is contractable iff it is mixed i.i.d. Forward: the reverse-martingale de Finetti chain (mixedIID_of_contractable), run on a measurable version; converse: MixedIID.contractable, which needs no side hypotheses.

TauCeti.Probability.contractable_iff_mixedIID.{u_1, u_2} {Ω : Type u_1} {α : Type u_2}
  {mΩ : MeasurableSpace Ω} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α}
  (hX_meas : ∀ (n : ℕ), AEMeasurable (X n) μ) :
  TauCeti.Probability.Contractable μ X ↔ TauCeti.Probability.MixedIID μ X

Lean

Formalized in Tau Ceti as TauCeti.Probability.contractable_iff_mixedIID.

Other forms

De Finetti–Ryll-Nardzewski, two-way conditional form. Formalized in Tau Ceti as TauCeti.Probability.contractable_iff_conditionallyIID.

TauCeti.Probability.contractable_iff_conditionallyIID.{u_1, u_2} {Ω : Type u_1} {α : Type u_2}
  {mΩ : MeasurableSpace Ω} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α}
  (hX_meas : ∀ (n : ℕ), AEMeasurable (X n) μ) :
  TauCeti.Probability.Contractable μ X ↔ TauCeti.Probability.ConditionallyIID μ X

Sources

• Tau Ceti documentation: TauCeti.Probability.contractable_iff_mixedIID
• Source of TauCeti.Probability.contractable_iff_mixedIID in TauCeti/Probability/DeFinetti/Theorem.lean

LeanTauCeti.Probability.contractable_iff_mixedIID · TauCeti.Probability.contractable_iff_conditionallyIID

Uses 1 · Used by 1

Proof usesDe Finetti's theorem

Used byThe de Finetti–Ryll-Nardzewski equivalence

TheoremExact finite de Finetti bound, exchangeable law to empirical mixture#

Under finite exchangeability and m ≤ n, the prefix law exceeds its with-replacement sample on a measurable event by at most the exact index-collision error.

TauCeti.Probability.ExchangeableAt.prefixLaw_le_sampleWithReplacement_add_exact_collision.{u_1, u_2}
  {α : Type u_1} [MeasurableSpace α] {Ω : Type u_2} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} {m n : ℕ}
  (h : TauCeti.Probability.ExchangeableAt μ X n) (hmn : m ≤ n)
  (hX : ∀ (i : Fin n), AEMeasurable (X ↑i) μ) {A : Set (Fin m → α)} (hA : MeasurableSet A) :
  (TauCeti.Probability.prefixLaw μ X m) A ≤
    (TauCeti.Probability.sampleWithReplacement (TauCeti.Probability.prefixLaw μ X n)) A +
      (1 - ↑(n.descFactorial m) / ↑n ^ m)

Lean

Formalized in Tau Ceti as TauCeti.Probability.ExchangeableAt.prefixLaw_le_sampleWithReplacement_add_exact_collision.

Other forms

Exact finite de Finetti bound, empirical mixture to exchangeable law. Formalized in Tau Ceti as TauCeti.Probability.ExchangeableAt.sampleWithReplacement_le_prefixLaw_add_exact_collision.

TauCeti.Probability.ExchangeableAt.sampleWithReplacement_le_prefixLaw_add_exact_collision.{u_1, u_2}
  {α : Type u_1} [MeasurableSpace α] {Ω : Type u_2} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} {m n : ℕ}
  (h : TauCeti.Probability.ExchangeableAt μ X n) (hmn : m ≤ n)
  (hX : ∀ (i : Fin n), AEMeasurable (X ↑i) μ) {A : Set (Fin m → α)} (hA : MeasurableSet A) :
  (TauCeti.Probability.sampleWithReplacement (TauCeti.Probability.prefixLaw μ X n)) A ≤
    (TauCeti.Probability.prefixLaw μ X m) A + (1 - ↑(n.descFactorial m) / ↑n ^ m)

Sources

• Tau Ceti documentation: TauCeti.Probability.ExchangeableAt.prefixLaw_le_sampleWithReplacement_add_exact_collision
• Source of TauCeti.Probability.ExchangeableAt.prefixLaw_le_sampleWithReplacement_add_exact_collision in TauCeti/Probability/Exchangeability/FiniteDeFinetti.lean

LeanTauCeti.Probability.ExchangeableAt.prefixLaw_le_sampleWithReplacement_add_exact_collision · TauCeti.Probability.ExchangeableAt.sampleWithReplacement_le_prefixLaw_add_exact_collision

TheoremQuantitative finite de Finetti bound, exchangeable law to empirical mixture#

If the first n coordinates of a process are exchangeable and m ≤ n, then every measurable event under the m-prefix law has mass at most its mass under sampling m entries with replacement from the first n coordinates, plus choose m 2 / n. For n > 0 that sample is the mixture of m-fold products of the empirical distribution of the first n coordinates.

TauCeti.Probability.ExchangeableAt.prefixLaw_le_sampleWithReplacement_add.{u_1, u_2} {α : Type u_1}
  [MeasurableSpace α] {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} {m n : ℕ}
  (h : TauCeti.Probability.ExchangeableAt μ X n) (hmn : m ≤ n)
  (hX : ∀ (i : Fin n), AEMeasurable (X ↑i) μ) {A : Set (Fin m → α)} (hA : MeasurableSet A) :
  (TauCeti.Probability.prefixLaw μ X m) A ≤
    (TauCeti.Probability.sampleWithReplacement (TauCeti.Probability.prefixLaw μ X n)) A +
      ↑(m.choose 2) / ↑n

Informally uses

• Finite de Finetti theorem, total-variation form

Lean

Formalized in Tau Ceti as TauCeti.Probability.ExchangeableAt.prefixLaw_le_sampleWithReplacement_add.

Other forms

Quantitative finite de Finetti bound, empirical mixture to exchangeable law. Formalized in Tau Ceti as TauCeti.Probability.ExchangeableAt.sampleWithReplacement_le_prefixLaw_add.

TauCeti.Probability.ExchangeableAt.sampleWithReplacement_le_prefixLaw_add.{u_1, u_2} {α : Type u_1}
  [MeasurableSpace α] {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {X : ℕ → Ω → α} {m n : ℕ}
  (h : TauCeti.Probability.ExchangeableAt μ X n) (hmn : m ≤ n)
  (hX : ∀ (i : Fin n), AEMeasurable (X ↑i) μ) {A : Set (Fin m → α)} (hA : MeasurableSet A) :
  (TauCeti.Probability.sampleWithReplacement (TauCeti.Probability.prefixLaw μ X n)) A ≤
    (TauCeti.Probability.prefixLaw μ X m) A + ↑(m.choose 2) / ↑n

Sources

• Tau Ceti documentation: TauCeti.Probability.ExchangeableAt.prefixLaw_le_sampleWithReplacement_add
• Source of TauCeti.Probability.ExchangeableAt.prefixLaw_le_sampleWithReplacement_add in TauCeti/Probability/Exchangeability/FiniteDeFinetti.lean

LeanTauCeti.Probability.ExchangeableAt.prefixLaw_le_sampleWithReplacement_add · TauCeti.Probability.ExchangeableAt.sampleWithReplacement_le_prefixLaw_add

Used by 1

Used byFinite de Finetti theorem, total-variation form

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.