theorem proposition_7_5 : oneDimensionalOuterMeasure (Set.univ \ Set.range Rat.cast) = ⊤ ∧ oneDimensionalOuterMeasure (Set.Icc 0 1 \ Set.range Rat.cast) = 1

Proposition 7.5: for the one-dimensional outer measure m* on ℝ, m*(ℝ \ ℚ) = +∞ and m*([0,1] \ ℚ) = 1.

theorem helperForProposition_7_6_segmentImage_eq_Icc_prodSingleton : (fun (x : ℝ) => (x, 0)) '' Set.Icc 0 1 = Set.Icc 0 1 ×ˢ {0}

Helper for Proposition 7.6: identify the segment image with a product set.

theorem helperForProposition_7_6_range_eq_univ_prodSingleton : (Set.range fun (x : ℝ) => (x, 0)) = Set.univ ×ˢ {0}

Helper for Proposition 7.6: identify the horizontal line as univ × {0}.

theorem helperForProposition_7_6_outerMeasure_prodSingleton_zero (s : Set ℝ) : MeasureTheory.volume.toOuterMeasure (s ×ˢ {0}) = 0

Helper for Proposition 7.6: every horizontal slice s × {0} has outer measure zero.

theorem proposition_7_6 : MeasureTheory.volume.toOuterMeasure ((fun (x : ℝ) => (x, 0)) '' Set.Icc 0 1) = 0 ∧ MeasureTheory.volume.toOuterMeasure (Set.range fun (x : ℝ) => (x, 0)) = 0

Proposition 7.6: for two-dimensional Lebesgue outer measure on ℝ², the horizontal segment {(x,0) : 0 ≤ x ≤ 1} has outer measure 0; consequently the full horizontal line {(x,0) : x ∈ ℝ} also has outer measure 0.

theorem helperForProposition_7_7_productOpenBox_lower_le_upper {n m : ℕ} (U : OpenBox n) (V : OpenBox m) (i : Fin (n + m)) : Fin.append U.lower V.lower i ≤ Fin.append U.upper V.upper i

Helper for Proposition 7.7: coordinatewise lower-upper compatibility for the product box.

def helperForProposition_7_7_productOpenBox {n m : ℕ} (U : OpenBox n) (V : OpenBox m) : OpenBox (n + m)

Helper for Proposition 7.7: product construction on open boxes in dimensions n and m.

Equations

• helperForProposition_7_7_productOpenBox U V = { lower := Fin.append U.lower V.lower, upper := Fin.append U.upper V.upper, lower_le_upper := ⋯ }

theorem helperForProposition_7_7_productOpenBox_toSet {n m : ℕ} (U : OpenBox n) (V : OpenBox m) : (helperForProposition_7_7_productOpenBox U V).toSet = ⇑(Fin.appendEquiv n m).symm ⁻¹' U.toSet ×ˢ V.toSet

Helper for Proposition 7.7: the set of the product box is the preimage of the Cartesian product under coordinate splitting.

theorem helperForProposition_7_7_productOpenBox_volume_mul {n m : ℕ} (U : OpenBox n) (V : OpenBox m) : ENNReal.ofReal (helperForProposition_7_7_productOpenBox U V).volume = ENNReal.ofReal U.volume * ENNReal.ofReal V.volume

Helper for Proposition 7.7: volume of a product box factors as the product of volumes.

theorem helperForProposition_7_7_tsum_unpair_productCover {n m : ℕ} (C : ℕ → OpenBox n) (D : ℕ → OpenBox m) : ∑' (k : ℕ), ENNReal.ofReal (helperForProposition_7_7_productOpenBox (C (Nat.unpair k).1) (D (Nat.unpair k).2)).volume = (∑' (i : ℕ), ENNReal.ofReal (C i).volume) * ∑' (j : ℕ), ENNReal.ofReal (D j).volume

Helper for Proposition 7.7: paired-index covering sums for product boxes factor as a product of covering sums.

theorem helperForProposition_7_7_fixedCovers_bound {n m : ℕ} (A : Set (Fin n → ℝ)) (B : Set (Fin m → ℝ)) (C : ℕ → OpenBox n) (D : ℕ → OpenBox m) (hA : IsCoveredByBoxes A C) (hB : IsCoveredByBoxes B D) : (boxOuterMeasure (n + m)) (⇑(Fin.appendEquiv n m).symm ⁻¹' A ×ˢ B) ≤ (∑' (i : ℕ), ENNReal.ofReal (C i).volume) * ∑' (j : ℕ), ENNReal.ofReal (D j).volume

Helper for Proposition 7.7: fixed box covers of A and B induce a product-cover bound for A × B (viewed in ℝ^(n+m) via Fin.appendEquiv).

theorem helperForProposition_7_7_exists_nonTop_of_sInf_ne_top (S : Set ENNReal) (hS : sInf S ≠ ⊤) : ∃ x ∈ S, x ≠ ⊤

Helper for Proposition 7.7: if the infimum of a set in ENNReal is not ⊤, then the set contains a non-⊤ element.

theorem helperForProposition_7_7_sInfProduct_of_rectBounds_finiteWitness {a : ENNReal} {SA SB : Set ENNReal} (hRect : ∀ r ∈ SA, ∀ s ∈ SB, a ≤ r * s) (hAfinite : ∃ r ∈ SA, r ≠ ⊤) (hBfinite : ∃ s ∈ SB, s ≠ ⊤) : a ≤ sInf SA * sInf SB

Helper for Proposition 7.7: from pointwise rectangle bounds and finite witnesses on both factors, one obtains the bound by products of infima.

theorem helperForProposition_7_7_sInf_setCoverCost_eq_iInf {d : ℕ} (Ω : Set (Fin d → ℝ)) : sInf {r : ENNReal | ∃ (S : ℕ → Set (Fin d → ℝ)), Ω ⊆ ⋃ (i : ℕ), S i ∧ r = ∑' (i : ℕ), boxOuterMeasureCoverCost d (S i)} = ⨅ (S : ℕ → Set (Fin d → ℝ)), ⨅ (_ : Ω ⊆ ⋃ (i : ℕ), S i), ∑' (i : ℕ), boxOuterMeasureCoverCost d (S i)

Helper for Proposition 7.7: rewrite the sInf over all set-cover costs as the corresponding double iInf over covers.

theorem helperForProposition_7_7_mem_cast_set_iff_aux {a b : ℕ} (h : a = b) (s : Set (Fin a → ℝ)) (x : Fin b → ℝ) : x ∈ cast ⋯ s ↔ (fun (i : Fin a) => x (Fin.cast h i)) ∈ s

Auxiliary cast-membership transport for Fin-indexed sets.

theorem helperForProposition_7_7_boxOuterMeasure_cast_eq_aux {a b : ℕ} (h : a = b) (s : Set (Fin a → ℝ)) : (boxOuterMeasure b) (cast ⋯ s) = (boxOuterMeasure a) s

Auxiliary cast transport for boxOuterMeasure.

theorem helperForProposition_7_7_zeroLeftDim_preimage_univ_prod_aux (m : ℕ) (B : Set (Fin m → ℝ)) : (boxOuterMeasure (0 + m)) (⇑(Fin.appendEquiv 0 m).symm ⁻¹' Set.univ ×ˢ B) = (boxOuterMeasure m) B

Auxiliary zero-left-dimension transport under Fin.appendEquiv.

theorem helperForProposition_7_7_zeroRightDim_preimage_prod_univ_aux (n : ℕ) (A : Set (Fin n → ℝ)) : (boxOuterMeasure (n + 0)) (⇑(Fin.appendEquiv n 0).symm ⁻¹' A ×ˢ Set.univ) = (boxOuterMeasure n) A

Auxiliary zero-right-dimension transport under Fin.appendEquiv.

theorem helperForProposition_7_7_standardOpenBox_lower_le_upper_aux (k : ℕ) : -(↑k + 1) ≤ ↑k + 1

Auxiliary coordinatewise bounds for (-(k+1), k+1).

def helperForProposition_7_7_standardOpenBox_aux (d k : ℕ) : OpenBox (d + 1)

Auxiliary standard box in positive dimension.

Equations

• helperForProposition_7_7_standardOpenBox_aux d k = { lower := fun (x : Fin (d + 1)) => -(↑k + 1), upper := fun (x : Fin (d + 1)) => ↑k + 1, lower_le_upper := ⋯ }

theorem helperForProposition_7_7_standardOpenBoxes_cover_univ_posDim_aux (d : ℕ) : Set.univ ⊆ ⋃ (k : ℕ), (helperForProposition_7_7_standardOpenBox_aux d k).toSet

Auxiliary cover of ℝ^(d+1) by standard boxes.

theorem helperForProposition_7_7_union_of_zeroProductSlices_zero_right_aux (n m : ℕ) (A : Set (Fin n → ℝ)) (B : Set (Fin m → ℝ)) (S : ℕ → Set (Fin n → ℝ)) (hAcover : A ⊆ ⋃ (k : ℕ), S k) (hSlices : ∀ (k : ℕ), (boxOuterMeasure (n + m)) (⇑(Fin.appendEquiv n m).symm ⁻¹' S k ×ˢ B) = 0) : (boxOuterMeasure (n + m)) (⇑(Fin.appendEquiv n m).symm ⁻¹' A ×ˢ B) = 0

Auxiliary union lemma (right-slice form).

theorem helperForProposition_7_7_union_of_zeroProductSlices_zero_left_aux (n m : ℕ) (A : Set (Fin n → ℝ)) (B : Set (Fin m → ℝ)) (T : ℕ → Set (Fin m → ℝ)) (hBcover : B ⊆ ⋃ (k : ℕ), T k) (hSlices : ∀ (k : ℕ), (boxOuterMeasure (n + m)) (⇑(Fin.appendEquiv n m).symm ⁻¹' A ×ˢ T k) = 0) : (boxOuterMeasure (n + m)) (⇑(Fin.appendEquiv n m).symm ⁻¹' A ×ˢ B) = 0

Auxiliary union lemma (left-slice form).

theorem helperForProposition_7_7_productSlice_zero_of_rightCoverCostZero_and_finiteLeftBox_aux (d m : ℕ) (U : OpenBox (d + 1)) (B : Set (Fin m → ℝ)) (hBcost0 : boxOuterMeasureCoverCost m B = 0) : (boxOuterMeasure (d + 1 + m)) (⇑(Fin.appendEquiv (d + 1) m).symm ⁻¹' U.toSet ×ˢ B) = 0

Auxiliary slice-zero lemma: right factor has zero cover-cost, left factor is a positive-dimensional open box.

theorem helperForProposition_7_7_productSlice_zero_of_leftCoverCostZero_and_finiteRightBox_aux (n d : ℕ) (A : Set (Fin n → ℝ)) (V : OpenBox (d + 1)) (hAcost0 : boxOuterMeasureCoverCost n A = 0) : (boxOuterMeasure (n + (d + 1))) (⇑(Fin.appendEquiv n (d + 1)).symm ⁻¹' A ×ˢ V.toSet) = 0

Auxiliary slice-zero lemma: left factor has zero cover-cost, right factor is a positive-dimensional open box.

theorem helperForProposition_7_7_rightFactor_zero_product_of_coverCostZero_aux (n m : ℕ) (A : Set (Fin n → ℝ)) (B : Set (Fin m → ℝ)) (hBcost0 : boxOuterMeasureCoverCost m B = 0) : (boxOuterMeasure (n + m)) (⇑(Fin.appendEquiv n m).symm ⁻¹' A ×ˢ B) = 0

Auxiliary product-zero result from zero right cover-cost.

theorem helperForProposition_7_7_leftFactor_zero_product_of_coverCostZero_aux (n m : ℕ) (A : Set (Fin n → ℝ)) (B : Set (Fin m → ℝ)) (hAcost0 : boxOuterMeasureCoverCost n A = 0) : (boxOuterMeasure (n + m)) (⇑(Fin.appendEquiv n m).symm ⁻¹' A ×ˢ B) = 0

Auxiliary product-zero result from zero left cover-cost.

theorem helperForProposition_7_7_coverCost_rect_bound {n m : ℕ} (A : Set (Fin n → ℝ)) (B : Set (Fin m → ℝ)) : (boxOuterMeasure (n + m)) (⇑(Fin.appendEquiv n m).symm ⁻¹' A ×ˢ B) ≤ boxOuterMeasureCoverCost n A * boxOuterMeasureCoverCost m B

Helper for Proposition 7.7: rectangle preimages are bounded by the product of the box-cover costs of the two factors.

theorem helperForProposition_7_7_setCovers_bound {n m : ℕ} (A : Set (Fin n → ℝ)) (B : Set (Fin m → ℝ)) (S : ℕ → Set (Fin n → ℝ)) (T : ℕ → Set (Fin m → ℝ)) (hA : A ⊆ ⋃ (i : ℕ), S i) (hB : B ⊆ ⋃ (j : ℕ), T j) : (boxOuterMeasure (n + m)) (⇑(Fin.appendEquiv n m).symm ⁻¹' A ×ˢ B) ≤ (∑' (i : ℕ), boxOuterMeasureCoverCost n (S i)) * ∑' (j : ℕ), boxOuterMeasureCoverCost m (T j)

Helper for Proposition 7.7: fixed covers by arbitrary sets induce the corresponding box-cover-cost product bound for rectangle preimages.

theorem helperForProposition_7_7_standardOpenBox_lower_le_upper (k : ℕ) : -(↑k + 1) ≤ ↑k + 1

Helper for Proposition 7.7: coordinatewise bounds for the standard box (-(k+1), k+1).

def helperForProposition_7_7_standardOpenBox (d k : ℕ) : OpenBox (d + 1)

Helper for Proposition 7.7: the standard box (-(k+1), k+1)^(d+1) in positive dimension.

Equations

• helperForProposition_7_7_standardOpenBox d k = { lower := fun (x : Fin (d + 1)) => -(↑k + 1), upper := fun (x : Fin (d + 1)) => ↑k + 1, lower_le_upper := ⋯ }

theorem helperForProposition_7_7_standardOpenBoxes_cover_univ_posDim (d : ℕ) : Set.univ ⊆ ⋃ (k : ℕ), (helperForProposition_7_7_standardOpenBox d k).toSet

Helper for Proposition 7.7: standard positive-dimensional boxes cover all of ℝ^(d+1).

theorem helperForProposition_7_7_union_of_zeroProductSlices_zero_right (n m : ℕ) (A : Set (Fin n → ℝ)) (B : Set (Fin m → ℝ)) (S : ℕ → Set (Fin n → ℝ)) (hAcover : A ⊆ ⋃ (k : ℕ), S k) (hSlices : ∀ (k : ℕ), (boxOuterMeasure (n + m)) (⇑(Fin.appendEquiv n m).symm ⁻¹' S k ×ˢ B) = 0) : (boxOuterMeasure (n + m)) (⇑(Fin.appendEquiv n m).symm ⁻¹' A ×ˢ B) = 0

Helper for Proposition 7.7: zero on each left-slice of a cover implies zero on the full product set.

theorem helperForProposition_7_7_union_of_zeroProductSlices_zero_left (n m : ℕ) (A : Set (Fin n → ℝ)) (B : Set (Fin m → ℝ)) (T : ℕ → Set (Fin m → ℝ)) (hBcover : B ⊆ ⋃ (k : ℕ), T k) (hSlices : ∀ (k : ℕ), (boxOuterMeasure (n + m)) (⇑(Fin.appendEquiv n m).symm ⁻¹' A ×ˢ T k) = 0) : (boxOuterMeasure (n + m)) (⇑(Fin.appendEquiv n m).symm ⁻¹' A ×ˢ B) = 0

Helper for Proposition 7.7: zero on each right-slice of a cover implies zero on the full product set.

theorem helperForProposition_7_7_productSlice_zero_of_rightZero_and_finiteLeftBox (d m : ℕ) (U : OpenBox (d + 1)) (B : Set (Fin m → ℝ)) (hBzero : (boxOuterMeasure m) B = 0) : (boxOuterMeasure (d + 1 + m)) (⇑(Fin.appendEquiv (d + 1) m).symm ⁻¹' U.toSet ×ˢ B) = 0

Helper for Proposition 7.7: if the right factor has zero outer measure, then every positive-dimensional finite-box slice has zero product outer measure.

theorem helperForProposition_7_7_productSlice_zero_of_leftZero_and_finiteRightBox (n d : ℕ) (A : Set (Fin n → ℝ)) (V : OpenBox (d + 1)) (hAzero : (boxOuterMeasure n) A = 0) : (boxOuterMeasure (n + (d + 1))) (⇑(Fin.appendEquiv n (d + 1)).symm ⁻¹' A ×ˢ V.toSet) = 0

Helper for Proposition 7.7: if the left factor has zero outer measure, then every positive-dimensional finite-box slice has zero product outer measure.

theorem helperForProposition_7_7_mem_cast_set_iff {a b : ℕ} (h : a = b) (s : Set (Fin a → ℝ)) (x : Fin b → ℝ) : x ∈ cast ⋯ s ↔ (fun (i : Fin a) => x (Fin.cast h i)) ∈ s

Helper for Proposition 7.7: transport membership through a type cast of Fin-indexed sets.

theorem helperForProposition_7_7_boxOuterMeasure_cast_eq {a b : ℕ} (h : a = b) (s : Set (Fin a → ℝ)) : (boxOuterMeasure b) (cast ⋯ s) = (boxOuterMeasure a) s

Helper for Proposition 7.7: transport boxOuterMeasure across a type cast of Fin-indexed ambient spaces.

theorem helperForProposition_7_7_zeroLeftDim_preimage_univ_prod (m : ℕ) (B : Set (Fin m → ℝ)) : (boxOuterMeasure (0 + m)) (⇑(Fin.appendEquiv 0 m).symm ⁻¹' Set.univ ×ˢ B) = (boxOuterMeasure m) B

Helper for Proposition 7.7: in zero left dimension, the preimage of univ × B under Fin.appendEquiv has the same outer measure as B.

theorem helperForProposition_7_7_zeroRightDim_preimage_prod_univ (n : ℕ) (A : Set (Fin n → ℝ)) : (boxOuterMeasure (n + 0)) (⇑(Fin.appendEquiv n 0).symm ⁻¹' A ×ˢ Set.univ) = (boxOuterMeasure n) A

Helper for Proposition 7.7: in zero right dimension, the preimage of A × univ under Fin.appendEquiv has the same outer measure as A.

theorem helperForProposition_7_7_rightFactor_zero_product (n m : ℕ) (A : Set (Fin n → ℝ)) (B : Set (Fin m → ℝ)) (hBzero : (boxOuterMeasure m) B = 0) : (boxOuterMeasure (n + m)) (⇑(Fin.appendEquiv n m).symm ⁻¹' A ×ˢ B) = 0

Helper for Proposition 7.7: if the right factor has zero box outer measure, then the product set has zero box outer measure.

theorem helperForProposition_7_7_leftFactor_zero_product (n m : ℕ) (A : Set (Fin n → ℝ)) (B : Set (Fin m → ℝ)) (hAzero : (boxOuterMeasure n) A = 0) : (boxOuterMeasure (n + m)) (⇑(Fin.appendEquiv n m).symm ⁻¹' A ×ˢ B) = 0

Helper for Proposition 7.7: if the left factor has zero box outer measure, then the product set has zero box outer measure.

theorem helperForProposition_7_7_nonTop_branch_finish {a : ENNReal} {n m : ℕ} {A : Set (Fin n → ℝ)} {B : Set (Fin m → ℝ)} {SA SB : Set ENNReal} (hAeq : (boxOuterMeasure n) A = sInf SA) (hBeq : (boxOuterMeasure m) B = sInf SB) (hRect : ∀ r ∈ SA, ∀ s ∈ SB, a ≤ r * s) (hA_top : (boxOuterMeasure n) A ≠ ⊤) (hB_top : (boxOuterMeasure m) B ≠ ⊤) : a ≤ (boxOuterMeasure n) A * (boxOuterMeasure m) B

Helper for Proposition 7.7: in the non-⊤ branch for both factors, the rectangle bounds imply the target product inequality.

theorem proposition_7_7 (n m : ℕ) (A : Set (Fin n → ℝ)) (B : Set (Fin m → ℝ)) : (boxOuterMeasure (n + m)) (⇑(Fin.appendEquiv n m).symm ⁻¹' A ×ˢ B) ≤ (boxOuterMeasure n) A * (boxOuterMeasure m) B

Proposition 7.7: for A ⊆ ℝ^n and B ⊆ ℝ^m, the box outer measure satisfies m*_{n+m}(A × B) ≤ m*_n(A) * m*_m(B), where A × B is viewed inside ℝ^(n+m) via the canonical splitting equivalence of coordinates, and with the usual ENNReal conventions for products involving +∞ (in particular 0 * +∞ = 0).