Congruence-invariant extensions of Lebesgue measure

DefinitionCongruent plane sets#✓fully proved

Two sets \(E\) and \(F\) in the Euclidean plane \(\mathbb{R}^2\) are congruent when some isometry of the plane onto itself maps \(E\) onto \(F\).

def AreCongruent (E F : Set (EuclideanSpace ℝ (Fin 2))) : Prop :=
  ∃ T : EuclideanSpace ℝ (Fin 2) ≃ᵢ EuclideanSpace ℝ (Fin 2), T '' E = F

Used by 1

Used byCongruence-invariant set functions on the plane

DefinitionCongruence-invariant set functions on the plane#✓fully proved

A function \(\mu\) that assigns to every subset of the Euclidean plane \(\mathbb{R}^2\) a value in \([0, \infty]\) is congruence invariant when \(\mu(E) = \mu(F)\) for all congruent plane sets \(E\) and \(F\).

def IsCongruenceInvariant (μ : Set (EuclideanSpace ℝ (Fin 2)) → ENNReal) : Prop :=
  ∀ E F : Set (EuclideanSpace ℝ (Fin 2)), AreCongruent E F → μ E = μ F

Uses 1 · Used by 1

Statement usesCongruent plane sets

Used byProblem of a congruence-invariant countably additive plane measure

DefinitionCountably additive set function#✓fully proved

μ is countably additive on pairwise-disjoint families. This is the countably-additive reading of "additive" in Problem 169; the typescript does not say whether finite or countable additivity is meant.

def IsCountablyAdditive (μ : Set (EuclideanSpace ℝ (Fin 2)) → ENNReal) : Prop :=
  ∀ E : ℕ → Set (EuclideanSpace ℝ (Fin 2)),
    Pairwise fun i j => Disjoint (E i) (E j) → μ (⋃ i, E i) = ∑' i, μ (E i)

Used by 1

Used byProblem of a congruence-invariant countably additive plane measure

DefinitionProblem of a congruence-invariant countably additive plane measure#✓fully proved

The countably additive reading of Problem 169: there is a function μ, defined for all plane sets, equal on congruent sets, countably additive, extending the Caratheodory linear measure (read as Lebesgue volume on measurable sets), with values in [0, +∞] (automatic for ENNReal).

def CountablyAdditiveCongruenceClaim : Prop :=
  ∃ μ : Set (EuclideanSpace ℝ (Fin 2)) → ENNReal,
    IsCongruenceInvariant μ ∧ IsCountablyAdditive μ ∧
    ∀ E : Set (EuclideanSpace ℝ (Fin 2)), MeasurableSet E →
      μ E = MeasureTheory.volume E

Uses 2 · Used by 1

Statement usesCongruence-invariant set functions on the plane · Countably additive set function

Used byNo countably additive congruence-invariant measure on all plane sets

TheoremNo countably additive congruence-invariant measure on all plane sets#●ready to prove

The countably additive reading is false in ZFC. Sketch: let V₀ ⊆ [0,1] meet each ℚ-coset of ℝ exactly once (Vitali selector) and put V = V₀ × [0,1]. Enumerating ℚ ∩ [-1,1] as (qₙ), the translates Tₙ = V + (qₙ, 0) are pairwise disjoint, each congruent to V, so all have the same mass c = μ V. Their union contains the unit square Q = [0,1] × [0,1] and lies in the strip [-1,2] × [0,1] of volume 3, so countable additivity and monotonicity give 1 = μ Q ≤ μ U ≤ 3, while countable additivity also gives μ U = ∑'ₙ c, which is 0 if c = 0 and +∞ if c > 0, a contradiction. Hence no such μ exists. This refutes the countably additive formalization only. The typescript says bare "additive"; the finite-additivity reading is Banach's 1923 theorem (a Banach measure: a finitely additive, isometry-invariant function on all plane sets extending Lebesgue measure), not this claim, and is not asserted here.

theorem_wanted no_countably_additive_congruence_measure :
  ¬ CountablyAdditiveCongruenceClaim

Sources

• E. Szpilrajn, Problem 169 of the Scottish Book; typescript PDF p.78, printed p.75. Banach, Fund. Math. 4 (1923), 7-33.

Uses 1

Statement usesProblem of a congruence-invariant countably additive plane measure

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.