Stat.Privacy
Differential privacy via the Laplace mechanism: the centered Laplace distribution and its density-ratio bound, scalar and finite-dimensional additive-noise release, pure and approximate ε-differential-privacy guarantees, post-processing closure, and Laplace-noise moment bounds.
LaplaceMechanism 9 core · 8 supporting This file supplies the classical centred Laplace distribution, its density-ratio bound, scalar and finite-dimensional Laplace mechanisms, and post-processing lemmas. ★ laplaceMech_pure_dp★ laplaceMechPi_pure_dp★ pure_dp_implies_approx_dp★ pure_dp_postprocess★ approx_dp_postprocess
The Laplace mechanism and pure differential privacy
This file supplies the classical centred Laplace distribution, its density-ratio bound, scalar and finite-dimensional Laplace mechanisms, and post-processing lemmas. Dataset types and adjacency relations remain completely abstract.
def laplacePDF reviewed
⚑ flagged
Causalean.Stat.Privacy
The centered Laplace density at a real value decays exponentially with its absolute distance from zero and is normalized by twice its positive scale.
Definition (Lean source)
def laplacePDF (b x : ℝ) : ℝ := (2 * b)⁻¹ * exp (-|x| / b)
def laplaceMeasure reviewed
⚑ flagged
Causalean.Stat.Privacy
The centered Laplace distribution is obtained by weighting Lebesgue measure with the centered Laplace density at the chosen scale.
Definition (Lean source)
def laplaceMech reviewed
⚑ flagged
Causalean.Stat.Privacy
The scalar Laplace mechanism releases a real-valued query after adding independent centered Laplace noise at the chosen scale.
Definition (Lean source)
def laplaceMech {D : Type*} (b : ℝ) (q : D → ℝ) : D → Measure ℝ :=
fun d => (laplaceMeasure b).map (fun z => z + q d)
theorem laplaceMech_pure_dp reviewed
⚑ flagged
Causalean.Stat.Privacy
Scalar Laplace mechanism is purely differentially private. Given a positive sensitivity bound and a positive privacy level such that the query q changes by at most between any pair of adjacent datasets, releasing q after adding independent Laplace noise of scale satisfies pure -differential privacy: for every adjacent pair, the probability of any measurable event under one release is at most times its probability under the other.
Formal statement
hypotheses
D :
Type*
Adj :
D → D → Prop
q :
D → ℝ
Δ ε :
ℝ
hΔ :
0 < Δ
hε :
0 < ε
hsens :
∀ d d'
if
Adj d d'
then
|q d - q d'| ≤ Δ
conclusion
∀ d d',
Proof (Lean source)
theorem laplaceMech_pure_dp {D : Type*} (Adj : D → D → Prop) (q : D → ℝ)
{Δ ε : ℝ} (hΔ : 0 < Δ) (hε : 0 < ε)
(hsens : ∀ d d', Adj d d' → |q d - q d'| ≤ Δ) :
∀ d d', Adj d d' → ∀ s, MeasurableSet s →
(laplaceMech (Δ / ε) q d).real s ≤
exp ε * (laplaceMech (Δ / ε) q d').real s := by
intro d d' hadd s hs
have hb : 0 < Δ / ε := div_pos hΔ hε
have hscale : |q d - q d'| / (Δ / ε) ≤ ε := by
apply (div_le_iff₀ hb).2
calc
|q d - q d'| ≤ Δ := hsens d d' hadd
_ = ε * (Δ / ε) := by field_simp
have hpdf (x : ℝ) : laplacePDF (Δ / ε) (x - q d) ≤
exp ε * laplacePDF (Δ / ε) (x - q d') := by
calc
laplacePDF (Δ / ε) (x - q d) ≤
exp (|q d - q d'| / (Δ / ε)) *
laplacePDF (Δ / ε) (x - q d') :=
laplacePDF_shift_le (Δ / ε) (q d) (q d') x hb
_ ≤ exp ε * laplacePDF (Δ / ε) (x - q d') := by
exact mul_le_mul_of_nonneg_right (Real.exp_le_exp.mpr hscale)
(laplacePDF_nonneg hb _)
have hmeasure : laplaceMech (Δ / ε) q d ≤
(ofReal (exp ε)) • laplaceMech (Δ / ε) q d' := by
rw [laplaceMech_eq_withDensity, laplaceMech_eq_withDensity]
let f : ℝ → ENNReal :=
fun x => ofReal (laplacePDF (Δ / ε) (x - q d'))
have hf : Measurable f :=
((measurable_laplacePDF (Δ / ε)).comp (by fun_prop)).ennreal_ofReal
change volume.withDensity _ ≤ ofReal (exp ε) • volume.withDensity f
rw [← withDensity_smul (μ := volume) (ofReal (exp ε)) hf]
apply withDensity_mono
filter_upwards with x
change ofReal (laplacePDF (Δ / ε) (x - q d)) ≤
ofReal (exp ε) *
ofReal (laplacePDF (Δ / ε) (x - q d'))
rw [← ENNReal.ofReal_mul (Real.exp_pos ε).le]
exact ENNReal.ofReal_le_ofReal (hpdf x)
have hle := hmeasure s
rw [Measure.smul_apply] at hle
letI : IsProbabilityMeasure (laplaceMech (Δ / ε) q d) :=
laplaceMech_isProbabilityMeasure (Δ / ε) hb q d
letI : IsProbabilityMeasure (laplaceMech (Δ / ε) q d') :=
laplaceMech_isProbabilityMeasure (Δ / ε) hb q d'
change ((laplaceMech (Δ / ε) q d) s).toReal ≤
exp ε * ((laplaceMech (Δ / ε) q d') s).toReal
rw [← ENNReal.toReal_ofReal (Real.exp_pos ε).le, ← ENNReal.toReal_mul]
· exact ENNReal.toReal_mono
(ENNReal.mul_ne_top ENNReal.ofReal_ne_top
(measure_ne_top (laplaceMech (Δ / ε) q d') s)) hle
def laplaceMechPi reviewed
⚑ flagged
Causalean.Stat.Privacy
The finite-dimensional Laplace mechanism releases a vector-valued query after adding mutually independent centered Laplace noise to its coordinates.
Definition (Lean source)
def laplaceMechPi {D ι : Type*} [Fintype ι] (b : ℝ) (q : D → (ι → ℝ)) :
D → Measure (ι → ℝ) :=
fun d => (Measure.pi (fun _ : ι => laplaceMeasure b)).map (fun z => z + q d)
theorem laplaceMechPi_pure_dp reviewed
⚑ flagged
Causalean.Stat.Privacy
Vector Laplace mechanism is purely differentially private. Given a positive -sensitivity bound and a positive privacy level such that the coordinatewise absolute differences of the query q sum to at most between any pair of adjacent datasets, releasing q after adding independent Laplace noise of scale to each coordinate satisfies pure -differential privacy: for every adjacent pair, the probability of any measurable event under one release is at most times its probability under the other.
Formal statement
hypotheses
D ι :
Type*
Fintype ι
Adj :
D → D → Prop
q :
D → (ι → ℝ)
Δ ε :
ℝ
hΔ :
0 < Δ
hε :
0 < ε
hsens :
∀ d d'
if
Adj d d'
then
∑ i, |q d i - q d' i| ≤ Δ
conclusion
∀ d d',
Proof (Lean source)
theorem laplaceMechPi_pure_dp {D ι : Type*} [Fintype ι]
(Adj : D → D → Prop) (q : D → (ι → ℝ)) {Δ ε : ℝ}
(hΔ : 0 < Δ) (hε : 0 < ε)
(hsens : ∀ d d', Adj d d' → ∑ i, |q d i - q d' i| ≤ Δ) :
∀ d d', Adj d d' → ∀ s, MeasurableSet s →
(laplaceMechPi (Δ / ε) q d).real s ≤
exp ε * (laplaceMechPi (Δ / ε) q d').real s := by
intro d d' hadd s hs
have hb : 0 < Δ / ε := div_pos hΔ hε
let μ : ι → Measure ℝ :=
fun i => (laplaceMeasure (Δ / ε)).map (fun z => z + q d i)
let ν : ι → Measure ℝ :=
fun i => (laplaceMeasure (Δ / ε)).map (fun z => z + q d' i)
let c : ι → ENNReal :=
fun i => ofReal (exp (|q d i - q d' i| / (Δ / ε)))
letI (i : ι) : IsProbabilityMeasure (μ i) := by
dsimp [μ]
letI := laplaceMeasure_isProbabilityMeasure (Δ / ε) hb
exact Measure.isProbabilityMeasure_map (by fun_prop)
letI (i : ι) : IsProbabilityMeasure (ν i) := by
dsimp [ν]
letI := laplaceMeasure_isProbabilityMeasure (Δ / ε) hb
exact Measure.isProbabilityMeasure_map (by fun_prop)
have hpi : Measure.pi μ ≤ (∏ i, c i) • Measure.pi ν :=
pi_le_smul_pi μ ν c (fun i => laplace_shift_measure_le _ _ _ hb)
have hsum : (∑ i, |q d i - q d' i| / (Δ / ε)) ≤ ε := by
rw [← Finset.sum_div]
apply (div_le_iff₀ hb).2
calc
(∑ i, |q d i - q d' i|) ≤ Δ := hsens d d' hadd
_ = ε * (Δ / ε) := by field_simp
have hc : (∏ i, c i) ≤ ofReal (exp ε) := by
change (∏ i, ofReal (exp (|q d i - q d' i| / (Δ / ε)))) ≤ _
rw [← ENNReal.ofReal_prod_of_nonneg (fun i _ => (Real.exp_pos _).le),
← Real.exp_sum]
exact ENNReal.ofReal_le_ofReal (Real.exp_le_exp.mpr hsum)
have hmeasure : laplaceMechPi (Δ / ε) q d ≤
ofReal (exp ε) • laplaceMechPi (Δ / ε) q d' := by
rw [laplaceMechPi_eq_pi_shift (hb := hb), laplaceMechPi_eq_pi_shift (hb := hb)]
apply hpi.trans
rw [Measure.le_iff']
intro t
simp only [Measure.smul_apply, smul_eq_mul]
change (∏ i, c i) * (Measure.pi ν) t ≤
ofReal (exp ε) * (Measure.pi ν) t
gcongr
have hle := hmeasure s
rw [Measure.smul_apply] at hle
letI := laplaceMechPi_isProbabilityMeasure (Δ / ε) hb q d
letI := laplaceMechPi_isProbabilityMeasure (Δ / ε) hb q d'
change ((laplaceMechPi (Δ / ε) q d) s).toReal ≤
exp ε * ((laplaceMechPi (Δ / ε) q d') s).toReal
rw [← ENNReal.toReal_ofReal (Real.exp_pos ε).le, ← ENNReal.toReal_mul]
exact ENNReal.toReal_mono
(ENNReal.mul_ne_top ENNReal.ofReal_ne_top
(measure_ne_top (laplaceMechPi (Δ / ε) q d') s)) hle
theorem pure_dp_implies_approx_dp reviewed
⚑ flagged
Causalean.Stat.Privacy
Pure DP implies approximate DP. Given a mechanism M satisfying pure -differential privacy between releases M d and M d', i.e. the probability of every measurable event under one release is at most times its probability under the other, adding any nonnegative failure allowance to the bound still yields a valid -approximate differential-privacy guarantee between M d and M d'.
Formal statement
Proof (Lean source)
theorem pure_dp_implies_approx_dp {α : Type*} [MeasurableSpace α]
(M : D → Measure α) (d d' : D) (ε δ : ℝ)
(hpure : ∀ s, MeasurableSet s →
(M d).real s ≤ exp ε * (M d').real s) (hδ : 0 ≤ δ) :
∀ s, MeasurableSet s →
(M d).real s ≤ exp ε * (M d').real s + δ := by
intro s hs
exact (hpure s hs).trans (le_add_of_nonneg_right hδ)
theorem pure_dp_postprocess reviewed
⚑ flagged
Causalean.Stat.Privacy
Post-processing preserves pure differential privacy. Given a vector-valued mechanism M satisfying pure -differential privacy between the releases M d and M d', post-processing the release by any measurable scalar summary f again satisfies pure -differential privacy, now between the f-summaries of M d and M d'.
Formal statement
hypotheses
Proof (Lean source)
theorem pure_dp_postprocess {D ι : Type*}
(M : D → Measure (ι → ℝ)) (d d' : D) (ε : ℝ)
(hM : ∀ s, MeasurableSet s →
(M d).real s ≤ exp ε * (M d').real s)
(f : (ι → ℝ) → ℝ) (hf : Measurable f) :
∀ s, MeasurableSet s →
((M d).map f).real s ≤ exp ε * ((M d').map f).real s := by
intro s hs
change ((M d).map f s).toReal ≤ exp ε * ((M d').map f s).toReal
rw [Measure.map_apply hf hs, Measure.map_apply hf hs]
exact hM (f ⁻¹' s) (hs.preimage hf)
theorem approx_dp_postprocess reviewed
⚑ flagged
Causalean.Stat.Privacy
Post-processing preserves approximate differential privacy. Given a vector-valued mechanism M obeying an -approximate DP bound between the releases M d and M d' for every measurable event, with a nonnegative failure allowance , post-processing the release by any measurable scalar summary f again satisfies the same -approximate DP bound, now between the f-summaries of M d and M d'.
Formal statement
hypotheses
Proof (Lean source)
theorem approx_dp_postprocess {D ι : Type*}
(M : D → Measure (ι → ℝ)) (d d' : D) (ε δ : ℝ)
(hM : ∀ s, MeasurableSet s →
(M d).real s ≤ exp ε * (M d').real s + δ)
(_hδ : 0 ≤ δ) (f : (ι → ℝ) → ℝ) (hf : Measurable f) :
∀ s, MeasurableSet s →
((M d).map f).real s ≤
exp ε * ((M d').map f).real s + δ := by
intro s hs
change ((M d).map f s).toReal ≤ exp ε * ((M d').map f s).toReal + δ
rw [Measure.map_apply hf hs, Measure.map_apply hf hs]
exact hM (f ⁻¹' s) (hs.preimage hf)
8 supporting declarations (lemmas, instances)
-
laplaceMeasure_isProbabilityMeasuretheorem — At every positive scale, the centered Laplace measure has total mass one and therefore defines a probability distribution.Proof (Lean source)
theorem laplaceMeasure_isProbabilityMeasure (b : ℝ) (hb : 0 < b) : IsProbabilityMeasure (laplaceMeasure b) := by refine ⟨?_⟩ rw [laplaceMeasure, withDensity_apply _ MeasurableSet.univ] rw [Measure.restrict_univ] have hdens : (fun x => ofReal (laplacePDF b x)) = fun x => (Real.toNNReal (laplacePDF b x) : ENNReal) := by funext x rw [ENNReal.ofReal_eq_coe_nnreal (laplacePDF_nonneg hb x)] congr 1 ext simp [Real.toNNReal_of_nonneg (laplacePDF_nonneg hb x)] rw [hdens, lintegral_coe_eq_integral] · convert congrArg ofReal (integral_laplacePDF hb) using 1 <;> simp [max_eq_left (laplacePDF_nonneg hb _)] · simpa [Real.toNNReal_of_nonneg, laplacePDF_nonneg hb] using integrable_laplacePDF hb -
laplacePDF_shift_letheorem — Moving the center of a positive-scale Laplace density changes its value at any observation by at most an exponential factor determined by the distance between the old and new centers divided by the scale.hypothesesb u v z :ℝhb :0 < bconclusionProof (Lean source)
theorem laplacePDF_shift_le (b u v z : ℝ) (hb : 0 < b) : laplacePDF b (z - u) ≤ exp (|u - v| / b) * laplacePDF b (z - v) := by have htri : |z - v| - |z - u| ≤ |u - v| := by calc |z - v| - |z - u| ≤ |(z - v) - (z - u)| := abs_sub_abs_le_abs_sub (z - v) (z - u) _ = |u - v| := by congr 1; simp have hexp : exp (-|z - u| / b) ≤ exp (|u - v| / b) * exp (-|z - v| / b) := by rw [← Real.exp_add, Real.exp_le_exp] rw [show |u - v| / b + -|z - v| / b = (|u - v| - |z - v|) / b by ring] exact (div_le_div_iff_of_pos_right hb).2 (by linarith) unfold laplacePDF calc (2 * b)⁻¹ * exp (-|z - u| / b) ≤ (2 * b)⁻¹ * (exp (|u - v| / b) * exp (-|z - v| / b)) := mul_le_mul_of_nonneg_left hexp (by positivity) _ = exp (|u - v| / b) * ((2 * b)⁻¹ * exp (-|z - v| / b)) := by ring -
laplaceMech_isProbabilityMeasuretheorem — Adding positive-scale Laplace noise to a scalar query produces a probability distribution for the release under every dataset.hypothesesD :Type*b :ℝhb :0 < bq :D → ℝd :DconclusionIsProbabilityMeasure (laplaceMech b q d)Proof (Lean source)
theorem laplaceMech_isProbabilityMeasure {D : Type*} (b : ℝ) (hb : 0 < b) (q : D → ℝ) (d : D) : IsProbabilityMeasure (laplaceMech b q d) := by letI : IsProbabilityMeasure (laplaceMeasure b) := laplaceMeasure_isProbabilityMeasure b hb unfold laplaceMech exact Measure.isProbabilityMeasure_map (by fun_prop) -
laplaceMechPi_isProbabilityMeasuretheorem — Adding independent positive-scale Laplace noise in finitely many coordinates produces a probability distribution for the vector release under every dataset.hypothesesconclusionIsProbabilityMeasure (laplaceMechPi b q d)Proof (Lean source)
theorem laplaceMechPi_isProbabilityMeasure {D ι : Type*} [Fintype ι] (b : ℝ) (hb : 0 < b) (q : D → (ι → ℝ)) (d : D) : IsProbabilityMeasure (laplaceMechPi b q d) := by letI : IsProbabilityMeasure (laplaceMeasure b) := laplaceMeasure_isProbabilityMeasure b hb haveI : IsProbabilityMeasure (Measure.pi (fun _ : ι => laplaceMeasure b)) := inferInstance unfold laplaceMechPi exact Measure.isProbabilityMeasure_map (by fun_prop) -
laplaceMeasure_integrable_abstheorem — The absolute value of a centered Laplace draw has a finite expectation at every positive scale.Proof (Lean source)
theorem laplaceMeasure_integrable_abs (b : ℝ) (hb : 0 < b) : Integrable (fun x : ℝ => |x|) (laplaceMeasure b) := by rw [laplaceMeasure, integrable_withDensity_iff_integrable_smul' (measurable_laplacePDF b).ennreal_ofReal (ae_of_all _ fun _ => ENNReal.ofReal_lt_top)] simpa only [ENNReal.toReal_ofReal (laplacePDF_nonneg hb _), smul_eq_mul, mul_comm] using integrable_abs_mul_laplacePDF b hb -
laplaceMeasure_integral_abstheorem — The expected absolute value of a centered Laplace draw equals its positive scale.Proof (Lean source)
theorem laplaceMeasure_integral_abs (b : ℝ) (hb : 0 < b) : ∫ x, |x| ∂(laplaceMeasure b) = b := by rw [laplaceMeasure, integral_withDensity_eq_integral_toReal_smul (measurable_laplacePDF b).ennreal_ofReal (ae_of_all _ fun _ => ENNReal.ofReal_lt_top)] simp_rw [ENNReal.toReal_ofReal (laplacePDF_nonneg hb _), smul_eq_mul] let f : ℝ → ℝ := fun x => (2 * b)⁻¹ * (x * exp (-x / b)) rw [show (fun x : ℝ => laplacePDF b x * |x|) = fun x => f |x| by funext x simp only [f, laplacePDF] ring, integral_comp_abs] have hplain : (∫ x in Ioi (0 : ℝ), x * exp (-x / b)) = b ^ 2 := by calc _ = ∫ x in Ioi (0 : ℝ), x ^ ((2 : ℝ) - 1) * exp (-((1 / b) * x)) := by apply setIntegral_congr_fun measurableSet_Ioi intro x hx simp only [show (2 : ℝ) - 1 = 1 by norm_num, Real.rpow_one] rw [show -x / b = -(1 / b * x) by ring] _ = (1 / (1 / b)) ^ (2 : ℝ) * Real.Gamma (2 : ℝ) := Real.integral_rpow_mul_exp_neg_mul_Ioi (by norm_num) (one_div_pos.mpr hb) _ = b ^ 2 := by rw [show Real.Gamma (2 : ℝ) = 1 by norm_num] field_simp [hb.ne'] exact Real.rpow_natCast b 2 have hright : (∫ x in Ioi (0 : ℝ), f x) = (2 * b)⁻¹ * b ^ 2 := by rw [show f = fun x => (2 * b)⁻¹ * (x * exp (-x / b)) by rfl, integral_const_mul, hplain] rw [hright] field_simp [hb.ne'] -
laplacePi_integral_euclidean_norm_letheorem — The expected Euclidean norm of a finite vector of independent centered Laplace draws is at most the number of coordinates times their common positive scale.hypothesesconclusion∫ w, sqrt (∑ i : ι, (w i) ^ 2) ∂(Measure.pi fun _ : ι => laplaceMeasure b)≤ (Fintype.card ι : ℝ) * bProof (Lean source)
theorem laplacePi_integral_euclidean_norm_le {ι : Type*} [Fintype ι] (b : ℝ) (hb : 0 < b) : ∫ w, sqrt (∑ i : ι, (w i) ^ 2) ∂(Measure.pi fun _ : ι => laplaceMeasure b) ≤ (Fintype.card ι : ℝ) * b := by letI : IsProbabilityMeasure (laplaceMeasure b) := laplaceMeasure_isProbabilityMeasure b hb let P : Measure (ι → ℝ) := Measure.pi fun _ : ι => laplaceMeasure b have hcoord (i : ι) : Integrable (fun w : ι → ℝ => |w i|) P := integrable_comp_eval (laplaceMeasure_integrable_abs b hb) have hsum : Integrable (fun w : ι → ℝ => ∑ i : ι, |w i|) P := integrable_finset_sum _ fun i _ => hcoord i have hnorm : Integrable (fun w : ι → ℝ => sqrt (∑ i : ι, (w i) ^ 2)) P := by have hcontinuous : Continuous (fun w : ι → ℝ => sqrt (∑ i : ι, (w i) ^ 2)) := Real.continuous_sqrt.comp (continuous_finset_sum _ fun i _ => (continuous_apply i).pow 2) refine hsum.mono' hcontinuous.aestronglyMeasurable (ae_of_all _ fun w => ?_) rw [Real.norm_of_nonneg (Real.sqrt_nonneg _)] exact sqrt_sum_sq_le_sum_abs w calc ∫ w, sqrt (∑ i : ι, (w i) ^ 2) ∂P ≤ ∫ w, ∑ i : ι, |w i| ∂P := integral_mono hnorm hsum (sqrt_sum_sq_le_sum_abs) _ = ∑ i : ι, ∫ w, |w i| ∂P := integral_finset_sum _ fun i _ => hcoord i _ = ∑ _i : ι, b := by congr 1 with i change (∫ w : ι → ℝ, |w i| ∂Measure.pi (fun _ : ι => laplaceMeasure b)) = b exact (integral_comp_eval (μ := fun _ : ι => laplaceMeasure b) (i := i) (f := fun x : ℝ => |x|) (Continuous.aestronglyMeasurable continuous_abs)).trans (laplaceMeasure_integral_abs b hb) _ = (Fintype.card ι : ℝ) * b := by simp -
laplacePi_integrable_euclidean_normtheorem — The Euclidean norm of finitely many independent centered Laplace draws has a finite expectation whenever their common scale is positive.hypothesesconclusionProof (Lean source)
theorem laplacePi_integrable_euclidean_norm {ι : Type*} [Fintype ι] (b : ℝ) (hb : 0 < b) : Integrable (fun w : ι → ℝ => sqrt (∑ i : ι, (w i) ^ 2)) (Measure.pi fun _ : ι => laplaceMeasure b) := by letI : IsProbabilityMeasure (laplaceMeasure b) := laplaceMeasure_isProbabilityMeasure b hb have hcoord (i : ι) : Integrable (fun w : ι → ℝ => |w i|) (Measure.pi fun _ : ι => laplaceMeasure b) := integrable_comp_eval (laplaceMeasure_integrable_abs b hb) have hsum : Integrable (fun w : ι → ℝ => ∑ i : ι, |w i|) (Measure.pi fun _ : ι => laplaceMeasure b) := integrable_finset_sum _ fun i _ => hcoord i have hcontinuous : Continuous (fun w : ι → ℝ => sqrt (∑ i : ι, (w i) ^ 2)) := Real.continuous_sqrt.comp (continuous_finset_sum _ fun i _ => (continuous_apply i).pow 2) refine hsum.mono' hcontinuous.aestronglyMeasurable (ae_of_all _ fun w => ?_) rw [Real.norm_of_nonneg (Real.sqrt_nonneg _)] exact sqrt_sum_sq_le_sum_abs w