PL1/HeadTail.lean
All source files · Download exact source
SHA-256: d58960a4175ec3a5ce6bb8a5ecee6e658a5f46f9781dc88434b4ae46ead7ab4d
1import PL1.KernelTranslations2import PL1.SingularConvolution3import PL1.SpikeSeparation4import Mathlib.Probability.Independence.InfinitePi5import Mathlib.Probability.Independence.Integration67/-! # Independence of actual finite head and tail coordinates89The normalized Haar measure is identified with the unbiased infinite product.10Finite-coordinate functions on disjoint coordinate sets are therefore genuinely11independent for Haar and for every actual product-noise probability.12-/1314noncomputable section15open MeasureTheory ProbabilityTheory16open scoped ENNReal NNReal BigOperators17namespace PL1.HeadTail18open Walsh FiniteCoordinateKernels1920/-- Dependence of a function on an actual finite set of coordinates. -/21def DependsOn {E : Type*} (S : Finset ℕ) (f : Walsh.Group → E) : Prop :=22 ∀ x y, (∀ j ∈ S, x j = y j) → f x = f y2324theorem DependsOn.factor {E : Type*} {S : Finset ℕ} {f : Walsh.Group → E}25 (hf : DependsOn S f) (x : Walsh.Group) : f (FiniteCoordinateKernels.extend S (S.restrict x)) = f x :=26 hf _ _ (fun j hj => by simp [FiniteCoordinateKernels.extend, hj])2728theorem DependsOn.continuous {E : Type*} [TopologicalSpace E]29 {S : Finset ℕ} {f : Walsh.Group → E} (hf : DependsOn S f) : Continuous f := by30 have he : f = (fun a : Assignments S => f (FiniteCoordinateKernels.extend S a)) ∘ S.restrict := by31 funext x32 exact (hf.factor x).symm33 rw [he]34 exact continuous_of_discreteTopology.comp (continuous_pi (fun j => continuous_apply (j : ℕ)))3536theorem DependsOn.comp {E F : Type*} {S : Finset ℕ} {f : Walsh.Group → E}37 (hf : DependsOn S f) (g : E → F) : DependsOn S (g ∘ f) :=38 fun x y hxy => congrArg g (hf x y hxy)3940theorem DependsOn.translate {E : Type*} {S : Finset ℕ} {f : Walsh.Group → E}41 (hf : DependsOn S f) (a : Walsh.Group) : DependsOn S (fun x => f (a * x)) :=42 fun _x _y hxy => hf _ _ (fun j hj => congrArg (fun z => a j * z) (hxy j hj))4344def uniformCoordinate : Measure Sign :=45 bernoulliMeasure 1 (Multiplicative.ofAdd 1) ⟨1 / 2, by constructor <;> norm_num⟩4647instance : IsProbabilityMeasure uniformCoordinate := by unfold uniformCoordinate; infer_instance4849theorem integral_sign_uniform : ∫ a, signValue a ∂uniformCoordinate = 0 := by50 rw [uniformCoordinate, integral_bernoulliMeasure]51 norm_num [signValue]5253/-- The Haar probability used throughout the project is the actual unbiased product. -/54theorem haar_eq_infinitePi : haar = Measure.infinitePi (fun _ : ℕ => uniformCoordinate) := by55 apply SingularConvolution.measure_eq_of_walsh_integrals56 intro F57 rw [Walsh.integral_character]58 have heq (x : Walsh.Group) : character F x = ∏ j : F, signValue (x j) :=59 (Finset.prod_coe_sort F (fun j => signValue (x j))).symm60 simp_rw [heq]61 change _ = ∫ x, (fun y : F → Sign => ∏ j, signValue (y j)) (F.restrict x)62 ∂Measure.infinitePi (fun _ : ℕ => uniformCoordinate)63 rw [integral_restrict_infinitePi (fun _ : ℕ => uniformCoordinate) (s := F) (f := fun y : F → Sign => ∏ j, signValue (y j))64 continuous_of_discreteTopology.aestronglyMeasurable, integral_fintype_prod_eq_prod]65 simp only [integral_sign_uniform]66 by_cases hF : F = ∅67 · subst F; simp68 · rw [ite_eq_right hF]69 obtain ⟨j, hj⟩ := Finset.nonempty_iff_ne_empty.mpr hF70 exact (Finset.prod_eq_zero (i := (⟨j, hj⟩ : F)) (Finset.mem_univ _) rfl).symm7172theorem independent_restrictions (μ : ℕ → Measure Sign) [∀ j, IsProbabilityMeasure (μ j)]73 (S T : Finset ℕ) (hST : Disjoint S T) :74 IndepFun S.restrict T.restrict (Measure.infinitePi μ) :=75 (iIndepFun_infinitePi (P := μ) (X := fun _ a => a) (fun _ => measurable_id)).indepFun_finset76 S T hST (fun j => measurable_pi_apply j)7778theorem indepFun {E F : Type*} [MeasurableSpace E] [MeasurableSpace F]79 (μ : ℕ → Measure Sign) [∀ j, IsProbabilityMeasure (μ j)]80 {S T : Finset ℕ} {f : Walsh.Group → E} {g : Walsh.Group → F}81 (hST : Disjoint S T) (hf : DependsOn S f) (hg : DependsOn T g) :82 IndepFun f g (Measure.infinitePi μ) := by83 have h := (independent_restrictions μ S T hST).comp84 (measurable_of_finite (fun a : Assignments S => f (FiniteCoordinateKernels.extend S a)))85 (measurable_of_finite (fun a : Assignments T => g (FiniteCoordinateKernels.extend T a)))86 simpa only [Function.comp_def, hf.factor, hg.factor] using h8788theorem indepFun_haar {E F : Type*} [MeasurableSpace E] [MeasurableSpace F]89 {S T : Finset ℕ} {f : Walsh.Group → E} {g : Walsh.Group → F}90 (hST : Disjoint S T) (hf : DependsOn S f) (hg : DependsOn T g) : IndepFun f g haar := by91 rw [haar_eq_infinitePi]92 exact indepFun _ hST hf hg9394theorem indepFun_noise {E F : Type*} [MeasurableSpace E] [MeasurableSpace F]95 (rates : ℕ → ℝ≥0) (u : ℝ≥0) {S T : Finset ℕ}96 {f : Walsh.Group → E} {g : Walsh.Group → F}97 (hST : Disjoint S T) (hf : DependsOn S f) (hg : DependsOn T g) :98 IndepFun f g (Noise.measure rates u) := indepFun _ hST hf hg99100end PL1.HeadTail101102namespace PL1.HeadTail103open Walsh FiniteCoordinateKernels104105/-- Arbitrary finite head/tail functions integrate as functions of independent copies. -/106theorem integral_headTail {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]107 (μ : Measure Walsh.Group) [IsProbabilityMeasure μ] (S T : Finset ℕ)108 (hi : IndepFun S.restrict T.restrict μ) (F : Assignments S × Assignments T → E) :109 (∫ x, F (S.restrict x, T.restrict x) ∂μ) =110 ∫ x, ∫ y, F (S.restrict x, T.restrict y) ∂μ ∂μ := by111 have hS : Measurable (S.restrict : Walsh.Group → Assignments S) :=112 Measurable.of_eval (fun j => measurable_pi_apply (j : ℕ))113 have hT : Measurable (T.restrict : Walsh.Group → Assignments T) :=114 Measurable.of_eval (fun j => measurable_pi_apply (j : ℕ))115 have hF : Continuous F := continuous_of_discreteTopology116 have hm := hi.map_prod_eq_prod_map_map hS.aemeasurable hT.aemeasurable117 calc118 _ = ∫ z, F z ∂μ.map (fun x => (S.restrict x, T.restrict x)) :=119 (integral_map (hS.prodMk hT).aemeasurable hF.aestronglyMeasurable).symm120 _ = ∫ z, F z ∂(μ.map S.restrict).prod (μ.map T.restrict) := by rw [hm]121 _ = ∫ a, ∫ b, F (a, b) ∂μ.map T.restrict ∂μ.map S.restrict :=122 integral_prod F (hF.integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace _))123 _ = ∫ x, ∫ b, F (S.restrict x, b) ∂μ.map T.restrict ∂μ :=124 integral_map hS.aemeasurable continuous_of_discreteTopology.aestronglyMeasurable125 _ = _ := by126 apply integral_congr_ae127 exact ae_of_all _ (fun x => integral_map hT.aemeasurable128 continuous_of_discreteTopology.aestronglyMeasurable)129130/-- A finite head/tail function separates under the project's actual Haar probability. -/131theorem integral_headTail_haar {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]132 (S T : Finset ℕ) (hST : Disjoint S T) (F : Assignments S × Assignments T → E) :133 (∫ x, F (S.restrict x, T.restrict x) ∂haar) =134 ∫ x, ∫ y, F (S.restrict x, T.restrict y) ∂haar ∂haar := by135 apply integral_headTail136 rw [haar_eq_infinitePi]137 exact independent_restrictions _ S T hST138139end PL1.HeadTail140141namespace PL1.HeadTail142open Walsh FiniteCoordinateKernels143144/-- Exact norm-product integration for functions on disjoint actual Haar coordinates. -/145theorem integral_norm_smul {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]146 {S T : Finset ℕ} (hST : Disjoint S T)147 (f : C(Walsh.Group, E)) (q : C(Walsh.Group, ℝ))148 (hf : DependsOn S f) (hq : DependsOn T q) :149 (∫ x, ‖q x • f x‖ ∂haar) = (∫ x, ‖q x‖ ∂haar) * ∫ x, ‖f x‖ ∂haar := by150 simp only [norm_smul]151 exact (indepFun_haar hST.symm (hq.comp norm) (hf.comp norm)).integral_fun_mul_eq_mul_integral152 q.continuous.norm.aestronglyMeasurable f.continuous.norm.aestronglyMeasurable153154/-- The concentration estimate on the original Haar space, with finite independent heads. -/155theorem concentration_lower_bound {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]156 {S T : Finset ℕ} (hST : Disjoint S T)157 (f g : C(Walsh.Group, E)) (q : C(Walsh.Group, ℝ))158 (hf : DependsOn S f) (hg : DependsOn S g) (hq : DependsOn T q)159 (hq0 : ∀ᵐ x ∂haar, 0 ≤ q x) (hq1 : ∫ x, q x ∂haar = 1)160 (B : Set Walsh.Group) (hB : MeasurableSet B) (δ : ℝ)161 (hsmall : haar.real B ≤ δ) (hconcentrated : 1 - δ ≤ ∫ x in B, q x ∂haar) :162 (1 - 2 * δ) * ((∫ x, ‖f x‖ ∂haar) + ∫ x, ‖g x‖ ∂haar) ≤163 ∫ x, ‖f x + q x • g x‖ ∂haar := by164 have he := integral_headTail_haar S T hST (fun z : Assignments S × Assignments T =>165 ‖f (FiniteCoordinateKernels.extend S z.1) +166 q (FiniteCoordinateKernels.extend T z.2) • g (FiniteCoordinateKernels.extend S z.1)‖)167 simp only [hf.factor, hg.factor, hq.factor] at he168 rw [he]169 have hiq : Integrable (q : Walsh.Group → ℝ) haar :=170 q.continuous.integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace _)171 have hif : Integrable (fun x => ‖f x‖) haar :=172 f.continuous.norm.integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace _)173 have hig : Integrable (fun x => ‖g x‖) haar :=174 g.continuous.norm.integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace _)175 have hiraw : DependsOn S (fun x => ∫ y, ‖f x + q y • g x‖ ∂haar) := by176 intro x z hxz177 simp only [hf x z hxz, hg x z hxz]178 have hi : Integrable (fun x => ∫ y, ‖f x + q y • g x‖ ∂haar) haar := hiraw.continuous.integrable_of_hasCompactSupport (HasCompactSupport.of_compactSpace _)179 have h := integral_mono ((hif.add hig).const_mul (1 - 2 * δ)) hi (fun x =>180 SpikeSeparation.concentration_lower_bound hiq hq0 hq1 B hB δ hsmall hconcentrated (f x) (g x))181 simpa only [integral_const_mul, Pi.add_apply, integral_add hif hig] using h182183#print axioms concentration_lower_bound184end PL1.HeadTail185