Moved Gaussian to util

leanprover · May 15, 2024 · b5f2c29 · b5f2c29
1 parent 1b253b3
commit b5f2c29
Show file tree

Hide file tree

Showing 14 changed files with 35 additions and 47 deletions.
diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean
@@ -4,14 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jean-Baptiste Tristan
 -/
 
-import SampCert.DifferentialPrivacy.ZeroConcentrated.DiscreteGaussian
-import SampCert.DifferentialPrivacy.ZeroConcentrated.GaussBound
-import SampCert.DifferentialPrivacy.ZeroConcentrated.GaussConvergence
-import SampCert.DifferentialPrivacy.ZeroConcentrated.GaussPeriodicity
+import SampCert.Util.Gaussian.DiscreteGaussian
+import SampCert.Util.Gaussian.GaussBound
+import SampCert.Util.Gaussian.GaussConvergence
+import SampCert.Util.Gaussian.GaussPeriodicity
 import SampCert.Util.Shift
 import SampCert.DifferentialPrivacy.RenyiDivergence
+import SampCert.Samplers.GaussianGen.Basic
 
-open Real
+open Real Nat
 
 theorem sg_sum_pos' {σ : ℝ} (h : σ ≠ 0) (μ : ℝ) (α : ℝ)  :
   0 < ((gauss_term_ℝ σ μ) x / ∑' (x : ℤ), (gauss_term_ℝ σ μ) x)^α := by
@@ -183,7 +184,7 @@ theorem RenyiDivergenceBound {σ : ℝ} (h : σ ≠ 0) (μ : ℤ) (α : ℝ) (h'
       right
       intro x
       rw [E]
-      rw [add_div]
+      rw [_root_.add_div]
       rw [exp_add]
     rw [tsum_mul_right]
     rw [mul_comm]
@@ -550,3 +551,22 @@ theorem RenyiDivergenceBound' {σ α : ℝ} (h : σ ≠ 0) (h' : 1 < α) (μ ν
     . apply SummableRenyiGauss h
   rw [A]
   apply RenyiDivergenceBound_pre h h'
+
+namespace SLang
+
+theorem DiscreteGaussianGenSampleZeroConcentrated {α : ℝ} (h : 1 < α) (num : PNat) (den : PNat) (μ ν : ℤ) :
+  RenyiDivergence ((DiscreteGaussianGenSample num den μ)) (DiscreteGaussianGenSample num den ν) α ≤
+  α * (((μ - ν) : ℤ)^2 / (2 * ((num : ℝ) / (den : ℝ))^2)) := by
+  have A : (num : ℝ) / (den : ℝ) ≠ 0 := by
+    simp only [ne_eq, div_eq_zero_iff, cast_eq_zero, PNat.ne_zero, or_self, not_false_eq_true]
+  conv =>
+    left
+    congr
+    . intro x
+      rw [DiscreteGaussianGenSample_apply]
+    . intro x
+      rw [DiscreteGaussianGenSample_apply]
+    . skip
+  apply RenyiDivergenceBound' A h
+
+end SLang
diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/DP.lean
@@ -18,10 +18,6 @@ import Mathlib.Probability.ProbabilityMassFunction.Integrals
 import Mathlib.Analysis.Convex.SpecificFunctions.Basic
 import Mathlib.Analysis.Convex.Integral
 
-noncomputable section
-
-open Classical Nat Int Real ENNReal MeasureTheory Measure
-
 def DP (q : List T → SLang U) (ε : ℝ) : Prop :=
   ∀ α : ℝ, 1 < α → ∀ l₁ l₂ : List T, Neighbour l₁ l₂ →
   RenyiDivergence (q l₁) (q l₂) α ≤ (1/2) * ε ^ 2 * α

diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Composition/Code.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Composition/Code.lean
@@ -4,12 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jean-Baptiste Tristan
 -/
 
-import SampCert.DifferentialPrivacy.ZeroConcentrated.DP
+import SampCert.SLang
 
 noncomputable section
 
-open Classical Nat Int Real ENNReal MeasureTheory Measure
-
 namespace SLang
 
 def Compose (nq1 nq2 : List T → SLang ℤ) (l : List T) : SLang (ℤ × ℤ) := do

diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Mechanism/Code.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Mechanism/Code.lean
@@ -4,12 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jean-Baptiste Tristan
 -/
 
-import SampCert.DifferentialPrivacy.ZeroConcentrated.DP
+import SampCert.Samplers.GaussianGen.Code
 
 noncomputable section
 
-open Classical Nat Int Real ENNReal MeasureTheory Measure
-
 namespace SLang
 
 def NoisedQuery (query : List T → ℤ) (Δ : ℕ+) (ε₁ ε₂ : ℕ+) (l : List T) : SLang ℤ := do

diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Postprocessing/Code.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Postprocessing/Code.lean
@@ -4,12 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jean-Baptiste Tristan
 -/
 
-import SampCert.DifferentialPrivacy.ZeroConcentrated.DP
+import SampCert.SLang
 
 noncomputable section
 
-open Classical Nat Int Real ENNReal MeasureTheory Measure
-
 namespace SLang
 
 def PostProcess (nq : List T → SLang U) (pp : U → ℤ) (l : List T) : SLang ℤ := do

diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Queries/BoundedMean/Code.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Queries/BoundedMean/Code.lean
@@ -9,8 +9,6 @@ import SampCert.DifferentialPrivacy.ZeroConcentrated.Foundations.Postprocessing.
 import SampCert.DifferentialPrivacy.ZeroConcentrated.Queries.Count.Code
 import SampCert.DifferentialPrivacy.ZeroConcentrated.Queries.BoundedSum.Code
 
-open Classical Nat Int Real
-
 noncomputable section
 
 namespace SLang

diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Queries/BoundedSum/Code.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Queries/BoundedSum/Code.lean
@@ -9,8 +9,6 @@ import Mathlib.Algebra.Group.Defs
 import Mathlib.Init.Algebra.Classes
 import Init.Data.Int.Order
 
-open Classical Nat Int Real
-
 noncomputable section
 
 namespace SLang

diff --git a/SampCert/DifferentialPrivacy/ZeroConcentrated/Queries/Count/Code.lean b/SampCert/DifferentialPrivacy/ZeroConcentrated/Queries/Count/Code.lean
@@ -6,8 +6,6 @@ Authors: Jean-Baptiste Tristan
 
 import SampCert.DifferentialPrivacy.ZeroConcentrated.Foundations.Mechanism.Code
 
-open Classical Nat Int Real
-
 noncomputable section
 
 namespace SLang

diff --git a/SampCert/Samplers/Gaussian/Properties.lean b/SampCert/Samplers/Gaussian/Properties.lean
@@ -12,7 +12,7 @@ import SampCert.Samplers.Laplace.Basic
 import Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
 import SampCert.Util.UtilMathlib
 import SampCert.Samplers.Gaussian.Code
-import SampCert.DifferentialPrivacy.ZeroConcentrated.DiscreteGaussian
+import SampCert.Util.Gaussian.DiscreteGaussian
 
 noncomputable section
 

diff --git a/SampCert/Samplers/GaussianGen/Properties.lean b/SampCert/Samplers/GaussianGen/Properties.lean
@@ -6,9 +6,8 @@ Authors: Jean-Baptiste Tristan
 
 import SampCert.Samplers.GaussianGen.Code
 import SampCert.Samplers.Gaussian.Properties
-import SampCert.DifferentialPrivacy.ZeroConcentrated.DiscreteGaussian
-import SampCert.DifferentialPrivacy.ZeroConcentrated.GaussPeriodicity
-import SampCert.DifferentialPrivacy.ZeroConcentrated.ConcentratedBound
+import SampCert.Util.Gaussian.DiscreteGaussian
+import SampCert.Util.Gaussian.GaussPeriodicity
 
 noncomputable section
 
@@ -47,19 +46,4 @@ theorem DiscreteGaussianGenSample_apply (num : PNat) (den : PNat) (μ x : ℤ) :
   . simp [gauss_term_ℝ]
   . rw [SG_periodic' A]
 
-theorem DiscreteGaussianGenSampleZeroConcentrated {α : ℝ} (h : 1 < α) (num : PNat) (den : PNat) (μ ν : ℤ) :
-  RenyiDivergence ((DiscreteGaussianGenSample num den μ)) (DiscreteGaussianGenSample num den ν) α ≤
-  α * (((μ - ν) : ℤ)^2 / (2 * ((num : ℝ) / (den : ℝ))^2)) := by
-  have A : (num : ℝ) / (den : ℝ) ≠ 0 := by
-    simp only [ne_eq, div_eq_zero_iff, cast_eq_zero, PNat.ne_zero, or_self, not_false_eq_true]
-  conv =>
-    left
-    congr
-    . intro x
-      rw [DiscreteGaussianGenSample_apply]
-    . intro x
-      rw [DiscreteGaussianGenSample_apply]
-    . skip
-  apply RenyiDivergenceBound' A h
-
 end SLang
diff --git a/...cy/ZeroConcentrated/DiscreteGaussian.lean → SampCert/Util/Gaussian/DiscreteGaussian.lean b/...cy/ZeroConcentrated/DiscreteGaussian.lean → SampCert/Util/Gaussian/DiscreteGaussian.lean
diff --git a/...lPrivacy/ZeroConcentrated/GaussBound.lean → SampCert/Util/Gaussian/GaussBound.lean b/...lPrivacy/ZeroConcentrated/GaussBound.lean → SampCert/Util/Gaussian/GaussBound.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jean-Baptiste Tristan
 -/
 
-import SampCert.DifferentialPrivacy.ZeroConcentrated.DiscreteGaussian
+import SampCert.Util.Gaussian.DiscreteGaussian
 
 noncomputable section
 

diff --git a/...cy/ZeroConcentrated/GaussConvergence.lean → SampCert/Util/Gaussian/GaussConvergence.lean b/...cy/ZeroConcentrated/GaussConvergence.lean → SampCert/Util/Gaussian/GaussConvergence.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jean-Baptiste Tristan
 -/
 
-import SampCert.DifferentialPrivacy.ZeroConcentrated.DiscreteGaussian
+import SampCert.Util.Gaussian.DiscreteGaussian
 
 open Classical Nat Real
 

diff --git a/...cy/ZeroConcentrated/GaussPeriodicity.lean → SampCert/Util/Gaussian/GaussPeriodicity.lean b/...cy/ZeroConcentrated/GaussPeriodicity.lean → SampCert/Util/Gaussian/GaussPeriodicity.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jean-Baptiste Tristan
 -/
 
-import SampCert.DifferentialPrivacy.ZeroConcentrated.GaussConvergence
+import SampCert.Util.Gaussian.GaussConvergence
 
 theorem SGShift (μ σ : ℝ) (n : ℤ) (k : ℤ) :
   (gauss_term_ℝ σ μ) (((n + k) : ℤ) : ℝ) = (gauss_term_ℝ σ (μ - k)) n := by