def helperForProposition_7_12_twoPieceFamily (E T : Set ℝ) : ℕ → Set ℝ

Helper for Proposition 7.12: a countable family built from a two-piece split of a set.

Equations

• helperForProposition_7_12_twoPieceFamily E T n = if n = 0 then T ∩ E else if n = 1 then T \ E else ∅

theorem helperForProposition_7_12_nullMeasurable_implies_isCaratheodory (μ : MeasureTheory.Measure ℝ) {E : Set ℝ} (hE : MeasureTheory.NullMeasurableSet E μ) : μ.IsCaratheodory E

Helper for Proposition 7.12: a null-measurable set is Carathéodory measurable for the associated outer measure.

theorem helperForProposition_7_12_isCaratheodory_implies_nullMeasurable {E : Set ℝ} (hE : MeasureTheory.volume.IsCaratheodory E) : MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: for Lebesgue outer measure on ℝ, Carathéodory measurability implies null measurability.

theorem helperForProposition_7_12_not_isCaratheodory_iff_not_nullMeasurable {E : Set ℝ} : ¬MeasureTheory.volume.IsCaratheodory E ↔ ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: for Lebesgue outer measure on ℝ, failing Carathéodory measurability is equivalent to failing null measurability for the associated measure.

theorem helperForProposition_7_12_exists_nonCaratheodorySet_of_exists_nonNullMeasurableSet (hExists : ∃ (E : Set ℝ), ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume) : ∃ (E : Set ℝ), ¬MeasureTheory.volume.IsCaratheodory E

Helper for Proposition 7.12: a non-Carathéodory witness follows from any witness of non-null-measurability for Lebesgue measure.

theorem helperForProposition_7_12_exists_nonNullMeasurableSet_of_exists_nonCaratheodorySet (hExists : ∃ (E : Set ℝ), ¬MeasureTheory.volume.IsCaratheodory E) : ∃ (E : Set ℝ), ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: any non-Carathéodory witness for Lebesgue outer measure yields a non-null-measurable set for Lebesgue measure.

theorem helperForProposition_7_12_exists_nonCaratheodorySet_iff_exists_nonNullMeasurableSet_for_volume : (∃ (E : Set ℝ), ¬MeasureTheory.volume.IsCaratheodory E) ↔ ∃ (E : Set ℝ), ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: existence of a non-Carathéodory witness for Lebesgue outer measure is equivalent to existence of a non-null-measurable witness for Lebesgue measure.

theorem helperForProposition_7_12_exists_notMeasurableSet_real : ∃ (E : Set ℝ), ¬MeasurableSet E

Helper for Proposition 7.12: by cardinality, there exists a subset of ℝ that is not measurable.

theorem helperForProposition_7_12_exists_nonNullMeasurableSet_volume_Icc_of_exists_nonNullMeasurableSet_for_volume (hExists : ∃ (E : Set ℝ), ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume) : ∃ E ⊆ Set.Icc 0 1, ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: any global non-null-measurable witness for Lebesgue measure can be translated to one contained in Set.Icc (0 : ℝ) 1.

theorem helperForProposition_7_12_exists_nonNullMeasurableSet_for_volume_of_isComplete [MeasureTheory.volume.IsComplete] : ∃ (E : Set ℝ), ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: if Lebesgue measure on ℝ were complete, then any witness of non-measurability would also be a witness of non-null-measurability.

theorem helperForProposition_7_12_notAEEq_any_measurable_of_notMeasurable_of_complete (μ : MeasureTheory.Measure ℝ) [μ.IsComplete] {E : Set ℝ} (hE_not_measurable : ¬MeasurableSet E) (t : Set ℝ) : MeasurableSet t → ¬E =ᵐ[μ] t

Helper for Proposition 7.12: for a complete measure on ℝ, any non-measurable set cannot be almost-everywhere equal to a measurable set.

theorem helperForProposition_7_12_exists_notAEEq_any_measurable_of_exists_notMeasurable_of_complete (μ : MeasureTheory.Measure ℝ) [μ.IsComplete] (hExists : ∃ (E : Set ℝ), ¬MeasurableSet E) : ∃ (E : Set ℝ), ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[μ] t

Helper for Proposition 7.12: for a complete measure on ℝ, existence of a non-measurable set implies existence of a set not almost-everywhere equal to any measurable set.

theorem helperForProposition_7_12_exists_set_notAEEq_any_measurableSet_volume_of_isComplete [MeasureTheory.volume.IsComplete] : ∃ (E : Set ℝ), ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t

Helper for Proposition 7.12: under completeness of Lebesgue measure on ℝ, one gets a global upstream witness not almost-everywhere equal to any measurable set.

theorem helperForProposition_7_12_nonNullMeasurable_of_notAEEq_any_measurable_for_volume {E : Set ℝ} (hNotAEEq : ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t) : ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: a set that is not almost-everywhere equal to any measurable set cannot be null measurable for Lebesgue measure.

theorem helperForProposition_7_12_notAEEq_any_measurable_of_nonNullMeasurable_for_volume {E : Set ℝ} (hE : ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume) (t : Set ℝ) : MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t

Helper for Proposition 7.12: a non-null-measurable set cannot be almost-everywhere equal to a measurable set for Lebesgue measure.

theorem helperForProposition_7_12_notAEEq_any_measurable_iff_nonNullMeasurable_for_volume {E : Set ℝ} : (∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t) ↔ ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: for Lebesgue measure, being not almost-everywhere equal to any measurable set is equivalent to failing null measurability.

theorem helperForProposition_7_12_exists_notAEEq_any_measurable_iff_exists_nonNullMeasurable_for_volume : (∃ (E : Set ℝ), ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t) ↔ ∃ (E : Set ℝ), ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: existential forms of the previous equivalence for Lebesgue measure.

theorem helperForProposition_7_12_exists_nonNullMeasurableSet_for_volume_of_exists_notAEEq_measurable (hExists : ∃ (E : Set ℝ), ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t) : ∃ (E : Set ℝ), ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: any witness not almost-everywhere equal to a measurable set gives a non-null-measurable witness for Lebesgue measure.

theorem helperForProposition_7_12_exists_set_notAEEq_any_measurableSet_volume_of_exists_IccWitness (hExists : ∃ E ⊆ Set.Icc 0 1, ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t) : ∃ (E : Set ℝ), ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t

Helper for Proposition 7.12: a bounded witness on Set.Icc (0 : ℝ) 1 that is not almost-everywhere equal to any measurable set is, in particular, such a global witness on ℝ.

theorem helperForProposition_7_12_exists_IccWitness_of_exists_set_notAEEq_any_measurableSet_volume (hExists : ∃ (E : Set ℝ), ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t) : ∃ E ⊆ Set.Icc 0 1, ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t

Helper for Proposition 7.12: any global witness on ℝ that is not almost-everywhere equal to any measurable set yields a bounded witness inside Set.Icc (0 : ℝ) 1.

theorem helperForProposition_7_12_exists_set_notAEEq_any_measurableSet_volume_iff_exists_IccWitness : (∃ (E : Set ℝ), ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t) ↔ ∃ E ⊆ Set.Icc 0 1, ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t

Helper for Proposition 7.12: existence of a global witness not almost-everywhere equal to any measurable set is equivalent to existence of such a witness already in Set.Icc (0 : ℝ) 1.

theorem helperForProposition_7_12_exists_IccWitness_notAEEq_any_measurableSet_volume_of_isComplete [MeasureTheory.volume.IsComplete] : ∃ E ⊆ Set.Icc 0 1, ∀ (t : Set ℝ), MeasurableSet t → ¬E =ᵐ[MeasureTheory.volume] t

Helper for Proposition 7.12: bounded upstream witness in Set.Icc (0 : ℝ) 1 that is not almost-everywhere equal to any measurable set for Lebesgue measure.

theorem helperForProposition_7_12_exists_nonNullMeasurableSet_volume_Icc_of_exists_fixedIcc_strictSplitWitness_for_volumeOuterMeasure (hExists : ∃ E ⊆ Set.Icc 0 1, MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 ∩ E) + MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)) : ∃ E ⊆ Set.Icc 0 1, ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: bounded upstream witness in Set.Icc (0 : ℝ) 1 that is not almost-everywhere equal to any measurable set for Lebesgue measure.

def helperForProposition_7_12_IccMeasurableHull (A : Set ℝ) : Set ℝ

Helper for Proposition 7.12: measurable-hull truncation of a set to Set.Icc (0 : ℝ) 1.

Equations

• helperForProposition_7_12_IccMeasurableHull A = MeasureTheory.toMeasurable MeasureTheory.volume A ∩ Set.Icc 0 1

def helperForProposition_7_12_IccFullOuterMeasureCandidate (A : Set ℝ) : Set ℝ

Helper for Proposition 7.12: full-outer-measure candidate built from a set inside Set.Icc (0 : ℝ) 1.

Equations

• helperForProposition_7_12_IccFullOuterMeasureCandidate A = A ∪ Set.Icc 0 1 \ helperForProposition_7_12_IccMeasurableHull A

theorem helperForProposition_7_12_IccFullOuterMeasureCandidate_properties {A : Set ℝ} (hA_subset_Icc : A ⊆ Set.Icc 0 1) : helperForProposition_7_12_IccFullOuterMeasureCandidate A ⊆ Set.Icc 0 1 ∧ MeasureTheory.volume.toOuterMeasure (helperForProposition_7_12_IccFullOuterMeasureCandidate A) = MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) ∧ Set.Icc 0 1 \ helperForProposition_7_12_IccFullOuterMeasureCandidate A = helperForProposition_7_12_IccMeasurableHull A \ A

Helper for Proposition 7.12: for A ⊆ Set.Icc (0 : ℝ) 1, the measurable-hull construction stays in the interval, has full Lebesgue outer measure there, and has explicit interval complement.

theorem helperForProposition_7_12_positiveComplement_of_nonNullMeasurable_IccFullOuterMeasureCandidate {A : Set ℝ} (hA_subset_Icc : A ⊆ Set.Icc 0 1) (hA_nonNull : ¬MeasureTheory.NullMeasurableSet A MeasureTheory.volume) : 0 < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ helperForProposition_7_12_IccFullOuterMeasureCandidate A)

Helper for Proposition 7.12: if A ⊆ Set.Icc (0 : ℝ) 1 is not null measurable for Lebesgue measure, then the interval complement of the measurable-hull construction has positive outer measure.

theorem helperForProposition_7_12_exists_fullOuterMeasure_IccSubset_with_positiveComplement_of_exists_nonNullMeasurableSet_volume_Icc (hExists : ∃ A ⊆ Set.Icc 0 1, ¬MeasureTheory.NullMeasurableSet A MeasureTheory.volume) : ∃ E ⊆ Set.Icc 0 1, MeasureTheory.volume.toOuterMeasure E = MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) ∧ 0 < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)

Helper for Proposition 7.12: any bounded non-null-measurable witness in Set.Icc (0 : ℝ) 1 yields a bounded witness with full outer measure and positive-complement outer measure.

theorem helperForProposition_7_12_exists_nonNullMeasurableSet_for_volume_of_exists_nonNullMeasurableSet_volume_Icc (hExists : ∃ A ⊆ Set.Icc 0 1, ¬MeasureTheory.NullMeasurableSet A MeasureTheory.volume) : ∃ (E : Set ℝ), ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: any bounded non-null-measurable witness in Set.Icc (0 : ℝ) 1 is in particular a global non-null-measurable witness.

theorem helperForProposition_7_12_exists_nonNullMeasurableSet_volume_Icc_iff_exists_nonNullMeasurableSet_for_volume : (∃ A ⊆ Set.Icc 0 1, ¬MeasureTheory.NullMeasurableSet A MeasureTheory.volume) ↔ ∃ (E : Set ℝ), ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: bounded and global existence forms of non-null-measurable witnesses for Lebesgue measure are equivalent.

theorem helperForProposition_7_12_exists_nonNullMeasurableSet_volume_Icc_iff_exists_nonCaratheodorySet : (∃ A ⊆ Set.Icc 0 1, ¬MeasureTheory.NullMeasurableSet A MeasureTheory.volume) ↔ ∃ (E : Set ℝ), ¬MeasureTheory.volume.IsCaratheodory E

Helper for Proposition 7.12: bounded non-null-measurable witnesses in Set.Icc (0 : ℝ) 1 are equivalent to non-Carathéodory witnesses for Lebesgue outer measure on ℝ.

theorem helperForProposition_7_12_isCaratheodory_of_measure_eq_zero {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) {E : Set α} (hE_zero : μ E = 0) : μ.IsCaratheodory E

Helper for Proposition 7.12: any measure-zero set is Carathéodory measurable for the outer measure induced by the same measure.

theorem helperForProposition_7_12_exists_zeroMeasure_notMeasurableSet_of_not_isComplete {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (hIncomplete : ¬μ.IsComplete) : ∃ (E : Set α), μ E = 0 ∧ ¬MeasurableSet E

Helper for Proposition 7.12: if a measure is not complete, then there exists a measure-zero set that is not measurable.

theorem helperForProposition_7_12_exists_nonCaratheodorySet_of_exists_notMeasurableSet_for_volume_of_isComplete [MeasureTheory.volume.IsComplete] (hExists : ∃ (E : Set ℝ), ¬MeasurableSet E) : ∃ (E : Set ℝ), ¬MeasureTheory.volume.IsCaratheodory E

Helper for Proposition 7.12: if Lebesgue measure on ℝ is complete, then any non-measurable subset witness yields a non-Carathéodory witness for Lebesgue outer measure.

theorem helperForProposition_7_12_exists_nonCaratheodorySet_for_volumeOuterMeasure_of_isComplete [MeasureTheory.volume.IsComplete] : ∃ (E : Set ℝ), ¬MeasureTheory.volume.IsCaratheodory E

Helper for Proposition 7.12: under completeness of Lebesgue measure on ℝ, there exists a non-Carathéodory witness for Lebesgue outer measure.

theorem helperForProposition_7_12_upstream_exists_nonNullMeasurableSet_volume_Icc_real : ∃ E ⊆ Set.Icc 0 1, ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: upstream Vitali-type bounded witness in Set.Icc (0 : ℝ) 1 that is not null measurable for Lebesgue measure.

theorem prereqForProposition_7_12_exists_nonCaratheodorySet_for_volumeOuterMeasure_upstream : ∃ (E : Set ℝ), ¬MeasureTheory.volume.IsCaratheodory E

Helper for Proposition 7.12: upstream non-Carathéodory witness for Lebesgue outer measure on ℝ.

theorem prereqForProposition_7_12_exists_nonNullMeasurableSet_volume_Icc_upstream : ∃ A ⊆ Set.Icc 0 1, ¬MeasureTheory.NullMeasurableSet A MeasureTheory.volume

Helper for Proposition 7.12: upstream bounded non-null-measurable witness inside Set.Icc (0 : ℝ) 1 for Lebesgue measure.

theorem prereqForProposition_7_12_exists_nonNullMeasurableSet_for_volume_upstream : ∃ (E : Set ℝ), ¬MeasureTheory.NullMeasurableSet E MeasureTheory.volume

Helper for Proposition 7.12: upstream global non-null-measurable witness for Lebesgue measure on ℝ, obtained from the bounded upstream witness inside Set.Icc (0 : ℝ) 1.

theorem helperForProposition_7_12_exists_fullOuterMeasure_IccSubset_with_positiveComplement_of_exists_nonCaratheodorySet (hExists : ∃ (E : Set ℝ), ¬MeasureTheory.volume.IsCaratheodory E) : ∃ E ⊆ Set.Icc 0 1, MeasureTheory.volume.toOuterMeasure E = MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) ∧ 0 < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)

Helper for Proposition 7.12: any non-Carathéodory witness for Lebesgue outer measure yields a bounded witness in Set.Icc (0 : ℝ) 1 with full interval outer measure and positive complement outer measure.

theorem prereqForProposition_7_12_exists_fullOuterMeasure_IccSubset_with_positiveComplement : ∃ E ⊆ Set.Icc 0 1, MeasureTheory.volume.toOuterMeasure E = MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) ∧ 0 < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)

theorem helperForProposition_7_12_exists_fixedIcc_strictSplitWitness_for_volumeOuterMeasure_of_exists_nonCaratheodorySet (hExists : ∃ (E : Set ℝ), ¬MeasureTheory.volume.IsCaratheodory E) : ∃ E ⊆ Set.Icc 0 1, MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 ∩ E) + MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)

Helper for Proposition 7.12: any non-Carathéodory witness for Lebesgue outer measure yields a fixed-interval strict-split witness on Set.Icc (0 : ℝ) 1.

theorem prereqForProposition_7_12_exists_fixedIcc_strictSplitWitness_for_volumeOuterMeasure : ∃ E ⊆ Set.Icc 0 1, MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 ∩ E) + MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)

Helper for Proposition 7.12: upstream fixed-interval strict-split witness prerequisite for Lebesgue outer measure on Set.Icc (0 : ℝ) 1.

theorem helperForProposition_7_12_positiveComplement_of_fixedIcc_strictSplitWitness_for_volumeOuterMeasure {E : Set ℝ} (hStrict : MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 ∩ E) + MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)) : 0 < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)

Helper for Proposition 7.12: any strict split at T = Set.Icc (0 : ℝ) 1 forces the interval complement term to have positive outer measure.

theorem helperForProposition_7_12_exists_positiveComplement_of_exists_fixedIcc_strictSplitWitness_for_volumeOuterMeasure (hExists : ∃ E ⊆ Set.Icc 0 1, MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1) < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 ∩ E) + MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)) : ∃ E ⊆ Set.Icc 0 1, 0 < MeasureTheory.volume.toOuterMeasure (Set.Icc 0 1 \ E)

Helper for Proposition 7.12: any fixed-interval strict-split witness yields a bounded witness with positive outer-measure complement inside Set.Icc (0 : ℝ) 1.