PL1/BonamiHaarBridge.lean
All source files · Download exact source
SHA-256: d09ed1fa688477c89df1cc5ee9f956a401d4dda2ff5739055d148ce5b37abe4f
1import PL1.BonamiTwoPoint2import PL1.BonamiTensorization3import PL1.NoiseSemigroup45/-! # Finite cubes inside the actual Haar sign group67The normalized finite-cube average is derived from Haar invariance under8coordinate flips. No independent-product description of Haar is assumed.9-/1011noncomputable section12set_option backward.isDefEq.respectTransparency false13open MeasureTheory14open scoped BigOperators ENNReal1516namespace PL1.Bonami17open Walsh1819instance cubeFintype : (n : ℕ) → Fintype (Cube n)20 | 0 => inferInstanceAs (Fintype Unit)21 | n + 1 => letI := cubeFintype n; inferInstanceAs (Fintype (Bool × Cube n))2223instance cubeTopologicalSpace : (n : ℕ) → TopologicalSpace (Cube n)24 | 0 => inferInstanceAs (TopologicalSpace Unit)25 | n + 1 => letI := cubeTopologicalSpace n26 inferInstanceAs (TopologicalSpace (Bool × Cube n))2728instance cubeDiscreteTopology : (n : ℕ) → DiscreteTopology (Cube n)29 | 0 => inferInstanceAs (DiscreteTopology Unit)30 | n + 1 => letI := cubeDiscreteTopology n31 inferInstanceAs (DiscreteTopology (Bool × Cube n))3233def signBit (a : Sign) : Bool := decide (a.toAdd ≠ 0)3435theorem signValue_eq_bit (a : Sign) : signValue a = if signBit a then -1 else 1 := by36 by_cases ha : a.toAdd = 0 <;> simp [signBit, signValue, ha]3738/-- Read the first n sign coordinates, with the newest coordinate first. -/39def sample : (n : ℕ) → Walsh.Group → Cube n40 | 0, _ => ()41 | n + 1, x => (signBit (x n), sample n x)4243theorem continuous_sample (n : ℕ) : Continuous (sample n) := by44 induction n with45 | zero => exact continuous_const46 | succ n ih =>47 exact ((continuous_of_discreteTopology : Continuous signBit).comp48 (continuous_apply n)).prodMk ih4950def liftContinuous (n : ℕ) (f : Cube n → ℝ) : C(Walsh.Group, ℝ) :=51 ⟨fun x => f (sample n x), continuous_of_discreteTopology.comp (continuous_sample n)⟩5253theorem continuous_lift (n : ℕ) (f : Cube n → ℝ) :54 Continuous (fun x => f (sample n x)) := (liftContinuous n f).continuous5556theorem integrable_lift (n : ℕ) (f : Cube n → ℝ) (μ : Measure Walsh.Group)57 [IsFiniteMeasure μ] : Integrable (fun x => f (sample n x)) μ :=58 (continuous_lift n f).integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace _)5960theorem sample_congr (n : ℕ) {x y : Walsh.Group} (h : ∀ j < n, x j = y j) :61 sample n x = sample n y := by62 induction n with63 | zero => rfl64 | succ n ih =>65 simp only [sample, h n (Nat.lt_succ_self n), ih (fun j hj => h j (Nat.lt_succ_of_lt hj))]6667theorem sample_flip (n : ℕ) (x : Walsh.Group) : sample n (flip n * x) = sample n x := by68 apply sample_congr69 intro j hj70 simp [Walsh.flip, Pi.mul_apply, Function.update_of_ne (Nat.ne_of_lt hj)]7172theorem integral_sign_mul_lift (n : ℕ) (f : Cube n → ℝ) :73 ∫ x, signValue (x n) * f (sample n x) ∂haar = 0 := by74 apply integral_eq_zero_of_mul_left_eq_neg (g := flip n)75 intro x76 rw [sample_flip, Pi.mul_apply, signValue_mul]77 norm_num [Walsh.flip, signValue]78 split_ifs <;> ring7980theorem lift_succ (n : ℕ) (f : Cube (n + 1) → ℝ) (x : Walsh.Group) :81 f (sample (n + 1) x) = meanSlice f (sample n x) +82 signValue (x n) * diffSlice f (sample n x) := by83 rw [signValue_eq_bit]84 cases h : signBit (x n) <;> simp [sample, h, meanSlice, diffSlice] <;> ring8586/-- Haar expectation of every finite-coordinate function is its normalized cube average. -/87theorem integral_lift (n : ℕ) (f : Cube n → ℝ) :88 ∫ x, f (sample n x) ∂haar = average n f := by89 induction n with90 | zero => simp [sample, average]91 | succ n ih =>92 have hf : Integrable (fun x : Walsh.Group => signValue (x n) * diffSlice f (sample n x)) haar :=93 (((continuous_of_discreteTopology : Continuous signValue).comp (continuous_apply n)).mul94 (continuous_lift n (diffSlice f))).integrable_of_hasCompactSupport95 (HasCompactSupport.of_compactSpace _)96 simp_rw [lift_succ]97 rw [integral_add (integrable_lift n _ haar) hf, integral_sign_mul_lift, add_zero, ih]98 change average n (fun x => (f (false, x) + f (true, x)) / 2) = _99 simp only [average, div_eq_mul_inv]100 rw [show (fun x : Cube n => (f (false, x) + f (true, x)) * 2⁻¹) =101 (fun x => 2⁻¹ * (f (false, x) + f (true, x))) by funext x; ring,102 average_mul, average_add]103 ring104105/-- A finite-cube Walsh character; coordinates outside the cube are ignored. -/106def cubeCharacter : (n : ℕ) → Finset ℕ → Cube n → ℝ107 | 0, _, _ => 1108 | n + 1, F, x => (if n ∈ F then (if x.1 then -1 else 1) else 1) *109 cubeCharacter n (F.erase n) x.2110111private theorem erase_subset_range {n : ℕ} {F : Finset ℕ} (hF : F ⊆ Finset.range (n + 1)) :112 F.erase n ⊆ Finset.range n := by113 intro j hj114 obtain ⟨hjn, hjF⟩ := Finset.mem_erase.mp hj115 have hjlt := Finset.mem_range.mp (hF hjF)116 exact Finset.mem_range.mpr (by omega)117118theorem cubeCharacter_sample (n : ℕ) (F : Finset ℕ) (hF : F ⊆ Finset.range n)119 (x : Walsh.Group) : cubeCharacter n F (sample n x) = character F x := by120 induction n generalizing F with121 | zero =>122 have hF0 : F = ∅ := Finset.subset_empty.mp (by simpa using hF)123 simp [hF0, cubeCharacter]124 | succ n ih =>125 have he := erase_subset_range hF126 by_cases hn : n ∈ F127 · have hc : character F x = signValue (x n) * character (F.erase n) x := by128 conv_lhs => rw [← Finset.insert_erase hn]129 rw [character, Finset.prod_insert (Finset.notMem_erase n F)]130 rfl131 simp only [cubeCharacter, hn, ↓reduceIte, sample, ih (F.erase n) he, hc,132 signValue_eq_bit]133 · simpa [cubeCharacter, hn, sample, Finset.erase_eq_of_notMem hn] using134 ih (F.erase n) he135136theorem noise_cubeCharacter (ρ : ℝ) (n : ℕ) (F : Finset ℕ)137 (hF : F ⊆ Finset.range n) (x : Cube n) :138 noise ρ n (cubeCharacter n F) x = ρ ^ F.card * cubeCharacter n F x := by139 induction n generalizing F with140 | zero =>141 have hF0 : F = ∅ := Finset.subset_empty.mp (by simpa using hF)142 simp [hF0, cubeCharacter, noise]143 | succ n ih =>144 have he := erase_subset_range hF145 by_cases hn : n ∈ F146 · have hm : meanSlice (cubeCharacter (n + 1) F) = fun _ => 0 := by147 funext y148 simp [meanSlice, cubeCharacter, hn]149 have hd : diffSlice (cubeCharacter (n + 1) F) = cubeCharacter n (F.erase n) := by150 funext y151 simp [diffSlice, cubeCharacter, hn]152 have hcard : F.card = (F.erase n).card + 1 := (Finset.card_erase_add_one hn).symm153 rw [noise, hm, hd, noise_zero]154 simp only [zero_add, ih (F.erase n) he, cubeCharacter, hn, ↓reduceIte, hcard, pow_succ]155 cases x.1 <;> simp <;> ring156 · have hm : meanSlice (cubeCharacter (n + 1) F) = cubeCharacter n (F.erase n) := by157 funext y158 simp [meanSlice, cubeCharacter, hn]159 have hd : diffSlice (cubeCharacter (n + 1) F) = fun _ => 0 := by160 funext y161 simp [diffSlice, cubeCharacter, hn]162 rw [noise, hm, hd, noise_zero]163 simp only [mul_zero, add_zero]164 rw [ih (F.erase n) he]165 simp only [166 cubeCharacter, hn, ↓reduceIte, one_mul,167 Finset.erase_eq_of_notMem hn]168169/-- Dimension-independent noise estimate for actual finite Walsh sums on Haar. -/170theorem finite_walsh_sum_bound (p ρ : ℝ) (hp : 1 ≤ p) (hp2 : p ≤ 2)171 (hρ : ρ ^ 2 ≤ p - 1) (s : Finset (Finset ℕ)) (c : Finset ℕ → ℝ) :172 (∫ x, (∑ F ∈ s, c F * ρ ^ F.card * character F x) ^ 2 ∂haar) ≤173 (∫ x, |∑ F ∈ s, c F * character F x| ^ p ∂haar) ^ (2 / p) := by174 classical175 let n := s.sup (fun F => F.sup id + 1)176 have hF : ∀ F ∈ s, F ⊆ Finset.range n := by177 intro F hFs j hj178 apply Finset.mem_range.mpr179 exact lt_of_lt_of_le (Nat.lt_succ_of_le (Finset.le_sup (f := id) hj))180 (Finset.le_sup (f := fun F : Finset ℕ => F.sup id + 1) hFs)181 let f : Cube n → ℝ := fun y => ∑ F ∈ s, c F * cubeCharacter n F y182 have hlift (x : Walsh.Group) : f (sample n x) = ∑ F ∈ s, c F * character F x := by183 apply Finset.sum_congr rfl184 intro F hFs185 rw [cubeCharacter_sample n F (hF F hFs)]186 have hnoise (x : Walsh.Group) : noise ρ n f (sample n x) =187 ∑ F ∈ s, c F * ρ ^ F.card * character F x := by188 dsimp only [f]189 rw [noise_sum]190 apply Finset.sum_congr rfl191 intro F hFs192 rw [noise_mul]193 change c F * noise ρ n (cubeCharacter n F) (sample n x) = _194 rw [noise_cubeCharacter ρ n F (hF F hFs), cubeCharacter_sample n F (hF F hFs)]195 ring196 calc197 _ = ∫ x, noise ρ n f (sample n x) ^ 2 ∂haar := by simp_rw [hnoise]198 _ = average n (fun y => noise ρ n f y ^ 2) :=199 integral_lift n (fun y => noise ρ n f y ^ 2)200 _ ≤ moment n p f ^ (2 / p) := noise_moment_bound_sharp hp hp2 hρ n f201 _ = _ := by202 congr 1203 rw [moment, ← integral_lift]204 simp_rw [hlift]205206#print axioms integral_lift207#print axioms finite_walsh_sum_bound208209/-- The same bound in the exponential eigenvalue normalization of the actual noise semigroup. -/210theorem finite_walsh_exp_sum_bound (p u : ℝ) (hp : 1 ≤ p) (hp2 : p ≤ 2)211 (hu : (Real.exp (-u)) ^ 2 ≤ p - 1) (s : Finset (Finset ℕ)) (c : Finset ℕ → ℝ) :212 (∫ x, (∑ F ∈ s, c F * Real.exp (-u * F.card) * character F x) ^ 2 ∂haar) ≤213 (∫ x, |∑ F ∈ s, c F * character F x| ^ p ∂haar) ^ (2 / p) := by214 have h := finite_walsh_sum_bound p (Real.exp (-u)) hp hp2 hu s c215 have he (F : Finset ℕ) : Real.exp (-u) ^ F.card = Real.exp (-u * F.card) := by216 rw [← Real.exp_nat_mul]217 congr 1218 ring219 simpa only [he] using h220221#print axioms finite_walsh_exp_sum_bound222223end PL1.Bonami224