From 2ebb2a15ec8bd976db2e8551019167db951ccd56 Mon Sep 17 00:00:00 2001 From: Taksh Date: Tue, 25 Aug 2026 08:08:48 +0530 Subject: [PATCH 1/7] feat(MeasureTheory): prove the product of elementary sets is elementary Exercise 1.1.4: a product of elementary sets is elementary, and elementary measure multiplies. The box-product identities (sides, toSet, injectivity, volume, pairwise disjointness) are the same partition argument already used for disjoint unions. --- Analysis/MeasureTheory/Section_1_1_1.lean | 187 +++++++++++++++++++++- 1 file changed, 185 insertions(+), 2 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_1_1.lean b/Analysis/MeasureTheory/Section_1_1_1.lean index 3d3e14cc0..aa1ac4729 100644 --- a/Analysis/MeasureTheory/Section_1_1_1.lean +++ b/Analysis/MeasureTheory/Section_1_1_1.lean @@ -1850,11 +1850,194 @@ abbrev Box.prod {d₁ d₂:ℕ} (B₁: Box d₁) (B₂: Box d₂) : Box (d₁ + obtain ⟨ i, hi ⟩ := i exact if h : i < d₁ then B₁.side ⟨i, h⟩ else (B₂.side ⟨i - d₁, by omega⟩) +/-- Unfold {name}`Box.prod` on a coordinate. -/ +lemma Box.prod_side {d₁ d₂:ℕ} (B₁: Box d₁) (B₂: Box d₂) (i : Fin (d₁ + d₂)) : + (B₁.prod B₂).side i = + if h : (i : ℕ) < d₁ then B₁.side ⟨i, h⟩ + else B₂.side ⟨(i : ℕ) - d₁, Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp h) i.isLt⟩ := by + rcases i with ⟨i, hi⟩ + rfl + +/-- Coordinate of a product vector in the first block. -/ +lemma EuclideanSpace'.prod_equiv_symm_apply_left {d₁ d₂:ℕ} + (y : EuclideanSpace' d₁) (z : EuclideanSpace' d₂) {i : ℕ} (hi : i < d₁) : + (EuclideanSpace'.prod_equiv d₁ d₂).symm (y, z) ⟨i, Nat.lt_add_right d₂ hi⟩ = y ⟨i, hi⟩ := by + simp [EuclideanSpace'.prod_equiv, dif_pos hi] + +/-- Coordinate of a product vector in the second block. -/ +lemma EuclideanSpace'.prod_equiv_symm_apply_right {d₁ d₂:ℕ} + (y : EuclideanSpace' d₁) (z : EuclideanSpace' d₂) {j : ℕ} (hj : j < d₂) : + (EuclideanSpace'.prod_equiv d₁ d₂).symm (y, z) ⟨d₁ + j, Nat.add_lt_add_left hj d₁⟩ = + z ⟨j, hj⟩ := by + have hnot : ¬ d₁ + j < d₁ := Nat.not_lt.mpr (Nat.le_add_right _ _) + simp [EuclideanSpace'.prod_equiv, dif_neg hnot, Nat.add_sub_cancel_left] + +/-- The set of a product box is the Cartesian product of the two boxes. -/ +lemma Box.prod_toSet {d₁ d₂:ℕ} (B₁: Box d₁) (B₂: Box d₂) : + EuclideanSpace'.prod B₁.toSet B₂.toSet = (B₁.prod B₂).toSet := by + ext x + constructor + · intro hx + obtain ⟨⟨y, z⟩, ⟨hy, hz⟩, rfl⟩ := hx + intro i + rw [Box.prod_side] + by_cases h : (i : ℕ) < d₁ + · rw [dif_pos h] + convert hy ⟨i, h⟩ + exact EuclideanSpace'.prod_equiv_symm_apply_left y z h + · rw [dif_neg h] + have hj : (i : ℕ) - d₁ < d₂ := Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp h) i.isLt + have hi_eq : (i : ℕ) = d₁ + ((i : ℕ) - d₁) := (Nat.add_sub_of_le (Nat.not_lt.mp h)).symm + convert hz ⟨(i : ℕ) - d₁, hj⟩ using 1 + have : i = ⟨d₁ + ((i : ℕ) - d₁), by omega⟩ := Fin.ext hi_eq + simpa [this] using EuclideanSpace'.prod_equiv_symm_apply_right y z hj + · intro hx + refine ⟨⟨(EuclideanSpace'.prod_equiv d₁ d₂ x).1, (EuclideanSpace'.prod_equiv d₁ d₂ x).2⟩, ?_, + (EuclideanSpace'.prod_equiv d₁ d₂).left_inv x⟩ + constructor + · intro i + have := hx ⟨i, Nat.lt_add_right d₂ i.isLt⟩ + rw [Box.prod_side, dif_pos i.isLt] at this + convert this + simp [EuclideanSpace'.prod_equiv] + · intro j + have := hx ⟨d₁ + j.val, Nat.add_lt_add_left j.isLt d₁⟩ + have hnot : ¬ d₁ + (j : ℕ) < d₁ := Nat.not_lt.mpr (Nat.le_add_right _ _) + rw [Box.prod_side, dif_neg hnot] at this + convert this + simp [EuclideanSpace'.prod_equiv, Nat.add_sub_cancel_left] + +/-- Recovering the factors from a product box. -/ +lemma Box.prod_injective {d₁ d₂:ℕ} : + Function.Injective (fun p : Box d₁ × Box d₂ => p.1.prod p.2) := by + intro ⟨B₁, C₁⟩ ⟨B₂, C₂⟩ h + have hside := congrArg Box.side h + refine Prod.ext ?_ ?_ + · ext i + have := congrFun hside ⟨i, Nat.lt_add_right d₂ i.isLt⟩ + simpa [Box.prod_side, dif_pos i.isLt] using this + · ext j + have hnot : ¬ d₁ + (j : ℕ) < d₁ := Nat.not_lt.mpr (Nat.le_add_right _ _) + have := congrFun hside ⟨d₁ + j.val, Nat.add_lt_add_left j.isLt d₁⟩ + simpa [Box.prod_side, dif_neg hnot, Nat.add_sub_cancel_left] using this + +/-- Volume of a product box is the product of the volumes. -/ +lemma Box.volume_prod {d₁ d₂:ℕ} (B₁: Box d₁) (B₂: Box d₂) : + |(B₁.prod B₂)|ᵥ = |B₁|ᵥ * |B₂|ᵥ := by + simp only [Box.volume] + rw [Fin.prod_univ_add] + congr 1 + · apply Finset.prod_congr rfl + intro i _ + simp [Box.prod_side, dif_pos i.isLt] + · apply Finset.prod_congr rfl + intro j _ + have hnot : ¬ d₁ + (j : ℕ) < d₁ := Nat.not_lt.mpr (Nat.le_add_right _ _) + simp [Box.prod_side, dif_neg hnot, Fin.natAdd, Nat.add_sub_cancel_left] + /-- Exercise 1.1.4: The Cartesian product of two elementary sets is elementary. -/ theorem IsElementary.prod {d₁ d₂:ℕ} {E₁: Set (EuclideanSpace' d₁)} {E₂: Set (EuclideanSpace' d₂)} - (hE₁: IsElementary E₁) (hE₂: IsElementary E₂) : IsElementary (EuclideanSpace'.prod E₁ E₂) := by sorry + (hE₁: IsElementary E₁) (hE₂: IsElementary E₂) : IsElementary (EuclideanSpace'.prod E₁ E₂) := by + classical + obtain ⟨S, rfl⟩ := hE₁ + obtain ⟨T, rfl⟩ := hE₂ + refine ⟨(S ×ˢ T).image (fun p => p.1.prod p.2), ?_⟩ + ext x + constructor + · intro hx + obtain ⟨⟨y, z⟩, ⟨hy, hz⟩, rfl⟩ := hx + simp only [Set.mem_iUnion] at hy hz ⊢ + obtain ⟨B, hB, hyB⟩ := hy + obtain ⟨C, hC, hzC⟩ := hz + refine ⟨B.prod C, ?_, ?_⟩ + · simp only [Finset.mem_image, Finset.mem_product, exists_prop, Prod.exists] + exact ⟨B, C, ⟨hB, hC⟩, rfl⟩ + · rw [← Box.prod_toSet] + exact ⟨⟨y, z⟩, ⟨hyB, hzC⟩, rfl⟩ + · intro hx + simp only [Set.mem_iUnion] at hx + obtain ⟨BC, hBC, hxBC⟩ := hx + simp only [Finset.mem_image, Finset.mem_product, exists_prop, Prod.exists] at hBC + obtain ⟨B, C, ⟨hB, hC⟩, rfl⟩ := hBC + rw [← Box.prod_toSet] at hxBC + obtain ⟨⟨y, z⟩, ⟨hy, hz⟩, rfl⟩ := hxBC + refine ⟨⟨y, z⟩, ⟨?_, ?_⟩, rfl⟩ + · exact Set.mem_iUnion.mpr ⟨B, ⟨hB, hy⟩⟩ + · exact Set.mem_iUnion.mpr ⟨C, ⟨hC, hz⟩⟩ + +/-- The product of two pairwise disjoint box families remains pairwise disjoint. -/ +lemma Box.prod_pairwiseDisjoint {d₁ d₂:ℕ} {S : Finset (Box d₁)} {T : Finset (Box d₂)} + (hS : (S : Set (Box d₁)).PairwiseDisjoint Box.toSet) + (hT : (T : Set (Box d₂)).PairwiseDisjoint Box.toSet) : + (((S ×ˢ T).image (fun p => p.1.prod p.2) : Finset (Box (d₁ + d₂))) : + Set (Box (d₁ + d₂))).PairwiseDisjoint Box.toSet := by + classical + rw [Set.pairwiseDisjoint_iff] + intro B₁ hB₁ B₂ hB₂ hne + simp only [Finset.mem_coe, Finset.mem_image, Finset.mem_product, exists_prop] at hB₁ hB₂ + obtain ⟨⟨C₁, D₁⟩, ⟨hC₁, hD₁⟩, rfl⟩ := hB₁ + obtain ⟨⟨C₂, D₂⟩, ⟨hC₂, hD₂⟩, rfl⟩ := hB₂ + obtain ⟨x, hx⟩ := hne + rw [Set.mem_inter_iff, ← Box.prod_toSet, ← Box.prod_toSet] at hx + obtain ⟨hx1, hx2⟩ := hx + obtain ⟨⟨y, z⟩, ⟨hy1, hz1⟩, rfl⟩ := hx1 + obtain ⟨⟨y', z'⟩, ⟨hy2, hz2⟩, hyz⟩ := hx2 + have hyz' : (y, z) = (y', z') := (EuclideanSpace'.prod_equiv d₁ d₂).symm.injective hyz + rcases hyz' with ⟨rfl, rfl⟩ + have hC : C₁ = C₂ := by + by_contra hneC + exact Set.disjoint_left.mp (hS hC₁ hC₂ hneC) hy1 hy2 + have hD : D₁ = D₂ := by + by_contra hneD + exact Set.disjoint_left.mp (hT hD₁ hD₂ hneD) hz1 hz2 + subst hC; subst hD + rfl /-- Measure is multiplicative on products: μ(E₁ × E₂) = μ(E₁) \* μ(E₂). -/ theorem IsElementary.measure_of_prod {d₁ d₂:ℕ} {E₁: Set (EuclideanSpace' d₁)} {E₂: Set (EuclideanSpace' d₂)} (hE₁: IsElementary E₁) (hE₂: IsElementary E₂) - : (hE₁.prod hE₂).measure = hE₁.measure * hE₂.measure := by sorry + : (hE₁.prod hE₂).measure = hE₁.measure * hE₂.measure := by + classical + set S := hE₁.partition.choose + set T := hE₂.partition.choose + have hS_disj : (S : Set (Box d₁)).PairwiseDisjoint Box.toSet := hE₁.partition.choose_spec.1 + have hT_disj : (T : Set (Box d₂)).PairwiseDisjoint Box.toSet := hE₂.partition.choose_spec.1 + have hE₁_eq : E₁ = ⋃ B ∈ S, B.toSet := hE₁.partition.choose_spec.2 + have hE₂_eq : E₂ = ⋃ C ∈ T, C.toSet := hE₂.partition.choose_spec.2 + set U := (S ×ˢ T).image (fun p => p.1.prod p.2) + have hU_disj : (U : Set (Box (d₁ + d₂))).PairwiseDisjoint Box.toSet := + Box.prod_pairwiseDisjoint hS_disj hT_disj + have hprod_eq : EuclideanSpace'.prod E₁ E₂ = ⋃ B ∈ U, B.toSet := by + rw [hE₁_eq, hE₂_eq] + ext x + constructor + · intro hx + obtain ⟨⟨y, z⟩, ⟨hy, hz⟩, rfl⟩ := hx + simp only [Set.mem_iUnion] at hy hz ⊢ + obtain ⟨B, hB, hyB⟩ := hy + obtain ⟨C, hC, hzC⟩ := hz + refine ⟨B.prod C, ?_, ?_⟩ + · exact Finset.mem_image.mpr ⟨⟨B, C⟩, ⟨Finset.mem_product.mpr ⟨hB, hC⟩, rfl⟩⟩ + · rw [← Box.prod_toSet] + exact ⟨⟨y, z⟩, ⟨hyB, hzC⟩, rfl⟩ + · intro hx + simp only [Set.mem_iUnion] at hx + obtain ⟨BC, hBC, hxBC⟩ := hx + obtain ⟨⟨B, C⟩, hBC', rfl⟩ := Finset.mem_image.mp hBC + obtain ⟨hB, hC⟩ := Finset.mem_product.mp hBC' + rw [← Box.prod_toSet] at hxBC + obtain ⟨⟨y, z⟩, ⟨hy, hz⟩, rfl⟩ := hxBC + refine ⟨⟨y, z⟩, ⟨?_, ?_⟩, rfl⟩ + · exact Set.mem_iUnion.mpr ⟨B, ⟨hB, hy⟩⟩ + · exact Set.mem_iUnion.mpr ⟨C, ⟨hC, hz⟩⟩ + have hmeas : (hE₁.prod hE₂).measure = ∑ B ∈ U, |B|ᵥ := + (hE₁.prod hE₂).measure_eq hU_disj hprod_eq + have hE₁m : hE₁.measure = ∑ B ∈ S, |B|ᵥ := hE₁.measure_eq hS_disj hE₁_eq + have hE₂m : hE₂.measure = ∑ C ∈ T, |C|ᵥ := hE₂.measure_eq hT_disj hE₂_eq + have hinj : ∀ p ∈ S ×ˢ T, ∀ q ∈ S ×ˢ T, + (fun r : Box d₁ × Box d₂ => r.1.prod r.2) p = (fun r => r.1.prod r.2) q → p = q := by + intro p _ q _ hpq + exact Box.prod_injective hpq + rw [hmeas, hE₁m, hE₂m, Finset.sum_image hinj, Finset.sum_product] + simp_rw [Box.volume_prod] + rw [Finset.sum_mul_sum] From d03b8044151bb5a6d1bdc9b4791caf814e32df97 Mon Sep 17 00:00:00 2001 From: Taksh Date: Tue, 25 Aug 2026 08:09:03 +0530 Subject: [PATCH 2/7] feat(MeasureTheory): prove Jordan measure is multiplicative on products Exercise 1.1.16: the product of Jordan measurable sets is Jordan measurable, and the measure multiplies. Inner/outer sandwich by elementary products, using Exercise 1.1.4. --- Analysis/MeasureTheory/Section_1_1_2.lean | 184 +++++++++++++++++++++- 1 file changed, 182 insertions(+), 2 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_1_2.lean b/Analysis/MeasureTheory/Section_1_1_2.lean index 59aa62bb2..85b4cb985 100644 --- a/Analysis/MeasureTheory/Section_1_1_2.lean +++ b/Analysis/MeasureTheory/Section_1_1_2.lean @@ -884,14 +884,194 @@ theorem JordanMeasure.measure_uniq' {d:ℕ} {m': (E: Set (EuclideanSpace' d)) sorry +/-- The Cartesian product of bounded sets is bounded. -/ +lemma EuclideanSpace'.norm_prod_equiv_symm {d₁ d₂:ℕ} + (y : EuclideanSpace' d₁) (z : EuclideanSpace' d₂) : + ‖(EuclideanSpace'.prod_equiv d₁ d₂).symm (y, z)‖ ^ 2 = ‖y‖ ^ 2 + ‖z‖ ^ 2 := by + have hsum : 0 ≤ ∑ i : Fin (d₁ + d₂), ((EuclideanSpace'.prod_equiv d₁ d₂).symm (y, z) i) ^ 2 := + Finset.sum_nonneg fun _ _ => sq_nonneg _ + simp only [EuclideanSpace'.norm_eq, Real.sq_sqrt hsum, Real.sq_sqrt + (Finset.sum_nonneg fun _ _ => sq_nonneg _), Real.sq_sqrt + (Finset.sum_nonneg (fun _ _ => sq_nonneg (_ : ℝ)))] + rw [Fin.sum_univ_add] + congr 1 + · apply Finset.sum_congr rfl + intro i _ + simp [EuclideanSpace'.prod_equiv_symm_apply_left y z i.isLt] + · apply Finset.sum_congr rfl + intro j _ + simp [EuclideanSpace'.prod_equiv_symm_apply_right y z j.isLt] + +lemma EuclideanSpace'.prod_mono {d₁ d₂:ℕ} + {E₁ E₁' : Set (EuclideanSpace' d₁)} {E₂ E₂' : Set (EuclideanSpace' d₂)} + (h₁ : E₁ ⊆ E₁') (h₂ : E₂ ⊆ E₂') : + EuclideanSpace'.prod E₁ E₂ ⊆ EuclideanSpace'.prod E₁' E₂' := + Set.image_mono (Set.prod_mono h₁ h₂) + +lemma EuclideanSpace'.prod_isBounded {d₁ d₂:ℕ} + {E₁ : Set (EuclideanSpace' d₁)} {E₂ : Set (EuclideanSpace' d₂)} + (hE₁ : Bornology.IsBounded E₁) (hE₂ : Bornology.IsBounded E₂) : + Bornology.IsBounded (EuclideanSpace'.prod E₁ E₂) := by + rw [Metric.isBounded_iff_subset_closedBall 0] at hE₁ hE₂ ⊢ + obtain ⟨M₁, hM₁⟩ := hE₁ + obtain ⟨M₂, hM₂⟩ := hE₂ + refine ⟨Real.sqrt (M₁ ^ 2 + M₂ ^ 2), ?_⟩ + intro x hx + obtain ⟨⟨y, z⟩, ⟨hy, hz⟩, rfl⟩ := hx + rw [Metric.mem_closedBall, dist_zero_right] + have hy' : ‖y‖ ≤ M₁ := by + have := hM₁ hy + simpa [Metric.mem_closedBall, dist_zero_right] using this + have hz' : ‖z‖ ≤ M₂ := by + have := hM₂ hz + simpa [Metric.mem_closedBall, dist_zero_right] using this + have : ‖(EuclideanSpace'.prod_equiv d₁ d₂).symm (y, z)‖ ^ 2 ≤ M₁ ^ 2 + M₂ ^ 2 := by + rw [EuclideanSpace'.norm_prod_equiv_symm] + nlinarith [norm_nonneg y, norm_nonneg z] + nlinarith [Real.sqrt_nonneg (M₁ ^ 2 + M₂ ^ 2), + Real.sq_sqrt (add_nonneg (sq_nonneg M₁) (sq_nonneg M₂)), + norm_nonneg ((EuclideanSpace'.prod_equiv d₁ d₂).symm (y, z))] + /-- Exercise 1.1.16 -/ theorem JordanMeasurable.prod {d₁ d₂:ℕ} {E₁: Set (EuclideanSpace' d₁)} {E₂: Set (EuclideanSpace' d₂)} - (hE₁: JordanMeasurable E₁) (hE₂: JordanMeasurable E₂) : JordanMeasurable (EuclideanSpace'.prod E₁ E₂) := by sorry + (hE₁: JordanMeasurable E₁) (hE₂: JordanMeasurable E₂) : JordanMeasurable (EuclideanSpace'.prod E₁ E₂) := by + have hbound := EuclideanSpace'.prod_isBounded hE₁.1 hE₂.1 + refine ⟨hbound, le_antisymm (Jordan_inner_le_outer hbound) ?_⟩ + have hμ₁ : 0 ≤ hE₁.measure := JordanMeasurable.nonneg hE₁ + have hμ₂ : 0 ≤ hE₂.measure := JordanMeasurable.nonneg hE₂ + -- outer(E₁ × E₂) ≤ μ(E₁) μ(E₂): sandwich by elementary supersets + have houter : Jordan_outer_measure (EuclideanSpace'.prod E₁ E₂) ≤ hE₁.measure * hE₂.measure := by + refine le_of_forall_pos_le_add fun ε hε => ?_ + have hε' : 0 < ε / 2 := by positivity + -- pick elementary supersets within ε of each outer measure + have hm₁ : Jordan_outer_measure E₁ < hE₁.measure + min ε 1 := by + rw [← hE₁.eq_outer]; linarith [min_le_right ε 1, min_le_left ε 1] + have hm₂ : Jordan_outer_measure E₂ < hE₂.measure + min ε 1 := by + rw [← hE₂.eq_outer]; linarith [min_le_right ε 1, min_le_left ε 1] + obtain ⟨A, hA, hAE, hAμ⟩ := le_Jordan_outer hm₁ hE₁.1 + obtain ⟨B, hB, hBF, hBμ⟩ := le_Jordan_outer hm₂ hE₂.1 + have hprod_le : Jordan_outer_measure (EuclideanSpace'.prod E₁ E₂) ≤ + (hA.prod hB).measure := + Jordan_outer_le (hA.prod hB) (EuclideanSpace'.prod_mono hAE hBF) + rw [IsElementary.measure_of_prod hA hB] at hprod_le + have hA_nn : 0 ≤ hA.measure := IsElementary.measure_nonneg hA + have hB_nn : 0 ≤ hB.measure := IsElementary.measure_nonneg hB + have hδ : (0 : ℝ) < min ε 1 := lt_min hε (by norm_num) + have hmul : hA.measure * hB.measure ≤ + (hE₁.measure + min ε 1) * (hE₂.measure + min ε 1) := + mul_le_mul (le_of_lt hAμ) (le_of_lt hBμ) hB_nn (add_nonneg hμ₁ (le_of_lt hδ)) + have hexp : (hE₁.measure + min ε 1) * (hE₂.measure + min ε 1) ≤ + hE₁.measure * hE₂.measure + ε := by + have hmin : min ε 1 ≤ 1 := min_le_right _ _ + have hminε : min ε 1 ≤ ε := min_le_left _ _ + nlinarith [hμ₁, hμ₂, hmin, hminε, mul_nonneg hμ₁ hμ₂] + linarith + -- inner(E₁ × E₂) ≥ μ(E₁) μ(E₂): sandwich by elementary subsets + have hinner : hE₁.measure * hE₂.measure ≤ Jordan_inner_measure (EuclideanSpace'.prod E₁ E₂) := by + refine le_of_forall_pos_le_add fun ε hε => ?_ + by_cases h0 : hE₁.measure = 0 ∨ hE₂.measure = 0 + · have : hE₁.measure * hE₂.measure = 0 := by + rcases h0 with h | h <;> simp [h] + linarith [Jordan_inner_measure_nonneg (EuclideanSpace'.prod E₁ E₂)] + · push_neg at h0 + have hpos₁ : 0 < hE₁.measure := lt_of_le_of_ne hμ₁ (Ne.symm h0.1) + have hpos₂ : 0 < hE₂.measure := lt_of_le_of_ne hμ₂ (Ne.symm h0.2) + set δ := min (min (hE₁.measure / 2) (hE₂.measure / 2)) (min ε 1) with hδdef + have hδpos : 0 < δ := by + dsimp [δ] + exact lt_min (lt_min (half_pos hpos₁) (half_pos hpos₂)) + (lt_min hε (by norm_num)) + have hm₁ : hE₁.measure - δ < Jordan_inner_measure E₁ := by + rw [← hE₁.eq_inner]; linarith + have hm₂ : hE₂.measure - δ < Jordan_inner_measure E₂ := by + rw [← hE₂.eq_inner]; linarith + obtain ⟨A, hA, hAE, hAμ⟩ := Jordan_inner_le hm₁ + obtain ⟨B, hB, hBF, hBμ⟩ := Jordan_inner_le hm₂ + have hprod_ge : (hA.prod hB).measure ≤ + Jordan_inner_measure (EuclideanSpace'.prod E₁ E₂) := + le_Jordan_inner (hA.prod hB) (EuclideanSpace'.prod_mono hAE hBF) hbound + rw [IsElementary.measure_of_prod hA hB] at hprod_ge + have hA_nn : 0 ≤ hA.measure := IsElementary.measure_nonneg hA + have hB_nn : 0 ≤ hB.measure := IsElementary.measure_nonneg hB + have hmul : (hE₁.measure - δ) * (hE₂.measure - δ) ≤ hA.measure * hB.measure := + mul_le_mul (le_of_lt hAμ) (le_of_lt hBμ) (by linarith) hA_nn + have : hE₁.measure * hE₂.measure ≤ (hE₁.measure - δ) * (hE₂.measure - δ) + ε := by + have hδle : δ ≤ ε := (min_le_right _ _).trans (min_le_left _ _) + have hδ1 : δ ≤ 1 := (min_le_right _ _).trans (min_le_right _ _) + nlinarith [hμ₁, hμ₂, hδle, hδ1, mul_nonneg hμ₁ hμ₂] + linarith + -- inner ≤ outer was used in the first conjunct; now outer ≤ inner + calc Jordan_outer_measure (EuclideanSpace'.prod E₁ E₂) + ≤ hE₁.measure * hE₂.measure := houter + _ ≤ Jordan_inner_measure (EuclideanSpace'.prod E₁ E₂) := hinner /-- Jordan measure is multiplicative on products: μ(E₁ × E₂) = μ(E₁) \* μ(E₂). -/ theorem JordanMeasurable.measure_of_prod {d₁ d₂:ℕ} {E₁: Set (EuclideanSpace' d₁)} {E₂: Set (EuclideanSpace' d₂)} (hE₁: JordanMeasurable E₁) (hE₂: JordanMeasurable E₂) - : (hE₁.prod hE₂).measure = hE₁.measure * hE₂.measure := by sorry + : (hE₁.prod hE₂).measure = hE₁.measure * hE₂.measure := by + have hμ₁ : 0 ≤ hE₁.measure := JordanMeasurable.nonneg hE₁ + have hμ₂ : 0 ≤ hE₂.measure := JordanMeasurable.nonneg hE₂ + refine le_antisymm ?_ ?_ + · -- measure = inner ≤? wait measure is inner; outer ≤ product from the prod proof + rw [JordanMeasurable.eq_outer (hE₁.prod hE₂)] + -- reuse the same outer bound: product of enclosing elementary sets + have hbound := EuclideanSpace'.prod_isBounded hE₁.1 hE₂.1 + refine le_of_forall_pos_le_add fun ε hε => ?_ + have hm₁ : Jordan_outer_measure E₁ < hE₁.measure + min ε 1 := by + rw [← hE₁.eq_outer]; linarith [min_le_right ε 1] + have hm₂ : Jordan_outer_measure E₂ < hE₂.measure + min ε 1 := by + rw [← hE₂.eq_outer]; linarith [min_le_right ε 1] + obtain ⟨A, hA, hAE, hAμ⟩ := le_Jordan_outer hm₁ hE₁.1 + obtain ⟨B, hB, hBF, hBμ⟩ := le_Jordan_outer hm₂ hE₂.1 + have hprod_le : Jordan_outer_measure (EuclideanSpace'.prod E₁ E₂) ≤ (hA.prod hB).measure := + Jordan_outer_le (hA.prod hB) (EuclideanSpace'.prod_mono hAE hBF) + rw [IsElementary.measure_of_prod hA hB] at hprod_le + have hA_nn : 0 ≤ hA.measure := IsElementary.measure_nonneg hA + have hB_nn : 0 ≤ hB.measure := IsElementary.measure_nonneg hB + have hδ : (0 : ℝ) < min ε 1 := lt_min hε (by norm_num) + have hmul : hA.measure * hB.measure ≤ + (hE₁.measure + min ε 1) * (hE₂.measure + min ε 1) := + mul_le_mul (le_of_lt hAμ) (le_of_lt hBμ) hB_nn (add_nonneg hμ₁ (le_of_lt hδ)) + have hexp : (hE₁.measure + min ε 1) * (hE₂.measure + min ε 1) ≤ + hE₁.measure * hE₂.measure + ε := by + have hmin : min ε 1 ≤ 1 := min_le_right _ _ + have hminε : min ε 1 ≤ ε := min_le_left _ _ + nlinarith [hμ₁, hμ₂, hmin, hminε] + linarith + · rw [JordanMeasurable.eq_inner (hE₁.prod hE₂)] + -- same inner bound as in `prod` + have hbound := EuclideanSpace'.prod_isBounded hE₁.1 hE₂.1 + refine le_of_forall_pos_le_add fun ε hε => ?_ + by_cases h0 : hE₁.measure = 0 ∨ hE₂.measure = 0 + · have : hE₁.measure * hE₂.measure = 0 := by + rcases h0 with h | h <;> simp [h] + linarith [Jordan_inner_measure_nonneg (EuclideanSpace'.prod E₁ E₂)] + · push_neg at h0 + have hpos₁ : 0 < hE₁.measure := lt_of_le_of_ne hμ₁ (Ne.symm h0.1) + have hpos₂ : 0 < hE₂.measure := lt_of_le_of_ne hμ₂ (Ne.symm h0.2) + set δ := min (min (hE₁.measure / 2) (hE₂.measure / 2)) (min ε 1) with hδdef + have hδpos : 0 < δ := by + dsimp [δ] + exact lt_min (lt_min (half_pos hpos₁) (half_pos hpos₂)) + (lt_min hε (by norm_num)) + have hm₁ : hE₁.measure - δ < Jordan_inner_measure E₁ := by + rw [← hE₁.eq_inner]; linarith + have hm₂ : hE₂.measure - δ < Jordan_inner_measure E₂ := by + rw [← hE₂.eq_inner]; linarith + obtain ⟨A, hA, hAE, hAμ⟩ := Jordan_inner_le hm₁ + obtain ⟨B, hB, hBF, hBμ⟩ := Jordan_inner_le hm₂ + have hprod_ge : (hA.prod hB).measure ≤ + Jordan_inner_measure (EuclideanSpace'.prod E₁ E₂) := + le_Jordan_inner (hA.prod hB) (EuclideanSpace'.prod_mono hAE hBF) hbound + rw [IsElementary.measure_of_prod hA hB] at hprod_ge + have hA_nn : 0 ≤ hA.measure := IsElementary.measure_nonneg hA + have hmul : (hE₁.measure - δ) * (hE₂.measure - δ) ≤ hA.measure * hB.measure := + mul_le_mul (le_of_lt hAμ) (le_of_lt hBμ) (by linarith) hA_nn + have : hE₁.measure * hE₂.measure ≤ (hE₁.measure - δ) * (hE₂.measure - δ) + ε := by + have hδle : δ ≤ ε := (min_le_right _ _).trans (min_le_left _ _) + have hδ1 : δ ≤ 1 := (min_le_right _ _).trans (min_le_right _ _) + nlinarith [hμ₁, hμ₂, hδle, hδ1] + linarith /-- Two sets are isometric if one is an orthogonal transformation plus translation of the other. -/ abbrev Isometric {d:ℕ} (E F: Set (EuclideanSpace' d)) : Prop := From 50630c0598f0e79fbf9a92b27e5bc9b9605315a3 Mon Sep 17 00:00:00 2001 From: Taksh Date: Tue, 25 Aug 2026 08:47:30 +0530 Subject: [PATCH 3/7] fix(MeasureTheory): close the product lemmas without convert/simp loops MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit CI failed on WithLp convert goals, mem_iUnion witnesses, and missing DecidableEq for Box. Rewrite membership via Fin.ext and iUnion₂. --- Analysis/MeasureTheory/Section_1_1_1.lean | 115 +++++++++++++--------- 1 file changed, 71 insertions(+), 44 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_1_1.lean b/Analysis/MeasureTheory/Section_1_1_1.lean index aa1ac4729..2424bda63 100644 --- a/Analysis/MeasureTheory/Section_1_1_1.lean +++ b/Analysis/MeasureTheory/Section_1_1_1.lean @@ -527,6 +527,11 @@ theorem Box.mem_toSet {d:ℕ} {B: Box d} {x : EuclideanSpace' d} : instance Box.inst_coeSet {d:ℕ} : Coe (Box d) (Set (EuclideanSpace' d)) where coe := toSet +open Classical in +/-- This is to make {name}`Finset`s of {name}`Box`es work properly. -/ +noncomputable instance Box.decidableEq {d:ℕ} : DecidableEq (Box d) := + fun a b => decidable_of_iff (a.side = b.side) ⟨Box.ext, fun h => h ▸ rfl⟩ + /-- Lifts a 1-dimensional interval to a 1-dimensional box. -/ @[coe] abbrev BoundedInterval.toBox (I: BoundedInterval) : Box 1 where @@ -1872,40 +1877,59 @@ lemma EuclideanSpace'.prod_equiv_symm_apply_right {d₁ d₂:ℕ} have hnot : ¬ d₁ + j < d₁ := Nat.not_lt.mpr (Nat.le_add_right _ _) simp [EuclideanSpace'.prod_equiv, dif_neg hnot, Nat.add_sub_cancel_left] +/-- First factor of {name}`prod_equiv`. -/ +lemma EuclideanSpace'.prod_equiv_apply_fst {d₁ d₂:ℕ} + (x : EuclideanSpace' (d₁ + d₂)) (i : Fin d₁) : + (EuclideanSpace'.prod_equiv d₁ d₂ x).1 i = x ⟨i, Nat.lt_add_right d₂ i.isLt⟩ := by + simp [EuclideanSpace'.prod_equiv] + +/-- Second factor of {name}`prod_equiv`. -/ +lemma EuclideanSpace'.prod_equiv_apply_snd {d₁ d₂:ℕ} + (x : EuclideanSpace' (d₁ + d₂)) (j : Fin d₂) : + (EuclideanSpace'.prod_equiv d₁ d₂ x).2 j = + x ⟨d₁ + (j : ℕ), Nat.add_lt_add_left j.isLt d₁⟩ := by + simp [EuclideanSpace'.prod_equiv] + /-- The set of a product box is the Cartesian product of the two boxes. -/ lemma Box.prod_toSet {d₁ d₂:ℕ} (B₁: Box d₁) (B₂: Box d₂) : EuclideanSpace'.prod B₁.toSet B₂.toSet = (B₁.prod B₂).toSet := by ext x constructor - · intro hx - obtain ⟨⟨y, z⟩, ⟨hy, hz⟩, rfl⟩ := hx + · rintro ⟨⟨y, z⟩, ⟨hy, hz⟩, rfl⟩ intro i rw [Box.prod_side] by_cases h : (i : ℕ) < d₁ · rw [dif_pos h] - convert hy ⟨i, h⟩ - exact EuclideanSpace'.prod_equiv_symm_apply_left y z h + have hi : i = ⟨(i : ℕ), Nat.lt_add_right d₂ h⟩ := Fin.ext rfl + rw [hi, EuclideanSpace'.prod_equiv_symm_apply_left y z h] + exact hy ⟨i, h⟩ · rw [dif_neg h] have hj : (i : ℕ) - d₁ < d₂ := Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp h) i.isLt - have hi_eq : (i : ℕ) = d₁ + ((i : ℕ) - d₁) := (Nat.add_sub_of_le (Nat.not_lt.mp h)).symm - convert hz ⟨(i : ℕ) - d₁, hj⟩ using 1 - have : i = ⟨d₁ + ((i : ℕ) - d₁), by omega⟩ := Fin.ext hi_eq - simpa [this] using EuclideanSpace'.prod_equiv_symm_apply_right y z hj + have hi : i = ⟨d₁ + ((i : ℕ) - d₁), Nat.add_lt_add_left hj d₁⟩ := + Fin.ext (Nat.add_sub_of_le (Nat.not_lt.mp h)).symm + rw [hi, EuclideanSpace'.prod_equiv_symm_apply_right y z hj] + exact hz ⟨(i : ℕ) - d₁, hj⟩ · intro hx refine ⟨⟨(EuclideanSpace'.prod_equiv d₁ d₂ x).1, (EuclideanSpace'.prod_equiv d₁ d₂ x).2⟩, ?_, (EuclideanSpace'.prod_equiv d₁ d₂).left_inv x⟩ constructor · intro i - have := hx ⟨i, Nat.lt_add_right d₂ i.isLt⟩ - rw [Box.prod_side, dif_pos i.isLt] at this - convert this - simp [EuclideanSpace'.prod_equiv] + have hx' := hx ⟨i, Nat.lt_add_right d₂ i.isLt⟩ + rw [Box.prod_side, dif_pos i.isLt] at hx' + rw [EuclideanSpace'.prod_equiv_apply_fst] + exact hx' · intro j - have := hx ⟨d₁ + j.val, Nat.add_lt_add_left j.isLt d₁⟩ have hnot : ¬ d₁ + (j : ℕ) < d₁ := Nat.not_lt.mpr (Nat.le_add_right _ _) - rw [Box.prod_side, dif_neg hnot] at this - convert this - simp [EuclideanSpace'.prod_equiv, Nat.add_sub_cancel_left] + have hx' := hx ⟨d₁ + j.val, Nat.add_lt_add_left j.isLt d₁⟩ + rw [Box.prod_side, dif_neg hnot] at hx' + have hside : B₂.side ⟨d₁ + (j : ℕ) - d₁, + Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp hnot) + (Nat.add_lt_add_left j.isLt d₁)⟩ = B₂.side j := by + congr 1 + exact Fin.ext (Nat.add_sub_cancel_left d₁ j.val) + rw [hside] at hx' + rw [EuclideanSpace'.prod_equiv_apply_snd] + exact hx' /-- Recovering the factors from a product box. -/ lemma Box.prod_injective {d₁ d₂:ℕ} : @@ -1915,11 +1939,18 @@ lemma Box.prod_injective {d₁ d₂:ℕ} : refine Prod.ext ?_ ?_ · ext i have := congrFun hside ⟨i, Nat.lt_add_right d₂ i.isLt⟩ - simpa [Box.prod_side, dif_pos i.isLt] using this + rw [Box.prod_side, Box.prod_side, dif_pos i.isLt, dif_pos i.isLt] at this + exact this · ext j have hnot : ¬ d₁ + (j : ℕ) < d₁ := Nat.not_lt.mpr (Nat.le_add_right _ _) have := congrFun hside ⟨d₁ + j.val, Nat.add_lt_add_left j.isLt d₁⟩ - simpa [Box.prod_side, dif_neg hnot, Nat.add_sub_cancel_left] using this + rw [Box.prod_side, Box.prod_side, dif_neg hnot, dif_neg hnot] at this + have hj (C : Box d₂) : C.side ⟨d₁ + (j : ℕ) - d₁, + Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp hnot) + (Nat.add_lt_add_left j.isLt d₁)⟩ = C.side j := by + congr 1 + exact Fin.ext (Nat.add_sub_cancel_left d₁ j.val) + rwa [hj C₁, hj C₂] at this /-- Volume of a product box is the product of the volumes. -/ lemma Box.volume_prod {d₁ d₂:ℕ} (B₁: Box d₁) (B₂: Box d₂) : @@ -1929,16 +1960,17 @@ lemma Box.volume_prod {d₁ d₂:ℕ} (B₁: Box d₁) (B₂: Box d₂) : congr 1 · apply Finset.prod_congr rfl intro i _ - simp [Box.prod_side, dif_pos i.isLt] + rw [Box.prod_side, dif_pos i.isLt] · apply Finset.prod_congr rfl intro j _ have hnot : ¬ d₁ + (j : ℕ) < d₁ := Nat.not_lt.mpr (Nat.le_add_right _ _) - simp [Box.prod_side, dif_neg hnot, Fin.natAdd, Nat.add_sub_cancel_left] + rw [Box.prod_side, dif_neg hnot] + congr 1 + exact Fin.ext (Nat.add_sub_cancel_left d₁ j.val) /-- Exercise 1.1.4: The Cartesian product of two elementary sets is elementary. -/ theorem IsElementary.prod {d₁ d₂:ℕ} {E₁: Set (EuclideanSpace' d₁)} {E₂: Set (EuclideanSpace' d₂)} (hE₁: IsElementary E₁) (hE₂: IsElementary E₂) : IsElementary (EuclideanSpace'.prod E₁ E₂) := by - classical obtain ⟨S, rfl⟩ := hE₁ obtain ⟨T, rfl⟩ := hE₂ refine ⟨(S ×ˢ T).image (fun p => p.1.prod p.2), ?_⟩ @@ -1946,24 +1978,21 @@ theorem IsElementary.prod {d₁ d₂:ℕ} {E₁: Set (EuclideanSpace' d₁)} {E constructor · intro hx obtain ⟨⟨y, z⟩, ⟨hy, hz⟩, rfl⟩ := hx - simp only [Set.mem_iUnion] at hy hz ⊢ - obtain ⟨B, hB, hyB⟩ := hy - obtain ⟨C, hC, hzC⟩ := hz + obtain ⟨B, hB, hyB⟩ := Set.mem_iUnion₂.mp hy + obtain ⟨C, hC, hzC⟩ := Set.mem_iUnion₂.mp hz refine ⟨B.prod C, ?_, ?_⟩ - · simp only [Finset.mem_image, Finset.mem_product, exists_prop, Prod.exists] - exact ⟨B, C, ⟨hB, hC⟩, rfl⟩ + · exact Finset.mem_image.mpr ⟨⟨B, C⟩, Finset.mem_product.mpr ⟨hB, hC⟩, rfl⟩ · rw [← Box.prod_toSet] exact ⟨⟨y, z⟩, ⟨hyB, hzC⟩, rfl⟩ · intro hx - simp only [Set.mem_iUnion] at hx - obtain ⟨BC, hBC, hxBC⟩ := hx - simp only [Finset.mem_image, Finset.mem_product, exists_prop, Prod.exists] at hBC - obtain ⟨B, C, ⟨hB, hC⟩, rfl⟩ := hBC + obtain ⟨BC, hBC, hxBC⟩ := Set.mem_iUnion₂.mp hx + obtain ⟨⟨B, C⟩, hBC', rfl⟩ := Finset.mem_image.mp hBC + obtain ⟨hB, hC⟩ := Finset.mem_product.mp hBC' rw [← Box.prod_toSet] at hxBC obtain ⟨⟨y, z⟩, ⟨hy, hz⟩, rfl⟩ := hxBC refine ⟨⟨y, z⟩, ⟨?_, ?_⟩, rfl⟩ - · exact Set.mem_iUnion.mpr ⟨B, ⟨hB, hy⟩⟩ - · exact Set.mem_iUnion.mpr ⟨C, ⟨hC, hz⟩⟩ + · exact Set.mem_iUnion₂.mpr ⟨B, hB, hy⟩ + · exact Set.mem_iUnion₂.mpr ⟨C, hC, hz⟩ /-- The product of two pairwise disjoint box families remains pairwise disjoint. -/ lemma Box.prod_pairwiseDisjoint {d₁ d₂:ℕ} {S : Finset (Box d₁)} {T : Finset (Box d₂)} @@ -1971,12 +2000,12 @@ lemma Box.prod_pairwiseDisjoint {d₁ d₂:ℕ} {S : Finset (Box d₁)} {T : Fin (hT : (T : Set (Box d₂)).PairwiseDisjoint Box.toSet) : (((S ×ˢ T).image (fun p => p.1.prod p.2) : Finset (Box (d₁ + d₂))) : Set (Box (d₁ + d₂))).PairwiseDisjoint Box.toSet := by - classical rw [Set.pairwiseDisjoint_iff] intro B₁ hB₁ B₂ hB₂ hne - simp only [Finset.mem_coe, Finset.mem_image, Finset.mem_product, exists_prop] at hB₁ hB₂ - obtain ⟨⟨C₁, D₁⟩, ⟨hC₁, hD₁⟩, rfl⟩ := hB₁ - obtain ⟨⟨C₂, D₂⟩, ⟨hC₂, hD₂⟩, rfl⟩ := hB₂ + obtain ⟨⟨C₁, D₁⟩, hmem₁, rfl⟩ := Finset.mem_image.mp (Finset.mem_coe.mp hB₁) + obtain ⟨⟨C₂, D₂⟩, hmem₂, rfl⟩ := Finset.mem_image.mp (Finset.mem_coe.mp hB₂) + obtain ⟨hC₁, hD₁⟩ := Finset.mem_product.mp hmem₁ + obtain ⟨hC₂, hD₂⟩ := Finset.mem_product.mp hmem₂ obtain ⟨x, hx⟩ := hne rw [Set.mem_inter_iff, ← Box.prod_toSet, ← Box.prod_toSet] at hx obtain ⟨hx1, hx2⟩ := hx @@ -2013,23 +2042,21 @@ theorem IsElementary.measure_of_prod {d₁ d₂:ℕ} {E₁: Set (EuclideanSpace' constructor · intro hx obtain ⟨⟨y, z⟩, ⟨hy, hz⟩, rfl⟩ := hx - simp only [Set.mem_iUnion] at hy hz ⊢ - obtain ⟨B, hB, hyB⟩ := hy - obtain ⟨C, hC, hzC⟩ := hz + obtain ⟨B, hB, hyB⟩ := Set.mem_iUnion₂.mp hy + obtain ⟨C, hC, hzC⟩ := Set.mem_iUnion₂.mp hz refine ⟨B.prod C, ?_, ?_⟩ - · exact Finset.mem_image.mpr ⟨⟨B, C⟩, ⟨Finset.mem_product.mpr ⟨hB, hC⟩, rfl⟩⟩ + · exact Finset.mem_image.mpr ⟨⟨B, C⟩, Finset.mem_product.mpr ⟨hB, hC⟩, rfl⟩ · rw [← Box.prod_toSet] exact ⟨⟨y, z⟩, ⟨hyB, hzC⟩, rfl⟩ · intro hx - simp only [Set.mem_iUnion] at hx - obtain ⟨BC, hBC, hxBC⟩ := hx + obtain ⟨BC, hBC, hxBC⟩ := Set.mem_iUnion₂.mp hx obtain ⟨⟨B, C⟩, hBC', rfl⟩ := Finset.mem_image.mp hBC obtain ⟨hB, hC⟩ := Finset.mem_product.mp hBC' rw [← Box.prod_toSet] at hxBC obtain ⟨⟨y, z⟩, ⟨hy, hz⟩, rfl⟩ := hxBC refine ⟨⟨y, z⟩, ⟨?_, ?_⟩, rfl⟩ - · exact Set.mem_iUnion.mpr ⟨B, ⟨hB, hy⟩⟩ - · exact Set.mem_iUnion.mpr ⟨C, ⟨hC, hz⟩⟩ + · exact Set.mem_iUnion₂.mpr ⟨B, hB, hy⟩ + · exact Set.mem_iUnion₂.mpr ⟨C, hC, hz⟩ have hmeas : (hE₁.prod hE₂).measure = ∑ B ∈ U, |B|ᵥ := (hE₁.prod hE₂).measure_eq hU_disj hprod_eq have hE₁m : hE₁.measure = ∑ B ∈ S, |B|ᵥ := hE₁.measure_eq hS_disj hE₁_eq From 022f9628c83b6b52948d44c62dc2010c570b7345 Mon Sep 17 00:00:00 2001 From: Taksh Date: Tue, 25 Aug 2026 09:06:19 +0530 Subject: [PATCH 4/7] fix(MeasureTheory): avoid dependent rewrites in the product lemmas CI still failed on Fin-index rewrites, nat-add commutation in prod_equiv, and underdetermined Finset.image. Use trans/congr for coordinates and pass explicit Finset.image arguments. --- Analysis/MeasureTheory/Section_1_1_1.lean | 41 ++++++++++++++++------- 1 file changed, 29 insertions(+), 12 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_1_1.lean b/Analysis/MeasureTheory/Section_1_1_1.lean index 2424bda63..1132fee4b 100644 --- a/Analysis/MeasureTheory/Section_1_1_1.lean +++ b/Analysis/MeasureTheory/Section_1_1_1.lean @@ -1889,6 +1889,8 @@ lemma EuclideanSpace'.prod_equiv_apply_snd {d₁ d₂:ℕ} (EuclideanSpace'.prod_equiv d₁ d₂ x).2 j = x ⟨d₁ + (j : ℕ), Nat.add_lt_add_left j.isLt d₁⟩ := by simp [EuclideanSpace'.prod_equiv] + congr 1 + exact Fin.ext (Nat.add_comm _ _) /-- The set of a product box is the Cartesian product of the two boxes. -/ lemma Box.prod_toSet {d₁ d₂:ℕ} (B₁: Box d₁) (B₂: Box d₂) : @@ -1900,14 +1902,24 @@ lemma Box.prod_toSet {d₁ d₂:ℕ} (B₁: Box d₁) (B₂: Box d₂) : rw [Box.prod_side] by_cases h : (i : ℕ) < d₁ · rw [dif_pos h] - have hi : i = ⟨(i : ℕ), Nat.lt_add_right d₂ h⟩ := Fin.ext rfl - rw [hi, EuclideanSpace'.prod_equiv_symm_apply_left y z h] + have hcoord : (EuclideanSpace'.prod_equiv d₁ d₂).symm (y, z) i = y ⟨i, h⟩ := by + trans (EuclideanSpace'.prod_equiv d₁ d₂).symm (y, z) + ⟨(i : ℕ), Nat.lt_add_right d₂ h⟩ + · congr 1 + exact Fin.ext rfl + · exact EuclideanSpace'.prod_equiv_symm_apply_left y z h + rw [hcoord] exact hy ⟨i, h⟩ · rw [dif_neg h] have hj : (i : ℕ) - d₁ < d₂ := Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp h) i.isLt - have hi : i = ⟨d₁ + ((i : ℕ) - d₁), Nat.add_lt_add_left hj d₁⟩ := - Fin.ext (Nat.add_sub_of_le (Nat.not_lt.mp h)).symm - rw [hi, EuclideanSpace'.prod_equiv_symm_apply_right y z hj] + have hcoord : (EuclideanSpace'.prod_equiv d₁ d₂).symm (y, z) i = + z ⟨(i : ℕ) - d₁, hj⟩ := by + trans (EuclideanSpace'.prod_equiv d₁ d₂).symm (y, z) + ⟨d₁ + ((i : ℕ) - d₁), Nat.add_lt_add_left hj d₁⟩ + · congr 1 + exact Fin.ext (Nat.add_sub_of_le (Nat.not_lt.mp h)).symm + · exact EuclideanSpace'.prod_equiv_symm_apply_right y z hj + rw [hcoord] exact hz ⟨(i : ℕ) - d₁, hj⟩ · intro hx refine ⟨⟨(EuclideanSpace'.prod_equiv d₁ d₂ x).1, (EuclideanSpace'.prod_equiv d₁ d₂ x).2⟩, ?_, @@ -1960,13 +1972,15 @@ lemma Box.volume_prod {d₁ d₂:ℕ} (B₁: Box d₁) (B₂: Box d₂) : congr 1 · apply Finset.prod_congr rfl intro i _ - rw [Box.prod_side, dif_pos i.isLt] + have hi : (Fin.castAdd d₂ i : ℕ) < d₁ := i.isLt + simp [dif_pos hi] · apply Finset.prod_congr rfl intro j _ - have hnot : ¬ d₁ + (j : ℕ) < d₁ := Nat.not_lt.mpr (Nat.le_add_right _ _) - rw [Box.prod_side, dif_neg hnot] + have hnot : ¬ (Fin.natAdd d₁ j : ℕ) < d₁ := + Nat.not_lt.mpr (Nat.le_add_right d₁ j.val) + simp [dif_neg hnot] congr 1 - exact Fin.ext (Nat.add_sub_cancel_left d₁ j.val) + exact Fin.ext (by simp [Fin.natAdd, Nat.add_sub_cancel_left]) /-- Exercise 1.1.4: The Cartesian product of two elementary sets is elementary. -/ theorem IsElementary.prod {d₁ d₂:ℕ} {E₁: Set (EuclideanSpace' d₁)} {E₂: Set (EuclideanSpace' d₂)} @@ -1981,7 +1995,8 @@ theorem IsElementary.prod {d₁ d₂:ℕ} {E₁: Set (EuclideanSpace' d₁)} {E obtain ⟨B, hB, hyB⟩ := Set.mem_iUnion₂.mp hy obtain ⟨C, hC, hzC⟩ := Set.mem_iUnion₂.mp hz refine ⟨B.prod C, ?_, ?_⟩ - · exact Finset.mem_image.mpr ⟨⟨B, C⟩, Finset.mem_product.mpr ⟨hB, hC⟩, rfl⟩ + · refine (Finset.mem_image (s := S ×ˢ T) (f := fun p => p.1.prod p.2)).mpr ?_ + exact ⟨⟨B, C⟩, Finset.mem_product.mpr ⟨hB, hC⟩, rfl⟩ · rw [← Box.prod_toSet] exact ⟨⟨y, z⟩, ⟨hyB, hzC⟩, rfl⟩ · intro hx @@ -2011,7 +2026,8 @@ lemma Box.prod_pairwiseDisjoint {d₁ d₂:ℕ} {S : Finset (Box d₁)} {T : Fin obtain ⟨hx1, hx2⟩ := hx obtain ⟨⟨y, z⟩, ⟨hy1, hz1⟩, rfl⟩ := hx1 obtain ⟨⟨y', z'⟩, ⟨hy2, hz2⟩, hyz⟩ := hx2 - have hyz' : (y, z) = (y', z') := (EuclideanSpace'.prod_equiv d₁ d₂).symm.injective hyz + have hyz' : (y, z) = (y', z') := + (EuclideanSpace'.prod_equiv d₁ d₂).symm.injective hyz.symm rcases hyz' with ⟨rfl, rfl⟩ have hC : C₁ = C₂ := by by_contra hneC @@ -2045,7 +2061,8 @@ theorem IsElementary.measure_of_prod {d₁ d₂:ℕ} {E₁: Set (EuclideanSpace' obtain ⟨B, hB, hyB⟩ := Set.mem_iUnion₂.mp hy obtain ⟨C, hC, hzC⟩ := Set.mem_iUnion₂.mp hz refine ⟨B.prod C, ?_, ?_⟩ - · exact Finset.mem_image.mpr ⟨⟨B, C⟩, Finset.mem_product.mpr ⟨hB, hC⟩, rfl⟩ + · refine (Finset.mem_image (s := S ×ˢ T) (f := fun p => p.1.prod p.2)).mpr ?_ + exact ⟨⟨B, C⟩, Finset.mem_product.mpr ⟨hB, hC⟩, rfl⟩ · rw [← Box.prod_toSet] exact ⟨⟨y, z⟩, ⟨hyB, hzC⟩, rfl⟩ · intro hx From 4a21fb4e91cce01d5cd5408b7a96475e9fa40fd3 Mon Sep 17 00:00:00 2001 From: Taksh Date: Tue, 25 Aug 2026 10:16:40 +0530 Subject: [PATCH 5/7] fix(MeasureTheory): match prod_equiv toFun indices in the product lemmas MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Unfold Box.prod on Nat indices instead of rewriting Fin equalities, and use mem_iUnion₂ the same way the translation proof does. --- Analysis/MeasureTheory/Section_1_1_1.lean | 123 +++++++++------------- 1 file changed, 48 insertions(+), 75 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_1_1.lean b/Analysis/MeasureTheory/Section_1_1_1.lean index 1132fee4b..2f9ee5cab 100644 --- a/Analysis/MeasureTheory/Section_1_1_1.lean +++ b/Analysis/MeasureTheory/Section_1_1_1.lean @@ -1883,14 +1883,12 @@ lemma EuclideanSpace'.prod_equiv_apply_fst {d₁ d₂:ℕ} (EuclideanSpace'.prod_equiv d₁ d₂ x).1 i = x ⟨i, Nat.lt_add_right d₂ i.isLt⟩ := by simp [EuclideanSpace'.prod_equiv] -/-- Second factor of {name}`prod_equiv`. -/ +/-- Second factor of {name}`prod_equiv`. Matches `toFun`, which uses `i + d₁`. -/ lemma EuclideanSpace'.prod_equiv_apply_snd {d₁ d₂:ℕ} (x : EuclideanSpace' (d₁ + d₂)) (j : Fin d₂) : (EuclideanSpace'.prod_equiv d₁ d₂ x).2 j = - x ⟨d₁ + (j : ℕ), Nat.add_lt_add_left j.isLt d₁⟩ := by + x ⟨(j : ℕ) + d₁, by omega⟩ := by simp [EuclideanSpace'.prod_equiv] - congr 1 - exact Fin.ext (Nat.add_comm _ _) /-- The set of a product box is the Cartesian product of the two boxes. -/ lemma Box.prod_toSet {d₁ d₂:ℕ} (B₁: Box d₁) (B₂: Box d₂) : @@ -1899,49 +1897,26 @@ lemma Box.prod_toSet {d₁ d₂:ℕ} (B₁: Box d₁) (B₂: Box d₂) : constructor · rintro ⟨⟨y, z⟩, ⟨hy, hz⟩, rfl⟩ intro i - rw [Box.prod_side] - by_cases h : (i : ℕ) < d₁ - · rw [dif_pos h] - have hcoord : (EuclideanSpace'.prod_equiv d₁ d₂).symm (y, z) i = y ⟨i, h⟩ := by - trans (EuclideanSpace'.prod_equiv d₁ d₂).symm (y, z) - ⟨(i : ℕ), Nat.lt_add_right d₂ h⟩ - · congr 1 - exact Fin.ext rfl - · exact EuclideanSpace'.prod_equiv_symm_apply_left y z h - rw [hcoord] + rcases i with ⟨i, hi⟩ + simp only [Box.prod] + split_ifs with h + · simp [EuclideanSpace'.prod_equiv, dif_pos h] exact hy ⟨i, h⟩ - · rw [dif_neg h] - have hj : (i : ℕ) - d₁ < d₂ := Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp h) i.isLt - have hcoord : (EuclideanSpace'.prod_equiv d₁ d₂).symm (y, z) i = - z ⟨(i : ℕ) - d₁, hj⟩ := by - trans (EuclideanSpace'.prod_equiv d₁ d₂).symm (y, z) - ⟨d₁ + ((i : ℕ) - d₁), Nat.add_lt_add_left hj d₁⟩ - · congr 1 - exact Fin.ext (Nat.add_sub_of_le (Nat.not_lt.mp h)).symm - · exact EuclideanSpace'.prod_equiv_symm_apply_right y z hj - rw [hcoord] - exact hz ⟨(i : ℕ) - d₁, hj⟩ + · simp [EuclideanSpace'.prod_equiv, dif_neg h] + exact hz ⟨i - d₁, Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp h) hi⟩ · intro hx refine ⟨⟨(EuclideanSpace'.prod_equiv d₁ d₂ x).1, (EuclideanSpace'.prod_equiv d₁ d₂ x).2⟩, ?_, (EuclideanSpace'.prod_equiv d₁ d₂).left_inv x⟩ constructor · intro i - have hx' := hx ⟨i, Nat.lt_add_right d₂ i.isLt⟩ - rw [Box.prod_side, dif_pos i.isLt] at hx' - rw [EuclideanSpace'.prod_equiv_apply_fst] + have hx' := hx ⟨(i : ℕ), Nat.lt_add_right d₂ i.isLt⟩ + simp [Box.prod, EuclideanSpace'.prod_equiv, dif_pos i.isLt] at hx' ⊢ exact hx' · intro j - have hnot : ¬ d₁ + (j : ℕ) < d₁ := Nat.not_lt.mpr (Nat.le_add_right _ _) - have hx' := hx ⟨d₁ + j.val, Nat.add_lt_add_left j.isLt d₁⟩ - rw [Box.prod_side, dif_neg hnot] at hx' - have hside : B₂.side ⟨d₁ + (j : ℕ) - d₁, - Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp hnot) - (Nat.add_lt_add_left j.isLt d₁)⟩ = B₂.side j := by - congr 1 - exact Fin.ext (Nat.add_sub_cancel_left d₁ j.val) - rw [hside] at hx' - rw [EuclideanSpace'.prod_equiv_apply_snd] - exact hx' + have hnot : ¬ (j : ℕ) + d₁ < d₁ := Nat.not_lt.mpr (Nat.le_add_left d₁ _) + have hx' := hx ⟨(j : ℕ) + d₁, by omega⟩ + simp [Box.prod, EuclideanSpace'.prod_equiv, dif_neg hnot] at hx' ⊢ + convert hx' <;> (apply Fin.ext; exact Nat.add_sub_cancel (j : ℕ) d₁) /-- Recovering the factors from a product box. -/ lemma Box.prod_injective {d₁ d₂:ℕ} : @@ -1954,14 +1929,14 @@ lemma Box.prod_injective {d₁ d₂:ℕ} : rw [Box.prod_side, Box.prod_side, dif_pos i.isLt, dif_pos i.isLt] at this exact this · ext j - have hnot : ¬ d₁ + (j : ℕ) < d₁ := Nat.not_lt.mpr (Nat.le_add_right _ _) - have := congrFun hside ⟨d₁ + j.val, Nat.add_lt_add_left j.isLt d₁⟩ + have hnot : ¬ (j : ℕ) + d₁ < d₁ := Nat.not_lt.mpr (Nat.le_add_left d₁ _) + have := congrFun hside ⟨(j : ℕ) + d₁, by omega⟩ rw [Box.prod_side, Box.prod_side, dif_neg hnot, dif_neg hnot] at this - have hj (C : Box d₂) : C.side ⟨d₁ + (j : ℕ) - d₁, + have hj (C : Box d₂) : C.side ⟨(j : ℕ) + d₁ - d₁, Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp hnot) - (Nat.add_lt_add_left j.isLt d₁)⟩ = C.side j := by - congr 1 - exact Fin.ext (Nat.add_sub_cancel_left d₁ j.val) + (by omega)⟩ = C.side j := by + apply Fin.ext + exact Nat.add_sub_cancel (j : ℕ) d₁ rwa [hj C₁, hj C₂] at this /-- Volume of a product box is the product of the volumes. -/ @@ -1969,18 +1944,14 @@ lemma Box.volume_prod {d₁ d₂:ℕ} (B₁: Box d₁) (B₂: Box d₂) : |(B₁.prod B₂)|ᵥ = |B₁|ᵥ * |B₂|ᵥ := by simp only [Box.volume] rw [Fin.prod_univ_add] - congr 1 + refine congrArg₂ (· * ·) ?_ ?_ · apply Finset.prod_congr rfl intro i _ - have hi : (Fin.castAdd d₂ i : ℕ) < d₁ := i.isLt - simp [dif_pos hi] + simp [Box.prod] · apply Finset.prod_congr rfl intro j _ - have hnot : ¬ (Fin.natAdd d₁ j : ℕ) < d₁ := - Nat.not_lt.mpr (Nat.le_add_right d₁ j.val) - simp [dif_neg hnot] - congr 1 - exact Fin.ext (by simp [Fin.natAdd, Nat.add_sub_cancel_left]) + simp [Box.prod] <;> + (apply Fin.ext; simp [Fin.natAdd, Nat.add_sub_cancel_left]) /-- Exercise 1.1.4: The Cartesian product of two elementary sets is elementary. -/ theorem IsElementary.prod {d₁ d₂:ℕ} {E₁: Set (EuclideanSpace' d₁)} {E₂: Set (EuclideanSpace' d₂)} @@ -1992,22 +1963,23 @@ theorem IsElementary.prod {d₁ d₂:ℕ} {E₁: Set (EuclideanSpace' d₁)} {E constructor · intro hx obtain ⟨⟨y, z⟩, ⟨hy, hz⟩, rfl⟩ := hx - obtain ⟨B, hB, hyB⟩ := Set.mem_iUnion₂.mp hy - obtain ⟨C, hC, hzC⟩ := Set.mem_iUnion₂.mp hz - refine ⟨B.prod C, ?_, ?_⟩ - · refine (Finset.mem_image (s := S ×ˢ T) (f := fun p => p.1.prod p.2)).mpr ?_ - exact ⟨⟨B, C⟩, Finset.mem_product.mpr ⟨hB, hC⟩, rfl⟩ - · rw [← Box.prod_toSet] - exact ⟨⟨y, z⟩, ⟨hyB, hzC⟩, rfl⟩ + rw [Set.mem_iUnion₂] at hy hz ⊢ + obtain ⟨B, hB, hyB⟩ := hy + obtain ⟨C, hC, hzC⟩ := hz + exact ⟨B.prod C, + Finset.mem_image.mpr ⟨⟨B, C⟩, Finset.mem_product.mpr ⟨hB, hC⟩, rfl⟩, + by + rw [← Box.prod_toSet] + exact ⟨⟨y, z⟩, ⟨hyB, hzC⟩, rfl⟩⟩ · intro hx - obtain ⟨BC, hBC, hxBC⟩ := Set.mem_iUnion₂.mp hx + rw [Set.mem_iUnion₂] at hx + obtain ⟨BC, hBC, hxBC⟩ := hx obtain ⟨⟨B, C⟩, hBC', rfl⟩ := Finset.mem_image.mp hBC obtain ⟨hB, hC⟩ := Finset.mem_product.mp hBC' rw [← Box.prod_toSet] at hxBC obtain ⟨⟨y, z⟩, ⟨hy, hz⟩, rfl⟩ := hxBC - refine ⟨⟨y, z⟩, ⟨?_, ?_⟩, rfl⟩ - · exact Set.mem_iUnion₂.mpr ⟨B, hB, hy⟩ - · exact Set.mem_iUnion₂.mpr ⟨C, hC, hz⟩ + exact ⟨⟨y, z⟩, + ⟨Set.mem_iUnion₂.mpr ⟨B, hB, hy⟩, Set.mem_iUnion₂.mpr ⟨C, hC, hz⟩⟩, rfl⟩ /-- The product of two pairwise disjoint box families remains pairwise disjoint. -/ lemma Box.prod_pairwiseDisjoint {d₁ d₂:ℕ} {S : Finset (Box d₁)} {T : Finset (Box d₂)} @@ -2058,22 +2030,23 @@ theorem IsElementary.measure_of_prod {d₁ d₂:ℕ} {E₁: Set (EuclideanSpace' constructor · intro hx obtain ⟨⟨y, z⟩, ⟨hy, hz⟩, rfl⟩ := hx - obtain ⟨B, hB, hyB⟩ := Set.mem_iUnion₂.mp hy - obtain ⟨C, hC, hzC⟩ := Set.mem_iUnion₂.mp hz - refine ⟨B.prod C, ?_, ?_⟩ - · refine (Finset.mem_image (s := S ×ˢ T) (f := fun p => p.1.prod p.2)).mpr ?_ - exact ⟨⟨B, C⟩, Finset.mem_product.mpr ⟨hB, hC⟩, rfl⟩ - · rw [← Box.prod_toSet] - exact ⟨⟨y, z⟩, ⟨hyB, hzC⟩, rfl⟩ + rw [Set.mem_iUnion₂] at hy hz ⊢ + obtain ⟨B, hB, hyB⟩ := hy + obtain ⟨C, hC, hzC⟩ := hz + exact ⟨B.prod C, + Finset.mem_image.mpr ⟨⟨B, C⟩, Finset.mem_product.mpr ⟨hB, hC⟩, rfl⟩, + by + rw [← Box.prod_toSet] + exact ⟨⟨y, z⟩, ⟨hyB, hzC⟩, rfl⟩⟩ · intro hx - obtain ⟨BC, hBC, hxBC⟩ := Set.mem_iUnion₂.mp hx + rw [Set.mem_iUnion₂] at hx + obtain ⟨BC, hBC, hxBC⟩ := hx obtain ⟨⟨B, C⟩, hBC', rfl⟩ := Finset.mem_image.mp hBC obtain ⟨hB, hC⟩ := Finset.mem_product.mp hBC' rw [← Box.prod_toSet] at hxBC obtain ⟨⟨y, z⟩, ⟨hy, hz⟩, rfl⟩ := hxBC - refine ⟨⟨y, z⟩, ⟨?_, ?_⟩, rfl⟩ - · exact Set.mem_iUnion₂.mpr ⟨B, hB, hy⟩ - · exact Set.mem_iUnion₂.mpr ⟨C, hC, hz⟩ + exact ⟨⟨y, z⟩, + ⟨Set.mem_iUnion₂.mpr ⟨B, hB, hy⟩, Set.mem_iUnion₂.mpr ⟨C, hC, hz⟩⟩, rfl⟩ have hmeas : (hE₁.prod hE₂).measure = ∑ B ∈ U, |B|ᵥ := (hE₁.prod hE₂).measure_eq hU_disj hprod_eq have hE₁m : hE₁.measure = ∑ B ∈ S, |B|ᵥ := hE₁.measure_eq hS_disj hE₁_eq From 5205895aa9f80e8f02d6a2d5d83d8d019a1c212b Mon Sep 17 00:00:00 2001 From: Taksh Date: Tue, 25 Aug 2026 10:34:13 +0530 Subject: [PATCH 6/7] fix(MeasureTheory): rewrite the product-box side via Fin.eq_of_val_eq apply Fin.ext was aimed at the Fin index, but the goal was an equality of sides. --- Analysis/MeasureTheory/Section_1_1_1.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_1_1.lean b/Analysis/MeasureTheory/Section_1_1_1.lean index 2f9ee5cab..ce582fcf3 100644 --- a/Analysis/MeasureTheory/Section_1_1_1.lean +++ b/Analysis/MeasureTheory/Section_1_1_1.lean @@ -1934,9 +1934,8 @@ lemma Box.prod_injective {d₁ d₂:ℕ} : rw [Box.prod_side, Box.prod_side, dif_neg hnot, dif_neg hnot] at this have hj (C : Box d₂) : C.side ⟨(j : ℕ) + d₁ - d₁, Nat.sub_lt_left_of_lt_add (Nat.not_lt.mp hnot) - (by omega)⟩ = C.side j := by - apply Fin.ext - exact Nat.add_sub_cancel (j : ℕ) d₁ + (by omega)⟩ = C.side j := + congrArg C.side (Fin.eq_of_val_eq (Nat.add_sub_cancel (j : ℕ) d₁)) rwa [hj C₁, hj C₂] at this /-- Volume of a product box is the product of the volumes. -/ From 930f9d1dc3d06510ce1c23173efcb27e90ca7afc Mon Sep 17 00:00:00 2001 From: Taksh Date: Tue, 25 Aug 2026 10:56:03 +0530 Subject: [PATCH 7/7] =?UTF-8?q?fix(MeasureTheory):=20control=20the=20produ?= =?UTF-8?q?ct=20error=20with=20a=20=CE=B4=20that=20scales=20with=20the=20m?= =?UTF-8?q?easures?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit min ε 1 is too coarse: (μ+δ)² can overshoot ε when the measures are large. Scale δ by 1/(μ₁+μ₂+1) instead, and rewrite the coordinate squares with rw. --- Analysis/MeasureTheory/Section_1_1_2.lean | 235 ++++++++++------------ 1 file changed, 101 insertions(+), 134 deletions(-) diff --git a/Analysis/MeasureTheory/Section_1_1_2.lean b/Analysis/MeasureTheory/Section_1_1_2.lean index 85b4cb985..2bfb12b07 100644 --- a/Analysis/MeasureTheory/Section_1_1_2.lean +++ b/Analysis/MeasureTheory/Section_1_1_2.lean @@ -888,19 +888,19 @@ theorem JordanMeasure.measure_uniq' {d:ℕ} {m': (E: Set (EuclideanSpace' d)) lemma EuclideanSpace'.norm_prod_equiv_symm {d₁ d₂:ℕ} (y : EuclideanSpace' d₁) (z : EuclideanSpace' d₂) : ‖(EuclideanSpace'.prod_equiv d₁ d₂).symm (y, z)‖ ^ 2 = ‖y‖ ^ 2 + ‖z‖ ^ 2 := by + have hy : 0 ≤ ∑ i : Fin d₁, (y i) ^ 2 := Finset.sum_nonneg fun _ _ => sq_nonneg _ + have hz : 0 ≤ ∑ j : Fin d₂, (z j) ^ 2 := Finset.sum_nonneg fun _ _ => sq_nonneg _ have hsum : 0 ≤ ∑ i : Fin (d₁ + d₂), ((EuclideanSpace'.prod_equiv d₁ d₂).symm (y, z) i) ^ 2 := Finset.sum_nonneg fun _ _ => sq_nonneg _ - simp only [EuclideanSpace'.norm_eq, Real.sq_sqrt hsum, Real.sq_sqrt - (Finset.sum_nonneg fun _ _ => sq_nonneg _), Real.sq_sqrt - (Finset.sum_nonneg (fun _ _ => sq_nonneg (_ : ℝ)))] + simp only [EuclideanSpace'.norm_eq, Real.sq_sqrt hsum, Real.sq_sqrt hy, Real.sq_sqrt hz] rw [Fin.sum_univ_add] - congr 1 + refine congrArg₂ (· + ·) ?_ ?_ · apply Finset.sum_congr rfl intro i _ - simp [EuclideanSpace'.prod_equiv_symm_apply_left y z i.isLt] + rw [EuclideanSpace'.prod_equiv_symm_apply_left y z i.isLt] · apply Finset.sum_congr rfl intro j _ - simp [EuclideanSpace'.prod_equiv_symm_apply_right y z j.isLt] + rw [EuclideanSpace'.prod_equiv_symm_apply_right y z j.isLt] lemma EuclideanSpace'.prod_mono {d₁ d₂:ℕ} {E₁ E₁' : Set (EuclideanSpace' d₁)} {E₂ E₂' : Set (EuclideanSpace' d₂)} @@ -932,146 +932,113 @@ lemma EuclideanSpace'.prod_isBounded {d₁ d₂:ℕ} Real.sq_sqrt (add_nonneg (sq_nonneg M₁) (sq_nonneg M₂)), norm_nonneg ((EuclideanSpace'.prod_equiv d₁ d₂).symm (y, z))] +/-- Outer Jordan measure of a product is at most the product of the measures. -/ +lemma Jordan_outer_measure_prod_le {d₁ d₂:ℕ} {E₁: Set (EuclideanSpace' d₁)} + {E₂: Set (EuclideanSpace' d₂)} (hE₁: JordanMeasurable E₁) (hE₂: JordanMeasurable E₂) : + Jordan_outer_measure (EuclideanSpace'.prod E₁ E₂) ≤ hE₁.measure * hE₂.measure := by + have hμ₁ : 0 ≤ hE₁.measure := JordanMeasurable.nonneg hE₁ + have hμ₂ : 0 ≤ hE₂.measure := JordanMeasurable.nonneg hE₂ + refine le_of_forall_pos_le_add fun ε hε => ?_ + set δ := min (1 : ℝ) (ε / (hE₁.measure + hE₂.measure + 1)) with hδdef + have hden : (0 : ℝ) < hE₁.measure + hE₂.measure + 1 := by positivity + have hδpos : 0 < δ := lt_min (by norm_num) (div_pos hε hden) + have hm₁ : Jordan_outer_measure E₁ < hE₁.measure + δ := by + rw [← hE₁.eq_outer]; exact lt_add_of_pos_right _ hδpos + have hm₂ : Jordan_outer_measure E₂ < hE₂.measure + δ := by + rw [← hE₂.eq_outer]; exact lt_add_of_pos_right _ hδpos + obtain ⟨A, hA, hAE, hAμ⟩ := le_Jordan_outer hm₁ hE₁.1 + obtain ⟨B, hB, hBF, hBμ⟩ := le_Jordan_outer hm₂ hE₂.1 + have hprod_le : Jordan_outer_measure (EuclideanSpace'.prod E₁ E₂) ≤ + (hA.prod hB).measure := + Jordan_outer_le (hA.prod hB) (EuclideanSpace'.prod_mono hAE hBF) + rw [IsElementary.measure_of_prod hA hB] at hprod_le + have hA_nn : 0 ≤ hA.measure := IsElementary.measure_nonneg hA + have hB_nn : 0 ≤ hB.measure := IsElementary.measure_nonneg hB + have hmul : hA.measure * hB.measure ≤ + (hE₁.measure + δ) * (hE₂.measure + δ) := + mul_le_mul (le_of_lt hAμ) (le_of_lt hBμ) hB_nn (add_nonneg hμ₁ hδpos.le) + have hδ1 : δ ≤ 1 := min_le_left _ _ + have hδε : δ * (hE₁.measure + hE₂.measure + 1) ≤ ε := + (le_div_iff₀ hden).mp (min_le_right _ _) + have hexp : (hE₁.measure + δ) * (hE₂.measure + δ) ≤ + hE₁.measure * hE₂.measure + ε := by + calc + (hE₁.measure + δ) * (hE₂.measure + δ) + = hE₁.measure * hE₂.measure + δ * (hE₁.measure + hE₂.measure + δ) := by ring + _ ≤ hE₁.measure * hE₂.measure + δ * (hE₁.measure + hE₂.measure + 1) := by + nlinarith [hμ₁, hμ₂, hδpos.le, hδ1] + _ ≤ hE₁.measure * hE₂.measure + ε := by nlinarith + linarith + +/-- Inner Jordan measure of a product is at least the product of the measures. -/ +lemma Jordan_inner_measure_prod_ge {d₁ d₂:ℕ} {E₁: Set (EuclideanSpace' d₁)} + {E₂: Set (EuclideanSpace' d₂)} (hE₁: JordanMeasurable E₁) (hE₂: JordanMeasurable E₂) : + hE₁.measure * hE₂.measure ≤ Jordan_inner_measure (EuclideanSpace'.prod E₁ E₂) := by + have hμ₁ : 0 ≤ hE₁.measure := JordanMeasurable.nonneg hE₁ + have hμ₂ : 0 ≤ hE₂.measure := JordanMeasurable.nonneg hE₂ + have hbound := EuclideanSpace'.prod_isBounded hE₁.1 hE₂.1 + refine le_of_forall_pos_le_add fun ε hε => ?_ + by_cases h0 : hE₁.measure = 0 ∨ hE₂.measure = 0 + · have : hE₁.measure * hE₂.measure = 0 := by + rcases h0 with h | h <;> simp [h] + linarith [Jordan_inner_measure_nonneg (EuclideanSpace'.prod E₁ E₂)] + · push_neg at h0 + have hpos₁ : 0 < hE₁.measure := lt_of_le_of_ne hμ₁ (Ne.symm h0.1) + have hpos₂ : 0 < hE₂.measure := lt_of_le_of_ne hμ₂ (Ne.symm h0.2) + have hden : (0 : ℝ) < hE₁.measure + hE₂.measure + 1 := by positivity + set δ := min (min (hE₁.measure / 2) (hE₂.measure / 2)) + (min (1 : ℝ) (ε / (hE₁.measure + hE₂.measure + 1))) with hδdef + have hδpos : 0 < δ := + lt_min (lt_min (half_pos hpos₁) (half_pos hpos₂)) + (lt_min (by norm_num) (div_pos hε hden)) + have hm₁ : hE₁.measure - δ < Jordan_inner_measure E₁ := by + rw [← hE₁.eq_inner]; linarith + have hm₂ : hE₂.measure - δ < Jordan_inner_measure E₂ := by + rw [← hE₂.eq_inner]; linarith + obtain ⟨A, hA, hAE, hAμ⟩ := Jordan_inner_le hm₁ + obtain ⟨B, hB, hBF, hBμ⟩ := Jordan_inner_le hm₂ + have hprod_ge : (hA.prod hB).measure ≤ + Jordan_inner_measure (EuclideanSpace'.prod E₁ E₂) := + le_Jordan_inner (hA.prod hB) (EuclideanSpace'.prod_mono hAE hBF) hbound + rw [IsElementary.measure_of_prod hA hB] at hprod_ge + have hA_nn : 0 ≤ hA.measure := IsElementary.measure_nonneg hA + have hδle₁ : δ ≤ hE₁.measure / 2 := (min_le_left _ _).trans (min_le_left _ _) + have hδle₂ : δ ≤ hE₂.measure / 2 := (min_le_left _ _).trans (min_le_right _ _) + have hsub₂ : 0 ≤ hE₂.measure - δ := by nlinarith + have hmul : (hE₁.measure - δ) * (hE₂.measure - δ) ≤ hA.measure * hB.measure := + mul_le_mul (le_of_lt hAμ) (le_of_lt hBμ) hsub₂ hA_nn + have hδ1 : δ ≤ 1 := (min_le_right _ _).trans (min_le_left _ _) + have hδε : δ * (hE₁.measure + hE₂.measure + 1) ≤ ε := + (le_div_iff₀ hden).mp ((min_le_right _ _).trans (min_le_right _ _)) + have : hE₁.measure * hE₂.measure ≤ (hE₁.measure - δ) * (hE₂.measure - δ) + ε := by + calc + hE₁.measure * hE₂.measure + = (hE₁.measure - δ) * (hE₂.measure - δ) + δ * (hE₁.measure + hE₂.measure - δ) := by ring + _ ≤ (hE₁.measure - δ) * (hE₂.measure - δ) + δ * (hE₁.measure + hE₂.measure + 1) := by + nlinarith [hμ₁, hμ₂, hδpos.le, hδ1] + _ ≤ (hE₁.measure - δ) * (hE₂.measure - δ) + ε := by nlinarith + linarith + /-- Exercise 1.1.16 -/ theorem JordanMeasurable.prod {d₁ d₂:ℕ} {E₁: Set (EuclideanSpace' d₁)} {E₂: Set (EuclideanSpace' d₂)} (hE₁: JordanMeasurable E₁) (hE₂: JordanMeasurable E₂) : JordanMeasurable (EuclideanSpace'.prod E₁ E₂) := by have hbound := EuclideanSpace'.prod_isBounded hE₁.1 hE₂.1 refine ⟨hbound, le_antisymm (Jordan_inner_le_outer hbound) ?_⟩ - have hμ₁ : 0 ≤ hE₁.measure := JordanMeasurable.nonneg hE₁ - have hμ₂ : 0 ≤ hE₂.measure := JordanMeasurable.nonneg hE₂ - -- outer(E₁ × E₂) ≤ μ(E₁) μ(E₂): sandwich by elementary supersets - have houter : Jordan_outer_measure (EuclideanSpace'.prod E₁ E₂) ≤ hE₁.measure * hE₂.measure := by - refine le_of_forall_pos_le_add fun ε hε => ?_ - have hε' : 0 < ε / 2 := by positivity - -- pick elementary supersets within ε of each outer measure - have hm₁ : Jordan_outer_measure E₁ < hE₁.measure + min ε 1 := by - rw [← hE₁.eq_outer]; linarith [min_le_right ε 1, min_le_left ε 1] - have hm₂ : Jordan_outer_measure E₂ < hE₂.measure + min ε 1 := by - rw [← hE₂.eq_outer]; linarith [min_le_right ε 1, min_le_left ε 1] - obtain ⟨A, hA, hAE, hAμ⟩ := le_Jordan_outer hm₁ hE₁.1 - obtain ⟨B, hB, hBF, hBμ⟩ := le_Jordan_outer hm₂ hE₂.1 - have hprod_le : Jordan_outer_measure (EuclideanSpace'.prod E₁ E₂) ≤ - (hA.prod hB).measure := - Jordan_outer_le (hA.prod hB) (EuclideanSpace'.prod_mono hAE hBF) - rw [IsElementary.measure_of_prod hA hB] at hprod_le - have hA_nn : 0 ≤ hA.measure := IsElementary.measure_nonneg hA - have hB_nn : 0 ≤ hB.measure := IsElementary.measure_nonneg hB - have hδ : (0 : ℝ) < min ε 1 := lt_min hε (by norm_num) - have hmul : hA.measure * hB.measure ≤ - (hE₁.measure + min ε 1) * (hE₂.measure + min ε 1) := - mul_le_mul (le_of_lt hAμ) (le_of_lt hBμ) hB_nn (add_nonneg hμ₁ (le_of_lt hδ)) - have hexp : (hE₁.measure + min ε 1) * (hE₂.measure + min ε 1) ≤ - hE₁.measure * hE₂.measure + ε := by - have hmin : min ε 1 ≤ 1 := min_le_right _ _ - have hminε : min ε 1 ≤ ε := min_le_left _ _ - nlinarith [hμ₁, hμ₂, hmin, hminε, mul_nonneg hμ₁ hμ₂] - linarith - -- inner(E₁ × E₂) ≥ μ(E₁) μ(E₂): sandwich by elementary subsets - have hinner : hE₁.measure * hE₂.measure ≤ Jordan_inner_measure (EuclideanSpace'.prod E₁ E₂) := by - refine le_of_forall_pos_le_add fun ε hε => ?_ - by_cases h0 : hE₁.measure = 0 ∨ hE₂.measure = 0 - · have : hE₁.measure * hE₂.measure = 0 := by - rcases h0 with h | h <;> simp [h] - linarith [Jordan_inner_measure_nonneg (EuclideanSpace'.prod E₁ E₂)] - · push_neg at h0 - have hpos₁ : 0 < hE₁.measure := lt_of_le_of_ne hμ₁ (Ne.symm h0.1) - have hpos₂ : 0 < hE₂.measure := lt_of_le_of_ne hμ₂ (Ne.symm h0.2) - set δ := min (min (hE₁.measure / 2) (hE₂.measure / 2)) (min ε 1) with hδdef - have hδpos : 0 < δ := by - dsimp [δ] - exact lt_min (lt_min (half_pos hpos₁) (half_pos hpos₂)) - (lt_min hε (by norm_num)) - have hm₁ : hE₁.measure - δ < Jordan_inner_measure E₁ := by - rw [← hE₁.eq_inner]; linarith - have hm₂ : hE₂.measure - δ < Jordan_inner_measure E₂ := by - rw [← hE₂.eq_inner]; linarith - obtain ⟨A, hA, hAE, hAμ⟩ := Jordan_inner_le hm₁ - obtain ⟨B, hB, hBF, hBμ⟩ := Jordan_inner_le hm₂ - have hprod_ge : (hA.prod hB).measure ≤ - Jordan_inner_measure (EuclideanSpace'.prod E₁ E₂) := - le_Jordan_inner (hA.prod hB) (EuclideanSpace'.prod_mono hAE hBF) hbound - rw [IsElementary.measure_of_prod hA hB] at hprod_ge - have hA_nn : 0 ≤ hA.measure := IsElementary.measure_nonneg hA - have hB_nn : 0 ≤ hB.measure := IsElementary.measure_nonneg hB - have hmul : (hE₁.measure - δ) * (hE₂.measure - δ) ≤ hA.measure * hB.measure := - mul_le_mul (le_of_lt hAμ) (le_of_lt hBμ) (by linarith) hA_nn - have : hE₁.measure * hE₂.measure ≤ (hE₁.measure - δ) * (hE₂.measure - δ) + ε := by - have hδle : δ ≤ ε := (min_le_right _ _).trans (min_le_left _ _) - have hδ1 : δ ≤ 1 := (min_le_right _ _).trans (min_le_right _ _) - nlinarith [hμ₁, hμ₂, hδle, hδ1, mul_nonneg hμ₁ hμ₂] - linarith - -- inner ≤ outer was used in the first conjunct; now outer ≤ inner calc Jordan_outer_measure (EuclideanSpace'.prod E₁ E₂) - ≤ hE₁.measure * hE₂.measure := houter - _ ≤ Jordan_inner_measure (EuclideanSpace'.prod E₁ E₂) := hinner + ≤ hE₁.measure * hE₂.measure := Jordan_outer_measure_prod_le hE₁ hE₂ + _ ≤ Jordan_inner_measure (EuclideanSpace'.prod E₁ E₂) := + Jordan_inner_measure_prod_ge hE₁ hE₂ /-- Jordan measure is multiplicative on products: μ(E₁ × E₂) = μ(E₁) \* μ(E₂). -/ theorem JordanMeasurable.measure_of_prod {d₁ d₂:ℕ} {E₁: Set (EuclideanSpace' d₁)} {E₂: Set (EuclideanSpace' d₂)} (hE₁: JordanMeasurable E₁) (hE₂: JordanMeasurable E₂) : (hE₁.prod hE₂).measure = hE₁.measure * hE₂.measure := by - have hμ₁ : 0 ≤ hE₁.measure := JordanMeasurable.nonneg hE₁ - have hμ₂ : 0 ≤ hE₂.measure := JordanMeasurable.nonneg hE₂ + have hp := hE₁.prod hE₂ refine le_antisymm ?_ ?_ - · -- measure = inner ≤? wait measure is inner; outer ≤ product from the prod proof - rw [JordanMeasurable.eq_outer (hE₁.prod hE₂)] - -- reuse the same outer bound: product of enclosing elementary sets - have hbound := EuclideanSpace'.prod_isBounded hE₁.1 hE₂.1 - refine le_of_forall_pos_le_add fun ε hε => ?_ - have hm₁ : Jordan_outer_measure E₁ < hE₁.measure + min ε 1 := by - rw [← hE₁.eq_outer]; linarith [min_le_right ε 1] - have hm₂ : Jordan_outer_measure E₂ < hE₂.measure + min ε 1 := by - rw [← hE₂.eq_outer]; linarith [min_le_right ε 1] - obtain ⟨A, hA, hAE, hAμ⟩ := le_Jordan_outer hm₁ hE₁.1 - obtain ⟨B, hB, hBF, hBμ⟩ := le_Jordan_outer hm₂ hE₂.1 - have hprod_le : Jordan_outer_measure (EuclideanSpace'.prod E₁ E₂) ≤ (hA.prod hB).measure := - Jordan_outer_le (hA.prod hB) (EuclideanSpace'.prod_mono hAE hBF) - rw [IsElementary.measure_of_prod hA hB] at hprod_le - have hA_nn : 0 ≤ hA.measure := IsElementary.measure_nonneg hA - have hB_nn : 0 ≤ hB.measure := IsElementary.measure_nonneg hB - have hδ : (0 : ℝ) < min ε 1 := lt_min hε (by norm_num) - have hmul : hA.measure * hB.measure ≤ - (hE₁.measure + min ε 1) * (hE₂.measure + min ε 1) := - mul_le_mul (le_of_lt hAμ) (le_of_lt hBμ) hB_nn (add_nonneg hμ₁ (le_of_lt hδ)) - have hexp : (hE₁.measure + min ε 1) * (hE₂.measure + min ε 1) ≤ - hE₁.measure * hE₂.measure + ε := by - have hmin : min ε 1 ≤ 1 := min_le_right _ _ - have hminε : min ε 1 ≤ ε := min_le_left _ _ - nlinarith [hμ₁, hμ₂, hmin, hminε] - linarith - · rw [JordanMeasurable.eq_inner (hE₁.prod hE₂)] - -- same inner bound as in `prod` - have hbound := EuclideanSpace'.prod_isBounded hE₁.1 hE₂.1 - refine le_of_forall_pos_le_add fun ε hε => ?_ - by_cases h0 : hE₁.measure = 0 ∨ hE₂.measure = 0 - · have : hE₁.measure * hE₂.measure = 0 := by - rcases h0 with h | h <;> simp [h] - linarith [Jordan_inner_measure_nonneg (EuclideanSpace'.prod E₁ E₂)] - · push_neg at h0 - have hpos₁ : 0 < hE₁.measure := lt_of_le_of_ne hμ₁ (Ne.symm h0.1) - have hpos₂ : 0 < hE₂.measure := lt_of_le_of_ne hμ₂ (Ne.symm h0.2) - set δ := min (min (hE₁.measure / 2) (hE₂.measure / 2)) (min ε 1) with hδdef - have hδpos : 0 < δ := by - dsimp [δ] - exact lt_min (lt_min (half_pos hpos₁) (half_pos hpos₂)) - (lt_min hε (by norm_num)) - have hm₁ : hE₁.measure - δ < Jordan_inner_measure E₁ := by - rw [← hE₁.eq_inner]; linarith - have hm₂ : hE₂.measure - δ < Jordan_inner_measure E₂ := by - rw [← hE₂.eq_inner]; linarith - obtain ⟨A, hA, hAE, hAμ⟩ := Jordan_inner_le hm₁ - obtain ⟨B, hB, hBF, hBμ⟩ := Jordan_inner_le hm₂ - have hprod_ge : (hA.prod hB).measure ≤ - Jordan_inner_measure (EuclideanSpace'.prod E₁ E₂) := - le_Jordan_inner (hA.prod hB) (EuclideanSpace'.prod_mono hAE hBF) hbound - rw [IsElementary.measure_of_prod hA hB] at hprod_ge - have hA_nn : 0 ≤ hA.measure := IsElementary.measure_nonneg hA - have hmul : (hE₁.measure - δ) * (hE₂.measure - δ) ≤ hA.measure * hB.measure := - mul_le_mul (le_of_lt hAμ) (le_of_lt hBμ) (by linarith) hA_nn - have : hE₁.measure * hE₂.measure ≤ (hE₁.measure - δ) * (hE₂.measure - δ) + ε := by - have hδle : δ ≤ ε := (min_le_right _ _).trans (min_le_left _ _) - have hδ1 : δ ≤ 1 := (min_le_right _ _).trans (min_le_right _ _) - nlinarith [hμ₁, hμ₂, hδle, hδ1] - linarith + · rw [JordanMeasurable.eq_outer hp] + exact Jordan_outer_measure_prod_le hE₁ hE₂ + · rw [JordanMeasurable.eq_inner hp] + exact Jordan_inner_measure_prod_ge hE₁ hE₂ /-- Two sets are isometric if one is an orthogonal transformation plus translation of the other. -/ abbrev Isometric {d:ℕ} (E F: Set (EuclideanSpace' d)) : Prop :=