PL1/DyadicCellMeasure.lean

All source files · Download exact source

SHA-256: 2f2a16b58991065a5bfb3e5988dbc1785692b6c2c9d0395bb1985716503fb3e6

1import PL1.DyadicTrace23noncomputable section4open MeasureTheory5open scoped ENNReal67namespace PL1.DyadicTrace89theorem cell_inter_Ico (n i : ℕ) (hi : i < 2 ^ n) :10    cell n i ∩ Set.Ico (0 : ℝ) 1 =11      Set.Ico ((i : ℝ) / 2 ^ n) (((i : ℝ) + 1) / 2 ^ n) := by12  have hp : (0 : ℝ) < 2 ^ n := pow_pos (by norm_num) n13  have hip : (i : ℝ) + 1 ≤ 2 ^ n := by exact_mod_cast hi14  have hindex (x : ℝ) (hx : x ∈ Set.Ico (0 : ℝ) 1) : index n x = ⌊(2 : ℝ) ^ n * x⌋₊ := by15    apply min_eq_left16    have hf : ⌊(2 : ℝ) ^ n * x⌋₊ < 2 ^ n :=17      (Nat.floor_lt (mul_nonneg hp.le hx.1)).mpr (by18        simpa only [Nat.cast_pow, Nat.cast_ofNat, mul_one] using mul_lt_mul_of_pos_left hx.2 hp)19    omega20  ext x21  constructor22  · rintro ⟨hc, hx⟩23    have hf : ⌊(2 : ℝ) ^ n * x⌋₊ = i := (hindex x hx).symm.trans hc24    obtain ⟨hl, hu⟩ := (Nat.floor_eq_iff (mul_nonneg hp.le hx.1)).mp hf25    exact ⟨(div_le_iff₀ hp).mpr (by simpa only [mul_comm] using hl),26      (lt_div_iff₀ hp).mpr (by simpa only [mul_comm] using hu)⟩27  · intro hx28    have hx0 : 0 ≤ x := (div_nonneg (Nat.cast_nonneg i) hp.le).trans hx.129    have hx1 : x < 1 := hx.2.trans_le ((div_le_one hp).mpr hip)30    refine ⟨?_, hx0, hx1⟩31    change index n x = i32    rw [hindex x ⟨hx0, hx1⟩]33    apply (Nat.floor_eq_iff (mul_nonneg hp.le hx0)).mpr34    exact ⟨by simpa only [mul_comm] using (div_le_iff₀ hp).mp hx.1,35      by simpa only [mul_comm] using (lt_div_iff₀ hp).mp hx.2⟩3637/-- Every nonempty indexed dyadic trace cell has exactly its usual dyadic38Lebesgue mass, including the clamped first and last cells. -/39theorem intervalMeasure_cell (n i : ℕ) (hi : i < 2 ^ n) :40    intervalMeasure (cell n i) = ENNReal.ofReal (((2 : ℝ) ^ n)⁻¹) := by41  rw [intervalMeasure, ← MeasureTheory.restrict_Ico_eq_restrict_Icc,42    Measure.restrict_apply (measurableSet_cell n i), cell_inter_Ico n i hi,43    Real.volume_Ico]44  have hp : (2 : ℝ) ^ n ≠ 0 := ne_of_gt (pow_pos (by norm_num) n)45  have heq : ((i : ℝ) + 1) / (2 : ℝ) ^ n - (i : ℝ) / 2 ^ n = ((2 : ℝ) ^ n)⁻¹ := by46    field_simp47    ring48  rw [heq]4950theorem intervalMeasure_cell_toReal (n i : ℕ) (hi : i < 2 ^ n) :51    (intervalMeasure (cell n i)).toReal = ((2 : ℝ) ^ n)⁻¹ := by52  rw [intervalMeasure_cell n i hi, ENNReal.toReal_ofReal]53  positivity5455end PL1.DyadicTrace56