PL1/TraceBounds.lean
All source files · Download exact source
SHA-256: 2a8d6aec908d02c43f0adf6c2b395892d9d703d4b442e6b12e1f3552b0fe2d92
1import PL1.WalshModel2import PL1.L1Masks3import PL1.LpInclusions4import Mathlib.MeasureTheory.Function.LpSpace.Indicator56/-! # Finite partition traces and the L-infinity to L1 norm bound -/78noncomputable section9set_option autoImplicit false10set_option maxHeartbeats 80000011open MeasureTheory Filter12open scoped ENNReal BigOperators Topology1314namespace PL1.TraceBounds1516variable {𝕜 : Type*} [RCLike 𝕜]1718private theorem integral_scalar_sign_mul (i j : ℕ) :19 (∫ x, Walsh.scalarCharacter 𝕜 {i} x * Walsh.scalarCharacter 𝕜 {j} x ∂Walsh.haar) =20 if i = j then 1 else 0 := by21 calc22 _ = ((∫ x, Walsh.character {i} x * Walsh.character {j} x ∂Walsh.haar : ℝ) : 𝕜) := by23 simp only [Walsh.scalarCharacter, ← RCLike.ofReal_mul, integral_ofReal]24 _ = _ := by rw [Walsh.integral_character_mul]; split_ifs <;> simp_all2526private theorem scalar_sign_integrable (i j : ℕ) (c : 𝕜) :27 Integrable (fun x => (Walsh.scalarCharacter 𝕜 {i} x *28 Walsh.scalarCharacter 𝕜 {j} x) * c) Walsh.haar :=29 ((Walsh.continuous_scalarCharacter 𝕜 {i}).mul30 (Walsh.continuous_scalarCharacter 𝕜 {j}) |>.mul continuous_const).integrable_of_hasCompactSupport31 (HasCompactSupport.of_compactSpace _)3233section AbstractTrace3435variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]36 [NormedAddCommGroup F] [NormedSpace 𝕜 F]3738/-- The diagonal sum associated with a finite family and finite tests. -/39def finiteTrace (s : Finset ℕ) (e : ℕ → E) (φ : ℕ → F →L[𝕜] 𝕜)40 (T : E →L[𝕜] F) : 𝕜 := ∑ i ∈ s, φ i (T (e i))4142theorem finiteTrace_sub (s : Finset ℕ) (e : ℕ → E) (φ : ℕ → F →L[𝕜] 𝕜)43 (T U : E →L[𝕜] F) :44 finiteTrace s e φ (T - U) = finiteTrace s e φ T - finiteTrace s e φ U := by45 simp only [finiteTrace, sub_apply, map_sub, Finset.sum_sub_distrib]4647theorem finiteTrace_eq_sign_average (s : Finset ℕ) (e : ℕ → E)48 (φ : ℕ → F →L[𝕜] 𝕜) (T : E →L[𝕜] F) :49 finiteTrace s e φ T = ∫ x,50 (∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x • φ i)51 (T (∑ j ∈ s, Walsh.scalarCharacter 𝕜 {j} x • e j)) ∂Walsh.haar := by52 simp only [sum_apply, map_sum, map_smul, smul_apply,53 smul_eq_mul, Finset.mul_sum]54 simp_rw [← mul_assoc]55 rw [integral_finsetSum]56 · unfold finiteTrace57 apply Finset.sum_congr rfl58 intro i hi59 rw [integral_finsetSum s (fun j _ => scalar_sign_integrable i j (φ j (T (e i))))]60 simp only [integral_mul_const, integral_scalar_sign_mul]61 simp [hi]62 · intro i hi63 exact integrable_finsetSum _ (fun j _ => scalar_sign_integrable i j _)6465/-- The sign averaging proof of the finite trace bound, over either field. -/66theorem norm_finiteTrace_le (s : Finset ℕ) (e : ℕ → E) (φ : ℕ → F →L[𝕜] 𝕜)67 (he : ∀ x : Walsh.Group, ‖∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x • e i‖ ≤ 1)68 (hφ : ∀ x : Walsh.Group, ‖∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x • φ i‖ ≤ 1)69 (T : E →L[𝕜] F) : ‖finiteTrace s e φ T‖ ≤ ‖T‖ := by70 rw [finiteTrace_eq_sign_average]71 have h := norm_integral_le_of_norm_le_const (μ := Walsh.haar)72 (C := ‖T‖) (ae_of_all _ (fun x =>73 calc74 _ ≤ ‖∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x • φ i‖ *75 ‖T (∑ j ∈ s, Walsh.scalarCharacter 𝕜 {j} x • e j)‖ :=76 ContinuousLinearMap.le_opNorm _ _77 _ ≤ 1 * (‖T‖ * 1) := mul_le_mul (hφ x)78 ((T.le_opNorm _).trans (mul_le_mul_of_nonneg_left (he x) (norm_nonneg _)))79 (norm_nonneg _) zero_le_one80 _ = ‖T‖ := by ring))81 simpa using h8283end AbstractTrace8485section MeasurablePartition8687variable {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]88variable (A : ℕ → Set Ω) (hA : ∀ i, MeasurableSet (A i))8990/-- A partition cell as an actual L-infinity class. -/91def cellVector (i : ℕ) : Lp 𝕜 ∞ μ :=92 indicatorConstLp ∞ (hA i) (measure_ne_top μ (A i)) (1 : 𝕜)9394/-- Integration over a cell, as a bounded linear functional on actual L1. -/95def cellFunctional (i : ℕ) : Lp 𝕜 1 μ →L[𝕜] 𝕜 :=96 (L1.integralCLM' 𝕜).comp (L1Masks.mask μ (A i) (hA i))9798omit [IsProbabilityMeasure μ] in99theorem cellFunctional_apply (i : ℕ) (f : Lp 𝕜 1 μ) :100 cellFunctional (𝕜 := 𝕜) μ A hA i f = ∫ x in A i, f x ∂μ := by101 change L1.integralCLM' 𝕜 (L1Masks.mask μ (A i) (hA i) f) = _102 rw [← L1.integral_eq', L1.integral_eq_integral]103 rw [integral_congr_ae (L1Masks.coeFn_mask μ (A i) (hA i) f), integral_indicator (hA i)]104105omit [IsProbabilityMeasure μ] in106theorem norm_cellFunctional_apply_le_mask (i : ℕ) (f : Lp 𝕜 1 μ) :107 ‖cellFunctional (𝕜 := 𝕜) μ A hA i f‖ ≤ ‖L1Masks.mask μ (A i) (hA i) f‖ := by108 change ‖L1.integralCLM' 𝕜 (L1Masks.mask μ (A i) (hA i) f)‖ ≤ _109 rw [← L1.integral_eq']110 exact L1.norm_integral_le _111112omit [IsProbabilityMeasure μ] in113theorem norm_sign_cellFunctional_le (s : Finset ℕ)114 (hdisj : Pairwise (fun i j => Disjoint (A i) (A j))) (x : Walsh.Group) :115 ‖∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x • cellFunctional (𝕜 := 𝕜) μ A hA i‖ ≤ 1 := by116 apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one117 intro f118 rw [one_mul, sum_apply]119 calc120 _ ≤ ∑ i ∈ s, ‖Walsh.scalarCharacter 𝕜 {i} x • cellFunctional (𝕜 := 𝕜) μ A hA i f‖ :=121 norm_sum_le _ _122 _ = ∑ i ∈ s, ‖cellFunctional (𝕜 := 𝕜) μ A hA i f‖ := by123 simp only [norm_smul, Walsh.norm_scalarCharacter, one_mul]124 _ ≤ ∑ i ∈ s, ‖L1Masks.mask μ (A i) (hA i) f‖ :=125 Finset.sum_le_sum (fun i _ => norm_cellFunctional_apply_le_mask μ A hA i f)126 _ ≤ ‖f‖ := L1Masks.sum_norm_mask_le μ s A hA hdisj f127128omit [MeasurableSpace Ω] in129private theorem norm_sum_disjoint_indicator_le (s : Finset ℕ)130 (hdisj : Pairwise (fun i j => Disjoint (A i) (A j))) (c : ℕ → 𝕜)131 (hc : ∀ i, ‖c i‖ ≤ 1) (y : Ω) :132 ‖∑ i ∈ s, c i * (A i).indicator (fun _ => (1 : 𝕜)) y‖ ≤ 1 := by133 classical134 by_cases hy : ∃ i ∈ s, y ∈ A i135 · obtain ⟨i, hi, hyi⟩ := hy136 rw [Finset.sum_eq_single i]137 · simpa only [Set.indicator_of_mem hyi, mul_one] using hc i138 · intro j hj hji139 have hyj : y ∉ A j := fun hyj => Set.disjoint_left.mp (hdisj hji) hyj hyi140 simp [Set.indicator_of_notMem hyj]141 · exact fun h => (h hi).elim142 · have hzero : ∀ i ∈ s, y ∉ A i := by simpa using hy143 have hz : (∑ i ∈ s, c i * (A i).indicator (fun _ => (1 : 𝕜)) y) = 0 := by144 apply Finset.sum_eq_zero145 intro i hi146 rw [Set.indicator_of_notMem (hzero i hi), mul_zero]147 rw [hz, norm_zero]148 exact zero_le_one149150set_option backward.isDefEq.respectTransparency false in151theorem norm_sign_cellVector_le (s : Finset ℕ)152 (hdisj : Pairwise (fun i j => Disjoint (A i) (A j))) (x : Walsh.Group) :153 ‖∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x • cellVector (𝕜 := 𝕜) μ A hA i‖ ≤ 1 := by154 have hcoe : (fun y => (∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x • cellVector (𝕜 := 𝕜) μ A hA i) y) =ᵐ[μ]155 (fun y => ∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x *156 (A i).indicator (fun _ => (1 : 𝕜)) y) := by157 refine (Lp.coeFn_fun_finsetSum s _).trans ?_158 filter_upwards [ae_all_iff.2 (fun i => Lp.coeFn_smul159 (Walsh.scalarCharacter 𝕜 {i} x) (cellVector (𝕜 := 𝕜) μ A hA i)),160 ae_all_iff.2 (fun i =>161 (indicatorConstLp_coeFn (p := ∞) (hs := hA i)162 (hμs := measure_ne_top μ (A i)) (c := (1 : 𝕜))))] with y hs hi163 apply Finset.sum_congr rfl164 intro i his165 rw [hs i]166 change Walsh.scalarCharacter 𝕜 {i} x * cellVector (𝕜 := 𝕜) μ A hA i y = _167 rw [show cellVector (𝕜 := 𝕜) μ A hA i y = (A i).indicator (fun _ => (1 : 𝕜)) y from hi i]168 have hn := Lp.norm_le_of_ae_bound169 (f := ∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x • cellVector (𝕜 := 𝕜) μ A hA i)170 zero_le_one (hcoe.mono (fun y hy => by171 exact le_of_eq_of_le (congrArg norm hy) (norm_sum_disjoint_indicator_le A s hdisj _172 (fun i => (Walsh.norm_scalarCharacter 𝕜 {i} x).le) y)))173 simpa using hn174175/-- The trace for an arbitrary finite measurable partition. -/176def partitionTrace (s : Finset ℕ) (R : Lp 𝕜 1 μ →L[𝕜] Lp 𝕜 1 μ) : 𝕜 :=177 finiteTrace s (cellVector (𝕜 := 𝕜) μ A hA) (cellFunctional (𝕜 := 𝕜) μ A hA)178 (R.comp (ProbabilityLp.inclusion μ 1 ∞ le_top))179180theorem norm_partitionTrace_le (s : Finset ℕ)181 (hdisj : Pairwise (fun i j => Disjoint (A i) (A j)))182 (R : Lp 𝕜 1 μ →L[𝕜] Lp 𝕜 1 μ) :183 ‖partitionTrace μ A hA s R‖ ≤ ‖R.comp (ProbabilityLp.inclusion μ 1 ∞ le_top)‖ :=184 norm_finiteTrace_le s (cellVector (𝕜 := 𝕜) μ A hA)185 (cellFunctional (𝕜 := 𝕜) μ A hA)186 (norm_sign_cellVector_le (𝕜 := 𝕜) μ A hA s hdisj)187 (norm_sign_cellFunctional_le (𝕜 := 𝕜) μ A hA s hdisj)188 (R.comp (ProbabilityLp.inclusion μ 1 ∞ le_top))189190theorem inclusion_cellVector (i : ℕ) :191 ProbabilityLp.inclusion μ 1 ∞ le_top (cellVector (𝕜 := 𝕜) μ A hA i) =192 indicatorConstLp 1 (hA i) (measure_ne_top μ (A i)) (1 : 𝕜) := by193 apply Lp.ext194 exact (ProbabilityLp.coeFn_inclusion μ 1 ∞ le_top _).trans195 (indicatorConstLp_coeFn.trans indicatorConstLp_coeFn.symm)196197/-- This is the manuscript's sum of cell integrals of images of cell indicators. -/198theorem partitionTrace_eq (s : Finset ℕ) (R : Lp 𝕜 1 μ →L[𝕜] Lp 𝕜 1 μ) :199 partitionTrace μ A hA s R = ∑ i ∈ s,200 ∫ x in A i, R (indicatorConstLp 1 (hA i) (measure_ne_top μ (A i)) (1 : 𝕜)) x ∂μ := by201 simp only [partitionTrace, finiteTrace, ContinuousLinearMap.comp_apply,202 inclusion_cellVector, cellFunctional_apply]203204theorem partitionTrace_sub (s : Finset ℕ) (R T : Lp 𝕜 1 μ →L[𝕜] Lp 𝕜 1 μ) :205 partitionTrace μ A hA s (R - T) =206 partitionTrace μ A hA s R - partitionTrace μ A hA s T := by207 simp only [partitionTrace, ContinuousLinearMap.sub_comp, finiteTrace_sub]208209theorem partitionTrace_id (s : Finset ℕ)210 (hdisj : Pairwise (fun i j => Disjoint (A i) (A j)))211 (hcover : (⋃ i ∈ s, A i) = Set.univ) :212 partitionTrace (𝕜 := 𝕜) μ A hA s (ContinuousLinearMap.id 𝕜 (Lp 𝕜 1 μ)) = 1 := by213 rw [partitionTrace_eq]214 simp only [ContinuousLinearMap.id_apply]215 have hi (i : ℕ) : (∫ x in A i,216 indicatorConstLp 1 (hA i) (measure_ne_top μ (A i)) (1 : 𝕜) x ∂μ) =217 (μ.real (A i) : 𝕜) := by218 rw [integral_congr_ae (ae_restrict_of_ae indicatorConstLp_coeFn)]219 rw [setIntegral_indicator (hA i)]220 simp [Algebra.smul_def]221 simp_rw [hi]222 rw [← RCLike.ofReal_sum]223 have hm : ∑ i ∈ s, μ.real (A i) = 1 := by224 rw [← measureReal_biUnion_finset (fun i _ j _ hij => hdisj hij)225 (fun i _ => hA i) (fun i _ => measure_ne_top μ (A i)), hcover]226 simp227 rw [hm, RCLike.ofReal_one]228229end MeasurablePartition230231section PartitionSequence232233variable {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ]234variable (A : ℕ → ℕ → Set Ω) (hA : ∀ n i, MeasurableSet (A n i)) (s : ℕ → Finset ℕ)235 (hdisj : ∀ n, Pairwise (fun i j => Disjoint (A n i) (A n j)))236237include hdisj238239/-- Vanishing traces force distance at least one from the identity in the240L-infinity to L1 norm. -/241theorem one_le_norm_id_sub_of_trace_tendsto_zero242 (hcover : ∀ n, (⋃ i ∈ s n, A n i) = Set.univ)243 (R : Lp 𝕜 1 μ →L[𝕜] Lp 𝕜 1 μ)244 (hR : Filter.Tendsto (fun n => partitionTrace μ (A n) (hA n) (s n) R)245 Filter.atTop (𝓝 0)) :246 1 ≤ ‖(ContinuousLinearMap.id 𝕜 (Lp 𝕜 1 μ) - R).comp247 (ProbabilityLp.inclusion μ 1 ∞ le_top)‖ := by248 have ht : Filter.Tendsto (fun n =>249 ‖partitionTrace μ (A n) (hA n) (s n) (ContinuousLinearMap.id 𝕜 (Lp 𝕜 1 μ) - R)‖)250 Filter.atTop (𝓝 1) := by251 simpa only [partitionTrace_sub, partitionTrace_id μ _ _ _ (hdisj _) (hcover _),252 sub_zero, norm_one] using253 ((tendsto_const_nhds : Tendsto (fun _ : ℕ => (1 : 𝕜)) atTop (𝓝 1)).sub hR).norm254 exact le_of_tendsto ht (Filter.Eventually.of_forall (fun n =>255 norm_partitionTrace_le μ (A n) (hA n) (s n) (hdisj n) _))256257/-- The trace-vanishing condition is preserved by approximation in the258L-infinity to L1 norm, the topology used in the matrix argument. -/259theorem trace_tendsto_zero_of_approximation260 (R : Lp 𝕜 1 μ →L[𝕜] Lp 𝕜 1 μ)261 (T : ℕ → Lp 𝕜 1 μ →L[𝕜] Lp 𝕜 1 μ)262 (hT : ∀ m, Filter.Tendsto (fun n => partitionTrace μ (A n) (hA n) (s n) (T m))263 Filter.atTop (𝓝 0))264 (happrox : Filter.Tendsto (fun m => ‖(R - T m).comp265 (ProbabilityLp.inclusion μ 1 ∞ le_top)‖) Filter.atTop (𝓝 0)) :266 Filter.Tendsto (fun n => partitionTrace μ (A n) (hA n) (s n) R)267 Filter.atTop (𝓝 0) := by268 apply Metric.tendsto_atTop.mpr269 intro ε hε270 obtain ⟨m, hm⟩ := Filter.Eventually.exists271 (happrox.eventually (gt_mem_nhds (half_pos hε)))272 obtain ⟨N, hN⟩ := Metric.tendsto_atTop.mp (hT m) (ε / 2) (half_pos hε)273 refine ⟨N, fun n hn => ?_⟩274 rw [dist_zero_right]275 have herr := norm_partitionTrace_le μ (A n) (hA n) (s n) (hdisj n) (R - T m)276 rw [partitionTrace_sub] at herr277 have hn' := hN n hn278 rw [dist_zero_right] at hn'279 have htri := norm_add_le280 (partitionTrace μ (A n) (hA n) (s n) R - partitionTrace μ (A n) (hA n) (s n) (T m))281 (partitionTrace μ (A n) (hA n) (s n) (T m))282 rw [sub_add_cancel] at htri283 linarith284285end PartitionSequence286287end PL1.TraceBounds288289