Independent bases of atomless measures

DefinitionConvex measure#✓fully proved

A measure \(\mu\) on a measurable space \(X\) is convex (in Fréchet's sense, "sans singularités") if \(\mu(X) = 1\) and every measurable set \(A\) with \(\mu(A) > 0\) contains a measurable subset \(B\) with \(0 < \mu(B) < \mu(A)\).

def IsConvexMeasure {X : Type} [MeasurableSpace X] (μ : MeasureTheory.Measure X) :
    Prop :=
  μ Set.univ = 1 ∧ ∀ A : Set X, MeasurableSet A → 0 < μ A →
    ∃ B : Set X, B ⊆ A ∧ MeasurableSet B ∧ μ A > μ B ∧ 0 < μ B

Used by 1

Used byThe claim of Szpilrajn's Problem 191

DefinitionStochastically independent class of sets#✓fully proved

Let \(\mu\) be a measure on a measurable space \(X\). A class \(B\) of subsets of \(X\) is stochastically independent with respect to \(\mu\) if for every finite collection of distinct sets \(A_1, \dots, A_n\) in \(B\), including the empty one, \(\mu(A_1 \cap \dots \cap A_n) = \mu(A_1) \cdots \mu(A_n)\). The empty intersection is \(X\) and the empty product is \(1\), so this forces \(\mu(X) = 1\). The sets in \(B\) need not be measurable; on such sets \(\mu\) is the outer measure.

def IsIndependentClass {X : Type} [MeasurableSpace X] (B : Set (Set X))
    (μ : MeasureTheory.Measure X) : Prop :=
  ∀ s : Finset (Set X), (↑s : Set (Set X)) ⊆ B →
    μ (⋂₀ (↑s : Set (Set X))) = ∏ A ∈ s, μ A

Used by 1

Used byBase of a measure

DefinitionBase of a measure#✓fully proved

Let \(\mu\) be a measure on a measurable space \(X\). A class \(B\) of subsets of \(X\) is a base of \(\mu\) if every set in \(B\) is measurable, \(B\) is stochastically independent with respect to \(\mu\), and every measurable set \(A \subseteq X\) agrees up to a null set with a set \(C\) in the \(\sigma\)-algebra generated by \(B\), that is, \(\mu(A \triangle C) = 0\).

def IsBase {X : Type} [MeasurableSpace X] (B : Set (Set X))
    (μ : MeasureTheory.Measure X) : Prop :=
  (∀ A ∈ B, MeasurableSet A) ∧ IsIndependentClass B μ ∧
    ∀ A : Set X, MeasurableSet A → ∃ C : Set X,
      @MeasurableSet X (MeasurableSpace.generateFrom B) C ∧
        μ (A \ C ∪ C \ A) = 0

Uses 1 · Used by 1

Statement usesStochastically independent class of sets

Used byThe claim of Szpilrajn's Problem 191

DefinitionThe claim of Szpilrajn's Problem 191#✓fully proved

The proposition, Szpilrajn's Problem 191 from the Scottish Book in its original form, that for every measurable space \(X\), every convex measure \(\mu\) on \(X\) has a base, that is, some class \(B\) of subsets of \(X\) is a base of \(\mu\).

def ScottishBookProblem191Claim : Prop :=
  ∀ (X : Type) [MeasurableSpace X] (μ : MeasureTheory.Measure X),
    IsConvexMeasure μ → ∃ B : Set (Set X), IsBase B μ

Uses 2 · Used by 1

Statement usesBase of a measure · Convex measure

Used bySzpilrajn's Problem 191 has a negative answer

TheoremSzpilrajn's Problem 191 has a negative answer#●ready to prove

The claim of Szpilrajn's Problem 191 is false: not every convex measure possesses a base. That is, there are a measurable space \(X\) and a convex measure \(\mu\) on \(X\) such that no class of subsets of \(X\) is a base of \(\mu\).

A non-atomic (convex) measure has a base if and only if its measure algebra is homogeneous, and the direct sum of Lebesgue measure spaces gives a counterexample whose measure algebra is not homogeneous.

theorem_wanted szpilrajn191_refuted : ¬ ScottishBookProblem191Claim

Sources

• E. Szpilrajn, Problem 191 of the Scottish Book; the sets B n of numbers in [0, 1] whose n-th binary digit is 1 form a base for Lebesgue measure on [0, 1]. See the commentary in R. D. Mauldin (ed.), The Scottish Book, 2nd ed. (Birkhäuser, 2015).

Uses 1

Statement usesThe claim of Szpilrajn's Problem 191

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.