Proved composition and mechanism with additinoal properties

SampCert/DiffPrivacy/BoundedAvg.lean

@@ -33,13 +33,17 @@ theorem BoundedSumQueryDP (L U : ℤ) (h : L < U) (ε₁ ε₂ : ℕ+) : DP (Noi
   unfold NoisedBoundedAvgQuery'
   simp only
 
-  have A := @NoisedCountingQueryDP ℤ ε₁ (2 * ε₂)
-  have B := @NoisedBoundedSumQueryDP L U h ε₁ (2 * ε₂)
-  have C := DPCompose B A
-  simp at C
-  ring_nf at C
-  rw [← division_def] at C
-  have D := DPPostProcess C (fun z => z.1 / z.2)
-  exact D
+  have A₁ := @NoisedCountingQueryDP ℤ ε₁ (2 * ε₂)
+  have A₂ := @NoisedCountingQuery_NonZeroNQ ℤ ε₁ (2 * ε₂)
+  have A₃ := @NoisedCountingQuery_NonTopNQ ℤ ε₁ (2 * ε₂)
+  have A₄ := @NoisedCountingQuery_NonTopRDNQ ℤ ε₁ (2 * ε₂)
+  sorry
+  -- have B := @NoisedBoundedSumQueryDP L U h ε₁ (2 * ε₂)
+  -- have C := DPCompose B A
+  -- simp at C
+  -- ring_nf at C
+  -- rw [← division_def] at C
+  -- have D := DPPostProcess C (fun z => z.1 / z.2)
+  -- exact D
 
 end SLang

SampCert/DiffPrivacy/ConcentratedBound.lean

@@ -548,8 +548,5 @@ theorem RenyiDivergenceBound' {σ α : ℝ} (h : σ ≠ 0) (h' : 1 < α) (μ ν
       apply RenyiSumSG_nonneg h
     . apply RenyiSumSG_nonneg h
     . apply SummableRenyiGauss h
-
-
-
   rw [A]
   apply RenyiDivergenceBound_pre h h'

SampCert/DiffPrivacy/Count.lean

@@ -34,8 +34,21 @@ theorem CountingQuery1Sensitive :
 def NoisedCountingQuery (ε₁ ε₂ : ℕ+) (l : List T) : SLang ℤ := do
   NoisedQuery CountingQuery 1 ε₁ ε₂ l
 
-theorem NoisedCountingQueryDP (ε₁ ε₂ : ℕ+) : @DP T ℤ (NoisedCountingQuery ε₁ ε₂) ((ε₁ : ℝ) / ε₂) := by
+theorem NoisedCountingQueryDP (ε₁ ε₂ : ℕ+) :
+  @DP T ℤ (NoisedCountingQuery ε₁ ε₂) ((ε₁ : ℝ) / ε₂) := by
   apply NoisedQueryDP
   apply CountingQuery1Sensitive
 
+theorem NoisedCountingQuery_NonZeroNQ (ε₁ ε₂ : ℕ+) :
+  @NonZeroNQ T ℤ (NoisedCountingQuery ε₁ ε₂) := by
+  apply NoisedQuery_NonZeroNQ
+
+theorem NoisedCountingQuery_NonTopNQ (ε₁ ε₂ : ℕ+) :
+  @NonTopNQ T ℤ (NoisedCountingQuery ε₁ ε₂) := by
+  apply NoisedQuery_NonTopNQ
+
+theorem NoisedCountingQuery_NonTopRDNQ (ε₁ ε₂ : ℕ+) :
+  @NonTopRDNQ T ℤ (NoisedCountingQuery ε₁ ε₂) := by
+  apply NoisedQuery_NonTopRDNQ
+
 end SLang