PL1/BalancedFragmentTree.lean
All source files · Download exact source
SHA-256: e7483c976835ade393128d9fbc6a30f03e72e7386051ef30c90c65caeb6be0b9
1import PL1.AtomicBandDecomposition2import Mathlib.Data.Fin.Tuple.Basic34/-!5# Balanced binary fragment trees67An actual exact-halving fragment map constructs finite lattice partitions.8The Boolean signs on each common refinement are the usual Rademacher signs.9-/1011noncomputable section12open scoped BigOperators Topology1314namespace PL1.BalancedFragmentTree1516abbrev Word (n : ℕ) := Fin n → Bool1718def snocEquiv (n : ℕ) : (Word n × Bool) ≃ Word (n + 1) where19 toFun p := Fin.snoc p.1 p.220 invFun w := (Fin.init w, w (Fin.last n))21 left_inv p := by simp22 right_inv w := Fin.snoc_init_self w2324theorem sum_word_succ {A : Type*} [AddCommMonoid A] (n : ℕ) (f : Word (n + 1) → A) :25 ∑ w, f w = ∑ w : Word n, (f (Fin.snoc w false) + f (Fin.snoc w true)) := by26 rw [← (snocEquiv n).sum_comp, Fintype.sum_prod_type]27 simp only [snocEquiv, Equiv.coe_fn_mk, Fintype.sum_bool, add_comm]2829def sign {n : ℕ} (i : Fin n) (w : Word n) : ℝ := if w i then -1 else 13031theorem sign_eq {n : ℕ} (i : Fin n) (w : Word n) : sign i w = 1 ∨ sign i w = -1 := by32 cases h : w i <;> simp [sign, h]3334@[simp] theorem abs_sign {n : ℕ} (i : Fin n) (w : Word n) : |sign i w| = 1 := by35 rcases sign_eq i w with h | h <;> simp [h]3637@[simp] theorem sign_sq {n : ℕ} (i : Fin n) (w : Word n) : sign i w * sign i w = 1 := by38 rcases sign_eq i w with h | h <;> simp [h]3940@[simp] theorem sign_snoc_castSucc {n : ℕ} (i : Fin n) (w : Word n) (b : Bool) :41 sign i.castSucc (Fin.snoc w b) = sign i w := by simp [sign]4243@[simp] theorem sign_snoc_last_false {n : ℕ} (w : Word n) :44 sign (Fin.last n) (Fin.snoc w false) = 1 := by simp [sign]4546@[simp] theorem sign_snoc_last_true {n : ℕ} (w : Word n) :47 sign (Fin.last n) (Fin.snoc w true) = -1 := by simp [sign]4849def flipEquiv {n : ℕ} (i : Fin n) : Word n ≃ Word n where50 toFun w := Function.update w i (!(w i))51 invFun w := Function.update w i (!(w i))52 left_inv w := by ext j; by_cases h : j = i <;> simp [h]53 right_inv w := by ext j; by_cases h : j = i <;> simp [h]5455@[simp] theorem sign_flip_self {n : ℕ} (i : Fin n) (w : Word n) :56 sign i (flipEquiv i w) = -sign i w := by57 cases h : w i <;> simp [sign, flipEquiv, h]5859theorem sign_flip_ne {n : ℕ} {i j : Fin n} (h : j ≠ i) (w : Word n) :60 sign j (flipEquiv i w) = sign j w := by simp [sign, flipEquiv, h]6162/-- Orthogonality is a finite Boolean identity, independent of a measure space. -/63theorem sign_orthogonality {n : ℕ} (i j : Fin n) :64 (∑ w : Word n, sign i w * sign j w) = if i = j then (2 : ℝ) ^ n else 0 := by65 classical66 by_cases hij : i = j67 · subst j68 simp [Word]69 · rw [ite_eq_right_iff.mpr (fun h => False.elim (hij h))]70 have h := (flipEquiv i).sum_comp (fun w => sign i w * sign j w)71 simp only [sign_flip_self, sign_flip_ne (fun h => hij h.symm), neg_mul,72 Finset.sum_neg_distrib] at h73 linarith7475variable {E : Type*} [NormedAddCommGroup E] [Lattice E]76 [IsOrderedAddMonoid E] [NormedVectorLattice E]7778/-- Exact halving by genuine disjoint fragments throughout `[0,u]`. -/79def IsBalancedSplit (φ : E →L[ℝ] ℝ) (u : E) (split : E → E) : Prop :=80 ∀ x : E, 0 ≤ x → x ≤ u →81 0 ≤ split x ∧ split x ≤ x ∧ IsVLDisjoint (split x) (x - split x) ∧82 φ (split x) = φ x / 28384/-- Actual cells; at each step the final Boolean coordinate chooses the child. -/85def cell (u : E) (split : E → E) : (n : ℕ) → Word n → E86 | 0, _ => u87 | n + 1, w =>88 let x := cell u split n (Fin.init w)89 if w (Fin.last n) then x - split x else split x9091omit [Lattice E] [IsOrderedAddMonoid E] [NormedVectorLattice E] in92@[simp] theorem cell_zero (u : E) (split : E → E) (w : Word 0) : cell u split 0 w = u := rfl9394omit [Lattice E] [IsOrderedAddMonoid E] [NormedVectorLattice E] in95@[simp] theorem cell_snoc_false (u : E) (split : E → E) {n : ℕ} (w : Word n) :96 cell u split (n + 1) (Fin.snoc w false) = split (cell u split n w) := by simp [cell]9798omit [Lattice E] [IsOrderedAddMonoid E] [NormedVectorLattice E] in99@[simp] theorem cell_snoc_true (u : E) (split : E → E) {n : ℕ} (w : Word n) :100 cell u split (n + 1) (Fin.snoc w true) = cell u split n w - split (cell u split n w) := by101 simp [cell]102103omit [Lattice E] [IsOrderedAddMonoid E] [NormedVectorLattice E] in104theorem cell_children_add (u : E) (split : E → E) {n : ℕ} (w : Word n) :105 cell u split (n + 1) (Fin.snoc w false) + cell u split (n + 1) (Fin.snoc w true) =106 cell u split n w := by simp107108theorem cell_mem_Icc {φ : E →L[ℝ] ℝ} {u : E} {split : E → E}109 (hu : 0 ≤ u) (hs : IsBalancedSplit φ u split) (n : ℕ) (w : Word n) :110 0 ≤ cell u split n w ∧ cell u split n w ≤ u := by111 induction n with112 | zero => exact ⟨hu, le_rfl⟩113 | succ n ih =>114 obtain ⟨hx, hxu⟩ := ih (Fin.init w)115 obtain ⟨hp, hpx, _, _⟩ := hs _ hx hxu116 simp only [cell]117 split118 · exact ⟨sub_nonneg.mpr hpx, (sub_le_self _ hp).trans hxu⟩119 · exact ⟨hp, hpx.trans hxu⟩120121theorem cell_child_le {φ : E →L[ℝ] ℝ} {u : E} {split : E → E}122 (hu : 0 ≤ u) (hs : IsBalancedSplit φ u split) {n : ℕ} (w : Word n) (b : Bool) :123 cell u split (n + 1) (Fin.snoc w b) ≤ cell u split n w := by124 have hx := cell_mem_Icc hu hs n w125 have hp := hs _ hx.1 hx.2126 cases b <;> simp only [cell_snoc_false, cell_snoc_true]127 · exact hp.2.1128 · exact sub_le_self _ hp.1129130omit [Lattice E] [IsOrderedAddMonoid E] [NormedVectorLattice E] in131theorem sum_cell (u : E) (split : E → E) (n : ℕ) : ∑ w : Word n, cell u split n w = u := by132 induction n with133 | zero => simp [Word]134 | succ n ih => rw [sum_word_succ]; simpa only [cell_children_add] using ih135136theorem cell_phi {φ : E →L[ℝ] ℝ} {u : E} {split : E → E}137 (hu : 0 ≤ u) (hs : IsBalancedSplit φ u split) (n : ℕ) (w : Word n) :138 φ (cell u split n w) = φ u / (2 : ℝ) ^ n := by139 induction n with140 | zero => simp141 | succ n ih =>142 have hx := cell_mem_Icc hu hs n (Fin.init w)143 have hp := (hs _ hx.1 hx.2).2.2.2144 simp only [cell]145 split146 · rw [map_sub, hp, ih]147 rw [pow_succ]148 ring149 · rw [hp, ih, pow_succ]150 ring151152theorem cell_pairwise_disjoint {φ : E →L[ℝ] ℝ} {u : E} {split : E → E}153 (hu : 0 ≤ u) (hs : IsBalancedSplit φ u split) (n : ℕ) :154 Pairwise (fun w z : Word n => IsVLDisjoint (cell u split n w) (cell u split n z)) := by155 induction n with156 | zero =>157 intro w z hne158 exact False.elim (hne (Subsingleton.elim w z))159 | succ n ih =>160 have hc (w z : Word n) (b c : Bool)161 (hne : (Fin.snoc w b : Word (n + 1)) ≠ Fin.snoc z c) :162 IsVLDisjoint (cell u split (n + 1) (Fin.snoc w b))163 (cell u split (n + 1) (Fin.snoc z c)) := by164 by_cases hwz : w = z165 · subst z166 have hbc : b ≠ c := fun h => hne (h ▸ rfl)167 have hx := cell_mem_Icc hu hs n w168 have hd := (hs _ hx.1 hx.2).2.2.1169 cases b <;> cases c170 · exact False.elim (hbc rfl)171 · simpa only [cell_snoc_false, cell_snoc_true] using hd172 · simpa only [cell_snoc_false, cell_snoc_true] using isVLDisjoint_comm.mp hd173 · exact False.elim (hbc rfl)174 · apply ((ih hwz).mono_left ?_).mono_right ?_175 · rw [abs_of_nonneg (cell_mem_Icc hu hs _ _).1,176 abs_of_nonneg (cell_mem_Icc hu hs _ _).1]177 exact cell_child_le hu hs w b178 · rw [abs_of_nonneg (cell_mem_Icc hu hs _ _).1,179 abs_of_nonneg (cell_mem_Icc hu hs _ _).1]180 exact cell_child_le hu hs z c181 intro w z hne182 simpa only [Fin.snoc_init_self] using183 hc (Fin.init w) (Fin.init z) (w (Fin.last n)) (z (Fin.last n))184 (by simpa only [Fin.snoc_init_self] using hne)185186theorem signed_refinement_one (u : E) (split : E → E) {n : ℕ} (i : Fin n) :187 (∑ w : Word (n + 1), sign i.castSucc w • cell u split (n + 1) w) =188 ∑ w : Word n, sign i w • cell u split n w := by189 rw [sum_word_succ]190 apply Finset.sum_congr rfl191 intro w _192 simp only [sign_snoc_castSucc, ← smul_add, cell_children_add]193194/-- The actual lattice Rademacher sequence generated by the fragment tree. -/195def rademacher (u : E) (split : E → E) (n : ℕ) : E :=196 ∑ w : Word (n + 1), sign (Fin.last n) w • cell u split (n + 1) w197198/-- All earlier Rademachers admit a simultaneous expansion on any deeper partition. -/199theorem rademacher_refinement (u : E) (split : E → E) {n m : ℕ} (hnm : n < m) :200 rademacher u split n = ∑ w : Word m, sign ⟨n, hnm⟩ w • cell u split m w := by201 induction m with202 | zero => exact False.elim (Nat.not_lt_zero n hnm)203 | succ m ih =>204 by_cases h : n = m205 · subst m206 rfl207 · have hlt : n < m := lt_of_le_of_ne (Nat.le_of_lt_succ hnm) h208 have hidx : (⟨n, hnm⟩ : Fin (m + 1)) = (⟨n, hlt⟩ : Fin m).castSucc := rfl209 rw [hidx, signed_refinement_one]210 exact ih hlt211212/-- BanLat's absolute-sum identity, reindexed over an arbitrary finite type. -/213theorem abs_sum_smul_disjoint {ι : Type*} [Fintype ι]214 (p : ι → E) (α : ι → ℝ) (hd : Pairwise (fun i j => IsVLDisjoint (p i) (p j))) :215 |∑ i, α i • p i| = ∑ i, |α i| • |p i| := by216 classical217 let e := (Fintype.equivFin ι).symm218 have h := abs_sum_of_pairwise_isVLDisjoint (x := fun i => p (e i))219 (α := fun i => α (e i)) (fun _ _ hij => hd (fun h => hij (e.injective h)))220 have h₁ := e.sum_comp (fun i => α i • p i)221 have h₂ := e.sum_comp (fun i => |α i| • |p i|)222 rw [h₁, h₂] at h223 exact h224225/-- Every Rademacher has exactly the absolute value of the root fragment. -/226theorem abs_rademacher {φ : E →L[ℝ] ℝ} {u : E} {split : E → E}227 (hu : 0 ≤ u) (hs : IsBalancedSplit φ u split) (n : ℕ) :228 |rademacher u split n| = u := by229 rw [rademacher, abs_sum_smul_disjoint _ _ (cell_pairwise_disjoint hu hs _)]230 simpa only [abs_sign, abs_of_nonneg (cell_mem_Icc hu hs _ _).1, one_smul] using231 sum_cell u split (n + 1)232233theorem weighted_sign_orthogonality {φ : E →L[ℝ] ℝ} {u : E} {split : E → E}234 (hu : 0 ≤ u) (hs : IsBalancedSplit φ u split) {n : ℕ} (i j : Fin n) :235 (∑ w : Word n, φ (cell u split n w) * sign i w * sign j w) =236 if i = j then φ u else 0 := by237 simp_rw [cell_phi hu hs]238 have heq : (∑ w : Word n, φ u / (2 : ℝ) ^ n * sign i w * sign j w) =239 (φ u / (2 : ℝ) ^ n) * ∑ w : Word n, sign i w * sign j w := by240 rw [Finset.mul_sum]241 apply Finset.sum_congr rfl242 intro w _243 ring244 rw [heq, sign_orthogonality]245 split246 · exact div_mul_cancel₀ _ (pow_ne_zero _ (by norm_num : (2 : ℝ) ≠ 0))247 · exact mul_zero _248249/-- An existential exact-halving theorem supplies the actual split map used250in the tree, including its value at zero. -/251theorem exists_balancedSplit (φ : E →L[ℝ] ℝ) (u : E)252 (hhalf : ∀ x : E, 0 < x → x ≤ u →253 ∃ y : E, 0 ≤ y ∧ y ≤ x ∧ IsVLDisjoint y (x - y) ∧ φ y = φ x / 2) :254 ∃ split : E → E, IsBalancedSplit φ u split := by255 classical256 let split : E → E := fun x => if h : 0 < x ∧ x ≤ u then (hhalf x h.1 h.2).choose else 0257 refine ⟨split, ?_⟩258 intro x hx hxu259 by_cases hx0 : x = 0260 · subst x261 simp [split, IsVLDisjoint]262 · have hxpos := lt_of_le_of_ne hx (fun h => hx0 h.symm)263 have hvalid : 0 < x ∧ x ≤ u := ⟨hxpos, hxu⟩264 simpa only [split, dite_eq_left hvalid] using (hhalf x hxpos hxu).choose_spec265266end PL1.BalancedFragmentTree267