Stat.Privacy.Staircase

theorem measurable_ray_selector (r : ℝ) (hr : 1 < r) : ∃ c : (Fin 4 → ℝ) → RayIndex → ℝ, (∀ S, Measurable fun f => c f S) ∧ ∀ f, PrivateCone r f → (∀ S, 0 ≤ c f S) ∧ ∀ i, f i = ∑ S, c f S * ray r S i := by exact ⟨coneRayCoeff r, measurable_coneRayCoeff r, fun f hf => coneRayCoeff_decomposition r hr f hf⟩

theorem measurable_density_decomposition (Q : Kernel (Fin 4) Z) [IsMarkovKernel Q] (r : ℝ) (hr : 1 < r) (hpriv : SetwisePrivate Q r) : ∃ c : Z → RayIndex → ℝ, (∀ S, Measurable fun z => c z S) ∧ (∀ z S, 0 ≤ c z S) ∧ ∀ᵐ z ∂rowSum Q, ∀ i, rowDensity Q i z = ∑ S, c z S * ray r S i := by let c : Z → RayIndex → ℝ := fun z S => max 0 (coneRayCoeff r (fun i => rowDensity Q i z) S) have hdensity : Measurable (fun z => fun i : Fin 4 => rowDensity Q i z) := by rw [measurable_pi_iff] intro i exact ((Q i).measurable_rnDeriv (rowSum Q)).ennreal_toReal refine ⟨c, ?_, ?_, ?_⟩ · intro S exact measurable_const.max ((measurable_coneRayCoeff r S).comp hdensity) · intro z S exact le_max_left _ _ · filter_upwards [ae_privateCone Q r hr hpriv] with z hz have hcoeff := (coneRayCoeff_decomposition r hr (fun i => rowDensity Q i z) hz) intro i calc rowDensity Q i z = ∑ S, coneRayCoeff r (fun j => rowDensity Q j z) S * ray r S i := hcoeff.2 i _ = ∑ S, c z S * ray r S i := by apply Finset.sum_congr rfl intro S _ simp only [c, max_eq_right (hcoeff.1 S)]

theorem coefficient_normalized (Q : Kernel (Fin 4) Z) [IsMarkovKernel Q] (r : ℝ) (hr : 1 < r) (D : CoefficientField Q r) (i : Fin 4) : (∑ S : RayIndex, (∫ z, D.c z S ∂rowSum Q) * ray r S i) = 1 := by have hint (S : RayIndex) : Integrable (fun z => D.c z S * ray r S i) (rowSum Q) := (coefficient_integrable Q r hr D S).mul_const _ have : IsFiniteMeasure (rowSum Q) := rowSum_finite Q calc (∑ S : RayIndex, (∫ z, D.c z S ∂rowSum Q) * ray r S i) = ∫ z, ∑ S : RayIndex, D.c z S * ray r S i ∂rowSum Q := by rw [integral_finsetSum] · congr 1 ext S rw [integral_mul_const] · intro S _ exact hint S _ = ∫ z, rowDensity Q i z ∂rowSum Q := by apply integral_congr_ae filter_upwards [D.reconstruct] with z hz exact (hz i).symm _ = 1 := by change (∫ z, ((Q i).rnDeriv (rowSum Q) z).toReal ∂rowSum Q) = 1 rw [Measure.integral_toReal_rnDeriv (row_absolutelyContinuous Q i)] simp [measureReal_def]

theorem exists_coefficientPostprocess (Q : Kernel (Fin 4) Z) [IsMarkovKernel Q] (r : ℝ) (hr : 1 < r) (D : CoefficientField Q r) : ∃ K : Kernel RayIndex Z, IsMarkovKernel K ∧ ∀ S : RayIndex, coefficientMeasure Q D S = ofReal (∫ z, D.c z S ∂rowSum Q) • K S := by let : Nonempty Z := nonempty_of_isProbabilityMeasure (Q 0) let ν : RayIndex → FiniteMeasure Z := fun S => ⟨coefficientMeasure Q D S, isFiniteMeasure_withDensity_ofReal (coefficient_integrable Q r hr D S).hasFiniteIntegral⟩ let K : Kernel RayIndex Z := Kernel.ofFunOfCountable fun S => if (ν S).mass = 0 then Q 0 else (ν S).normalize refine ⟨K, ?_, ?_⟩ · constructor intro S change IsProbabilityMeasure (if (ν S).mass = 0 then Q 0 else ((ν S).normalize : Measure Z)) split_ifs <;> infer_instance · intro S have hmass : ((ν S).mass : ℝ≥0∞) = ofReal (∫ z, D.c z S ∂rowSum Q) := by rw [FiniteMeasure.ennreal_mass] exact coefficientMeasure_mass Q r hr D S change (ν S : Measure Z) = ofReal (∫ z, D.c z S ∂rowSum Q) • K S rw [← hmass] by_cases hzero : (ν S).mass = 0 · have hν : ν S = 0 := (ν S).mass_zero_iff.mp hzero simp [K, hν] · apply Measure.ext intro s hs simp only [K, Kernel.ofFunOfCountable, Kernel.coe_mk, if_neg hzero] rw [Measure.smul_apply, smul_eq_mul] have h := congrArg (fun x : ℝ≥0 => (x : ℝ≥0∞)) ((ν S).self_eq_mass_mul_normalize s) simpa only [ENNReal.coe_mul, FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure, ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure] using h

theorem exists_refinement (Q : Kernel (Fin 4) Z) [IsMarkovKernel Q] (r : ℝ) (hr : 1 < r) (hpriv : SetwisePrivate Q r) : Nonempty (Refinement Q r) := by obtain ⟨D⟩ := exists_coefficientField Q r hr hpriv obtain ⟨α, T, hmarkovT, hα, hnorm, hT⟩ := exists_coefficientRelease Q r hr D obtain ⟨K, hmarkovK, hK⟩ := exists_coefficientPostprocess Q r hr D exact ⟨⟨α, T, K, hmarkovT, hmarkovK, hnorm, hT, coefficient_factorizes Q r hr D α T K hα hT hK⟩⟩

theorem cubeWeight_coordinate (t : Fin 4 → ℝ) (i : Fin 4) : (∑ S : Finset (Fin 4), cubeWeight t S * (if i ∈ S then 1 else 0)) = t i := by let g : Fin 4 → ℝ := fun j => if j = i then 0 else 1 - t j have hterm (S : Finset (Fin 4)) : cubeWeight t S * (if i ∈ S then 1 else 0) = ∏ j : Fin 4, if j ∈ S then t j else g j := by by_cases hi : i ∈ S · simp only [if_pos hi, mul_one] unfold cubeWeight apply Finset.prod_congr rfl intro j _ by_cases hji : j = i <;> simp [g, hji, hi] · simp only [if_neg hi, mul_zero] exact (Finset.prod_eq_zero (Finset.mem_univ i) (by simp [g, hi])).symm have hweight (S : Finset (Fin 4)) : (∏ j : Fin 4, if j ∈ S then t j else g j) = (∏ j ∈ S, t j) * ∏ j ∈ Sᶜ, g j := by have h : (Finset.univ.filter (fun j : Fin 4 => j ∉ S)) = Sᶜ := by ext j simp simp [Finset.prod_ite, h] calc (∑ S : Finset (Fin 4), cubeWeight t S * (if i ∈ S then 1 else 0)) = ∏ j : Fin 4, (t j + g j) := by rw [Fintype.prod_add] simp only [← hweight, ← hterm] _ = t i := by have h : (fun j : Fin 4 => t j + g j) = (fun j => if j = i then t i else 1) := by funext j by_cases hji : j = i <;> simp [g, hji] rw [h] simp [Finset.prod_ite_eq']

theorem fisher_gap_nonneg {d : ℕ} (Q : Kernel (Fin 4) Z) [IsMarkovKernel Q] (r : ℝ) (R : Refinement Q r) (p : Fin 4 → ℝ) (hp : ∀ i, 0 < p i) (u : Fin 4 → Fin d → ℝ) (v : Fin d → ℝ) : 0 ≤ finiteFisher R.T p (projectedScore u v) - outputFisher Q p (projectedScore u v) := by rw [fisher_gap_eq_variance Q r R p (projectedScore u v) hp] unfold varianceGap apply Finset.sum_nonneg intro S _ apply mul_nonneg · unfold releaseMass apply Finset.sum_nonneg intro i _ exact mul_nonneg (le_of_lt (hp i)) ENNReal.toReal_nonneg · exact integral_nonneg fun z => sq_nonneg _

theorem equality_rigidity {d : ℕ} (Q : Kernel (Fin 4) Z) [IsMarkovKernel Q] (r : ℝ) (R : Refinement Q r) (p : Fin 4 → ℝ) (hp : ∀ i, 0 < p i) (u : Fin 4 → Fin d → ℝ) (v : Fin d → ℝ) (hgap : finiteFisher R.T p (projectedScore u v) - outputFisher Q p (projectedScore u v) = 0) (S U : RayIndex) (hS : 0 < releaseMass R.T p S) (hU : 0 < releaseMass R.T p U) (hdiff : releaseScore R.T p (projectedScore u v) S ≠ releaseScore R.T p (projectedScore u v) U) : R.K S ⟂ₘ R.K U := by let w := projectedScore u v have hvar : (∑ V, releaseMass R.T p V * ∫ z, (releaseScore R.T p w V - outputScore Q p w z) ^ 2 ∂(R.K V)) = 0 := by simpa only [varianceGap] using ((fisher_gap_eq_variance Q r R p w hp).symm.trans hgap) have hterm_nonneg (V : RayIndex) : 0 ≤ releaseMass R.T p V * ∫ z, (releaseScore R.T p w V - outputScore Q p w z) ^ 2 ∂(R.K V) := by apply mul_nonneg · unfold releaseMass apply Finset.sum_nonneg intro i _ exact mul_nonneg (le_of_lt (hp i)) ENNReal.toReal_nonneg · exact integral_nonneg fun z => sq_nonneg _ have hscore (V : RayIndex) (hV : 0 < releaseMass R.T p V) : ∀ᵐ z ∂(R.K V), outputScore Q p w z = releaseScore R.T p w V := by have hterm : releaseMass R.T p V * ∫ z, (releaseScore R.T p w V - outputScore Q p w z) ^ 2 ∂(R.K V) = 0 := ((Finset.sum_eq_zero_iff_of_nonneg (fun V _ => hterm_nonneg V)).mp hvar) V (Finset.mem_univ V) have hint : (∫ z, (releaseScore R.T p w V - outputScore Q p w z) ^ 2 ∂(R.K V)) = 0 := (mul_eq_zero.mp hterm).resolve_left (ne_of_gt hV) letI : IsMarkovKernel R.K := R.markovK have hscoreInt : Integrable (outputScore Q p w) (R.K V) := outputScore_integrable Q p w (fun i => le_of_lt (hp i)) _ have hscoreSqInt : Integrable (fun z => (outputScore Q p w z) ^ 2) (R.K V) := outputScore_sq_integrable Q p w (fun i => le_of_lt (hp i)) _ have hfi : Integrable (fun z => (releaseScore R.T p w V - outputScore Q p w z) ^ 2) (R.K V) := by have hfun : (fun z => (releaseScore R.T p w V - outputScore Q p w z) ^ 2) = (fun z => (releaseScore R.T p w V) ^ 2 - (2 * releaseScore R.T p w V) * outputScore Q p w z + (outputScore Q p w z) ^ 2) := by funext z ring rw [hfun] exact ((integrable_const _).sub (hscoreInt.const_mul _)).add hscoreSqInt have hae := (integral_eq_zero_iff_of_nonneg (fun z => sq_nonneg _) hfi).mp hint filter_upwards [hae] with z hz have hz' : (releaseScore R.T p w V - outputScore Q p w z) ^ 2 = 0 := by simpa only [Pi.zero_apply] using hz have hz0 : releaseScore R.T p w V - outputScore Q p w z = 0 := (mul_self_eq_zero.mp (by simpa only [pow_two] using hz')) linarith have hm : Measurable (outputScore Q p w) := by unfold outputScore rowDensity fun_prop let s : Set Z := {z | outputScore Q p w z ≠ releaseScore R.T p w S} refine ⟨s, ?_, ?_, ?_⟩ · exact (measurableSet_eq_fun hm measurable_const).compl · have h := ae_iff.mp (hscore S hS) simpa only [s, Set.compl_setOf, not_not] using h · have h : ∀ᵐ z ∂(R.K U), outputScore Q p w z ≠ releaseScore R.T p w S := by filter_upwards [hscore U hU] with z hz intro heq exact hdiff (heq.symm.trans hz) have h0 := ae_iff.mp h simpa only [s, Set.compl_setOf, not_not] using h0

theorem exists_coefficientRelease (Q : Kernel (Fin 4) Z) [IsMarkovKernel Q] (r : ℝ) (hr : 1 < r) (D : CoefficientField Q r) : ∃ (α : RayIndex → ℝ≥0) (T : Kernel (Fin 4) RayIndex), IsMarkovKernel T ∧ (∀ S, (α S : ℝ) = ∫ z, D.c z S ∂rowSum Q) ∧ (∀ i, ∑ S, (α S : ℝ) * ray r S i = 1) ∧ ∀ i S, T i {S} = (α S : ℝ≥0∞) * ofReal (ray r S i) := by let α : RayIndex → ℝ≥0 := fun S => ⟨∫ z, D.c z S ∂rowSum Q, integral_nonneg (fun z => D.nonneg z S)⟩ have hα (S : RayIndex) : (α S : ℝ) = ∫ z, D.c z S ∂rowSum Q := rfl have hnorm (i : Fin 4) : ∑ S, (α S : ℝ) * ray r S i = 1 := by simpa only [hα] using coefficient_normalized Q r hr D i let T : Kernel (Fin 4) RayIndex := Kernel.ofFunOfCountable fun i => Measure.sum fun S : RayIndex => ofReal ((α S : ℝ) * ray r S i) • Measure.dirac S refine ⟨α, T, ?_, hα, hnorm, ?_⟩ · constructor intro i change IsProbabilityMeasure (Measure.sum fun S : RayIndex => ofReal ((α S : ℝ) * ray r S i) • Measure.dirac S) apply HasSum.isProbabilityMeasure_sum_dirac · intro S exact mul_nonneg (α S).property (by unfold ray split_ifs <;> linarith) · simpa only [hnorm i] using (hasSum_fintype (fun S : RayIndex => (α S : ℝ) * ray r S i)) · intro i S change (Measure.sum fun U : RayIndex => ofReal ((α U : ℝ) * ray r U i) • Measure.dirac U) {S} = _ rw [Measure.sum_smul_dirac_singleton] simpa using ENNReal.ofReal_mul (α S).property (y := ray r S i)