def IsLebesgueMeasurableScalarFunction (n : ℕ) (Ω : Set (EuclideanSpace ℝ (Fin n))) (g : ↑Ω → ℝ) : Prop

Real-valued version of the textbook Lebesgue measurability predicate on a subset Ω ⊆ ℝ^n.

Equations

• One or more equations did not get rendered due to their size.

theorem helperForTheorem_7_3_coordinateFunctions_of_isLebesgueMeasurableFunction {n m : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin m)} (hf : IsLebesgueMeasurableFunction n m Ω f) (j : Fin m) : IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j

Helper for Theorem 7.3: every coordinate of a Lebesgue measurable vector map is Lebesgue measurable as a scalar map.

theorem helperForTheorem_7_3_nullMeasurableSet_of_coordinateFunctions {n m : ℕ} (hm : 0 < m) {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin m)} (hcoord : ∀ (j : Fin m), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) : MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume

Helper for Theorem 7.3: in positive codimension, coordinate measurability implies Ω is null measurable.

theorem helperForTheorem_7_3_preimage_openBox_eq_iInter_coordinatePreimages {n m : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin m)} (a b : Fin m → ℝ) : Subtype.val '' (f ⁻¹' {x : EuclideanSpace ℝ (Fin m) | ∀ (i : Fin m), a i < x.ofLp i ∧ x.ofLp i < b i}) = Ω ∩ ⋂ (i : Fin m), Subtype.val '' ((fun (x : { x : EuclideanSpace ℝ (Fin n) // x ∈ Ω }) => (f x).ofLp i) ⁻¹' Set.Ioo (a i) (b i))

Helper for Theorem 7.3: preimages of open coordinate boxes are intersections of coordinate interval preimages.

theorem helperForTheorem_7_3_isLebesgueMeasurableFunction_of_coordinateFunctions {n m : ℕ} (hm : 0 < m) {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin m)} (hcoord : ∀ (j : Fin m), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) : IsLebesgueMeasurableFunction n m Ω f

Helper for Theorem 7.3: for m > 0, coordinatewise scalar measurability implies vector-valued measurability.

theorem helperForTheorem_7_3_iff_coordinateFunctions_of_pos {n m : ℕ} (hm : 0 < m) {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin m)} : IsLebesgueMeasurableFunction n m Ω f ↔ ∀ (j : Fin m), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j

Helper for Theorem 7.3: for positive target dimension, vector measurability is equivalent to coordinatewise scalar measurability.

theorem helperForTheorem_7_3_iff_coordinateFunctions_with_nullMeasurableSet {n m : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin m)} : IsLebesgueMeasurableFunction n m Ω f ↔ MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume ∧ ∀ (j : Fin m), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j

Helper for Theorem 7.3: adding explicit domain null measurability yields the coordinatewise characterization in all target dimensions, including m = 0.

theorem isLebesgueMeasurableFunction_iff_coordinateFunctions_of_pos_or_nullMeasurableSet {n m : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin m)} : 0 < m ∨ MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume → (IsLebesgueMeasurableFunction n m Ω f ↔ ∀ (j : Fin m), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j)

Helper for Theorem 7.3: if either m > 0 or Ω is null measurable, then vector-valued measurability is equivalent to coordinatewise scalar measurability.

theorem helperForTheorem_7_3_iff_nullMeasurableSet_zeroCodomain {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} : IsLebesgueMeasurableFunction n 0 Ω f ↔ MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume

Helper for Theorem 7.3: when the codomain has dimension 0, vector-valued Lebesgue measurability is equivalent to null measurability of the domain.

theorem helperForTheorem_7_3_coordinateFunctions_zeroCodomain {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} (j : Fin 0) : IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j

Helper for Theorem 7.3: when the codomain is ℝ^0, the coordinatewise scalar measurability condition is always satisfied.

theorem helperForTheorem_7_3_coordinateFunctions_zeroCodomain_subsingleton {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} (hcoord1 hcoord2 : ∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) : hcoord1 = hcoord2

Helper for Theorem 7.3: in codimension 0, the coordinatewise measurability witness is unique because Fin 0 is empty.

theorem helperForTheorem_7_3_coordinateFunctions_zeroCodomain_iff_true {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} : (∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) ↔ True

Helper for Theorem 7.3: when the codomain is ℝ^0, the coordinatewise scalar measurability condition is equivalent to True.

theorem helperForTheorem_7_3_target_zeroCodomain_iff_isLebesgueMeasurableFunction {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} : (IsLebesgueMeasurableFunction n 0 Ω f ↔ ∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) ↔ IsLebesgueMeasurableFunction n 0 Ω f

Helper for Theorem 7.3: in codimension 0, the theorem's biconditional reduces to plain vector-valued measurability because the coordinate condition is vacuous.

theorem helperForTheorem_7_3_reverse_zeroCodomain_reduces_to_nullMeasurableSet {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} : (∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) → IsLebesgueMeasurableFunction n 0 Ω f ↔ True → MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume

Helper for Theorem 7.3: in codimension 0, the reverse direction of the coordinatewise characterization is equivalent to proving domain null measurability from True.

theorem helperForTheorem_7_3_reverse_zeroCodomain_of_nullMeasurableSet {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} (hΩ : MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume) : (∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) → IsLebesgueMeasurableFunction n 0 Ω f

Helper for Theorem 7.3: in codimension 0, domain null measurability is sufficient to obtain the reverse coordinate implication.

theorem helperForTheorem_7_3_reverse_zeroCodomain_imp_nullMeasurableSet {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} (hReverse : (∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) → IsLebesgueMeasurableFunction n 0 Ω f) : MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume

Helper for Theorem 7.3: in codimension 0, any proof of the reverse coordinate implication forces domain null measurability.

theorem helperForTheorem_7_3_not_isLebesgueMeasurableFunction_zeroCodomain_of_not_nullMeasurableSet {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} (hΩ : ¬MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume) : ¬IsLebesgueMeasurableFunction n 0 Ω f

Helper for Theorem 7.3: in codimension 0, if Ω is not null measurable, then no map f : Ω → ℝ^0 can be Lebesgue measurable.

theorem helperForTheorem_7_3_coordinatewise_and_not_measurable_zeroCodomain_of_not_nullMeasurableSet {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} (hΩ : ¬MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume) : (∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) ∧ ¬IsLebesgueMeasurableFunction n 0 Ω f

Helper for Theorem 7.3: in codimension 0, non-null-measurable Ω gives a fixed-map counterexample with vacuous coordinate measurability and failed vector-valued measurability.

theorem helperForTheorem_7_3_not_reverse_zeroCodomain_of_not_nullMeasurableSet {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} (hΩ : ¬MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume) : ¬((∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) → IsLebesgueMeasurableFunction n 0 Ω f)

Helper for Theorem 7.3: in codimension 0, if Ω is not null measurable then the reverse coordinate implication cannot hold for any fixed map f : Ω → ℝ^0.

theorem helperForTheorem_7_3_reverse_zeroCodomain_iff_false_of_not_nullMeasurableSet {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} (hΩ : ¬MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume) : (∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) → IsLebesgueMeasurableFunction n 0 Ω f ↔ False

Helper for Theorem 7.3: in codimension 0, if Ω is not null measurable then the reverse coordinate implication is equivalent to False.

theorem helperForTheorem_7_3_false_of_reverse_zeroCodomain_and_not_nullMeasurableSet {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} (hΩ : ¬MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume) (hcoord : ∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) (hReverse : (∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) → IsLebesgueMeasurableFunction n 0 Ω f) : False

Helper for Theorem 7.3: in codimension 0, a reverse coordinate implication combined with the vacuous coordinate hypothesis contradicts non-null-measurability of Ω.

theorem helperForTheorem_7_3_reverse_zeroCodomain_iff_nullMeasurableSet {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} : (∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) → IsLebesgueMeasurableFunction n 0 Ω f ↔ MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume

Helper for Theorem 7.3: in codimension 0, the reverse coordinate implication is equivalent to domain null measurability.

theorem helperForTheorem_7_3_goal_zeroCodomain_iff_nullMeasurableSet_of_coordinateHypothesis {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} (hcoord : ∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) : IsLebesgueMeasurableFunction n 0 Ω f ↔ MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume

Helper for Theorem 7.3: for a fixed codimension-0 coordinate hypothesis, the remaining reverse-direction goal is exactly domain null measurability.

theorem helperForTheorem_7_3_not_nullMeasurableSet_not_derivable_from_zeroCodomain_coordinates {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} (hΩ : ¬MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume) : ¬((∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) → MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume)

Helper for Theorem 7.3: in codimension 0, vacuous coordinatewise measurability cannot by itself force domain null measurability.

theorem helperForTheorem_7_3_target_zeroCodomain_iff_nullMeasurableSet {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} : (IsLebesgueMeasurableFunction n 0 Ω f ↔ ∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) ↔ MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume

Helper for Theorem 7.3: in codimension 0, the theorem's full biconditional is equivalent to null measurability of the domain.

theorem helperForTheorem_7_3_target_zeroCodomain_not_iff_of_not_nullMeasurableSet {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} (hΩ : ¬MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume) : ¬(IsLebesgueMeasurableFunction n 0 Ω f ↔ ∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j)

Helper for Theorem 7.3: in codimension 0, if Ω is not null measurable, then the theorem's biconditional fails for any f : Ω → ℝ^0.

theorem helperForTheorem_7_3_not_target_zeroCodomain_iff_not_nullMeasurableSet {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} : ¬(IsLebesgueMeasurableFunction n 0 Ω f ↔ ∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) ↔ ¬MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume

Helper for Theorem 7.3: in codimension 0, failure of the theorem's biconditional is equivalent to failure of domain null measurability.

theorem helperForTheorem_7_3_exists_counterexample_zeroCodomain_of_not_nullMeasurableSet {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} (hΩ : ¬MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume) : ∃ (f : ↑Ω → EuclideanSpace ℝ (Fin 0)), ¬(IsLebesgueMeasurableFunction n 0 Ω f ↔ ∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j)

Helper for Theorem 7.3: in codimension 0, non-null-measurable Ω produces an explicit counterexample map to the unguarded biconditional.

theorem helperForTheorem_7_3_exists_coordinatewise_not_measurable_zeroCodomain_of_not_nullMeasurableSet {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} (hΩ : ¬MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume) : ∃ (f : ↑Ω → EuclideanSpace ℝ (Fin 0)), (∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) ∧ ¬IsLebesgueMeasurableFunction n 0 Ω f

Helper for Theorem 7.3: in codimension 0, non-null-measurable Ω yields a specific map whose coordinate functions are vacuously measurable while the map itself is not Lebesgue measurable.

theorem helperForTheorem_7_3_nullMeasurableSet_of_target_zeroCodomain_iff {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} (hIff : IsLebesgueMeasurableFunction n 0 Ω f ↔ ∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) : MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume

Helper for Theorem 7.3: in codimension 0, any proof of the theorem's target biconditional for a fixed map forces domain null measurability.

theorem helperForTheorem_7_3_nullMeasurableSet_of_coordinateHypothesis_and_reverse_zeroCodomain {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} (hcoord : ∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) (hReverse : (∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) → IsLebesgueMeasurableFunction n 0 Ω f) : MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume

Helper for Theorem 7.3: in codimension 0, combining a fixed coordinate hypothesis with any reverse-direction implication forces domain null measurability.

theorem helperForTheorem_7_3_false_of_not_nullMeasurableSet_and_coordinateHypothesis_and_reverse_zeroCodomain {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} (hΩ : ¬MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume) (hcoord : ∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) (hReverse : (∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) → IsLebesgueMeasurableFunction n 0 Ω f) : False

Helper for Theorem 7.3: in codimension 0, if Ω is not null measurable then no reverse-direction implication can hold for a fixed coordinate hypothesis.

theorem helperForTheorem_7_3_isLebesgueMeasurableFunction_zeroCodomain_of_coordinateHypothesis_and_nullMeasurableSet {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} (hcoord : ∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) (hΩ : MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume) : IsLebesgueMeasurableFunction n 0 Ω f

Helper for Theorem 7.3: in codimension 0, coordinatewise scalar measurability together with domain null measurability implies vector measurability.

theorem helperForTheorem_7_3_not_isLebesgueMeasurableFunction_zeroCodomain_of_coordinateHypothesis_and_not_nullMeasurableSet {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} (hcoord : ∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) (hΩ : ¬MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume) : ¬IsLebesgueMeasurableFunction n 0 Ω f

Helper for Theorem 7.3: in codimension 0, coordinatewise scalar measurability together with failure of domain null measurability rules out vector measurability.

theorem helperForTheorem_7_3_nullMeasurableSet_of_coordinateFunctions_zeroCodomain {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} (hcoord : ∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) : MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume ↔ (∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) → IsLebesgueMeasurableFunction n 0 Ω f

Helper for Theorem 7.3: in codimension 0, the remaining reverse-direction subgoal can be reformulated as proving the reverse implication from domain null measurability, and conversely any such reverse implication forces domain null measurability for the fixed coordinate hypothesis.

theorem helperForTheorem_7_3_reverse_goal_zeroCodomain_iff_nullMeasurableSet_from_coordinateHypothesis {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} (hcoord : ∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) : IsLebesgueMeasurableFunction n 0 Ω f ↔ (∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) → MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume

Helper for Theorem 7.3: in codimension 0, for a fixed coordinatewise measurability witness, the remaining reverse goal is equivalent to deriving domain null measurability from that same witness.

theorem helperForTheorem_7_3_reverseSubgoal_zeroCodomain_iff_nullMeasurableSet {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} : (∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) → MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume ↔ MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume

Helper for Theorem 7.3: in codimension 0, the reverse-direction subgoal (∀ j : Fin 0, ...) → NullMeasurableSet Ω is equivalent to domain null measurability itself.

theorem helperForTheorem_7_3_nullMeasurableSet_of_reverseSubgoal_zeroCodomain {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin 0)} (hReverseSubgoal : (∀ (j : Fin 0), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j) → MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume) : MeasureTheory.NullMeasurableSet Ω MeasureTheory.volume

Helper for Theorem 7.3: in codimension 0, any proof of the reverse subgoal (∀ j : Fin 0, ...) → NullMeasurableSet Ω immediately yields domain null measurability.

theorem helperForTheorem_7_3_iff_coordinateFunctions_of_measurableSet {n m : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin m)} (hΩ : MeasurableSet Ω) : IsLebesgueMeasurableFunction n m Ω f ↔ ∀ (j : Fin m), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j

Helper for Theorem 7.3: if Ω is measurable, then coordinatewise scalar measurability is equivalent to vector-valued Lebesgue measurability in every target dimension.

theorem isLebesgueMeasurableFunction_iff_coordinateFunctions {n m : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → EuclideanSpace ℝ (Fin m)} (hm : 0 < m) : IsLebesgueMeasurableFunction n m Ω f ↔ ∀ (j : Fin m), IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => (f x).ofLp j

Theorem 7.3 (positive target dimension): for a Lebesgue measurable set Ω ⊆ ℝ^n and a map f : Ω → ℝ^m with 0 < m, f is Lebesgue measurable if and only if each coordinate function is Lebesgue measurable.

theorem helperForTheorem_7_4_comp_continuous_scalar {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → ℝ} {φ : ℝ → ℝ} (hφ : Continuous φ) (hf : IsLebesgueMeasurableScalarFunction n Ω f) : IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => φ (f x)

Helper for Theorem 7.4: composing a scalar Lebesgue measurable function with a continuous scalar map preserves scalar measurability.

theorem helperForTheorem_7_4_abs_measurable {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → ℝ} (hf : IsLebesgueMeasurableScalarFunction n Ω f) : IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => |f x|

Helper for Theorem 7.4: the absolute value of a scalar Lebesgue measurable function is scalar Lebesgue measurable.

theorem helperForTheorem_7_4_max_min_zero_measurable {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → ℝ} (hf : IsLebesgueMeasurableScalarFunction n Ω f) : (IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => max (f x) 0) ∧ IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => min (f x) 0

Helper for Theorem 7.4: the positive and negative truncations max(f,0) and min(f,0) of a scalar Lebesgue measurable function are scalar measurable.

theorem isLebesgueMeasurableScalarFunction_abs_max_min_zero {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f : ↑Ω → ℝ} (hf : IsLebesgueMeasurableScalarFunction n Ω f) : (IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => |f x|) ∧ (IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => max (f x) 0) ∧ IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => min (f x) 0

Theorem 7.4: if Ω ⊆ ℝ^n is measurable and f : Ω → ℝ is measurable, then the pointwise functions |f|, max(f, 0), and min(f, 0) are measurable on Ω.

theorem helperForTheorem_7_5_pair_isLebesgueMeasurableFunction {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {u v : ↑Ω → ℝ} (hu : IsLebesgueMeasurableScalarFunction n Ω u) (hv : IsLebesgueMeasurableScalarFunction n Ω v) : IsLebesgueMeasurableFunction n 2 Ω fun (x : ↑Ω) => !₂[u x, v x]

Helper for Theorem 7.5: two scalar measurable functions form a measurable ℝ²-valued pair map.

theorem helperForTheorem_7_5_comp_continuous_scalar_of_vector {n m : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {F : ↑Ω → EuclideanSpace ℝ (Fin m)} {φ : EuclideanSpace ℝ (Fin m) → ℝ} (hF : IsLebesgueMeasurableFunction n m Ω F) (hφ : Continuous φ) : IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => φ (F x)

Helper for Theorem 7.5: composing a measurable vector map into ℝ^m with a continuous scalar map yields a measurable scalar function.

theorem helperForTheorem_7_5_binaryContinuous_measurable {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {u v : ↑Ω → ℝ} {ψ : EuclideanSpace ℝ (Fin 2) → ℝ} (hu : IsLebesgueMeasurableScalarFunction n Ω u) (hv : IsLebesgueMeasurableScalarFunction n Ω v) (hψ : Continuous ψ) : IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => ψ !₂[u x, v x]

Helper for Theorem 7.5: binary scalar operations induced by a continuous map ℝ² → ℝ preserve scalar Lebesgue measurability.

theorem helperForTheorem_7_5_comp_continuous_scalar_on_openSubtype {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {u : ↑Ω → ℝ} {W : Set ℝ} {φ : ↑W → ℝ} (hu : IsLebesgueMeasurableScalarFunction n Ω u) (_hW : IsOpen W) (huW : ∀ (x : ↑Ω), u x ∈ W) (hφ : Continuous φ) : IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => φ ⟨u x, ⋯⟩

Helper for Theorem 7.5: composing a scalar measurable function with a continuous map on an open subtype preserves scalar measurability.

theorem isLebesgueMeasurableScalarFunction_add_sub_mul_max_min_div {n : ℕ} {Ω : Set (EuclideanSpace ℝ (Fin n))} {f g : ↑Ω → ℝ} (hf : IsLebesgueMeasurableScalarFunction n Ω f) (hg : IsLebesgueMeasurableScalarFunction n Ω g) : (IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => f x + g x) ∧ (IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => f x - g x) ∧ (IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => f x * g x) ∧ (IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => max (f x) (g x)) ∧ (IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => min (f x) (g x)) ∧ ((∀ (x : ↑Ω), g x ≠ 0) → IsLebesgueMeasurableScalarFunction n Ω fun (x : ↑Ω) => f x / g x)

Theorem 7.5: if Ω ⊆ ℝ^n is measurable and f, g : Ω → ℝ are measurable, then f + g, f - g, f * g, max(f, g), and min(f, g) are measurable on Ω. If additionally g x ≠ 0 for all x ∈ Ω, then f / g is measurable on Ω.