PL1/HilbertTraceBounds.lean
All source files · Download exact source
SHA-256: 7f47d00efca220abf4f91769712502309f9ed3b845f0e13c892daf36c2394ca0
1import PL1.TraceBounds2import Mathlib.Analysis.InnerProductSpace.Dual34/-! # Hilbert space bounds for finite partition traces -/56noncomputable section7set_option autoImplicit false8set_option maxHeartbeats 8000009open MeasureTheory Filter10open scoped ENNReal BigOperators Topology1112namespace PL1.HilbertTraceBounds1314variable {𝕜 H : Type*} [RCLike 𝕜] [NormedAddCommGroup H]15 [InnerProductSpace 𝕜 H] [CompleteSpace H]1617theorem integral_norm_sign_sum_sq (s : Finset ℕ) (v : ℕ → H) :18 (∫ x, ‖∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x • v i‖ ^ 2 ∂Walsh.haar) =19 ∑ i ∈ s, ‖v i‖ ^ 2 := by20 have h := TraceBounds.finiteTrace_eq_sign_average s v21 (fun i => InnerProductSpace.toDual 𝕜 H (v i)) (ContinuousLinearMap.id 𝕜 H)22 have hsum (x : Walsh.Group) :23 (∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x • InnerProductSpace.toDual 𝕜 H (v i)) =24 InnerProductSpace.toDual 𝕜 H (∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x • v i) := by25 simp only [map_sum, map_smulₛₗ, starRingEnd_apply, Walsh.star_scalarCharacter]26 simp only [TraceBounds.finiteTrace, ContinuousLinearMap.id_apply,27 InnerProductSpace.toDual_apply_apply, inner_self_eq_norm_sq_to_K] at h28 simp_rw [hsum, InnerProductSpace.toDual_apply_apply, inner_self_eq_norm_sq_to_K] at h29 have hc : ((∑ i ∈ s, ‖v i‖ ^ 2 : ℝ) : 𝕜) =30 ((∫ x, ‖∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x • v i‖ ^ 2 ∂Walsh.haar : ℝ) : 𝕜) := by31 simp only [← RCLike.ofReal_pow] at h32 rw [integral_ofReal] at h33 simpa only [RCLike.ofReal_sum] using h34 exact (RCLike.ofReal_injective hc).symm3536theorem sum_norm_sq_le_of_sign_bound (s : Finset ℕ) (v : ℕ → H) (C : ℝ)37 (_hC : 0 ≤ C)38 (hv : ∀ x : Walsh.Group, ‖∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x • v i‖ ≤ C) :39 (∑ i ∈ s, ‖v i‖ ^ 2) ≤ C ^ 2 := by40 rw [← integral_norm_sign_sum_sq (𝕜 := 𝕜) s v]41 have hint := integral_mono_of_nonneg (μ := Walsh.haar)42 (ae_of_all _ (fun x => sq_nonneg _)) (integrable_const (C ^ 2))43 (ae_of_all _ (fun x => pow_le_pow_left₀ (norm_nonneg _) (hv x) 2))44 simpa using hint4546theorem sum_dual_norm_sq_le_of_sign_bound (s : Finset ℕ) (φ : ℕ → H →L[𝕜] 𝕜)47 (C : ℝ) (hC : 0 ≤ C)48 (hφ : ∀ x : Walsh.Group, ‖∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x • φ i‖ ≤ C) :49 (∑ i ∈ s, ‖φ i‖ ^ 2) ≤ C ^ 2 := by50 let v (i : ℕ) : H := (InnerProductSpace.toDual 𝕜 H).symm (φ i)51 have hv : ∀ x : Walsh.Group, ‖∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x • v i‖ ≤ C := by52 intro x53 have heq : (∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x • v i) =54 (InnerProductSpace.toDual 𝕜 H).symm55 (∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x • φ i) := by56 simp only [map_sum, map_smulₛₗ, starRingEnd_apply, Walsh.star_scalarCharacter, v]57 rw [heq, LinearIsometryEquiv.norm_map]58 exact hφ x59 simpa only [v, LinearIsometryEquiv.norm_map] using60 sum_norm_sq_le_of_sign_bound (𝕜 := 𝕜) s v C hC hv6162theorem norm_sum_dual_apply_le (s : Finset ℕ) (φ : ℕ → H →L[𝕜] 𝕜)63 (v : ℕ → H) (C : ℝ) (hC : 0 ≤ C)64 (hφ : ∀ x : Walsh.Group, ‖∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x • φ i‖ ≤ C) :65 ‖∑ i ∈ s, φ i (v i)‖ ≤ C * Real.sqrt (∑ i ∈ s, ‖v i‖ ^ 2) := by66 calc67 _ ≤ ∑ i ∈ s, ‖φ i (v i)‖ := norm_sum_le _ _68 _ ≤ ∑ i ∈ s, ‖φ i‖ * ‖v i‖ := Finset.sum_le_sum (fun i _ => (φ i).le_opNorm _)69 _ ≤ Real.sqrt (∑ i ∈ s, ‖φ i‖ ^ 2) * Real.sqrt (∑ i ∈ s, ‖v i‖ ^ 2) :=70 Real.sum_mul_le_sqrt_mul_sqrt s _ _71 _ ≤ C * Real.sqrt (∑ i ∈ s, ‖v i‖ ^ 2) := by72 apply mul_le_mul_of_nonneg_right _ (Real.sqrt_nonneg _)73 exact (Real.sqrt_le_sqrt (sum_dual_norm_sq_le_of_sign_bound s φ C hC hφ)).trans_eq74 (Real.sqrt_sq hC)7576section Partition7778variable {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω)79 (A : ℕ → Set Ω) (hA : ∀ i, MeasurableSet (A i))8081/-- The square sum of Hilbert dual rows is controlled by the operator norm, without82choosing any L-infinity representative of a Banach dual functional. -/83theorem sum_cell_dual_norm_sq_le (s : Finset ℕ)84 (hdisj : Pairwise (fun i j => Disjoint (A i) (A j)))85 (T : H →L[𝕜] Lp 𝕜 1 μ) :86 (∑ i ∈ s, ‖(TraceBounds.cellFunctional (𝕜 := 𝕜) μ A hA i).comp T‖ ^ 2) ≤ ‖T‖ ^ 2 := by87 apply sum_dual_norm_sq_le_of_sign_bound s _ ‖T‖ (norm_nonneg _)88 intro x89 have heq : (∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x •90 (TraceBounds.cellFunctional (𝕜 := 𝕜) μ A hA i).comp T) =91 (∑ i ∈ s, Walsh.scalarCharacter 𝕜 {i} x •92 TraceBounds.cellFunctional (𝕜 := 𝕜) μ A hA i).comp T := by93 apply ContinuousLinearMap.ext94 intro y95 simp only [sum_apply, smul_apply, ContinuousLinearMap.comp_apply]96 rw [heq]97 exact (ContinuousLinearMap.opNorm_comp_le _ _).trans (by98 simpa only [one_mul] using mul_le_mul_of_nonneg_right99 (TraceBounds.norm_sign_cellFunctional_le μ A hA s hdisj x) (norm_nonneg T))100101theorem norm_sum_cell_apply_le (s : Finset ℕ)102 (hdisj : Pairwise (fun i j => Disjoint (A i) (A j)))103 (T : H →L[𝕜] Lp 𝕜 1 μ) (v : ℕ → H) :104 ‖∑ i ∈ s, TraceBounds.cellFunctional (𝕜 := 𝕜) μ A hA i (T (v i))‖ ≤105 ‖T‖ * Real.sqrt (∑ i ∈ s, ‖v i‖ ^ 2) := by106 calc107 _ ≤ ∑ i ∈ s, ‖(TraceBounds.cellFunctional (𝕜 := 𝕜) μ A hA i).comp T (v i)‖ :=108 norm_sum_le _ _109 _ ≤ ∑ i ∈ s, ‖(TraceBounds.cellFunctional (𝕜 := 𝕜) μ A hA i).comp T‖ * ‖v i‖ :=110 Finset.sum_le_sum (fun i _ => ContinuousLinearMap.le_opNorm _ _)111 _ ≤ Real.sqrt (∑ i ∈ s, ‖(TraceBounds.cellFunctional (𝕜 := 𝕜) μ A hA i).comp T‖ ^ 2) *112 Real.sqrt (∑ i ∈ s, ‖v i‖ ^ 2) := Real.sum_mul_le_sqrt_mul_sqrt s _ _113 _ ≤ ‖T‖ * Real.sqrt (∑ i ∈ s, ‖v i‖ ^ 2) := by114 apply mul_le_mul_of_nonneg_right _ (Real.sqrt_nonneg _)115 exact (Real.sqrt_le_sqrt (sum_cell_dual_norm_sq_le μ A hA s hdisj T)).trans_eq116 (Real.sqrt_sq (norm_nonneg T))117118end Partition119120end PL1.HilbertTraceBounds121