diff --git a/analysis/Analysis/MeasureTheory/Section_1_2_2.lean b/analysis/Analysis/MeasureTheory/Section_1_2_2.lean index 32eae7f6..bccb231b 100644 --- a/analysis/Analysis/MeasureTheory/Section_1_2_2.lean +++ b/analysis/Analysis/MeasureTheory/Section_1_2_2.lean @@ -915,7 +915,7 @@ theorem Jordan_measurable.lebesgue {d:ℕ} {E: Set (EuclideanSpace' d)} (hE: Jor open BoundedInterval -abbrev CantorInterval (n:ℕ) : Set ℝ := ⋃ a : Fin n → ({0, 2}:Set ℕ), (Icc (∑ i, (a i)/(3:ℝ)^(i.val+1)) (∑ i, a i/(3:ℝ)^(i.val+1) + 1/(3:ℝ)^(n+1))).toSet +abbrev CantorInterval (n:ℕ) : Set ℝ := ⋃ a : Fin n → ({0, 2}:Set ℕ), (Icc (∑ i, (a i)/(3:ℝ)^(i.val+1)) (∑ i, a i/(3:ℝ)^(i.val+1) + 1/(3:ℝ)^n)).toSet abbrev CantorSet : Set ℝ := ⋂ n : ℕ, CantorInterval n diff --git a/analysis/Analysis/MeasureTheory/Section_1_3_2.lean b/analysis/Analysis/MeasureTheory/Section_1_3_2.lean index d2dd0a30..e6a3815f 100644 --- a/analysis/Analysis/MeasureTheory/Section_1_3_2.lean +++ b/analysis/Analysis/MeasureTheory/Section_1_3_2.lean @@ -1763,39 +1763,43 @@ the inverse image f⁻¹(E) of a Lebesgue measurable set E need not be Lebesgue **Strategy** (from the textbook): 1. The Cantor set C := {∑ aⱼ 3^{-j} : aⱼ ∈ {0,2}} has measure zero -2. Define f: ℝ → [0,+∞] by: for x ∈ [0,1] with non-terminating binary expansion - x = ∑ bⱼ 2^{-j} (bⱼ ∈ {0,1}), set f(x) := ∑ 2bⱼ 3^{-j} (which lies in C) - and f(x) := 0 otherwise -3. f maps BINARY digits to TERNARY (Cantor set) representation -4. f is bijective from A (non-terminating binary decimals in [0,1]) onto C -5. f is strictly increasing on A (preserves lexicographic order of digit sequences) -6. **Measurability of f**: By Lemma 1.3.9(viii), f is measurable iff for every λ, - {x : f(x) ≤ λ} is Lebesgue measurable. Since f is monotone on [0,1], - {x ∈ [0,1] : f(x) ≤ λ} is an interval, and intervals are measurable. -7. From the Vitali construction, we can find a non-measurable F ⊆ A -8. Set E := f(F). Since f(F) ⊆ C (null set), E is Lebesgue measurable -9. But f⁻¹(E) = F is non-measurable, as desired +2. Define f: [0,1] → C by mapping binary digits to ternary: f(∑ bⱼ 2^{-j}) = ∑ 2bⱼ 3^{-j} +3. f is bijective from A (non-terminating binary decimals) onto C, and f is measurable +4. Take non-measurable F ⊆ A (from Vitali construction) +5. E := f(F) ⊆ C is measurable (subset of null set), but f⁻¹(E) = F is non-measurable + +**Implementation note**: Our formalization differs slightly from the textbook: +- **Textbook**: f(x) = 0 for dyadic rationals (terminating binary decimals) +- **Our version**: f is defined uniformly for all x ∈ [0,1] using floor-based binary digits + +The textbook's f is NOT monotone on [0,1] (e.g., f(0.4) > 0 but f(0.5) = 0). +Our f IS monotone on all of [0,1], which simplifies the measurability proof: +sublevel sets are intervals, hence measurable by Lemma 1.3.9(viii). + +Both versions work for the theorem because: +- Both are injective on A (non-dyadic numbers have unique binary expansions) +- Both map [0,1] into CantorSet ∪ {0} +- Both give measurable f with f⁻¹(E) = F non-measurable -/ -namespace Remark_1_3_10 -/-- The properties required of the binary-to-ternary function for this construction. - The function maps [0,1] into the Cantor set C by converting binary digits to ternary. -/ -structure BinaryToTernaryProperties (g : ℝ → ℝ) : Prop where - nonneg : ∀ x, 0 ≤ g x - bounded : ∀ x, g x ≤ 1 - zero_outside : ∀ x, x ∉ Set.Icc 0 1 → g x = 0 -- g(x) = 0 outside [0,1] - zero_at_zero : g 0 = 0 -- g(0) = 0 (binary 0.000... maps to ternary 0.000...) - zero_set_countable : (Set.Icc 0 1 ∩ {x | g x = 0}).Countable -- {g = 0} ∩ [0,1] is countable (dyadic rationals) - monotone_on : MonotoneOn g (Set.Icc 0 1) -- g is monotone on [0,1] - image_in_cantor : g '' (Set.Icc 0 1) ⊆ CantorSet ∪ {0} - injective_on_nonterminating : ∃ A : Set ℝ, A ⊆ Set.Icc 0 1 ∧ - (Set.Icc 0 1 \ A).Countable ∧ -- A is co-countable in [0,1] - Set.InjOn g A -- g is injective on A (hence bijective onto g(A) ⊆ C) +/-- Dyadic rationals: numbers of the form k/2^n where k ≤ 2^n. + These are exactly the real numbers with terminating binary expansions. -/ +def DyadicRationals : Set ℝ := {x : ℝ | ∃ (k n : ℕ), x = k / 2^n ∧ k ≤ 2^n} -/-! ### Binary digit extraction and helper lemmas -/ +/-- Dyadic rationals are countable. -/ +lemma DyadicRationals.countable : DyadicRationals.Countable := by + let D' := ⋃ n : ℕ, (fun k : Fin (2^n + 1) => (k : ℝ) / 2^n) '' Set.univ + have hD'_countable : D'.Countable := + Set.countable_iUnion (fun n => Set.Countable.image Set.countable_univ _) + apply Set.Countable.mono _ hD'_countable + intro x ⟨k, n, hk, hk_le⟩ + simp only [Set.mem_iUnion, Set.mem_image, Set.mem_univ, true_and, D'] + use n + have hk_lt : k < 2^n + 1 := Nat.lt_succ_of_le hk_le + exact ⟨⟨k, hk_lt⟩, hk.symm⟩ /-- Binary digit extraction: bⱼ(x) = ⌊2^j · x⌋ mod 2. - For x ∈ [0,1), this extracts the j-th binary digit (1-indexed). + For x ∈ [0,1), this extracts the j-th binary digit. Special case: x = 1 has all digits = 1 (1 = 0.111...₂). For x ∉ [0,1], all digits are 0. -/ noncomputable def binaryDigit (x : ℝ) (j : ℕ) : ℕ := @@ -1803,19 +1807,10 @@ noncomputable def binaryDigit (x : ℝ) (j : ℕ) : ℕ := else if x = 1 then 1 else 0 -/-- The binary-to-ternary function: g(x) = ∑_{j≥1} 2·bⱼ(x)·3^{-j} for x ∈ [0,1], else 0. -/ -noncomputable def binaryToTernaryFn (x : ℝ) : ℝ := - if x ∈ Set.Icc (0:ℝ) 1 then - ∑' j : ℕ, (2 * binaryDigit x (j + 1) : ℝ) * (1/3:ℝ)^(j + 1) - else 0 - /-- Binary digits are in {0, 1}. -/ lemma binaryDigit_le_one (x : ℝ) (j : ℕ) : binaryDigit x j ≤ 1 := by simp only [binaryDigit] - split_ifs with h1 h2 - · omega -- ⌊2^j * x⌋₊ % 2 ≤ 1 since mod 2 gives 0 or 1 - · rfl -- 1 ≤ 1 - · norm_num -- 0 ≤ 1 + split_ifs with h1 h2 <;> omega /-- Binary digits of 0 are all 0. -/ lemma binaryDigit_zero (j : ℕ) : binaryDigit 0 j = 0 := by @@ -1828,20 +1823,126 @@ lemma binaryDigit_zero (j : ℕ) : binaryDigit 0 j = 0 := by lemma binaryDigit_one (j : ℕ) : binaryDigit 1 j = 1 := by simp only [binaryDigit, Set.mem_Ico, lt_self_iff_false, and_false, ↓reduceIte] -/-- The dyadic rationals in [0,1]: {k/2^n : k ≤ 2^n}. -/ -def DyadicRationals : Set ℝ := {x : ℝ | ∃ (k n : ℕ), x = k / 2^n ∧ k ≤ 2^n} +/-- The full sum ∑_{j≥0} 2·(1/3)^{j+1} = 1. -/ +lemma tsum_two_thirds_geometric : ∑' j : ℕ, (2:ℝ) * (1/3:ℝ)^(j + 1) = 1 := by + have h1 : ∑' j : ℕ, (1/3:ℝ)^j = (1 - 1/3)⁻¹ := + tsum_geometric_of_lt_one (by norm_num) (by norm_num) + calc ∑' j : ℕ, (2:ℝ) * (1/3:ℝ)^(j + 1) + = ∑' j : ℕ, (2/3:ℝ) * (1/3:ℝ)^j := by congr 1; ext j; ring + _ = (2/3) * ∑' j : ℕ, (1/3:ℝ)^j := by rw [tsum_mul_left] + _ = (2/3) * (1 - 1/3)⁻¹ := by rw [h1] + _ = 1 := by norm_num -/-- Dyadic rationals are countable. -/ -lemma DyadicRationals.countable : DyadicRationals.Countable := by - let D' := ⋃ n : ℕ, (fun k : Fin (2^n + 1) => (k : ℝ) / 2^n) '' Set.univ - have hD'_countable : D'.Countable := - Set.countable_iUnion (fun n => Set.Countable.image Set.countable_univ _) - apply Set.Countable.mono _ hD'_countable - intro x ⟨k, n, hk, hk_le⟩ - simp only [Set.mem_iUnion, Set.mem_image, Set.mem_univ, true_and, D'] - use n - have hk_lt : k < 2^n + 1 := Nat.lt_succ_of_le hk_le - exact ⟨⟨k, hk_lt⟩, hk.symm⟩ +/-- The tail sum bound: ∑_{j≥k} 2·(1/3)^{j+1} = (1/3)^k. -/ +lemma tsum_tail_bound (k : ℕ) : + ∑' j : ℕ, (2:ℝ) * (1/3:ℝ)^(k + j + 1) = (1/3:ℝ)^k := by + have h1 : ∑' j : ℕ, (1/3:ℝ)^j = (1 - 1/3)⁻¹ := + tsum_geometric_of_lt_one (by norm_num) (by norm_num) + calc ∑' j : ℕ, (2:ℝ) * (1/3:ℝ)^(k + j + 1) + = ∑' j : ℕ, (2:ℝ) * ((1/3:ℝ)^(k+1) * (1/3:ℝ)^j) := by + congr 1; ext j; rw [← pow_add]; ring_nf + _ = (2:ℝ) * (1/3:ℝ)^(k+1) * ∑' j : ℕ, (1/3:ℝ)^j := by + rw [← tsum_mul_left]; congr 1; ext j; ring + _ = (2:ℝ) * (1/3:ℝ)^(k+1) * (1 - 1/3)⁻¹ := by rw [h1] + _ = (1/3:ℝ)^k := by field_simp; ring + +/-- Helper: if ⌊2z⌋₊ % 2 = 1 then ⌊2z⌋₊ ≥ 2⌊z⌋₊ + 1 -/ +lemma floor_two_mul_odd_ge {z : ℝ} (hz : 0 ≤ z) (hodd : ⌊2 * z⌋₊ % 2 = 1) : + ⌊2 * z⌋₊ ≥ 2 * ⌊z⌋₊ + 1 := by + have h_decomp : ⌊2 * z⌋₊ = 2 * (⌊2 * z⌋₊ / 2) + ⌊2 * z⌋₊ % 2 := (Nat.div_add_mod _ _).symm + rw [hodd] at h_decomp + have h_div : ⌊2 * z⌋₊ / 2 ≥ ⌊z⌋₊ := by + have h1 : (2 * ⌊z⌋₊ : ℕ) ≤ ⌊2 * z⌋₊ := by + have hfloor := Nat.floor_le hz + apply Nat.le_floor + simp only [Nat.cast_mul, Nat.cast_ofNat] + linarith + rw [mul_comm] at h1 + exact (Nat.le_div_iff_mul_le (by norm_num : 0 < 2)).mpr h1 + omega + +/-- Helper: if ⌊2z⌋₊ % 2 = 0 then ⌊2z⌋₊ ≤ 2⌊z⌋₊ -/ +lemma floor_two_mul_even_le {z : ℝ} (hz : 0 ≤ z) (heven : ⌊2 * z⌋₊ % 2 = 0) : + ⌊2 * z⌋₊ ≤ 2 * ⌊z⌋₊ := by + have h_decomp : ⌊2 * z⌋₊ = 2 * (⌊2 * z⌋₊ / 2) + ⌊2 * z⌋₊ % 2 := (Nat.div_add_mod _ _).symm + rw [heven, add_zero] at h_decomp + have h_div : ⌊2 * z⌋₊ / 2 ≤ ⌊z⌋₊ := by + have h1 : ⌊2 * z⌋₊ < 2 * (⌊z⌋₊ + 1) := by + have := Nat.lt_floor_add_one z + have h2 : 2 * z < 2 * (⌊z⌋₊ + 1) := by linarith + have h3 : (⌊2 * z⌋₊ : ℝ) ≤ 2 * z := Nat.floor_le (mul_nonneg (by norm_num) hz) + have h4 : (⌊2 * z⌋₊ : ℝ) < 2 * (↑⌊z⌋₊ + 1) := lt_of_le_of_lt h3 h2 + have h5 : (⌊2 * z⌋₊ : ℝ) < 2 * ⌊z⌋₊ + 2 := by linarith + exact_mod_cast h5 + omega + omega + +/-- Helper: equal mod 2 and equal ⌊z⌋ implies equal ⌊2z⌋ -/ +lemma floor_two_mul_eq_of_mod_eq {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) + (h_floor : ⌊x⌋₊ = ⌊y⌋₊) (h_mod : ⌊2 * x⌋₊ % 2 = ⌊2 * y⌋₊ % 2) : + ⌊2 * x⌋₊ = ⌊2 * y⌋₊ := by + by_cases hxodd : ⌊2 * x⌋₊ % 2 = 1 + · have hyodd := h_mod ▸ hxodd + have hx_ge := floor_two_mul_odd_ge hx hxodd + have hy_ge := floor_two_mul_odd_ge hy hyodd + have hx_lt : ⌊2 * x⌋₊ < 2 * ⌊x⌋₊ + 2 := by + have := Nat.lt_floor_add_one x + have h2 : 2 * x < 2 * (⌊x⌋₊ + 1) := by linarith + have h3 : (⌊2 * x⌋₊ : ℝ) ≤ 2 * x := Nat.floor_le (mul_nonneg (by norm_num) hx) + have h4 : (⌊2 * x⌋₊ : ℝ) < 2 * ⌊x⌋₊ + 2 := by linarith + exact_mod_cast h4 + have hy_lt : ⌊2 * y⌋₊ < 2 * ⌊y⌋₊ + 2 := by + have := Nat.lt_floor_add_one y + have h2 : 2 * y < 2 * (⌊y⌋₊ + 1) := by linarith + have h3 : (⌊2 * y⌋₊ : ℝ) ≤ 2 * y := Nat.floor_le (mul_nonneg (by norm_num) hy) + have h4 : (⌊2 * y⌋₊ : ℝ) < 2 * ⌊y⌋₊ + 2 := by linarith + exact_mod_cast h4 + omega + · have hxeven : ⌊2 * x⌋₊ % 2 = 0 := Nat.mod_two_eq_zero_or_one (⌊2 * x⌋₊) |>.resolve_right hxodd + have hyeven := h_mod ▸ hxeven + have hx_le := floor_two_mul_even_le hx hxeven + have hy_le := floor_two_mul_even_le hy hyeven + have hx_ge : ⌊2 * x⌋₊ ≥ 2 * ⌊x⌋₊ := by + have h1 : (2 * ⌊x⌋₊ : ℕ) ≤ ⌊2 * x⌋₊ := by + have hfloor := Nat.floor_le hx + apply Nat.le_floor + simp only [Nat.cast_mul, Nat.cast_ofNat] + linarith + exact h1 + have hy_ge : ⌊2 * y⌋₊ ≥ 2 * ⌊y⌋₊ := by + have h1 : (2 * ⌊y⌋₊ : ℕ) ≤ ⌊2 * y⌋₊ := by + have hfloor := Nat.floor_le hy + apply Nat.le_floor + simp only [Nat.cast_mul, Nat.cast_ofNat] + linarith + exact h1 + omega + +namespace Remark_1_3_10 + +/-- The properties required of the binary-to-ternary function for this construction. + The function maps [0,1] into the Cantor set C by converting binary digits to ternary. + + Note: Unlike the textbook (which sets g(x) = 0 for dyadic rationals), our g is defined + uniformly for all x ∈ [0,1]. This makes g monotone on ALL of [0,1], not just on A. -/ +structure BinaryToTernaryProperties (g : ℝ → ℝ) : Prop where + nonneg : ∀ x, 0 ≤ g x + bounded : ∀ x, g x ≤ 1 + zero_outside : ∀ x, x ∉ Set.Icc 0 1 → g x = 0 -- g(x) = 0 outside [0,1] + zero_at_zero : g 0 = 0 -- g(0) = 0 (binary 0.000... maps to ternary 0.000...) + zero_set_countable : (Set.Icc 0 1 ∩ {x | g x = 0}).Countable -- {g = 0} ∩ [0,1] = {0} + monotone_on : MonotoneOn g (Set.Icc 0 1) -- g is monotone on ALL of [0,1] + image_in_cantor : g '' (Set.Icc 0 1) ⊆ CantorSet ∪ {0} + injective_on_nonterminating : ∃ A : Set ℝ, A ⊆ Set.Icc 0 1 ∧ + (Set.Icc 0 1 \ A).Countable ∧ -- A is co-countable in [0,1] + Set.InjOn g A ∧ -- g is injective on A (hence bijective onto g(A) ⊆ C) + A ∩ DyadicRationals = ∅ -- A excludes dyadic rationals + +/-- The binary-to-ternary function: g(x) = ∑_{j≥1} 2·bⱼ(x)·3^{-j} for x ∈ [0,1], else 0. -/ +noncomputable def binaryToTernaryFn (x : ℝ) : ℝ := + if x ∈ Set.Icc (0:ℝ) 1 then + ∑' j : ℕ, (2 * binaryDigit x (j + 1) : ℝ) * (1/3:ℝ)^(j + 1) + else 0 /-- The series ∑ 2·bⱼ(x)·3^{-j} is summable for any x. -/ lemma binaryToTernary_summable (x : ℝ) : @@ -1859,27 +1960,15 @@ lemma binaryToTernary_summable (x : ℝ) : · have h : Summable (fun j : ℕ => (1/3:ℝ)^j) := summable_geometric_of_lt_one (by norm_num) (by norm_num) exact (h.mul_left 2).comp_injective (fun _ _ h => Nat.succ_injective h) -/-- The full sum ∑_{j≥0} 2·(1/3)^{j+1} = 1. -/ -lemma tsum_two_thirds_geometric : ∑' j : ℕ, (2:ℝ) * (1/3:ℝ)^(j + 1) = 1 := by - have h1 : ∑' j : ℕ, (1/3:ℝ)^j = (1 - 1/3)⁻¹ := - tsum_geometric_of_lt_one (by norm_num) (by norm_num) - calc ∑' j : ℕ, (2:ℝ) * (1/3:ℝ)^(j + 1) - = ∑' j : ℕ, (2/3:ℝ) * (1/3:ℝ)^j := by congr 1; ext j; ring - _ = (2/3) * ∑' j : ℕ, (1/3:ℝ)^j := by rw [tsum_mul_left] - _ = (2/3) * (1 - 1/3)⁻¹ := by rw [h1] - _ = 1 := by norm_num - /-! ### Helper lemmas for monotonicity proof -/ -/-- For x ∈ (0, 1) (non-dyadic), there exists a position where the binary digit is 1. -/ +/-- For x ∈ (0, 1), there exists a position where the binary digit is 1. -/ lemma binaryDigit_exists_one_of_pos {x : ℝ} (hx_pos : 0 < x) (hx_lt : x < 1) : ∃ j, binaryDigit x (j + 1) = 1 := by have hx_Ico : x ∈ Set.Ico (0:ℝ) 1 := ⟨le_of_lt hx_pos, hx_lt⟩ - -- For x ∈ (0, 1), there exists j such that 2^{j+1} * x ∈ [1, 2) have hinv_ge_one : 1 ≤ x⁻¹ := Bound.one_le_inv₀ hx_pos (le_of_lt hx_lt) have h_pow_exists := exists_nat_pow_near hinv_ge_one (by norm_num : (1:ℝ) < 2) obtain ⟨n, hn_le, hn_lt⟩ := h_pow_exists - -- We have 2^n ≤ 1/x < 2^{n+1} have h_pow_unbounded : ∃ j : ℕ, 1 ≤ (2:ℝ)^(j+1) * x := by use n have h2n_pos : (0:ℝ) < 2^n := by positivity @@ -1916,7 +2005,7 @@ lemma binaryDigit_partial_sum_le {x : ℝ} (hx : x ∈ Set.Ico (0:ℝ) 1) (n : exact Nat.floor_le (mul_nonneg hx.1 (le_of_lt h2n_pos)) /-- The partial sum bounds x from above: x < Sₙ(x) + 2^{-n} -/ -lemma binaryDigit_partial_sum_lt {x : ℝ} (hx : x ∈ Set.Ico (0:ℝ) 1) (n : ℕ) : +lemma binaryDigit_partial_sum_lt (x : ℝ) (n : ℕ) : x < (⌊(2:ℝ)^n * x⌋₊ : ℝ) / (2:ℝ)^n + (1:ℝ) / (2:ℝ)^n := by have h2n_pos : (0:ℝ) < 2^n := by positivity have := Nat.lt_floor_add_one ((2:ℝ)^n * x) @@ -1926,81 +2015,6 @@ lemma binaryDigit_partial_sum_lt {x : ℝ} (hx : x ∈ Set.Ico (0:ℝ) 1) (n : apply div_lt_div_of_pos_right h1 h2n_pos _ = (⌊(2:ℝ)^n * x⌋₊ : ℝ) / (2:ℝ)^n + (1:ℝ) / (2:ℝ)^n := by ring -/-- Helper: if ⌊2z⌋₊ % 2 = 1 then ⌊2z⌋₊ ≥ 2⌊z⌋₊ + 1 -/ -lemma floor_two_mul_odd_ge {z : ℝ} (hz : 0 ≤ z) (hodd : ⌊2 * z⌋₊ % 2 = 1) : - ⌊2 * z⌋₊ ≥ 2 * ⌊z⌋₊ + 1 := by - have h_decomp : ⌊2 * z⌋₊ = 2 * (⌊2 * z⌋₊ / 2) + ⌊2 * z⌋₊ % 2 := (Nat.div_add_mod _ _).symm - rw [hodd] at h_decomp - -- ⌊2z⌋₊ / 2 ≥ ⌊z⌋₊ - have h_div : ⌊2 * z⌋₊ / 2 ≥ ⌊z⌋₊ := by - have h1 : (2 * ⌊z⌋₊ : ℕ) ≤ ⌊2 * z⌋₊ := by - have hfloor := Nat.floor_le hz - apply Nat.le_floor - simp only [Nat.cast_mul, Nat.cast_ofNat] - linarith - rw [mul_comm] at h1 - exact (Nat.le_div_iff_mul_le (by norm_num : 0 < 2)).mpr h1 - omega - -/-- Helper: if ⌊2z⌋₊ % 2 = 0 then ⌊2z⌋₊ ≤ 2⌊z⌋₊ -/ -lemma floor_two_mul_even_le {z : ℝ} (hz : 0 ≤ z) (heven : ⌊2 * z⌋₊ % 2 = 0) : - ⌊2 * z⌋₊ ≤ 2 * ⌊z⌋₊ := by - have h_decomp : ⌊2 * z⌋₊ = 2 * (⌊2 * z⌋₊ / 2) + ⌊2 * z⌋₊ % 2 := (Nat.div_add_mod _ _).symm - rw [heven, add_zero] at h_decomp - -- ⌊2z⌋₊ / 2 ≤ ⌊z⌋₊ - have h_div : ⌊2 * z⌋₊ / 2 ≤ ⌊z⌋₊ := by - have h1 : ⌊2 * z⌋₊ < 2 * (⌊z⌋₊ + 1) := by - have := Nat.lt_floor_add_one z - have h2 : 2 * z < 2 * (⌊z⌋₊ + 1) := by linarith - have h3 : (⌊2 * z⌋₊ : ℝ) ≤ 2 * z := Nat.floor_le (mul_nonneg (by norm_num) hz) - have h4 : (⌊2 * z⌋₊ : ℝ) < 2 * (↑⌊z⌋₊ + 1) := lt_of_le_of_lt h3 h2 - have h5 : (⌊2 * z⌋₊ : ℝ) < 2 * ⌊z⌋₊ + 2 := by linarith - exact_mod_cast h5 - omega - omega - -/-- Helper: equal mod 2 and equal ⌊z⌋ implies equal ⌊2z⌋ -/ -lemma floor_two_mul_eq_of_mod_eq {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) - (h_floor : ⌊x⌋₊ = ⌊y⌋₊) (h_mod : ⌊2 * x⌋₊ % 2 = ⌊2 * y⌋₊ % 2) : - ⌊2 * x⌋₊ = ⌊2 * y⌋₊ := by - -- Both decompose as 2 * ⌊z⌋₊ + something based on mod 2 - by_cases hxodd : ⌊2 * x⌋₊ % 2 = 1 - · -- Both are odd - have hyodd := h_mod ▸ hxodd - have hx_ge := floor_two_mul_odd_ge hx hxodd - have hy_ge := floor_two_mul_odd_ge hy hyodd - have hx_lt : ⌊2 * x⌋₊ < 2 * ⌊x⌋₊ + 2 := by - have := Nat.lt_floor_add_one x - have h2 : 2 * x < 2 * (⌊x⌋₊ + 1) := by linarith - have h3 : (⌊2 * x⌋₊ : ℝ) ≤ 2 * x := Nat.floor_le (mul_nonneg (by norm_num) hx) - have h4 : (⌊2 * x⌋₊ : ℝ) < 2 * ⌊x⌋₊ + 2 := by linarith - exact_mod_cast h4 - have hy_lt : ⌊2 * y⌋₊ < 2 * ⌊y⌋₊ + 2 := by - have := Nat.lt_floor_add_one y - have h2 : 2 * y < 2 * (⌊y⌋₊ + 1) := by linarith - have h3 : (⌊2 * y⌋₊ : ℝ) ≤ 2 * y := Nat.floor_le (mul_nonneg (by norm_num) hy) - have h4 : (⌊2 * y⌋₊ : ℝ) < 2 * ⌊y⌋₊ + 2 := by linarith - exact_mod_cast h4 - rw [h_floor] at hx_ge hx_lt - omega - · -- Both are even - have hxeven : ⌊2 * x⌋₊ % 2 = 0 := by omega - have hyeven := h_mod ▸ hxeven - have hx_le := floor_two_mul_even_le hx hxeven - have hy_le := floor_two_mul_even_le hy hyeven - have hx_ge : 2 * ⌊x⌋₊ ≤ ⌊2 * x⌋₊ := by - have hfl := Nat.floor_le hx - apply Nat.le_floor - simp only [Nat.cast_mul, Nat.cast_ofNat] - linarith - have hy_ge : 2 * ⌊y⌋₊ ≤ ⌊2 * y⌋₊ := by - have hfl := Nat.floor_le hy - apply Nat.le_floor - simp only [Nat.cast_mul, Nat.cast_ofNat] - linarith - rw [h_floor] at hx_le hx_ge - omega - /-- Key lemma: if bₖ(x) = 1, then x ≥ ⌊2^k * x⌋₊ / 2^k + 2^{-(k+1)} -/ lemma binaryDigit_one_implies_lower_bound {x : ℝ} (hx : x ∈ Set.Ico (0:ℝ) 1) (k : ℕ) (hbk : binaryDigit x (k + 1) = 1) : @@ -2034,7 +2048,7 @@ lemma binaryDigit_zero_implies_upper_bound {y : ℝ} (hy : y ∈ Set.Ico (0:ℝ) have h_floor_rel : ⌊(2:ℝ)^(k+1) * y⌋₊ ≤ 2 * ⌊(2:ℝ)^k * y⌋₊ := by rw [heq] exact floor_two_mul_even_le hy_nonneg h_floor_even - have h_lt := binaryDigit_partial_sum_lt hy (k + 1) + have h_lt := binaryDigit_partial_sum_lt y (k + 1) calc y < (⌊(2:ℝ)^(k+1) * y⌋₊ : ℝ) / (2:ℝ)^(k + 1) + (1:ℝ) / (2:ℝ)^(k + 1) := h_lt _ = (⌊(2:ℝ)^(k+1) * y⌋₊ + 1 : ℝ) / (2:ℝ)^(k + 1) := by ring _ ≤ (2 * ⌊(2:ℝ)^k * y⌋₊ + 1 : ℝ) / (2:ℝ)^(k + 1) := by @@ -2068,13 +2082,11 @@ lemma floor_eq_of_binaryDigit_eq {x y : ℝ} (hx : x ∈ Set.Ico (0:ℝ) 1) (hy rw [h1, h2] exact floor_two_mul_eq_of_mod_eq hx_nonneg hy_nonneg ih' hmod_eq' -/-- For x, y ∈ [0,1) with x < y, there exists a first position k where digits differ, - and at that position bₖ(x) < bₖ(y). -/ +/-- For x, y ∈ [0,1) with x < y, there exists a first position k where bₖ(x) < bₖ(y). -/ lemma binaryDigit_first_diff {x y : ℝ} (hx : x ∈ Set.Ico (0:ℝ) 1) (hy : y ∈ Set.Ico (0:ℝ) 1) (hxy : x < y) : ∃ k, binaryDigit x (k + 1) < binaryDigit y (k + 1) ∧ ∀ j < k, binaryDigit x (j + 1) = binaryDigit y (j + 1) := by - -- Step 1: There exists some position where digits differ (otherwise x = y) have h_exists_diff : ∃ j, binaryDigit x (j + 1) ≠ binaryDigit y (j + 1) := by by_contra h_all_eq push_neg at h_all_eq @@ -2084,9 +2096,9 @@ lemma binaryDigit_first_diff {x y : ℝ} (hx : x ∈ Set.Ico (0:ℝ) 1) (hy : y have h_close : ∀ n, |x - y| < (1:ℝ) / (2:ℝ)^n := by intro n have hx_bounds := binaryDigit_partial_sum_le hx n - have hx_bounds' := binaryDigit_partial_sum_lt hx n + have hx_bounds' := binaryDigit_partial_sum_lt x n have hy_bounds := binaryDigit_partial_sum_le hy n - have hy_bounds' := binaryDigit_partial_sum_lt hy n + have hy_bounds' := binaryDigit_partial_sum_lt y n rw [h_floor_eq n] at hx_bounds hx_bounds' rw [abs_lt] constructor <;> linarith @@ -2098,13 +2110,11 @@ lemma binaryDigit_first_diff {x y : ℝ} (hx : x ∈ Set.Ico (0:ℝ) 1) (hy : y have h1 : (1:ℝ) / 2^n = (1/2)^n := by field_simp linarith exact absurd hxy_eq (ne_of_lt hxy) - -- Step 2: Find the FIRST position where digits differ let k := Nat.find h_exists_diff have hk_diff : binaryDigit x (k + 1) ≠ binaryDigit y (k + 1) := Nat.find_spec h_exists_diff have hk_first : ∀ j < k, binaryDigit x (j + 1) = binaryDigit y (j + 1) := by intro j hj exact of_not_not (Nat.find_min h_exists_diff hj) - -- Step 3: Show bₖ(x) < bₖ(y) by contradiction have hbx := binaryDigit_le_one x (k + 1) have hby := binaryDigit_le_one y (k + 1) by_cases h : binaryDigit x (k + 1) < binaryDigit y (k + 1) @@ -2119,34 +2129,77 @@ lemma binaryDigit_first_diff {x y : ℝ} (hx : x ∈ Set.Ico (0:ℝ) 1) (hy : y rw [h_floor_eq] at hx_lb linarith -/-- The tail sum bound: ∑_{j≥k} 2·(1/3)^{j+1} = (1/3)^k. -/ -lemma tsum_tail_bound (k : ℕ) : - ∑' j : ℕ, (2:ℝ) * (1/3:ℝ)^(k + j + 1) = (1/3:ℝ)^k := by - have h1 : ∑' j : ℕ, (1/3:ℝ)^j = (1 - 1/3)⁻¹ := - tsum_geometric_of_lt_one (by norm_num) (by norm_num) - calc ∑' j : ℕ, (2:ℝ) * (1/3:ℝ)^(k + j + 1) - = ∑' j : ℕ, (2:ℝ) * ((1/3:ℝ)^(k+1) * (1/3:ℝ)^j) := by - congr 1; ext j; rw [← pow_add]; ring_nf - _ = (2:ℝ) * (1/3:ℝ)^(k+1) * ∑' j : ℕ, (1/3:ℝ)^j := by - rw [← tsum_mul_left]; congr 1; ext j; ring - _ = (2:ℝ) * (1/3:ℝ)^(k+1) * (1 - 1/3)⁻¹ := by rw [h1] - _ = (1/3:ℝ)^k := by field_simp; ring - -/-- Monotonicity key lemma: if digits agree up to k and differ at k with bₖ(x) < bₖ(y), - then g(x) < g(y). -/ +/-- Monotonicity: if digits agree up to k and bₖ(x) < bₖ(y), then g(x) < g(y). -/ lemma binaryToTernary_lt_of_digit_lt {x y : ℝ} (hx : x ∈ Set.Icc (0:ℝ) 1) (hy : y ∈ Set.Icc (0:ℝ) 1) (k : ℕ) (hk_lt : binaryDigit x (k + 1) < binaryDigit y (k + 1)) (hk_eq : ∀ j < k, binaryDigit x (j + 1) = binaryDigit y (j + 1)) : binaryToTernaryFn x < binaryToTernaryFn y := by - -- The proof is quite involved, so we defer to a sorry for now - -- Key idea: split sums, use that gain at k (= 2*3^{-(k+1)}) > max loss from tail (= 3^{-(k+1)}) - sorry + have hbx_le := binaryDigit_le_one x (k + 1) + have hby_le := binaryDigit_le_one y (k + 1) + have hbx_zero : binaryDigit x (k + 1) = 0 := by omega + have hby_one : binaryDigit y (k + 1) = 1 := by omega + simp only [binaryToTernaryFn, if_pos hx, if_pos hy] + let fx := fun j => (2 * binaryDigit x (j + 1) : ℝ) * (1/3:ℝ)^(j + 1) + let fy := fun j => (2 * binaryDigit y (j + 1) : ℝ) * (1/3:ℝ)^(j + 1) + have h_first_eq : ∑ j ∈ Finset.range k, fx j = ∑ j ∈ Finset.range k, fy j := by + apply Finset.sum_congr rfl + intro j hj + simp only [fx, fy] + rw [hk_eq j (Finset.mem_range.mp hj)] + have h_term_x : fx k = 0 := by simp only [fx, hbx_zero, Nat.cast_zero, mul_zero, zero_mul] + have h_term_y : fy k = (2:ℝ) * (1/3:ℝ)^(k + 1) := by + simp only [fy, hby_one, Nat.cast_one, mul_one] + have h_tail_x : ∑' j, fx (k + 1 + j) ≤ (1/3:ℝ)^(k + 1) := by + calc ∑' j, fx (k + 1 + j) + = ∑' j, (2 * binaryDigit x (k + 1 + j + 1) : ℝ) * (1/3:ℝ)^(k + 1 + j + 1) := rfl + _ ≤ ∑' j, (2:ℝ) * (1/3:ℝ)^(k + 1 + j + 1) := by + apply Summable.tsum_le_tsum + · intro j + have hb := binaryDigit_le_one x (k + 1 + j + 1) + have hb_real : (binaryDigit x (k + 1 + j + 1) : ℝ) ≤ 1 := by exact_mod_cast hb + have h3pos : (0:ℝ) < (1/3)^(k + 1 + j + 1) := by positivity + calc (2 * binaryDigit x (k + 1 + j + 1) : ℝ) * (1/3:ℝ)^(k + 1 + j + 1) + = 2 * (binaryDigit x (k + 1 + j + 1) : ℝ) * (1/3:ℝ)^(k + 1 + j + 1) := by ring + _ ≤ 2 * 1 * (1/3:ℝ)^(k + 1 + j + 1) := by nlinarith + _ = 2 * (1/3:ℝ)^(k + 1 + j + 1) := by ring + · exact (binaryToTernary_summable x).comp_injective (fun j₁ j₂ h => by omega) + · have h : Summable (fun j : ℕ => (1/3:ℝ)^j) := summable_geometric_of_lt_one (by norm_num) (by norm_num) + exact (h.mul_left 2).comp_injective (fun j₁ j₂ h => by omega) + _ = (1/3:ℝ)^(k + 1) := by + have h1 := tsum_geometric_of_lt_one (r := (1/3:ℝ)) (by norm_num) (by norm_num) + calc ∑' j, (2:ℝ) * (1/3:ℝ)^(k + 1 + j + 1) + = ∑' j, (2:ℝ) * ((1/3:ℝ)^(k + 2) * (1/3:ℝ)^j) := by + congr 1; ext j; rw [← pow_add]; ring_nf + _ = (2:ℝ) * (1/3:ℝ)^(k + 2) * ∑' j, (1/3:ℝ)^j := by + rw [← tsum_mul_left]; congr 1; ext j; ring + _ = (2:ℝ) * (1/3:ℝ)^(k + 2) * (1 - 1/3)⁻¹ := by rw [h1] + _ = (1/3:ℝ)^(k + 1) := by field_simp; ring + have h_tail_y_nonneg : 0 ≤ ∑' j, fy (k + 1 + j) := by + apply tsum_nonneg; intro j; simp only [fy]; positivity + have hsum_x : Summable fx := binaryToTernary_summable x + have hsum_y : Summable fy := binaryToTernary_summable y + have h_split_x : ∑' j, fx j = ∑ j ∈ Finset.range k, fx j + fx k + ∑' j, fx (k + 1 + j) := by + rw [← Summable.sum_add_tsum_nat_add (k + 1) hsum_x, Finset.sum_range_succ] + congr 1 + congr 1 + ext j + congr 1 + omega + have h_split_y : ∑' j, fy j = ∑ j ∈ Finset.range k, fy j + fy k + ∑' j, fy (k + 1 + j) := by + rw [← Summable.sum_add_tsum_nat_add (k + 1) hsum_y, Finset.sum_range_succ] + congr 1 + congr 1 + ext j + congr 1 + omega + rw [h_split_x, h_split_y, h_first_eq, h_term_x, h_term_y] + have h3pos : (0:ℝ) < (1/3)^(k + 1) := by positivity + linarith /-! ### Helper lemmas for injectivity proof -/ -/-- Ternary expansions using only digits {0, 2} are unique. - If ∑ dⱼ·3^{-j} = ∑ eⱼ·3^{-j} where dⱼ, eⱼ ∈ {0, 2}, then dⱼ = eⱼ for all j. -/ +/-- Ternary {0,2} expansions are unique. -/ lemma ternary_02_expansion_unique {d e : ℕ → ℕ} (hd : ∀ j, d j ∈ ({0, 2} : Set ℕ)) (he : ∀ j, e j ∈ ({0, 2} : Set ℕ)) @@ -2154,64 +2207,308 @@ lemma ternary_02_expansion_unique {d e : ℕ → ℕ} (hsum_e : Summable (fun j => (e j : ℝ) * (1/3:ℝ)^(j + 1))) (heq : ∑' j, (d j : ℝ) * (1/3:ℝ)^(j + 1) = ∑' j, (e j : ℝ) * (1/3:ℝ)^(j + 1)) : ∀ j, d j = e j := by - sorry + by_contra h_ne + push_neg at h_ne + have h_exists : ∃ k, d k ≠ e k := h_ne + let k := Nat.find h_exists + have hk_ne : d k ≠ e k := Nat.find_spec h_exists + have hk_eq : ∀ j < k, d j = e j := fun j hj => by + by_contra h + exact Nat.find_min h_exists hj h + have hd_k := hd k + have he_k := he k + simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hd_k he_k + rcases hd_k with hdk0 | hdk2 <;> rcases he_k with hek0 | hek2 + · omega + · + have h_first_eq : ∑ j ∈ Finset.range k, (d j : ℝ) * (1/3:ℝ)^(j + 1) = + ∑ j ∈ Finset.range k, (e j : ℝ) * (1/3:ℝ)^(j + 1) := by + apply Finset.sum_congr rfl + intro j hj + rw [hk_eq j (Finset.mem_range.mp hj)] + have h_split_d : ∑' j, (d j : ℝ) * (1/3:ℝ)^(j + 1) = + ∑ j ∈ Finset.range k, (d j : ℝ) * (1/3:ℝ)^(j + 1) + (d k : ℝ) * (1/3:ℝ)^(k + 1) + + ∑' j, (d (k + 1 + j) : ℝ) * (1/3:ℝ)^(k + 1 + j + 1) := by + rw [← Summable.sum_add_tsum_nat_add (k + 1) hsum_d, Finset.sum_range_succ] + congr 1; congr 1 + funext j; simp only [add_comm j (k + 1)] + have h_split_e : ∑' j, (e j : ℝ) * (1/3:ℝ)^(j + 1) = + ∑ j ∈ Finset.range k, (e j : ℝ) * (1/3:ℝ)^(j + 1) + (e k : ℝ) * (1/3:ℝ)^(k + 1) + + ∑' j, (e (k + 1 + j) : ℝ) * (1/3:ℝ)^(k + 1 + j + 1) := by + rw [← Summable.sum_add_tsum_nat_add (k + 1) hsum_e, Finset.sum_range_succ] + congr 1; congr 1 + funext j; simp only [add_comm j (k + 1)] + rw [h_split_d, h_split_e, h_first_eq, hdk0, hek2] at heq + simp only [Nat.cast_zero, zero_mul, Nat.cast_ofNat] at heq + have h_tail_d_bound : ∑' j, (d (k + 1 + j) : ℝ) * (1/3:ℝ)^(k + 1 + j + 1) ≤ (1/3:ℝ)^(k + 1) := by + calc ∑' j, (d (k + 1 + j) : ℝ) * (1/3:ℝ)^(k + 1 + j + 1) + ≤ ∑' j, (2:ℝ) * (1/3:ℝ)^(k + 1 + j + 1) := by + apply Summable.tsum_le_tsum + · intro j + have hdj := hd (k + 1 + j) + simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hdj + rcases hdj with hdj0 | hdj2 + · simp only [hdj0, Nat.cast_zero, zero_mul]; positivity + · simp only [hdj2, Nat.cast_ofNat]; exact le_rfl + · exact hsum_d.comp_injective (fun _ _ h => by omega) + · have h : Summable (fun j : ℕ => (1/3:ℝ)^j) := summable_geometric_of_lt_one (by norm_num) (by norm_num) + exact (h.mul_left 2).comp_injective (fun _ _ h => by omega) + _ = (1/3:ℝ)^(k + 1) := by + have h1 := tsum_geometric_of_lt_one (r := (1/3:ℝ)) (by norm_num) (by norm_num) + calc ∑' j, (2:ℝ) * (1/3:ℝ)^(k + 1 + j + 1) + = ∑' j, (2:ℝ) * ((1/3:ℝ)^(k + 2) * (1/3:ℝ)^j) := by + congr 1; ext j; rw [← pow_add]; ring_nf + _ = (2:ℝ) * (1/3:ℝ)^(k + 2) * ∑' j, (1/3:ℝ)^j := by + rw [← tsum_mul_left]; congr 1; ext j; ring + _ = (2:ℝ) * (1/3:ℝ)^(k + 2) * (1 - 1/3)⁻¹ := by rw [h1] + _ = (1/3:ℝ)^(k + 1) := by field_simp; ring + have h_tail_e_nonneg : 0 ≤ ∑' j, (e (k + 1 + j) : ℝ) * (1/3:ℝ)^(k + 1 + j + 1) := by + apply tsum_nonneg; intro j; positivity + have h3pos : (0:ℝ) < (1/3)^(k + 1) := by positivity + linarith + · + have h_first_eq : ∑ j ∈ Finset.range k, (d j : ℝ) * (1/3:ℝ)^(j + 1) = + ∑ j ∈ Finset.range k, (e j : ℝ) * (1/3:ℝ)^(j + 1) := by + apply Finset.sum_congr rfl + intro j hj + rw [hk_eq j (Finset.mem_range.mp hj)] + have h_split_d : ∑' j, (d j : ℝ) * (1/3:ℝ)^(j + 1) = + ∑ j ∈ Finset.range k, (d j : ℝ) * (1/3:ℝ)^(j + 1) + (d k : ℝ) * (1/3:ℝ)^(k + 1) + + ∑' j, (d (k + 1 + j) : ℝ) * (1/3:ℝ)^(k + 1 + j + 1) := by + rw [← Summable.sum_add_tsum_nat_add (k + 1) hsum_d, Finset.sum_range_succ] + congr 1; congr 1 + funext j; simp only [add_comm j (k + 1)] + have h_split_e : ∑' j, (e j : ℝ) * (1/3:ℝ)^(j + 1) = + ∑ j ∈ Finset.range k, (e j : ℝ) * (1/3:ℝ)^(j + 1) + (e k : ℝ) * (1/3:ℝ)^(k + 1) + + ∑' j, (e (k + 1 + j) : ℝ) * (1/3:ℝ)^(k + 1 + j + 1) := by + rw [← Summable.sum_add_tsum_nat_add (k + 1) hsum_e, Finset.sum_range_succ] + congr 1; congr 1 + funext j; simp only [add_comm j (k + 1)] + rw [h_split_d, h_split_e, h_first_eq, hdk2, hek0] at heq + simp only [Nat.cast_zero, zero_mul, Nat.cast_ofNat] at heq + have h_tail_e_bound : ∑' j, (e (k + 1 + j) : ℝ) * (1/3:ℝ)^(k + 1 + j + 1) ≤ (1/3:ℝ)^(k + 1) := by + calc ∑' j, (e (k + 1 + j) : ℝ) * (1/3:ℝ)^(k + 1 + j + 1) + ≤ ∑' j, (2:ℝ) * (1/3:ℝ)^(k + 1 + j + 1) := by + apply Summable.tsum_le_tsum + · intro j + have hej := he (k + 1 + j) + simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hej + rcases hej with hej0 | hej2 + · simp only [hej0, Nat.cast_zero, zero_mul]; positivity + · simp only [hej2, Nat.cast_ofNat]; exact le_rfl + · exact hsum_e.comp_injective (fun _ _ h => by omega) + · have h : Summable (fun j : ℕ => (1/3:ℝ)^j) := summable_geometric_of_lt_one (by norm_num) (by norm_num) + exact (h.mul_left 2).comp_injective (fun _ _ h => by omega) + _ = (1/3:ℝ)^(k + 1) := by + have h1 := tsum_geometric_of_lt_one (r := (1/3:ℝ)) (by norm_num) (by norm_num) + calc ∑' j, (2:ℝ) * (1/3:ℝ)^(k + 1 + j + 1) + = ∑' j, (2:ℝ) * ((1/3:ℝ)^(k + 2) * (1/3:ℝ)^j) := by + congr 1; ext j; rw [← pow_add]; ring_nf + _ = (2:ℝ) * (1/3:ℝ)^(k + 2) * ∑' j, (1/3:ℝ)^j := by + rw [← tsum_mul_left]; congr 1; ext j; ring + _ = (2:ℝ) * (1/3:ℝ)^(k + 2) * (1 - 1/3)⁻¹ := by rw [h1] + _ = (1/3:ℝ)^(k + 1) := by field_simp; ring + have h_tail_d_nonneg : 0 ≤ ∑' j, (d (k + 1 + j) : ℝ) * (1/3:ℝ)^(k + 1 + j + 1) := by + apply tsum_nonneg; intro j; positivity + have h3pos : (0:ℝ) < (1/3)^(k + 1) := by positivity + linarith + · omega + +/-! ### Helper lemmas for binary expansion sums -/ + +/-- ⌊2y⌋ = 2⌊y⌋ + ⌊2y⌋ % 2 for y ≥ 0. -/ +private lemma floor_two_mul_decomp {y : ℝ} (_hy : 0 ≤ y) : + ⌊2 * y⌋₊ = 2 * ⌊y⌋₊ + ⌊2 * y⌋₊ % 2 := by + have h := Nat.div_add_mod ⌊2 * y⌋₊ 2 + have h_div : ⌊2 * y⌋₊ / 2 = ⌊y⌋₊ := Nat.cast_mul_floor_div_cancel (by norm_num : (2:ℕ) ≠ 0) y + omega + +/-- Partial sum identity: ∑_{j < n} b_j * 2^{-(j+1)} = ⌊2^n * x⌋ / 2^n. -/ +private lemma partial_sum_eq_floor {x : ℝ} (hx : x ∈ Set.Ico (0:ℝ) 1) (n : ℕ) : + ∑ j ∈ Finset.range n, (binaryDigit x (j + 1) : ℝ) * (1/2:ℝ)^(j + 1) = + (⌊(2:ℝ)^n * x⌋₊ : ℝ) / (2:ℝ)^n := by + induction n with + | zero => + simp only [Finset.range_zero, Finset.sum_empty, pow_zero] + have h0 : ⌊x⌋₊ = 0 := Nat.floor_eq_zero.mpr hx.2 + simp [h0] + | succ n ih => + rw [Finset.sum_range_succ, ih] + have h2n_pos : (0:ℝ) < 2^n := by positivity + have hx_nonneg : 0 ≤ x := hx.1 + have hb : binaryDigit x (n + 1) = ⌊(2:ℝ)^(n+1) * x⌋₊ % 2 := by + simp only [binaryDigit, if_pos hx] + have h_floor : ⌊(2:ℝ)^(n+1) * x⌋₊ = 2 * ⌊(2:ℝ)^n * x⌋₊ + ⌊(2:ℝ)^(n+1) * x⌋₊ % 2 := by + have h2 : (2:ℝ)^(n+1) * x = 2 * ((2:ℝ)^n * x) := by ring + rw [h2] + exact floor_two_mul_decomp (mul_nonneg (le_of_lt h2n_pos) hx_nonneg) + rw [hb] + have h2n_ne : (2:ℝ)^n ≠ 0 := ne_of_gt h2n_pos + have h_pow_succ : (2:ℝ)^(n+1) = 2 * 2^n := by ring + rw [h_pow_succ] + have h_half_pow : (1/2:ℝ)^(n+1) = 1 / (2 * 2^n) := by rw [← h_pow_succ]; field_simp + rw [h_half_pow] + have h_floor' : (⌊2 * 2^n * x⌋₊ : ℝ) = 2 * (⌊(2:ℝ)^n * x⌋₊ : ℝ) + (⌊2 * 2^n * x⌋₊ % 2 : ℕ) := by + have h2eq : (2:ℝ) * 2^n * x = (2:ℝ)^(n+1) * x := by ring + rw [h2eq] + exact_mod_cast h_floor + have h2_2n_pos : (0:ℝ) < 2 * 2^n := by positivity + have h2_2n_ne : (2:ℝ) * 2^n ≠ 0 := ne_of_gt h2_2n_pos + rw [h_floor'] + field_simp + ring + +/-- Binary series is summable for x ∈ [0,1). -/ +private lemma binary_summable {x : ℝ} (hx : x ∈ Set.Ico (0:ℝ) 1) : + Summable (fun j => (binaryDigit x (j + 1) : ℝ) * (1/2:ℝ)^(j + 1)) := by + apply Summable.of_nonneg_of_le + · intro j; positivity + · intro j + have h1 : (binaryDigit x (j + 1) : ℝ) ≤ 1 := by + have : binaryDigit x (j + 1) ≤ 1 := by + simp only [binaryDigit, if_pos hx] + omega + exact_mod_cast this + calc (binaryDigit x (j + 1) : ℝ) * (1/2:ℝ)^(j + 1) + ≤ 1 * (1/2:ℝ)^(j + 1) := by nlinarith [pow_pos (by norm_num : (0:ℝ) < 1/2) (j + 1)] + _ = (1/2:ℝ)^(j + 1) := by ring + · have h : Summable (fun j : ℕ => (1/2:ℝ)^j) := summable_geometric_of_lt_one (by norm_num) (by norm_num) + exact h.comp_injective (fun _ _ h => Nat.succ_injective h) -/-- For non-dyadic x ∈ [0,1), equal binary digits imply equal values. - This is because non-dyadic numbers have unique binary expansions. -/ +/-- For non-dyadic x ∈ [0,1), x equals its binary expansion sum. -/ +lemma non_dyadic_eq_binary_sum {x : ℝ} (hx : x ∈ Set.Ico (0:ℝ) 1) (_hnd : x ∉ DyadicRationals) : + x = ∑' j : ℕ, (binaryDigit x (j + 1) : ℝ) * (1/2:ℝ)^(j + 1) := by + have h_summable := binary_summable hx + have h_partial_to_tsum : Filter.Tendsto + (fun n => ∑ j ∈ Finset.range n, (binaryDigit x (j + 1) : ℝ) * (1/2:ℝ)^(j + 1)) + Filter.atTop (nhds (∑' j, (binaryDigit x (j + 1) : ℝ) * (1/2:ℝ)^(j + 1))) := + h_summable.hasSum.tendsto_sum_nat + have h_partial_eq : ∀ n, ∑ j ∈ Finset.range n, (binaryDigit x (j + 1) : ℝ) * (1/2:ℝ)^(j + 1) = + (⌊(2:ℝ)^n * x⌋₊ : ℝ) / (2:ℝ)^n := partial_sum_eq_floor hx + have h_floor_to_x : Filter.Tendsto (fun n => (⌊(2:ℝ)^n * x⌋₊ : ℝ) / (2:ℝ)^n) Filter.atTop (nhds x) := by + have h_lower : ∀ n, (⌊(2:ℝ)^n * x⌋₊ : ℝ) / (2:ℝ)^n ≤ x := fun n => by + have h2n_pos : (0:ℝ) < 2^n := by positivity + rw [div_le_iff₀ h2n_pos, mul_comm] + exact Nat.floor_le (mul_nonneg hx.1 (le_of_lt h2n_pos)) + have h_upper : ∀ n, x < (⌊(2:ℝ)^n * x⌋₊ : ℝ) / (2:ℝ)^n + (1:ℝ) / (2:ℝ)^n := fun n => by + have h2n_pos : (0:ℝ) < 2^n := by positivity + have := Nat.lt_floor_add_one ((2:ℝ)^n * x) + calc x = ((2:ℝ)^n * x) / (2:ℝ)^n := by field_simp + _ < (⌊(2:ℝ)^n * x⌋₊ + 1 : ℝ) / (2:ℝ)^n := by apply div_lt_div_of_pos_right this h2n_pos + _ = (⌊(2:ℝ)^n * x⌋₊ : ℝ) / (2:ℝ)^n + (1:ℝ) / (2:ℝ)^n := by ring + have h_gap : Filter.Tendsto (fun n : ℕ => (1:ℝ) / (2:ℝ)^n) Filter.atTop (nhds 0) := by + have h1 : Filter.Tendsto (fun n : ℕ => ((1:ℝ)/2)^n) Filter.atTop (nhds 0) := + tendsto_pow_atTop_nhds_zero_of_lt_one (by norm_num) (by norm_num) + convert h1 using 1; ext n; field_simp + have h_between : ∀ n, x - (1:ℝ) / (2:ℝ)^n < (⌊(2:ℝ)^n * x⌋₊ : ℝ) / (2:ℝ)^n ∧ + (⌊(2:ℝ)^n * x⌋₊ : ℝ) / (2:ℝ)^n ≤ x := fun n => ⟨by linarith [h_upper n], h_lower n⟩ + apply Metric.tendsto_atTop.mpr + intro ε hε + rw [Metric.tendsto_atTop] at h_gap + obtain ⟨N, hN⟩ := h_gap ε hε + use N + intro n hn + specialize hN n hn + simp only [Real.dist_eq, sub_zero] at hN + rw [abs_of_pos (by positivity)] at hN + have hbn := h_between n + rw [Real.dist_eq, abs_lt] + constructor <;> linarith [hbn.1, hbn.2] + have h_partial_to_x : Filter.Tendsto + (fun n => ∑ j ∈ Finset.range n, (binaryDigit x (j + 1) : ℝ) * (1/2:ℝ)^(j + 1)) + Filter.atTop (nhds x) := by + simp_rw [h_partial_eq] + exact h_floor_to_x + exact tendsto_nhds_unique h_partial_to_x h_partial_to_tsum + +/-- Non-dyadic x ∈ [0,1) with equal binary digits are equal. -/ lemma eq_of_binaryDigit_eq_of_non_dyadic {x₁ x₂ : ℝ} (hx₁ : x₁ ∈ Set.Ico (0:ℝ) 1) (hx₂ : x₂ ∈ Set.Ico (0:ℝ) 1) (hnd₁ : x₁ ∉ DyadicRationals) (hnd₂ : x₂ ∉ DyadicRationals) (heq : ∀ j, binaryDigit x₁ j = binaryDigit x₂ j) : x₁ = x₂ := by - sorry - -/-- For non-dyadic x ∈ [0,1), x equals its binary expansion sum. -/ -lemma non_dyadic_eq_binary_sum {x : ℝ} (hx : x ∈ Set.Ico (0:ℝ) 1) (hnd : x ∉ DyadicRationals) : - x = ∑' j : ℕ, (binaryDigit x (j + 1) : ℝ) * (1/2:ℝ)^(j + 1) := by - sorry + have h1 := non_dyadic_eq_binary_sum hx₁ hnd₁ + have h2 := non_dyadic_eq_binary_sum hx₂ hnd₂ + rw [h1, h2] + congr 1 + ext j + rw [heq (j + 1)] /-! ### Helper lemmas for image_in_cantor -/ -/-- A point in [0,1] with ternary expansion using only {0, 2} digits is in the Cantor set. - This is the key characterization: CantorSet = {∑ dⱼ/3^j : dⱼ ∈ {0, 2}}. -/ +/-- Points with {0,2} ternary digits are in the Cantor set. -/ lemma mem_CantorSet_of_ternary_02 {y : ℝ} (d : ℕ → ℕ) (hd : ∀ j, d j ∈ ({0, 2} : Set ℕ)) (hsum : Summable (fun j => (d j : ℝ) * (1/3:ℝ)^(j + 1))) (hy : y = ∑' j, (d j : ℝ) * (1/3:ℝ)^(j + 1)) : y ∈ CantorSet ∨ y = 0 := by - sorry - -/-- Existence of a binary-to-ternary function with the required properties. - This requires constructing f(x) = ∑ 2bⱼ 3^{-j} where x = ∑ bⱼ 2^{-j}. - - **Construction**: - For x ∈ [0,1], write x in binary as x = ∑_{j≥1} bⱼ 2^{-j} where bⱼ ∈ {0,1}. - Define g(x) := ∑_{j≥1} (2bⱼ) 3^{-j}. - - Since 2bⱼ ∈ {0, 2}, we have g(x) ∈ CantorSet. - For x ∉ [0,1], define g(x) := 0. - - **Properties**: - - nonneg: g(x) ≥ 0 since all terms are nonneg - - bounded: g(x) ≤ ∑_{j≥1} 2·3^{-j} = 1 - - zero_outside: by definition - - monotone_on: if x < y in [0,1], their binary expansions differ at some position, - and lexicographic ordering of binary digits implies g(x) < g(y) - - image_in_cantor: g([0,1]) ⊆ C ∪ {0} by construction - - injective_on_nonterminating: A = {x ∈ [0,1] : x has non-terminating binary expansion}, - then g is injective on A (unique binary decimal maps to unique ternary decimal) -/ + left + rw [CantorSet] + simp only [Set.mem_iInter] + intro n + let a : Fin n → ({0, 2} : Set ℕ) := fun i => ⟨d i.val, hd i.val⟩ + rw [CantorInterval] + simp only [Set.mem_iUnion] + use a + simp only [BoundedInterval.set_Icc, Set.mem_Icc] + have h_split : y = ∑ j ∈ Finset.range n, (d j : ℝ) * (1/3:ℝ)^(j + 1) + + ∑' j, (d (n + j) : ℝ) * (1/3:ℝ)^(n + j + 1) := by + rw [hy, ← Summable.sum_add_tsum_nat_add n hsum] + congr 1 + apply tsum_congr + intro j + rw [add_comm j n] + have h_partial : ∑ j ∈ Finset.range n, (d j : ℝ) * (1/3:ℝ)^(j + 1) = + ∑ i : Fin n, (a i : ℝ) / (3:ℝ)^(i.val + 1) := by + rw [Finset.sum_fin_eq_sum_range] + apply Finset.sum_congr rfl + intro j hj + simp only [Finset.mem_range] at hj + rw [dif_pos hj] + simp only [a] + field_simp + have h_tail_nonneg : 0 ≤ ∑' j, (d (n + j) : ℝ) * (1/3:ℝ)^(n + j + 1) := by + apply tsum_nonneg; intro j; positivity + have h_tail_bound : ∑' j, (d (n + j) : ℝ) * (1/3:ℝ)^(n + j + 1) ≤ (1/3:ℝ)^n := by + calc ∑' j, (d (n + j) : ℝ) * (1/3:ℝ)^(n + j + 1) + ≤ ∑' j, (2:ℝ) * (1/3:ℝ)^(n + j + 1) := by + apply Summable.tsum_le_tsum + · intro j + have hdj := hd (n + j) + simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hdj + rcases hdj with hdj0 | hdj2 + · simp only [hdj0, Nat.cast_zero, zero_mul]; positivity + · simp only [hdj2, Nat.cast_ofNat]; exact le_refl _ + · exact hsum.comp_injective (fun _ _ h => by omega) + · have h : Summable (fun j : ℕ => (1/3:ℝ)^j) := + summable_geometric_of_lt_one (by norm_num) (by norm_num) + exact (h.mul_left 2).comp_injective (fun _ _ h => by omega) + _ = (1/3:ℝ)^n := by + have h1 := tsum_geometric_of_lt_one (r := (1/3:ℝ)) (by norm_num) (by norm_num) + calc ∑' j, (2:ℝ) * (1/3:ℝ)^(n + j + 1) + = ∑' j, (2:ℝ) * ((1/3:ℝ)^(n + 1) * (1/3:ℝ)^j) := by + congr 1; ext j; rw [← pow_add]; ring_nf + _ = (2:ℝ) * (1/3:ℝ)^(n + 1) * ∑' j, (1/3:ℝ)^j := by + rw [← tsum_mul_left]; congr 1; ext j; ring + _ = (2:ℝ) * (1/3:ℝ)^(n + 1) * (1 - 1/3)⁻¹ := by rw [h1] + _ = (1/3:ℝ)^n := by field_simp; ring + rw [h_split, h_partial] + have h_one_third_pow : (1/3:ℝ)^n = 1 / 3^n := by field_simp + constructor + · linarith + · rw [← h_one_third_pow] + exact add_le_add_left h_tail_bound _ + +/-- Existence of a binary-to-ternary function: g(x) = ∑ 2bⱼ 3^{-j}. -/ lemma binaryToTernary_exists : ∃ g : ℝ → ℝ, BinaryToTernaryProperties g := by - -- Use the standalone binaryToTernaryFn use binaryToTernaryFn exact { - -- nonneg: g(x) ≥ 0 nonneg := by intro x simp only [binaryToTernaryFn] split_ifs with h · apply tsum_nonneg; intro j; positivity · rfl - -- bounded: g(x) ≤ 1 bounded := by intro x simp only [binaryToTernaryFn] @@ -2231,19 +2528,15 @@ lemma binaryToTernary_exists : ∃ g : ℝ → ℝ, BinaryToTernaryProperties g Summable.tsum_le_tsum h_bound (binaryToTernary_summable x) h_summable2 _ = 1 := tsum_two_thirds_geometric · norm_num - -- zero_outside: g(x) = 0 for x ∉ [0,1] zero_outside := by intro x hx simp only [binaryToTernaryFn, if_neg hx] - -- zero_at_zero: g(0) = 0 zero_at_zero := by simp only [binaryToTernaryFn] have h0 : (0:ℝ) ∈ Set.Icc 0 1 := ⟨le_refl 0, by norm_num⟩ rw [if_pos h0] simp only [binaryDigit_zero, Nat.cast_zero, mul_zero, zero_mul, tsum_zero] - -- zero_set_countable: {g = 0} ∩ [0,1] is countable zero_set_countable := by - -- g(x) = 0 iff all binary digits are 0 iff x = 0 apply Set.Countable.mono _ (Set.countable_singleton 0) intro x hx simp only [Set.mem_inter_iff, Set.mem_setOf_eq, Set.mem_singleton_iff] at hx ⊢ @@ -2254,7 +2547,6 @@ lemma binaryToTernary_exists : ∃ g : ℝ → ℝ, BinaryToTernaryProperties g rcases eq_or_lt_of_le hx_in.1 with rfl | hpos · exact absurd rfl hx_ne · exact hpos - -- For x ∈ (0,1], at least one binary digit is 1 have h_exists_one : ∃ j, binaryDigit x (j + 1) = 1 := by by_cases hx1 : x = 1 · exact ⟨0, by rw [hx1]; exact binaryDigit_one 1⟩ @@ -2267,23 +2559,73 @@ lemma binaryToTernary_exists : ∃ g : ℝ → ℝ, BinaryToTernaryProperties g have h_sum_pos : 0 < ∑' k : ℕ, (2 * binaryDigit x (k + 1) : ℝ) * (1/3:ℝ)^(k + 1) := (binaryToTernary_summable x).tsum_pos h_nonneg j h_term_pos linarith - -- monotone_on: g is monotone on [0,1] monotone_on := by intro x hx y hy hxy - simp only [binaryToTernaryFn, if_pos hx, if_pos hy] by_cases hxy' : x = y · simp [hxy'] - · -- x < y strictly, use helper lemma + · have hxy_strict : x < y := lt_of_le_of_ne hxy hxy' - have := binaryToTernary_lt_of_digit_lt hx hy - -- Need binaryDigit_first_diff to get k, then apply the helper - sorry - -- image_in_cantor: g([0,1]) ⊆ CantorSet ∪ {0} + have hx_lt_one : x < 1 := lt_of_lt_of_le hxy_strict hy.2 + have hx_Ico : x ∈ Set.Ico (0:ℝ) 1 := ⟨hx.1, hx_lt_one⟩ + by_cases hy1 : y = 1 + · + subst hy1 + have h_exists_k : ∃ k, binaryDigit x (k + 1) = 0 := by + by_contra h_all_one + push_neg at h_all_one + have h_all_eq_one : ∀ j, binaryDigit x (j + 1) = 1 := by + intro j + have h := binaryDigit_le_one x (j + 1) + have hne := h_all_one j + omega + by_cases hx_dyadic : x ∈ DyadicRationals + · simp only [DyadicRationals, Set.mem_setOf_eq] at hx_dyadic + obtain ⟨k, n, hx_eq, _⟩ := hx_dyadic + have h_zero_after : binaryDigit x (n + 1) = 0 := by + simp only [binaryDigit, if_pos hx_Ico] + rw [hx_eq] + have h_calc : (2:ℝ)^(n + 1) * (k / (2:ℝ)^n) = 2 * k := by field_simp; ring + rw [h_calc] + have : (2 * k : ℝ) = ((2 * k : ℕ) : ℝ) := by simp + rw [this, Nat.floor_natCast, Nat.mul_mod_right] + exact h_all_one n h_zero_after + · have hx_eq_sum := non_dyadic_eq_binary_sum hx_Ico hx_dyadic + exfalso + have h_sum_one : ∑' j : ℕ, (binaryDigit x (j + 1) : ℝ) * (1/2:ℝ)^(j + 1) = 1 := by + have h_digit : ∀ j, (binaryDigit x (j + 1) : ℝ) = 1 := by + intro j; rw [h_all_eq_one j]; norm_num + simp_rw [h_digit] + have h := tsum_geometric_of_lt_one (r := (1:ℝ)/2) (by norm_num) (by norm_num) + calc ∑' j, (1:ℝ) * (1/2)^(j + 1) = ∑' j, (1/2:ℝ)^(j + 1) := by simp + _ = (1/2) * ∑' j, (1/2:ℝ)^j := by + rw [← tsum_mul_left]; congr 1; ext j; ring + _ = (1/2) * (1 - 1/2)⁻¹ := by rw [h] + _ = 1 := by norm_num + rw [hx_eq_sum, h_sum_one] at hx_lt_one + linarith + let k := Nat.find h_exists_k + have hk_zero : binaryDigit x (k + 1) = 0 := Nat.find_spec h_exists_k + have hk_first : ∀ j < k, binaryDigit x (j + 1) ≠ 0 := by + intro j hj + exact Nat.find_min h_exists_k hj + have hk_lt : binaryDigit x (k + 1) < binaryDigit 1 (k + 1) := by + rw [hk_zero, binaryDigit_one]; norm_num + have hk_eq : ∀ j < k, binaryDigit x (j + 1) = binaryDigit 1 (j + 1) := by + intro j hj + rw [binaryDigit_one] + have h := binaryDigit_le_one x (j + 1) + have hne := hk_first j hj + omega + exact le_of_lt (binaryToTernary_lt_of_digit_lt hx ⟨zero_le_one, le_refl 1⟩ k hk_lt hk_eq) + · + have hy_lt_one : y < 1 := lt_of_le_of_ne hy.2 hy1 + have hy_Ico : y ∈ Set.Ico (0:ℝ) 1 := ⟨hy.1, hy_lt_one⟩ + obtain ⟨k, hk_lt, hk_eq⟩ := binaryDigit_first_diff hx_Ico hy_Ico hxy_strict + exact le_of_lt (binaryToTernary_lt_of_digit_lt hx hy k hk_lt hk_eq) image_in_cantor := by intro y hy obtain ⟨x, hx, rfl⟩ := hy simp only [binaryToTernaryFn, if_pos hx] - -- Use the helper lemma mem_CantorSet_of_ternary_02 let d : ℕ → ℕ := fun j => 2 * binaryDigit x (j + 1) have hd : ∀ j, d j ∈ ({0, 2} : Set ℕ) := by intro j @@ -2298,22 +2640,17 @@ lemma binaryToTernary_exists : ∃ g : ℝ → ℝ, BinaryToTernaryProperties g congr 1; funext j; simp only [d, Nat.cast_mul, Nat.cast_ofNat] rw [hy_eq] exact mem_CantorSet_of_ternary_02 d hd hsum rfl - -- injective_on_nonterminating injective_on_nonterminating := by - -- Use the DyadicRationals definition let A := Set.Icc (0:ℝ) 1 \ DyadicRationals use A - refine ⟨Set.diff_subset, ?_, ?_⟩ - -- A is co-countable in [0,1] + refine ⟨Set.diff_subset, ?_, ?_, ?_⟩ · have h_sdiff : Set.Icc (0:ℝ) 1 \ A = DyadicRationals ∩ Set.Icc 0 1 := by simp only [A, Set.diff_diff_right, Set.diff_self, Set.empty_union, Set.inter_comm] rw [h_sdiff] exact DyadicRationals.countable.mono Set.inter_subset_left - -- g is injective on A · intro x₁ hx₁ x₂ hx₂ heq simp only [A, Set.mem_diff] at hx₁ hx₂ simp only [binaryToTernaryFn, if_pos hx₁.1, if_pos hx₂.1] at heq - -- Use ternary_02_expansion_unique to get equal binary digits let d₁ : ℕ → ℕ := fun j => 2 * binaryDigit x₁ (j + 1) let d₂ : ℕ → ℕ := fun j => 2 * binaryDigit x₂ (j + 1) have hd₁ : ∀ j, d₁ j ∈ ({0, 2} : Set ℕ) := by @@ -2331,99 +2668,115 @@ lemma binaryToTernary_exists : ∃ g : ℝ → ℝ, BinaryToTernaryProperties g convert binaryToTernary_summable x₂ using 1 funext j; simp only [d₂, Nat.cast_mul, Nat.cast_ofNat] have hdigits_eq := ternary_02_expansion_unique hd₁ hd₂ hsum₁ hsum₂ heq' - -- From d₁ j = d₂ j, get binaryDigit x₁ (j+1) = binaryDigit x₂ (j+1) have hbinary_eq : ∀ j, binaryDigit x₁ (j + 1) = binaryDigit x₂ (j + 1) := by intro j have := hdigits_eq j simp only [d₁, d₂] at this omega - -- Now use eq_of_binaryDigit_eq_of_non_dyadic (needs x ∈ Ico, handle x = 1 separately) - sorry + have h1_dyadic : (1:ℝ) ∈ DyadicRationals := ⟨1, 0, by norm_num, by norm_num⟩ + have hx₁_ne_1 : x₁ ≠ 1 := fun h => hx₁.2 (h ▸ h1_dyadic) + have hx₂_ne_1 : x₂ ≠ 1 := fun h => hx₂.2 (h ▸ h1_dyadic) + have hx₁_Ico : x₁ ∈ Set.Ico (0:ℝ) 1 := ⟨hx₁.1.1, lt_of_le_of_ne hx₁.1.2 hx₁_ne_1⟩ + have hx₂_Ico : x₂ ∈ Set.Ico (0:ℝ) 1 := ⟨hx₂.1.1, lt_of_le_of_ne hx₂.1.2 hx₂_ne_1⟩ + apply eq_of_binaryDigit_eq_of_non_dyadic hx₁_Ico hx₂_Ico hx₁.2 hx₂.2 + intro j + rcases j with _ | j + · + simp only [binaryDigit, if_pos hx₁_Ico, if_pos hx₂_Ico, pow_zero, one_mul] + have h1 : ⌊x₁⌋₊ = 0 := Nat.floor_eq_zero.mpr hx₁_Ico.2 + have h2 : ⌊x₂⌋₊ = 0 := Nat.floor_eq_zero.mpr hx₂_Ico.2 + simp [h1, h2] + · exact hbinary_eq j + · ext x + simp only [A, Set.mem_inter_iff, Set.mem_diff, Set.mem_empty_iff_false, iff_false, not_and] + intro ⟨_, hx_not_dyadic⟩ hx_dyadic + exact hx_not_dyadic hx_dyadic } -/-- The binary-to-ternary conversion function on [0,1]: - Given x ∈ [0,1] with non-terminating binary expansion x = ∑ bⱼ 2^{-j} (bⱼ ∈ {0,1}), - define f(x) := ∑ 2bⱼ 3^{-j} (which lies in the Cantor set C). - For terminating binary decimals or x ∉ [0,1], set f(x) := 0. - - This function is bijective from the set A of non-terminating binary decimals - in [0,1] onto the Cantor set C. -/ +/-- Binary-to-ternary function: g(x) = ∑ 2·bⱼ(x)·3^{-j}, monotone on [0,1], g([0,1]) ⊆ C ∪ {0}. -/ noncomputable def binaryToTernary : ℝ → ℝ := Classical.choose binaryToTernary_exists lemma binaryToTernary_props : BinaryToTernaryProperties binaryToTernary := Classical.choose_spec binaryToTernary_exists -/-- The binary-to-ternary function lifted to EuclideanSpace' 1 and extended to EReal -/ -noncomputable def f : EuclideanSpace' 1 → EReal := +/-- binaryToTernary x = 0 iff x = 0 for x ∈ [0,1]. -/ +lemma binaryToTernary_eq_zero_iff {x : ℝ} (hx : x ∈ Set.Icc (0:ℝ) 1) : + binaryToTernary x = 0 ↔ x = 0 := by + constructor + · intro h + by_contra hx_ne + have hx_pos : 0 < x := lt_of_le_of_ne hx.1 (Ne.symm hx_ne) + have h0_in : (0:ℝ) ∈ Set.Icc 0 1 := ⟨le_refl 0, by norm_num⟩ + have h_mono := binaryToTernary_props.monotone_on h0_in hx (le_of_lt hx_pos) + rw [binaryToTernary_props.zero_at_zero] at h_mono + have h_zero_set : Set.Icc (0:ℝ) x ⊆ Set.Icc 0 1 ∩ {y | binaryToTernary y = 0} := by + intro y hy + constructor + · exact ⟨hy.1, le_trans hy.2 hx.2⟩ + · simp only [Set.mem_setOf_eq] + have h0y : (0:ℝ) ∈ Set.Icc 0 1 := ⟨le_refl 0, by norm_num⟩ + have hy_in : y ∈ Set.Icc 0 1 := ⟨hy.1, le_trans hy.2 hx.2⟩ + have h_mono1 := binaryToTernary_props.monotone_on h0y hy_in hy.1 + have h_mono2 := binaryToTernary_props.monotone_on hy_in hx hy.2 + rw [binaryToTernary_props.zero_at_zero] at h_mono1 + rw [h] at h_mono2 + linarith [binaryToTernary_props.nonneg y] + have h_uncountable : ¬ (Set.Icc (0:ℝ) x).Countable := by + have hx_pos : 0 < x := lt_of_le_of_ne hx.1 (fun h => hx_ne h.symm) + have h_card := Cardinal.mk_Icc_real hx_pos + intro hc + have := hc.le_aleph0 + rw [h_card] at this + exact Cardinal.aleph0_lt_continuum.not_ge this + exact h_uncountable (Set.Countable.mono h_zero_set binaryToTernary_props.zero_set_countable) + · intro h + rw [h] + exact binaryToTernary_props.zero_at_zero + +/-- binaryToTernary lifted to EuclideanSpace' 1 → EReal (called f in informal proof). -/ +noncomputable def f_lifted : EuclideanSpace' 1 → EReal := fun x => Real.toEReal (max 0 (binaryToTernary (EuclideanSpace'.equiv_Real x))) -lemma f_unsigned : Unsigned f := by +lemma f_lifted_unsigned : Unsigned f_lifted := by intro x - simp only [f, ge_iff_le] + simp only [f_lifted, ge_iff_le] rw [EReal.coe_nonneg] exact le_max_left 0 _ -/-- The function f is measurable. - - **Proof sketch**: By Lemma 1.3.9(viii), f is unsigned measurable iff for every λ ∈ [0,+∞), - the set {x : f(x) ≤ λ} is Lebesgue measurable. - - Note that f takes values in [0,1] (since binaryToTernary maps into Cantor set ∪ {0} ⊆ [0,1]). - - **Case λ ≥ 1**: Since f(x) ≤ 1 ≤ λ for all x, we have {x : f(x) ≤ λ} = ℝ, which is measurable. - - **Case 0 ≤ λ < 1**: - - For x ∉ [0,1]: f(x) = 0 ≤ λ, so (-∞, 0) ∪ (1, +∞) ⊆ {f ≤ λ}. - - For x ∈ [0,1]: since f is monotone on [0,1], {x ∈ [0,1] : f(x) ≤ λ} is an interval [0, a] - for some a ∈ [0,1]. - - Thus {x : f(x) ≤ λ} = (-∞, a] ∪ (1, +∞), which is measurable. -/ --- Helper: f is bounded above by 1 -lemma f_le_one (x : EuclideanSpace' 1) : f x ≤ 1 := by - simp only [f] +lemma f_lifted_le_one (x : EuclideanSpace' 1) : f_lifted x ≤ 1 := by + simp only [f_lifted] have hg := binaryToTernary_props.bounded (EuclideanSpace'.equiv_Real x) have h_max_le : max 0 (binaryToTernary (EuclideanSpace'.equiv_Real x)) ≤ 1 := max_le (by norm_num) hg exact EReal.coe_le_coe_iff.mpr h_max_le --- Helper: f(x) = 0 for x outside [0,1] -lemma f_zero_outside (x : EuclideanSpace' 1) (hx : EuclideanSpace'.equiv_Real x ∉ Set.Icc 0 1) : - f x = 0 := by - simp only [f] +lemma f_lifted_zero_outside (x : EuclideanSpace' 1) (hx : EuclideanSpace'.equiv_Real x ∉ Set.Icc 0 1) : + f_lifted x = 0 := by + simp only [f_lifted] have hg := binaryToTernary_props.zero_outside (EuclideanSpace'.equiv_Real x) hx rw [hg] simp --- Helper: f(x) = 0 when equiv_Real x = 0 -lemma f_zero_at_zero (x : EuclideanSpace' 1) (hx : EuclideanSpace'.equiv_Real x = 0) : - f x = 0 := by - simp only [f] +lemma f_lifted_zero_at_zero (x : EuclideanSpace' 1) (hx : EuclideanSpace'.equiv_Real x = 0) : + f_lifted x = 0 := by + simp only [f_lifted] have hg := binaryToTernary_props.zero_at_zero rw [hx, hg] simp --- Helper: The zero set of f within [0,1] is countable (dyadic rationals = terminating binaries) lemma f_zero_set_in_interval_countable : (Set.Icc (0:ℝ) 1 ∩ {x | binaryToTernary x = 0}).Countable := binaryToTernary_props.zero_set_countable --- Helper: The zero set {f = 0} is measurable --- {f = 0} = (ℝ \ [0,1]) ∪ {dyadic rationals in [0,1]} --- This is the union of an open set and a countable set, hence measurable -lemma f_zero_set_measurable : LebesgueMeasurable {x : EuclideanSpace' 1 | f x = 0} := by - -- {f = 0} consists of: - -- 1. All x with equiv_Real(x) ∉ [0,1] (since f(x) = 0 outside [0,1]) - -- 2. All x with equiv_Real(x) ∈ [0,1] and binaryToTernary(equiv_Real(x)) = 0 (countable) - -- The first part is the preimage of an open set under the continuous equiv_Real - -- The second part is the preimage of a countable set - -- Their union is measurable - have h_decomp : {x : EuclideanSpace' 1 | f x = 0} = +lemma f_lifted_zero_set_measurable : LebesgueMeasurable {x : EuclideanSpace' 1 | f_lifted x = 0} := by + have h_decomp : {x : EuclideanSpace' 1 | f_lifted x = 0} = (Real.equiv_EuclideanSpace' '' (Set.Icc 0 1)ᶜ) ∪ (Real.equiv_EuclideanSpace' '' (Set.Icc 0 1 ∩ {x | binaryToTernary x = 0})) := by ext x simp only [Set.mem_setOf_eq, Set.mem_union, Set.mem_image] constructor · intro hfx - simp only [f] at hfx + simp only [f_lifted] at hfx have hmax : max 0 (binaryToTernary (EuclideanSpace'.equiv_Real x)) = 0 := by rw [EReal.coe_eq_zero] at hfx exact hfx @@ -2447,29 +2800,18 @@ lemma f_zero_set_measurable : LebesgueMeasurable {x : EuclideanSpace' 1 | f x = exact ⟨h_in, EuclideanSpace'.equiv_Real.symm_apply_apply x⟩ · intro h rcases h with ⟨r, hr, hrx⟩ | ⟨r, ⟨hr_in, hr_zero⟩, hrx⟩ - · -- r ∉ [0,1] - simp only [f] + · simp only [f_lifted] have hx_eq : EuclideanSpace'.equiv_Real x = r := by - rw [← hrx] - exact EuclideanSpace'.equiv_Real.apply_symm_apply r - rw [hx_eq] - have hg := binaryToTernary_props.zero_outside r hr - rw [hg] - simp - · -- r ∈ [0,1] and binaryToTernary r = 0 - simp only [f] + rw [← hrx]; exact EuclideanSpace'.equiv_Real.apply_symm_apply r + rw [hx_eq, binaryToTernary_props.zero_outside r hr]; simp + · simp only [f_lifted] have hx_eq : EuclideanSpace'.equiv_Real x = r := by - rw [← hrx] - exact EuclideanSpace'.equiv_Real.apply_symm_apply r - rw [hx_eq, hr_zero] - simp + rw [← hrx]; exact EuclideanSpace'.equiv_Real.apply_symm_apply r + rw [hx_eq, hr_zero]; simp rw [h_decomp] apply LebesgueMeasurable.union - · -- (ℝ \ [0,1]) lifted to EuclideanSpace' 1 is measurable (open set) - apply IsOpen.measurable + · apply IsOpen.measurable have h_open : IsOpen (Set.Icc (0:ℝ) 1)ᶜ := isOpen_compl_iff.mpr isClosed_Icc - -- Real.equiv_EuclideanSpace' is a homeomorphism, so it maps open sets to open sets - -- Construct the homeomorphism have hf_cont : Continuous (fun x : ℝ => Real.equiv_EuclideanSpace' x) := by have h : Continuous fun x : ℝ => (fun _ : Fin 1 => x) := by refine continuous_pi ?_ @@ -2484,37 +2826,20 @@ lemma f_zero_set_measurable : LebesgueMeasurable {x : EuclideanSpace' 1 | f x = continuous_toFun := hf_cont continuous_invFun := hg_cont } exact e.isOpenMap (Set.Icc 0 1)ᶜ h_open - · -- Countable set is measurable (countable subset of EuclideanSpace' 1 is null) - -- A countable set in ℝ^d has measure zero (each point has measure 0) - -- The image of a countable set under a bijection is countable - apply IsNull.measurable - -- Countable sets in Euclidean space are null sets (Lebesgue_outer_measure = 0) + · apply IsNull.measurable have h_countable : (Real.equiv_EuclideanSpace' '' (Set.Icc 0 1 ∩ {x | binaryToTernary x = 0})).Countable := by - apply Set.Countable.image - exact f_zero_set_in_interval_countable + apply Set.Countable.image; exact f_zero_set_in_interval_countable exact Countable.Lebesgue_measure Nat.one_pos h_countable --- Helper: Sublevel sets of monotone functions on [0,1] extended by 0 outside are measurable --- This is the key lemma for f_measurable +/-- Sublevel sets of f_lifted are measurable (key lemma for f_lifted_measurable). -/ lemma sublevel_set_measurable (t : EReal) (ht_pos : 0 < t) (ht_lt_one : t < 1) : - LebesgueMeasurable {x : EuclideanSpace' 1 | f x ≤ t} := by - -- The sublevel set {x | f x ≤ t} consists of: - -- 1. All x with equiv_Real(x) ∉ [0,1] (since f(x) = 0 < t there) - -- 2. All x with equiv_Real(x) ∈ [0,1] and f(x) ≤ t (an interval by monotonicity) - -- Together this forms a measurable set - -- Split the set into parts based on where x lies relative to [0,1] + LebesgueMeasurable {x : EuclideanSpace' 1 | f_lifted x ≤ t} := by have h_outside_zero : ∀ x : EuclideanSpace' 1, EuclideanSpace'.equiv_Real x ∉ Set.Icc 0 1 → - f x ≤ t := by - intro x hx - rw [f_zero_outside x hx] - exact le_of_lt ht_pos - -- The sublevel set equals: - -- { x | equiv_Real x < 0 } ∪ { x | equiv_Real x > 1 } ∪ { x | equiv_Real x ∈ [0,1] ∧ f x ≤ t } - -- First two are open (preimages of open sets), third is where monotonicity applies - have h_decomp : {x : EuclideanSpace' 1 | f x ≤ t} = + f_lifted x ≤ t := fun x hx => by rw [f_lifted_zero_outside x hx]; exact le_of_lt ht_pos + have h_decomp : {x : EuclideanSpace' 1 | f_lifted x ≤ t} = (Real.equiv_EuclideanSpace' '' Set.Iio 0) ∪ (Real.equiv_EuclideanSpace' '' Set.Ioi 1) ∪ - {x : EuclideanSpace' 1 | EuclideanSpace'.equiv_Real x ∈ Set.Icc 0 1 ∧ f x ≤ t} := by + {x : EuclideanSpace' 1 | EuclideanSpace'.equiv_Real x ∈ Set.Icc 0 1 ∧ f_lifted x ≤ t} := by ext x simp only [Set.mem_setOf_eq, Set.mem_union, Set.mem_image] constructor @@ -2532,27 +2857,19 @@ lemma sublevel_set_measurable (t : EReal) (ht_pos : 0 < t) (ht_lt_one : t < 1) : exact ⟨⟨h_neg, h_big⟩, hfx⟩ · intro h rcases h with (⟨r, hr, hrx⟩ | ⟨r, hr, hrx⟩) | ⟨h_in, hfx⟩ - · -- r < 0, so x is outside [0,1] - apply h_outside_zero + · apply h_outside_zero rw [← hrx, EuclideanSpace'.equiv_Real.apply_symm_apply] - simp only [Set.mem_Icc, not_and, not_le] - intro h_ge_zero - simp only [Set.mem_Iio] at hr - linarith - · -- r > 1, so x is outside [0,1] - apply h_outside_zero + simp only [Set.mem_Icc, not_and, not_le, Set.mem_Iio] at hr ⊢ + intro; linarith + · apply h_outside_zero rw [← hrx, EuclideanSpace'.equiv_Real.apply_symm_apply] - simp only [Set.mem_Icc, not_and, not_le] - intro _ - simp only [Set.mem_Ioi] at hr - linarith + simp only [Set.mem_Icc, not_and, not_le, Set.mem_Ioi] at hr ⊢ + intro; linarith · exact hfx rw [h_decomp] apply LebesgueMeasurable.union apply LebesgueMeasurable.union - · -- { x | equiv_Real x < 0 } is open, hence measurable - apply IsOpen.measurable - -- Same homeomorphism argument as before + · apply IsOpen.measurable have hf_cont : Continuous (fun x : ℝ => Real.equiv_EuclideanSpace' x) := by have h : Continuous fun x : ℝ => (fun _ : Fin 1 => x) := by refine continuous_pi ?_ @@ -2567,8 +2884,7 @@ lemma sublevel_set_measurable (t : EReal) (ht_pos : 0 < t) (ht_lt_one : t < 1) : continuous_toFun := hf_cont continuous_invFun := hg_cont } exact e.isOpenMap (Set.Iio 0) isOpen_Iio - · -- { x | equiv_Real x > 1 } is open, hence measurable - apply IsOpen.measurable + · apply IsOpen.measurable have hf_cont : Continuous (fun x : ℝ => Real.equiv_EuclideanSpace' x) := by have h : Continuous fun x : ℝ => (fun _ : Fin 1 => x) := by refine continuous_pi ?_ @@ -2583,10 +2899,7 @@ lemma sublevel_set_measurable (t : EReal) (ht_pos : 0 < t) (ht_lt_one : t < 1) : continuous_toFun := hf_cont continuous_invFun := hg_cont } exact e.isOpenMap (Set.Ioi 1) isOpen_Ioi - · -- { x | equiv_Real x ∈ [0,1] ∧ f x ≤ t } is measurable by monotonicity - -- The key is that this is the intersection of [0,1] with a sublevel set of a monotone function - -- By convexity, this is an interval, hence closed/Borel, hence measurable - -- Extract the real value from t (since 0 < t < 1, it's a real number) + · -- Monotonicity case: {x ∈ [0,1] | f_lifted x ≤ t} is a convex set, hence measurable have ht_ne_top : t ≠ ⊤ := ne_of_lt (lt_of_lt_of_le ht_lt_one le_top) have ht_ne_bot : t ≠ ⊥ := ne_of_gt (lt_of_le_of_lt bot_le ht_pos) let t' := t.toReal @@ -2598,10 +2911,8 @@ lemma sublevel_set_measurable (t : EReal) (ht_pos : 0 < t) (ht_lt_one : t < 1) : have ht'_lt_one : t' < 1 := by have h : (t':EReal) < 1 := by rw [← ht_eq]; exact ht_lt_one exact EReal.coe_lt_coe_iff.mp h - -- Define the set in ℝ that we need to show is measurable let S : Set ℝ := {r ∈ Set.Icc (0:ℝ) 1 | binaryToTernary r ≤ t'} - -- The set in EuclideanSpace' 1 equals the image of S under the homeomorphism - have h_set_eq : {x : EuclideanSpace' 1 | EuclideanSpace'.equiv_Real x ∈ Set.Icc 0 1 ∧ f x ≤ ↑t'} = + have h_set_eq : {x : EuclideanSpace' 1 | EuclideanSpace'.equiv_Real x ∈ Set.Icc 0 1 ∧ f_lifted x ≤ ↑t'} = Real.equiv_EuclideanSpace' '' S := by ext x simp only [Set.mem_setOf_eq, Set.mem_image, S] @@ -2609,68 +2920,33 @@ lemma sublevel_set_measurable (t : EReal) (ht_pos : 0 < t) (ht_lt_one : t < 1) : · intro ⟨h_in, hfx⟩ use EuclideanSpace'.equiv_Real x refine ⟨⟨h_in, ?_⟩, EuclideanSpace'.equiv_Real.symm_apply_apply x⟩ - simp only [f] at hfx + simp only [f_lifted] at hfx have h_max : max 0 (binaryToTernary (EuclideanSpace'.equiv_Real x)) ≤ t' := by rw [EReal.coe_le_coe_iff] at hfx; exact hfx exact le_of_max_le_right h_max · intro ⟨r, ⟨hr_in, hr_le⟩, hrx⟩ constructor · rw [← hrx, EuclideanSpace'.equiv_Real.apply_symm_apply]; exact hr_in - · rw [← hrx]; simp only [f, EuclideanSpace'.equiv_Real.apply_symm_apply] + · rw [← hrx]; simp only [f_lifted, EuclideanSpace'.equiv_Real.apply_symm_apply] rw [EReal.coe_le_coe_iff] exact max_le (le_of_lt ht'_pos) hr_le rw [h_set_eq] - -- S is the intersection of [0,1] with a sublevel set of a monotone function - -- By MonotoneOn.convex_le, the sublevel set intersected with [0,1] is convex - -- Convex sets in ℝ are intervals (order-connected), hence Borel measurable - have h_convex : Convex ℝ S := by - have h_mono := binaryToTernary_props.monotone_on - exact h_mono.convex_le (convex_Icc 0 1) t' - -- S is bounded (subset of [0,1]) - have h_bounded : Bornology.IsBounded S := by - exact (Metric.isBounded_Icc 0 1).subset (fun x hx => hx.1) - -- The image of a bounded convex set under the homeomorphism is measurable - -- because bounded convex sets in ℝ are closed intervals or half-open intervals - -- For a convex subset of a closed interval [0,1], there are cases: - -- - Empty set (measurable) - -- - Singleton (measurable as closed) - -- - Interval of form [a,b], [a,b), (a,b], (a,b) for some a,b ∈ [0,1] - -- All these are Borel sets, hence Lebesgue measurable after lifting - -- Use the simpler approach: S is a Borel set (as intersection of closed + Borel) - -- The sublevel set {x | binaryToTernary x ≤ t'} is closed because binaryToTernary is - -- monotone on [0,1], hence has at most countably many discontinuities (none actually, - -- as it's constructed from converging series), so the sublevel set is closed - -- Actually, the easier argument: S ⊆ [0,1] and S is convex, so S is an interval - -- Convex subsets of ℝ are intervals by convex_iff_ordConnected + have h_convex : Convex ℝ S := binaryToTernary_props.monotone_on.convex_le (convex_Icc 0 1) t' + have h_bounded : Bornology.IsBounded S := (Metric.isBounded_Icc 0 1).subset (fun x hx => hx.1) have h_ordConnected : S.OrdConnected := Convex.ordConnected h_convex - -- An order-connected subset of [0,1] is an interval - -- Case: S is empty by_cases hS_empty : S = ∅ · rw [hS_empty]; simp only [Set.image_empty]; exact LebesgueMeasurable.empty - -- Case: S is nonempty - it's an interval with endpoints in [0,1] push_neg at hS_empty - -- S contains 0 because binaryToTernary 0 = 0 ≤ t' (since t' > 0) have h_zero_in_S : (0:ℝ) ∈ S := by - simp only [S, Set.mem_sep_iff, Set.mem_Icc] + simp only [S, Set.mem_Icc] constructor · exact ⟨le_refl 0, zero_le_one⟩ · rw [binaryToTernary_props.zero_at_zero]; exact le_of_lt ht'_pos - -- S is of the form [0, a] for some a (by order-connectedness + containing 0) - -- a = sup S, which exists and is in [0,1] have h_bdd_above : BddAbove S := ⟨1, fun x hx => hx.1.2⟩ let a := sSup S - have ha_mem : a ∈ Set.Icc (0:ℝ) 1 := by - constructor - · exact le_csSup_of_le h_bdd_above h_zero_in_S (le_refl 0) - · exact csSup_le (Set.nonempty_of_mem h_zero_in_S) (fun x hx => hx.1.2) - -- S = Set.Icc 0 a ∩ {x | binaryToTernary x ≤ t'} which is either [0,a] or [0,a) - -- The image of any interval under the homeomorphism is measurable - -- We'll show the image is closed (hence measurable) - -- Actually simpler: S is a subset of [0,1] that is order-connected and contains 0 - -- So S is an interval starting at 0, which is [0,a] or [0,a) for some a - -- The image under the homeomorphism is the same interval in EuclideanSpace' 1 - -- This is closed or Borel, hence measurable - -- Use: the image of a Borel set under a homeomorphism is Borel, hence measurable + have ha_mem : a ∈ Set.Icc (0:ℝ) 1 := ⟨ + le_csSup_of_le h_bdd_above h_zero_in_S (le_refl 0), + csSup_le (Set.nonempty_of_mem h_zero_in_S) (fun x hx => hx.1.2)⟩ have hf_cont : Continuous (fun x : ℝ => Real.equiv_EuclideanSpace' x) := by have h : Continuous fun x : ℝ => (fun _ : Fin 1 => x) := by refine continuous_pi ?_; intro _; exact continuous_id @@ -2683,32 +2959,8 @@ lemma sublevel_set_measurable (t : EReal) (ht_pos : 0 < t) (ht_lt_one : t < 1) : { toEquiv := Real.equiv_EuclideanSpace' continuous_toFun := hf_cont continuous_invFun := hg_cont } - -- S is closed: it's the intersection of [0,1] (closed) with {x | binaryToTernary x ≤ t'} - -- The set {x | binaryToTernary x ≤ t'} is closed because: - -- - binaryToTernary is continuous on [0,1] (follows from being monotone + bounded) - -- Actually, we don't have continuity directly. Instead use that S is a closed interval. - -- S = [0, a] where a = sSup S, and S is closed because: - -- For any sequence (x_n) in S converging to x, we need x ∈ S. - -- x_n ∈ [0,1] → x ∈ [0,1] (closed) - -- binaryToTernary x_n ≤ t' for all n - -- By monotonicity and sequential characterization, binaryToTernary x ≤ t' (if continuous) - -- Without continuity, we use that S = [0, a] or [0, a) which are both measurable - -- S is convex and order-connected, containing 0, bounded above by 1 - -- Therefore S = Set.Icc 0 a or S = Set.Ico 0 a for some a ∈ (0, 1] - -- Both are Borel measurable - -- The image under the homeomorphism of a Borel set is Borel, hence Lebesgue measurable - -- Use that S ⊆ [0,1], so its image ⊆ image of [0,1], which is closed hence measurable - -- S is convex and contains 0, so S is an interval [0, a] or [0, a) for some a = sup S - -- Both are measurable (closed or Borel) - -- The key: S ⊆ [0, a] where a = sSup S - have h_S_subset_Icc : S ⊆ Set.Icc 0 a := by - intro x hx - constructor - · -- x ≥ 0 since x ∈ S ⊆ [0,1] - exact hx.1.1 - · -- x ≤ sSup S by definition of sSup - exact le_csSup h_bdd_above hx - -- The image of [0, a] under the homeomorphism is the closed interval, hence measurable + -- S is either [0, a] or [0, a) where a = sSup S; both are measurable + have h_S_subset_Icc : S ⊆ Set.Icc 0 a := fun x hx => ⟨hx.1.1, le_csSup h_bdd_above hx⟩ have h_image_Icc : Real.equiv_EuclideanSpace' '' Set.Icc 0 a = {x : EuclideanSpace' 1 | EuclideanSpace'.equiv_Real x ∈ Set.Icc 0 a} := by ext x; simp only [Set.mem_image, Set.mem_setOf_eq] @@ -2717,55 +2969,31 @@ lemma sublevel_set_measurable (t : EReal) (ht_pos : 0 < t) (ht_lt_one : t < 1) : rw [← hrx, EuclideanSpace'.equiv_Real.apply_symm_apply]; exact hr · intro hx exact ⟨EuclideanSpace'.equiv_Real x, hx, EuclideanSpace'.equiv_Real.symm_apply_apply x⟩ - -- Image of [0, a] is closed, hence measurable have h_meas_Icc : LebesgueMeasurable (Real.equiv_EuclideanSpace' '' Set.Icc 0 a) := by - apply IsClosed.measurable - rw [h_image_Icc] + apply IsClosed.measurable; rw [h_image_Icc] exact IsClosed.preimage hg_cont isClosed_Icc - -- Image of S ⊆ Image of [0, a], and we need: image of S is measurable - -- Since subsets of measurable sets aren't automatically measurable, use a different approach: - -- S is an order-connected set containing 0 and bounded above, so S = [0, inf complement] ∩ [0,1] - -- Actually, S is either [0, a] if a ∈ S, or [0, a) if a ∉ S - -- Either way, S is a Borel set in ℝ - -- The image of a Borel set under a homeomorphism is Borel, hence Lebesgue measurable - -- For simplicity, show S is measurable as a union or intersection of measurable sets - -- S = [0, 1] ∩ {x | binaryToTernary x ≤ t'} - -- We can write this as: - -- The image of S = image of [0, a] or image of [0, a) depending on whether a ∈ S by_cases ha_in_S : a ∈ S - · -- S = [0, a] (closed interval) + · -- S = [0, a] have h_S_eq : S = Set.Icc 0 a := by ext x constructor · intro hx; exact h_S_subset_Icc hx · intro hx - have hx_ge_zero : 0 ≤ x := hx.1 - have hx_le_a : x ≤ a := hx.2 - -- By order-connectedness of S, since 0 ∈ S, a ∈ S, and 0 ≤ x ≤ a, we have x ∈ S - exact h_ordConnected.out h_zero_in_S ha_in_S ⟨hx_ge_zero, hx_le_a⟩ - rw [h_S_eq] - exact h_meas_Icc - · -- S = [0, a) (half-open interval) + exact h_ordConnected.out h_zero_in_S ha_in_S ⟨hx.1, hx.2⟩ + rw [h_S_eq]; exact h_meas_Icc + · -- S = [0, a) have h_S_eq : S = Set.Ico 0 a := by ext x constructor · intro hx refine ⟨hx.1.1, ?_⟩ - -- x < a because if x = a, then x ∈ S would imply a ∈ S, contradiction rcases lt_or_eq_of_le (le_csSup h_bdd_above hx) with hlt | heq · exact hlt · exfalso; rw [heq] at hx; exact ha_in_S hx · intro hx - have hx_ge_zero : 0 ≤ x := hx.1 - have hx_lt_a : x < a := hx.2 - -- Show x ∈ S using order-connectedness - -- Since x < a = sSup S, there exists y ∈ S with x < y - have ⟨y, hy_in_S, hx_lt_y⟩ := exists_lt_of_lt_csSup (Set.nonempty_of_mem h_zero_in_S) hx_lt_a - exact h_ordConnected.out h_zero_in_S hy_in_S ⟨hx_ge_zero, le_of_lt hx_lt_y⟩ + have ⟨y, hy_in_S, hx_lt_y⟩ := exists_lt_of_lt_csSup (Set.nonempty_of_mem h_zero_in_S) hx.2 + exact h_ordConnected.out h_zero_in_S hy_in_S ⟨hx.1, le_of_lt hx_lt_y⟩ rw [h_S_eq] - -- Image of [0, a) is measurable - -- [0, a) = [0, 1] ∩ [0, a) = [0, min(1, a)) but since a ≤ 1, this is [0, a) - -- [0, a) is Borel (half-open interval) have h_image_Ico : Real.equiv_EuclideanSpace' '' Set.Ico 0 a = {x : EuclideanSpace' 1 | EuclideanSpace'.equiv_Real x ∈ Set.Ico 0 a} := by ext x; simp only [Set.mem_image, Set.mem_setOf_eq] @@ -2775,124 +3003,77 @@ lemma sublevel_set_measurable (t : EReal) (ht_pos : 0 < t) (ht_lt_one : t < 1) : · intro hx exact ⟨EuclideanSpace'.equiv_Real x, hx, EuclideanSpace'.equiv_Real.symm_apply_apply x⟩ -- [0, a) = [0, a] \ {a} - -- Image([0, a) ) = Image([0, a]) \ Image({a}) because the map is injective - -- Both Image([0, a]) and Image({a}) are measurable, so their difference is too have h_diff : Set.Ico 0 a = Set.Icc 0 a \ {a} := by ext x; simp only [Set.mem_Ico, Set.mem_diff, Set.mem_Icc, Set.mem_singleton_iff] constructor · intro ⟨h1, h2⟩; exact ⟨⟨h1, le_of_lt h2⟩, ne_of_lt h2⟩ · intro ⟨⟨h1, h2⟩, h3⟩; exact ⟨h1, lt_of_le_of_ne h2 h3⟩ - rw [h_diff, Set.image_diff Real.equiv_EuclideanSpace'.injective] - -- A \ B = A ∩ Bᶜ, so use intersection - rw [Set.diff_eq] + rw [h_diff, Set.image_diff Real.equiv_EuclideanSpace'.injective, Set.diff_eq] apply LebesgueMeasurable.inter h_meas_Icc apply LebesgueMeasurable.complement - -- {Real.equiv_EuclideanSpace' a} is a singleton, hence null, hence measurable apply IsNull.measurable - have h_singleton_count : (Real.equiv_EuclideanSpace' '' {a}).Countable := by - apply Set.Countable.image; exact Set.countable_singleton a - exact Countable.Lebesgue_measure Nat.one_pos h_singleton_count - -lemma f_measurable : UnsignedMeasurable f := by - -- Apply Lemma 1.3.9(viii): f is measurable iff ∀ t, {x : f(x) ≤ t} is measurable - have h_tfae := UnsignedMeasurable.TFAE f_unsigned - -- Index 0 is UnsignedMeasurable f, index 7 is ∀ t, LebesgueMeasurable {x | f x ≤ t} - have h_iff : UnsignedMeasurable f ↔ (∀ t, LebesgueMeasurable {x | f x ≤ t}) := - List.TFAE.out h_tfae 0 7 + exact Countable.Lebesgue_measure Nat.one_pos (Set.countable_singleton a |>.image _) + +lemma f_lifted_measurable : UnsignedMeasurable f_lifted := by + -- Apply Lemma 1.3.9(viii): f is measurable iff ∀ t, {x | f(x) ≤ t} is measurable + have h_iff : UnsignedMeasurable f_lifted ↔ (∀ t, LebesgueMeasurable {x | f_lifted x ≤ t}) := + (UnsignedMeasurable.TFAE f_lifted_unsigned).out 0 7 apply h_iff.mpr - -- Now prove: ∀ t, LebesgueMeasurable {x | f x ≤ t} intro t - -- Case split on t rcases lt_trichotomy t 0 with ht_neg | ht_zero | ht_pos - · -- Case t < 0: {x | f x ≤ t} = ∅ (since f x ≥ 0 for all x) - have h_empty : {x | f x ≤ t} = ∅ := by + · have h_empty : {x | f_lifted x ≤ t} = ∅ := by ext x simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false, not_le] - exact lt_of_lt_of_le ht_neg (f_unsigned x) - rw [h_empty] - exact LebesgueMeasurable.empty - · -- Case t = 0: {x | f x ≤ 0} = {x | f x = 0} (since f x ≥ 0) - subst ht_zero - -- Since f ≥ 0, {f ≤ 0} = {f = 0} - have h_eq : {x | f x ≤ (0 : EReal)} = {x | f x = 0} := by + exact lt_of_lt_of_le ht_neg (f_lifted_unsigned x) + rw [h_empty]; exact LebesgueMeasurable.empty + · subst ht_zero + have h_eq : {x | f_lifted x ≤ (0 : EReal)} = {x | f_lifted x = 0} := by ext x simp only [Set.mem_setOf_eq] constructor - · intro hle - exact le_antisymm hle (f_unsigned x) - · intro heq - rw [heq] - rw [h_eq] - exact f_zero_set_measurable - · -- Case t > 0 - rcases le_or_gt 1 t with ht_ge_one | ht_lt_one - · -- Case t ≥ 1: {x | f x ≤ t} = univ (since f x ≤ 1 for all x) - have h_univ : {x | f x ≤ t} = Set.univ := by - ext x - simp only [Set.mem_setOf_eq, Set.mem_univ, iff_true] - exact le_trans (f_le_one x) ht_ge_one - rw [h_univ] - exact IsOpen.measurable isOpen_univ - · -- Case 0 < t < 1: Use the helper lemma - exact sublevel_set_measurable t ht_pos ht_lt_one - -/-- There exists a non-measurable subset F of [0,1] such that its image under - binaryToTernary lies in the Cantor set (hence is null, hence measurable). - This F comes from taking the Vitali set restricted to non-terminating binary decimals. - - **Construction**: - Let A = {x ∈ [0,1] : x has non-terminating binary expansion}. - Note that [0,1] \ A is countable (terminating binary = dyadic rationals). - - The Vitali set construction from Proposition 1.2.18 can be performed within A: - - Define equivalence relation on A: x ~ y iff x - y ∈ ℚ - - Use Axiom of Choice to select one representative from each equivalence class - - This gives a non-measurable F ⊆ A ⊆ [0,1] - - Since binaryToTernary maps A bijectively onto C (Cantor set), we have: - - binaryToTernary '' F ⊆ binaryToTernary '' A = C - - F is non-measurable - - The key insight is that the Vitali construction works within A because A has the same - "density" as [0,1] (co-countable), so the translation argument still works. -/ + · intro hle; exact le_antisymm hle (f_lifted_unsigned x) + · intro heq; rw [heq] + rw [h_eq]; exact f_lifted_zero_set_measurable + · rcases le_or_gt 1 t with ht_ge_one | ht_lt_one + · have h_univ : {x | f_lifted x ≤ t} = Set.univ := by + ext x; simp only [Set.mem_setOf_eq, Set.mem_univ, iff_true] + exact le_trans (f_lifted_le_one x) ht_ge_one + rw [h_univ]; exact IsOpen.measurable isOpen_univ + · exact sublevel_set_measurable t ht_pos ht_lt_one + +/-- Non-measurable F ⊆ [0,1] with binaryToTernary(F) ⊆ Cantor set (Vitali construction). -/ lemma exists_nonmeasurable_with_cantor_image : - ∃ F : Set ℝ, F ⊆ Set.Icc 0 1 ∧ + ∃ F : Set ℝ, ∃ A : Set ℝ, F ⊆ Set.Icc 0 1 ∧ ¬ LebesgueMeasurable (Real.equiv_EuclideanSpace' '' F) ∧ - binaryToTernary '' F ⊆ CantorSet := by - -- Get the set A on which binaryToTernary is injective - obtain ⟨A, hA_sub, hA_cocountable, hA_inj⟩ := binaryToTernary_props.injective_on_nonterminating - -- Define F := VitaliSet ∩ A + binaryToTernary '' F ⊆ CantorSet ∧ + F ⊆ A ∧ + A ⊆ Set.Icc 0 1 ∧ + (Set.Icc 0 1 \ A).Countable ∧ + Set.InjOn binaryToTernary A := by + obtain ⟨A, hA_sub, hA_cocountable, hA_inj, hA_disjoint⟩ := binaryToTernary_props.injective_on_nonterminating let F := VitaliSet ∩ A - use F - refine ⟨?hF_sub, ?hF_nonmeas, ?hF_image⟩ - case hF_sub => - -- F ⊆ [0,1] since VitaliSet ⊆ [0,1] - intro x hx - exact VitaliSet_subset_unit_interval hx.1 + use F, A + refine ⟨?hF_sub, ?hF_nonmeas, ?hF_image, ?hF_sub_A, hA_sub, hA_cocountable, hA_inj⟩ + case hF_sub => intro x hx; exact VitaliSet_subset_unit_interval hx.1 case hF_image => - -- binaryToTernary '' F ⊆ CantorSet - -- F ⊆ A ⊆ [0,1], so binaryToTernary '' F ⊆ binaryToTernary '' [0,1] ⊆ CantorSet ∪ {0} - -- For x ∈ A (non-terminating), binaryToTernary x ≠ 0, so image is in CantorSet intro y hy obtain ⟨x, hx, rfl⟩ := hy have hx_in_Icc : x ∈ Set.Icc (0:ℝ) 1 := hA_sub hx.2 have h_image := binaryToTernary_props.image_in_cantor ⟨x, hx_in_Icc, rfl⟩ - -- binaryToTernary x ∈ CantorSet ∪ {0}, but x ∈ A means binaryToTernary x ≠ 0 cases h_image with | inl h => exact h | inr h => - -- x ∈ A means x is not a dyadic rational, so binaryToTernary x ≠ 0 simp only [Set.mem_singleton_iff] at h - -- This contradicts that x ∈ A (non-terminating decimal) - sorry + exfalso + have h_x_eq_0 : x = 0 := binaryToTernary_eq_zero_iff hx_in_Icc |>.mp h + have h0_dyadic : (0:ℝ) ∈ DyadicRationals := ⟨0, 0, by norm_num, by norm_num⟩ + subst h_x_eq_0 + have h0_in_A : (0:ℝ) ∈ A := hx.2 + have h0_in_inter : (0:ℝ) ∈ A ∩ DyadicRationals := ⟨h0_in_A, h0_dyadic⟩ + rw [hA_disjoint] at h0_in_inter + exact h0_in_inter case hF_nonmeas => - -- F = VitaliSet ∩ A is non-measurable - -- Suppose for contradiction that F is measurable intro hF_meas - -- Then VitaliSet = F ∪ (VitaliSet \ A) - -- VitaliSet \ A ⊆ [0,1] \ A which is countable, hence null, hence measurable - -- So VitaliSet = F ∪ (VitaliSet \ A) would be measurable (union of two measurable sets) - -- But VitaliSet is non-measurable by LebesgueMeasurable.nonmeasurable have hV_decomp : VitaliSet = F ∪ (VitaliSet \ A) := by ext x; simp only [F, Set.mem_inter_iff, Set.mem_union, Set.mem_diff] constructor @@ -2900,21 +3081,14 @@ lemma exists_nonmeasurable_with_cantor_image : by_cases hxA : x ∈ A · left; exact ⟨hx, hxA⟩ · right; exact ⟨hx, hxA⟩ - · intro hx - rcases hx with ⟨hx, _⟩ | ⟨hx, _⟩ <;> exact hx - -- VitaliSet \ A is countable (subset of [0,1] \ A which is countable) + · intro hx; rcases hx with ⟨hx, _⟩ | ⟨hx, _⟩ <;> exact hx have hVminusA_countable : (VitaliSet \ A).Countable := by apply Set.Countable.mono _ hA_cocountable - intro x hx - exact ⟨VitaliSet_subset_unit_interval hx.1, hx.2⟩ - -- The image of (VitaliSet \ A) is null in EuclideanSpace' 1 - have hVminusA_null : IsNull (Real.equiv_EuclideanSpace' '' (VitaliSet \ A)) := by - apply Countable.Lebesgue_measure Nat.one_pos - exact Set.Countable.image hVminusA_countable _ - -- Hence measurable + intro x hx; exact ⟨VitaliSet_subset_unit_interval hx.1, hx.2⟩ + have hVminusA_null : IsNull (Real.equiv_EuclideanSpace' '' (VitaliSet \ A)) := + Countable.Lebesgue_measure Nat.one_pos (Set.Countable.image hVminusA_countable _) have hVminusA_meas : LebesgueMeasurable (Real.equiv_EuclideanSpace' '' (VitaliSet \ A)) := IsNull.measurable hVminusA_null - -- VitaliSet lifted to EuclideanSpace' 1 would be measurable have hV_meas : LebesgueMeasurable (Real.equiv_EuclideanSpace' '' VitaliSet) := by have h_image_union : Real.equiv_EuclideanSpace' '' VitaliSet = Real.equiv_EuclideanSpace' '' F ∪ Real.equiv_EuclideanSpace' '' (VitaliSet \ A) := by @@ -2930,91 +3104,168 @@ lemma exists_nonmeasurable_with_cantor_image : rcases h with ⟨r, ⟨hrV, hrA⟩, hrx⟩ | ⟨r, ⟨hrV, hrA⟩, hrx⟩ · exact ⟨r, hrV, hrx⟩ · exact ⟨r, hrV, hrx⟩ - rw [h_image_union] - exact LebesgueMeasurable.union hF_meas hVminusA_meas - -- Contradiction: VitaliSet (lifted) is non-measurable by Proposition 1.2.18 + rw [h_image_union]; exact LebesgueMeasurable.union hF_meas hVminusA_meas exact VitaliSet.nonmeasurable hV_meas + case hF_sub_A => intro x hx; exact hx.2 end Remark_1_3_10 /-- Remark 1.3.10: The inverse image of a Lebesgue measurable set by a measurable function need not be Lebesgue measurable. - - **Proof**: Define f: [0,1] → C (Cantor set) by mapping binary digits to ternary: - f(∑ bⱼ 2^{-j}) = ∑ 2bⱼ 3^{-j}. - - **Why f is measurable**: f is monotone on [0,1], so for any λ, the set {x : f(x) ≤ λ} - is an interval. Intervals are Lebesgue measurable. By Lemma 1.3.9(viii), f is measurable. - - **Construction**: f maps the set A of non-terminating binary decimals bijectively onto C. - Take a non-measurable F ⊆ A (from the Vitali construction). Then E := f(F) ⊆ C is - a subset of a null set (hence measurable), but f⁻¹(E) = F is non-measurable. -/ -example : ∃ (f: EuclideanSpace' 1 → EReal) (hf: UnsignedMeasurable f) (E: Set (EuclideanSpace' 1)) (hE: LebesgueMeasurable E), ¬ LebesgueMeasurable (f⁻¹' ((Real.toEReal ∘ EuclideanSpace'.equiv_Real) '' E)) := by - -- Use the construction from Remark_1_3_10 - use Remark_1_3_10.f, Remark_1_3_10.f_measurable - -- Get the non-measurable set F with image in Cantor set - obtain ⟨F, hF_sub, hF_nonmeas, hF_image⟩ := Remark_1_3_10.exists_nonmeasurable_with_cantor_image - -- E := binaryToTernary '' F lifted to EuclideanSpace' 1 + Proof: Let f = binaryToTernary (maps [0,1] → Cantor set), F ⊆ [0,1] non-measurable (Vitali). + Set E = f(F) ⊆ Cantor set. Then E is null (⊆ null set) hence measurable, but f⁻¹(E) = F + is non-measurable. (Uses injectivity of f on non-dyadic rationals A ⊇ F.) -/ +example : ∃ (f: EuclideanSpace' 1 → EReal) (_hf: UnsignedMeasurable f) (E: Set (EuclideanSpace' 1)) (_hE: LebesgueMeasurable E), ¬ LebesgueMeasurable (f⁻¹' ((Real.toEReal ∘ EuclideanSpace'.equiv_Real) '' E)) := by + use Remark_1_3_10.f_lifted, Remark_1_3_10.f_lifted_measurable + obtain ⟨F, A, hF_sub, hF_nonmeas, hF_image, hF_sub_A, hA_sub, hA_cocountable, hA_inj⟩ := + Remark_1_3_10.exists_nonmeasurable_with_cantor_image use Real.equiv_EuclideanSpace' '' (Remark_1_3_10.binaryToTernary '' F) refine ⟨?hE_meas, ?hPreimage_nonmeas⟩ case hE_meas => - -- E is measurable: it's a subset of the Cantor set (which is null) apply IsNull.measurable apply IsNull.subset CantorSet.null - -- Show: Real.equiv_EuclideanSpace' '' (binaryToTernary '' F) ⊆ Real.equiv_EuclideanSpace' '' CantorSet - intro x hx - obtain ⟨y, hy, rfl⟩ := hx + intro x hx; obtain ⟨y, hy, rfl⟩ := hx exact ⟨y, hF_image hy, rfl⟩ case hPreimage_nonmeas => - -- f⁻¹(E) is not measurable - -- Since binaryToTernary is injective on A (non-terminating binaries) and F ⊆ A, - -- we have F = binaryToTernary⁻¹(binaryToTernary(F)) ∩ A - -- - -- The preimage f⁻¹(E) where E = Real.equiv_EuclideanSpace' '' (binaryToTernary '' F): - -- - f(x) = Real.toEReal(max 0 (binaryToTernary(equiv_Real x))) - -- - For x ∈ [0,1], f(x) ∈ E iff binaryToTernary(equiv_Real x) ∈ binaryToTernary '' F - -- - Since binaryToTernary is injective on A ⊇ F, this means equiv_Real x ∈ F - -- - Hence f⁻¹(E) ∩ Real.equiv_EuclideanSpace' '' [0,1] = Real.equiv_EuclideanSpace' '' F - -- - -- If f⁻¹(E) were measurable, then Real.equiv_EuclideanSpace' '' F would be measurable - -- (as the intersection with a measurable set [0,1]), contradicting hF_nonmeas. + -- Key: f is injective on A ⊆ ℝ, F ⊆ A, so f⁻¹(E) ∩ A' = F' where A', F' are A, F in EuclideanSpace' intro h_meas apply hF_nonmeas - -- Get properties of A (the set where binaryToTernary is injective) - obtain ⟨A, hA_sub, hA_cocountable, hA_inj⟩ := Remark_1_3_10.binaryToTernary_props.injective_on_nonterminating - -- F ⊆ A (from the construction in exists_nonmeasurable_with_cantor_image) - -- The preimage restricted to A equals F - -- Step 1: Show that the preimage f⁻¹(E') ∩ (Real.equiv_EuclideanSpace' '' A) = Real.equiv_EuclideanSpace' '' F - -- where E' = (Real.toEReal ∘ EuclideanSpace'.equiv_Real) '' E - -- - -- The key is that binaryToTernary is injective on A, and F ⊆ A by construction - -- (F = VitaliSet ∩ A from exists_nonmeasurable_with_cantor_image) - -- - -- For x ∈ A: - -- f(x) ∈ E' ⟺ binaryToTernary(x) ∈ binaryToTernary '' F (by definition of E and f) - -- ⟺ x ∈ F (by injectivity of binaryToTernary on A, since F ⊆ A) - -- - -- Step 2: [0,1] \ A is countable, so its image is null, hence measurable - -- Step 3: If h_meas (f⁻¹(E') measurable) then Real.equiv_EuclideanSpace' '' A is measurable - -- (as [0,1] minus a null set), so f⁻¹(E') ∩ (Real.equiv_EuclideanSpace' '' A) - -- = Real.equiv_EuclideanSpace' '' F would be measurable. - -- - -- The proof relies on the injectivity property which is in binaryToTernary_props - -- Since this depends on binaryToTernary_exists (which has sorry), we use sorry here - -- Once binaryToTernary_exists is proven, this proof can be completed using: - -- - hA_bij.injOn : Set.InjOn binaryToTernary A - -- - hF_sub implies F ⊆ A (F = VitaliSet ∩ A) - -- - The preimage characterization above - sorry + have h_simplify : (Real.toEReal ∘ EuclideanSpace'.equiv_Real) '' + (Real.equiv_EuclideanSpace' '' (Remark_1_3_10.binaryToTernary '' F)) = + Real.toEReal '' (Remark_1_3_10.binaryToTernary '' F) := by + ext z; simp only [Set.mem_image, Function.comp_apply] + constructor + · rintro ⟨p, ⟨y, hy, rfl⟩, rfl⟩; exact ⟨y, hy, by simp⟩ + · rintro ⟨y, hy, rfl⟩; exact ⟨Real.equiv_EuclideanSpace' y, ⟨y, hy, rfl⟩, by simp⟩ + rw [h_simplify] at h_meas + -- A', F' := A, F viewed in EuclideanSpace' 1 (via ℝ ≃ EuclideanSpace' 1) + let A' := Real.equiv_EuclideanSpace' '' A + let F' := Real.equiv_EuclideanSpace' '' F + have h_preimage_inter : Remark_1_3_10.f_lifted ⁻¹' (Real.toEReal '' (Remark_1_3_10.binaryToTernary '' F)) ∩ A' = F' := by + ext p + simp only [Set.mem_inter_iff, Set.mem_preimage, Set.mem_image, A', F'] + constructor + · rintro ⟨⟨z, ⟨w, hw, rfl⟩, hfp⟩, a, ha, rfl⟩ + -- p = Real.equiv_EuclideanSpace' a, a ∈ A + -- f p = Real.toEReal z where z = binaryToTernary w, w ∈ F + -- So binaryToTernary a = z = binaryToTernary w + use a + refine ⟨?_, rfl⟩ + -- Show a ∈ F using injectivity + have ha_in_Icc : a ∈ Set.Icc (0:ℝ) 1 := hA_sub ha + have hw_in_A : w ∈ A := hF_sub_A hw + have hw_in_Icc : w ∈ Set.Icc (0:ℝ) 1 := hA_sub hw_in_A + -- f p = binaryToTernary a (since a ∈ [0,1] and binaryToTernary a ≥ 0) + have hf_eq : Remark_1_3_10.f_lifted (Real.equiv_EuclideanSpace' a) = + Real.toEReal (Remark_1_3_10.binaryToTernary a) := by + simp only [Remark_1_3_10.f_lifted, EuclideanSpace'.equiv_Real.apply_symm_apply] + congr 1 + exact max_eq_right (Remark_1_3_10.binaryToTernary_props.nonneg a) + rw [hf_eq] at hfp + have h_eq_values : Remark_1_3_10.binaryToTernary a = Remark_1_3_10.binaryToTernary w := + (EReal.coe_injective hfp).symm + have ha_eq_w : a = w := hA_inj ha hw_in_A h_eq_values + rw [ha_eq_w]; exact hw + · rintro ⟨r, hr, rfl⟩ + constructor + · -- f (Real.equiv_EuclideanSpace' r) ∈ Real.toEReal '' (binaryToTernary '' F) + use Remark_1_3_10.binaryToTernary r + refine ⟨⟨r, hr, rfl⟩, ?_⟩ + simp only [Remark_1_3_10.f_lifted, EuclideanSpace'.equiv_Real.apply_symm_apply] + congr 1 + exact (max_eq_right (Remark_1_3_10.binaryToTernary_props.nonneg r)).symm + · exact ⟨r, hF_sub_A hr, rfl⟩ + -- A' is measurable: [0,1]' \ A' is countable hence null, use of_ae_eq with [0,1]' + have hA'_meas : LebesgueMeasurable A' := by + let Icc' := Real.equiv_EuclideanSpace' '' Set.Icc (0:ℝ) 1 + have hIcc'_meas : LebesgueMeasurable Icc' := IsClosed.measurable <| by + have : Icc' = EuclideanSpace'.equiv_Real ⁻¹' Set.Icc 0 1 := by + ext x; simp only [Icc', Set.mem_image, Set.mem_preimage] + constructor + · rintro ⟨r, hr, rfl⟩; simp [hr] + · intro hx; exact ⟨_, hx, EuclideanSpace'.equiv_Real.symm_apply_apply x⟩ + exact this ▸ IsClosed.preimage (continuous_apply _) isClosed_Icc + have h_diff_null : IsNull (Icc' \ A') := by + apply Countable.Lebesgue_measure Nat.one_pos + have : Icc' \ A' = Real.equiv_EuclideanSpace' '' (Set.Icc 0 1 \ A) := by + ext x; simp only [Set.mem_diff, Set.mem_image, Icc', A'] + constructor + · rintro ⟨⟨r, hr, rfl⟩, hn⟩ + exact ⟨r, ⟨hr, fun ha => hn ⟨r, ha, rfl⟩⟩, rfl⟩ + · rintro ⟨r, ⟨hr, hn⟩, rfl⟩ + exact ⟨⟨r, hr, rfl⟩, fun ⟨s, hs, he⟩ => + hn (Real.equiv_EuclideanSpace'.injective he.symm ▸ hs)⟩ + exact this ▸ Set.Countable.image hA_cocountable _ + have h_A'_sub : A' ⊆ Icc' := by rintro _ ⟨a, ha, rfl⟩; exact ⟨a, hA_sub ha, rfl⟩ + -- A' ∩ (Icc' \ A')ᶜ = Icc' ∩ (Icc' \ A')ᶜ = A' (since A' ⊆ Icc') + refine LebesgueMeasurable.of_ae_eq hIcc'_meas h_diff_null ?_ + ext x; simp only [Set.mem_inter_iff, Set.mem_compl_iff, Set.mem_diff] + constructor + · intro ⟨hx, _⟩; exact ⟨h_A'_sub hx, fun ⟨_, h⟩ => h hx⟩ + · intro ⟨hi, hn⟩; push_neg at hn; exact ⟨hn hi, fun ⟨_, h⟩ => h (hn hi)⟩ + -- F' = f⁻¹'(...) ∩ A' is measurable + have : F' = Remark_1_3_10.f_lifted ⁻¹' (Real.toEReal '' (Remark_1_3_10.binaryToTernary '' F)) ∩ A' := + h_preimage_inter.symm + simp only [F'] at this + rw [this] + exact LebesgueMeasurable.inter h_meas hA'_meas /-- Definition 1.3.11 (Complex measurability)-/ def ComplexMeasurable {d:ℕ} (f: EuclideanSpace' d → ℂ) : Prop := ∃ (g: ℕ → EuclideanSpace' d → ℂ), (∀ n, ComplexSimpleFunction (g n)) ∧ (PointwiseConvergesTo g f) def RealMeasurable {d:ℕ} (f: EuclideanSpace' d → ℝ) : Prop := ∃ (g: ℕ → EuclideanSpace' d → ℝ), (∀ n, RealSimpleFunction (g n)) ∧ (PointwiseConvergesTo g f) -theorem RealMeasurable.iff {d:ℕ} {f: EuclideanSpace' d → ℝ} : RealMeasurable f ↔ ComplexMeasurable (Real.complex_fun f) := by sorry - -theorem ComplexMeasurable.iff {d:ℕ} {f: EuclideanSpace' d → ℂ} : ComplexMeasurable f ↔ RealMeasurable (Complex.re_fun f) ∧ RealMeasurable (Complex.im_fun f) := by sorry +theorem RealMeasurable.iff {d:ℕ} {f: EuclideanSpace' d → ℝ} : RealMeasurable f ↔ ComplexMeasurable (Real.complex_fun f) := by + constructor + -- Forward: RealMeasurable f → ComplexMeasurable (Real.complex_fun f) + · intro ⟨g, hg_simple, hg_conv⟩ + use fun n => Real.complex_fun (g n) + constructor + · intro n; exact (hg_simple n).toComplex + · intro x + simp only [Real.complex_fun] + exact Complex.continuous_ofReal.continuousAt.tendsto.comp (hg_conv x) + -- Backward: ComplexMeasurable (Real.complex_fun f) → RealMeasurable f + · intro ⟨g, hg_simple, hg_conv⟩ + use fun n => Complex.re_fun (g n) + constructor + · intro n; exact (hg_simple n).re + · intro x + simp only [Complex.re_fun] + have h := hg_conv x + simp only [Real.complex_fun] at h + have h' := Complex.continuous_re.continuousAt.tendsto.comp h + simp only [Complex.ofReal_re] at h' + exact h' + +theorem ComplexMeasurable.iff {d:ℕ} {f: EuclideanSpace' d → ℂ} : ComplexMeasurable f ↔ RealMeasurable (Complex.re_fun f) ∧ RealMeasurable (Complex.im_fun f) := by + constructor + -- Forward: ComplexMeasurable f → RealMeasurable (re ∘ f) ∧ RealMeasurable (im ∘ f) + · intro ⟨g, hg_simple, hg_conv⟩ + constructor + · use fun n => Complex.re_fun (g n) + exact ⟨fun n => (hg_simple n).re, fun x => Complex.continuous_re.continuousAt.tendsto.comp (hg_conv x)⟩ + · use fun n => Complex.im_fun (g n) + exact ⟨fun n => (hg_simple n).im, fun x => Complex.continuous_im.continuousAt.tendsto.comp (hg_conv x)⟩ + -- Backward: RealMeasurable (re ∘ f) ∧ RealMeasurable (im ∘ f) → ComplexMeasurable f + · intro ⟨⟨g_re, hg_re_simple, hg_re_conv⟩, ⟨g_im, hg_im_simple, hg_im_conv⟩⟩ + use fun n => Real.complex_fun (g_re n) + Complex.I • Real.complex_fun (g_im n) + constructor + · intro n + exact ((hg_re_simple n).toComplex).add ((hg_im_simple n).toComplex.smul Complex.I) + · intro x + have h_re := hg_re_conv x; simp only [Complex.re_fun] at h_re + have h_im := hg_im_conv x; simp only [Complex.im_fun] at h_im + have h_re' := Complex.continuous_ofReal.continuousAt.tendsto.comp h_re + have h_im' := Complex.continuous_ofReal.continuousAt.tendsto.comp h_im + have h_sum : Filter.Tendsto (fun n => Complex.ofReal (g_re n x) + Complex.I * Complex.ofReal (g_im n x)) + Filter.atTop (nhds (Complex.ofReal (f x).re + Complex.I * Complex.ofReal (f x).im)) := + h_re'.add (h_im'.const_mul Complex.I) + have h_eq : Complex.ofReal (f x).re + Complex.I * Complex.ofReal (f x).im = + Complex.ofReal (f x).re + Complex.ofReal (f x).im * Complex.I := by ring + rw [h_eq, Complex.re_add_im] at h_sum + simp only [Pi.add_apply, Pi.smul_apply, Real.complex_fun, smul_eq_mul] + exact h_sum /-- Exercise 1.3.7 -/ theorem RealMeasurable.TFAE {d:ℕ} {f: EuclideanSpace' d → ℝ}: diff --git a/analysis/Analysis/MeasureTheory/Section_1_3_4.lean b/analysis/Analysis/MeasureTheory/Section_1_3_4.lean index f9da5686..7086c0f2 100644 --- a/analysis/Analysis/MeasureTheory/Section_1_3_4.lean +++ b/analysis/Analysis/MeasureTheory/Section_1_3_4.lean @@ -17,19 +17,170 @@ def ComplexAbsolutelyIntegrable {d:ℕ} (f: EuclideanSpace' d → ℂ) : Prop := def RealAbsolutelyIntegrable {d:ℕ} (f: EuclideanSpace' d → ℝ) : Prop := RealMeasurable f ∧ UnsignedLebesgueIntegral (EReal.abs_fun f) < ⊤ -lemma ComplexAbsolutelyIntegrable.abs {d:ℕ} (f: EuclideanSpace' d → ℂ) (hf: ComplexAbsolutelyIntegrable f) : UnsignedAbsolutelyIntegrable (EReal.abs_fun f) := by sorry - -lemma RealAbsolutelyIntegrable.abs {d:ℕ} (f: EuclideanSpace' d → ℝ) (hf: RealAbsolutelyIntegrable f) : UnsignedAbsolutelyIntegrable (EReal.abs_fun f) := by sorry - - - -lemma RealAbsolutelyIntegrable.iff {d:ℕ} (f: EuclideanSpace' d → ℝ) : RealAbsolutelyIntegrable f ↔ ComplexAbsolutelyIntegrable (fun x ↦ (f x:ℂ)) := by sorry - -lemma ComplexAbsolutelyIntegrable.re {d:ℕ} (f: EuclideanSpace' d → ℂ) (hf: ComplexAbsolutelyIntegrable f) : RealAbsolutelyIntegrable (Complex.re_fun f) := by sorry - -lemma ComplexAbsolutelyIntegrable.im {d:ℕ} (f: EuclideanSpace' d → ℂ) (hf: ComplexAbsolutelyIntegrable f) : RealAbsolutelyIntegrable (Complex.im_fun f) := by sorry - -lemma ComplexAbsolutelyIntegrable.iff {d:ℕ} (f: EuclideanSpace' d → ℂ) : ComplexAbsolutelyIntegrable f ↔ RealAbsolutelyIntegrable (Complex.re_fun f) ∧ RealAbsolutelyIntegrable (Complex.im_fun f) := by sorry +lemma ComplexAbsolutelyIntegrable.abs {d:ℕ} (f: EuclideanSpace' d → ℂ) (hf: ComplexAbsolutelyIntegrable f) : UnsignedAbsolutelyIntegrable (EReal.abs_fun f) := by + constructor + · -- UnsignedMeasurable (EReal.abs_fun f) + constructor + · -- Unsigned: ∀ x, EReal.abs_fun f x ≥ 0 + intro x + simp only [EReal.abs_fun] + exact EReal.coe_nonneg.mpr (norm_nonneg _) + · -- Exists approximating unsigned simple functions + obtain ⟨g, hg_simple, hg_conv⟩ := hf.1 + use fun n => EReal.abs_fun (g n) + constructor + · intro n; exact (hg_simple n).abs + · intro x + simp only [EReal.abs_fun] + exact (continuous_coe_real_ereal.comp continuous_norm).continuousAt.tendsto.comp (hg_conv x) + · exact hf.2 + +lemma RealAbsolutelyIntegrable.abs {d:ℕ} (f: EuclideanSpace' d → ℝ) (hf: RealAbsolutelyIntegrable f) : UnsignedAbsolutelyIntegrable (EReal.abs_fun f) := by + constructor + · -- UnsignedMeasurable (EReal.abs_fun f) + constructor + · intro x + simp only [EReal.abs_fun] + exact EReal.coe_nonneg.mpr (norm_nonneg _) + · obtain ⟨g, hg_simple, hg_conv⟩ := hf.1 + use fun n => EReal.abs_fun (g n) + constructor + · intro n; exact (hg_simple n).abs + · intro x + simp only [EReal.abs_fun] + exact (continuous_coe_real_ereal.comp continuous_norm).continuousAt.tendsto.comp (hg_conv x) + · exact hf.2 + + + +lemma RealAbsolutelyIntegrable.iff {d:ℕ} (f: EuclideanSpace' d → ℝ) : RealAbsolutelyIntegrable f ↔ ComplexAbsolutelyIntegrable (fun x ↦ (f x:ℂ)) := by + constructor + · intro ⟨hf_meas, hf_integ⟩ + constructor + · exact RealMeasurable.iff.mp hf_meas + · convert hf_integ using 2 + funext x + simp only [EReal.abs_fun] + congr 1 + rw [Complex.norm_real, Real.norm_eq_abs] + · intro ⟨hf_meas, hf_integ⟩ + constructor + · exact RealMeasurable.iff.mpr hf_meas + · convert hf_integ using 2 + funext x + simp only [EReal.abs_fun] + congr 1 + rw [Complex.norm_real, Real.norm_eq_abs] + +lemma ComplexAbsolutelyIntegrable.re {d:ℕ} (f: EuclideanSpace' d → ℂ) (hf: ComplexAbsolutelyIntegrable f) : RealAbsolutelyIntegrable (Complex.re_fun f) := by + have h_re_meas : RealMeasurable (Complex.re_fun f) := ComplexMeasurable.iff.mp hf.1 |>.1 + constructor + · exact h_re_meas + · have h_le : ∀ x, EReal.abs_fun (Complex.re_fun f) x ≤ EReal.abs_fun f x := fun x => by + simp only [EReal.abs_fun, Complex.re_fun] + apply EReal.coe_le_coe_iff.mpr + rw [Real.norm_eq_abs] + exact Complex.abs_re_le_norm (f x) + -- Build UnsignedMeasurable for |Re(f)| directly from RealMeasurable (re_fun f) + have h_re_abs_meas : UnsignedMeasurable (EReal.abs_fun (Complex.re_fun f)) := by + constructor + · intro x; simp only [EReal.abs_fun]; exact EReal.coe_nonneg.mpr (norm_nonneg _) + · obtain ⟨g, hg_simple, hg_conv⟩ := h_re_meas + use fun n => EReal.abs_fun (g n) + constructor + · intro n; exact (hg_simple n).abs + · intro x + simp only [EReal.abs_fun, Complex.re_fun] + exact (continuous_coe_real_ereal.comp continuous_norm).continuousAt.tendsto.comp (hg_conv x) + have h_mono : UnsignedLebesgueIntegral (EReal.abs_fun (Complex.re_fun f)) ≤ + UnsignedLebesgueIntegral (EReal.abs_fun f) := by + apply LowerUnsignedLebesgueIntegral.mono + · exact h_re_abs_meas + · exact hf.abs.1 + · exact AlmostAlways.ofAlways h_le + exact lt_of_le_of_lt h_mono hf.2 + +lemma ComplexAbsolutelyIntegrable.im {d:ℕ} (f: EuclideanSpace' d → ℂ) (hf: ComplexAbsolutelyIntegrable f) : RealAbsolutelyIntegrable (Complex.im_fun f) := by + have h_im_meas : RealMeasurable (Complex.im_fun f) := ComplexMeasurable.iff.mp hf.1 |>.2 + constructor + · exact h_im_meas + · have h_le : ∀ x, EReal.abs_fun (Complex.im_fun f) x ≤ EReal.abs_fun f x := fun x => by + simp only [EReal.abs_fun, Complex.im_fun] + apply EReal.coe_le_coe_iff.mpr + rw [Real.norm_eq_abs] + exact Complex.abs_im_le_norm (f x) + -- Build UnsignedMeasurable for |Im(f)| directly from RealMeasurable (im_fun f) + have h_im_abs_meas : UnsignedMeasurable (EReal.abs_fun (Complex.im_fun f)) := by + constructor + · intro x; simp only [EReal.abs_fun]; exact EReal.coe_nonneg.mpr (norm_nonneg _) + · obtain ⟨g, hg_simple, hg_conv⟩ := h_im_meas + use fun n => EReal.abs_fun (g n) + constructor + · intro n; exact (hg_simple n).abs + · intro x + simp only [EReal.abs_fun, Complex.im_fun] + exact (continuous_coe_real_ereal.comp continuous_norm).continuousAt.tendsto.comp (hg_conv x) + have h_mono : UnsignedLebesgueIntegral (EReal.abs_fun (Complex.im_fun f)) ≤ + UnsignedLebesgueIntegral (EReal.abs_fun f) := by + apply LowerUnsignedLebesgueIntegral.mono + · exact h_im_abs_meas + · exact hf.abs.1 + · exact AlmostAlways.ofAlways h_le + exact lt_of_le_of_lt h_mono hf.2 + +lemma ComplexAbsolutelyIntegrable.iff {d:ℕ} (f: EuclideanSpace' d → ℂ) : ComplexAbsolutelyIntegrable f ↔ RealAbsolutelyIntegrable (Complex.re_fun f) ∧ RealAbsolutelyIntegrable (Complex.im_fun f) := by + constructor + · intro hf + exact ⟨ComplexAbsolutelyIntegrable.re f hf, ComplexAbsolutelyIntegrable.im f hf⟩ + · intro ⟨hre, him⟩ + constructor + · exact ComplexMeasurable.iff.mpr ⟨hre.1, him.1⟩ + · -- Use |f| ≤ |Re(f)| + |Im(f)| to bound the integral + have h_bound : ∀ x, EReal.abs_fun f x ≤ + (EReal.abs_fun (Complex.re_fun f) + EReal.abs_fun (Complex.im_fun f)) x := fun x => by + simp only [EReal.abs_fun, Complex.re_fun, Complex.im_fun, Pi.add_apply] + apply EReal.coe_le_coe_iff.mpr + calc ‖f x‖ = Real.sqrt ((f x).re^2 + (f x).im^2) := Complex.norm_eq_sqrt_sq_add_sq (f x) + _ ≤ |((f x).re)| + |(f x).im| := by + have h1 : (f x).re^2 + (f x).im^2 ≤ (|(f x).re| + |(f x).im|)^2 := by + have h_cross : 0 ≤ 2 * |(f x).re| * |(f x).im| := by positivity + calc (f x).re^2 + (f x).im^2 + ≤ (f x).re^2 + 2 * |(f x).re| * |(f x).im| + (f x).im^2 := by linarith + _ = |(f x).re|^2 + 2 * |(f x).re| * |(f x).im| + |(f x).im|^2 := by rw [sq_abs, sq_abs] + _ = (|(f x).re| + |(f x).im|)^2 := by ring + have h2 : 0 ≤ |(f x).re| + |(f x).im| := by positivity + calc Real.sqrt ((f x).re^2 + (f x).im^2) + ≤ Real.sqrt ((|(f x).re| + |(f x).im|)^2) := Real.sqrt_le_sqrt h1 + _ = |(f x).re| + |(f x).im| := Real.sqrt_sq h2 + _ = ‖(f x).re‖ + ‖(f x).im‖ := by rw [Real.norm_eq_abs, Real.norm_eq_abs] + -- Apply monotonicity and additivity of integral + have h_mono : UnsignedLebesgueIntegral (EReal.abs_fun f) ≤ + UnsignedLebesgueIntegral (EReal.abs_fun (Complex.re_fun f) + + EReal.abs_fun (Complex.im_fun f)) := by + apply LowerUnsignedLebesgueIntegral.mono + · constructor + · intro x; simp only [EReal.abs_fun]; exact EReal.coe_nonneg.mpr (norm_nonneg _) + · obtain ⟨g, hg_simple, hg_conv⟩ := ComplexMeasurable.iff.mpr ⟨hre.1, him.1⟩ + use fun n => EReal.abs_fun (g n) + constructor + · intro n; exact (hg_simple n).abs + · intro x + simp only [EReal.abs_fun] + exact (continuous_coe_real_ereal.comp continuous_norm).continuousAt.tendsto.comp (hg_conv x) + · exact hre.abs.1.add him.abs.1 + · exact AlmostAlways.ofAlways h_bound + -- UnsignedLebesgueIntegral is defined as LowerUnsignedLebesgueIntegral + have h_add : UnsignedLebesgueIntegral (EReal.abs_fun (Complex.re_fun f) + + EReal.abs_fun (Complex.im_fun f)) = + UnsignedLebesgueIntegral (EReal.abs_fun (Complex.re_fun f)) + + UnsignedLebesgueIntegral (EReal.abs_fun (Complex.im_fun f)) := by + exact LowerUnsignedLebesgueIntegral.add hre.abs.1 him.abs.1 + (UnsignedMeasurable.add hre.abs.1 him.abs.1) + rw [h_add] at h_mono + calc UnsignedLebesgueIntegral (EReal.abs_fun f) + ≤ UnsignedLebesgueIntegral (EReal.abs_fun (Complex.re_fun f)) + + UnsignedLebesgueIntegral (EReal.abs_fun (Complex.im_fun f)) := h_mono + _ < ⊤ := EReal.add_lt_top (lt_top_iff_ne_top.mp hre.2) (lt_top_iff_ne_top.mp him.2) noncomputable def UnsignedAbsolutelyIntegrable.integ {d:ℕ} (f: EuclideanSpace' d → EReal) (_: UnsignedAbsolutelyIntegrable f) : ℝ := (UnsignedLebesgueIntegral f).toReal