Formalization: Optimal Treatment Welfare under Local Privacy: Minimax Estimation and Honest Inference
The complete Lean development behind this paper — every definition, lemma, and theorem of its module, including helpers the paper text never cites. Identifiers link within this page, into the Causalean library, or out to the official Mathlib docs. Note: this index was generated at a different commit than the paper's audited pin (3a4c7a8) — statements may have moved since the audit.
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Basic 39 declarations Finite original-record private value frontiers: Basic.
Basic
Finite original-record private value frontiers: Basic.
Fix the sample size and the dimension and the privacy budget. Public resource tuples in the paper's domain.
Definition (Lean source)
Fix the dimension. Full binary potential-outcome records, in the order X,A,Y,Y0,Y1.
Fix the dimension. Observed records.
Fix the dimension. Paired input alphabet with Bool coding signs.
Fix the full participant record. Cell coordinate.
Definition (Lean source)
Fix the full participant record. Assignment coordinate.
Definition (Lean source)
Fix the full participant record. Observed outcome coordinate.
Definition (Lean source)
Fix the full participant record. Control potential outcome.
Definition (Lean source)
Fix the full participant record. Treated potential outcome.
Definition (Lean source)
Fix the binary value a and the full participant record. Arm-indexed potential outcome.
Definition (Lean source)
Fix the full participant record. Observation projection.
Definition (Lean source)
Fix the binary value a. Binary value in the real line.
Definition (Lean source)
Fix the binary value s. Sign coding.
Definition (Lean source)
Fix the observed participant record. Signed observation.
Fix the observed participant record. Paired observation projection.
Definition (Lean source)
Fix the probability law P. Observed marginal.
Definition (Lean source)
Fix the probability law P, the binary value a, and the coordinate index. Conditional cell mean, with division at zero cells interpreted by Lean.
Definition (Lean source)
Fix the probability law P and the coordinate index. Cellwise contrast.
Definition (Lean source)
Fix the probability law P. Baseline mean.
Definition (Lean source)
Fix the probability law P. First-best population value.
Definition (Lean source)
Fix the dimension. Parameter cube.
Fix the function theta. Signed average absolute norm.
Definition (Lean source)
Fix the function w. Finite atomic law constructor.
Definition (Lean source)
Fix the function theta. Paired signed law.
Definition (Lean source)
Fix the dimension. Public uniform paired law.
Definition (Lean source)
Fix the probability law P. Uniform covariate marginal.
Definition (Lean source)
Fix the probability law P. Fair assignment conditional on both potential outcomes and the cell.
Fix the probability law P. Almost-sure consistency.
Definition (Lean source)
Fix the probability law P. Interior Bernoulli arm means.
Definition (Lean source)
Fix the probability law P. The four defining causal model atoms.
Definition (Lean source)
Fix the dimension. The complete law class, including ambient probability typing.
Definition (Lean source)
Fix the density or prior under consideration and the binary value y. Bernoulli atom weight.
Definition (Lean source)
Fix the function theta. Uniform cells, independent arm potentials, independent fair assignment, and consistency.
Definition (Lean source)
Protocol class labels.
Definition (Lean source)
Equality of protocol-class labels is decidable.
Definition (Lean source)
Fix the dimension. Logarithmic dimension.
Fix the real parameter t and the dimension. Evaluated finite-resource rate.
Fix the protocol-class label, the sample size and the dimension, and the privacy budget. Class-independent squared-error rate.
Definition (Lean source)
Fix the protocol-class label, the sample size and the dimension, and the privacy budget. Connected honest-length rate.
Definition (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.AncillaryReconstruction 8 declarations The signed input and assignment bit factor as a product law.
Ancillary reconstruction of symmetric samples
The signed input and assignment bit factor as a product law. Coordinatewise reconstruction consequently recovers the full iid observed sample.
The ancillary assignment has the parameter-independent fair law.
Each assignment has probability one half.
Formal statement
Proof (Lean source)
The ancillary bit law is a probability measure.
Definition (Lean source)
Assume the stated htheta condition and positive dimension. Splitting an observed record produces a paired input and an independent fair assignment.
Formal statement
Proof (Lean source)
Assume the stated htheta condition and positive dimension. Reattaching the fair bit recovers exactly the original observed law.
Formal statement
Proof (Lean source)
Assume the stated htheta condition and positive dimension. Splitting every participant preserves iid sampling and separates all ancillary bits.
Formal statement
Proof (Lean source)
Assume the stated htheta condition and positive dimension. Reconstructing every participant recovers the full iid observed experiment.
Formal statement
Proof (Lean source)
Assume the stated htheta condition and positive dimension. All signed inputs are independent of the entire vector of ancillary assignments.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Bridge.AncillarySample 3 declarations The signed sample and the assignment vector factor into independent product laws.
Independent ancillary assignments for the entire sample
The signed sample and the assignment vector factor into independent product laws. Reconstruction therefore works simultaneously for all participants, before any adaptive transcript is generated.
Assume the stated htheta condition and positive dimension. Reconstructing the complete observed sample from the independent signed sample and fair assignment vector recovers its iid law.
Formal statement
Proof (Lean source)
Assume the stated htheta condition, positive dimension, and measurability of f. The iid experiment identity also holds after arbitrary measurable processing of the complete original sample.
Formal statement
Proof (Lean source)
Assume independent and identically distributed participant records, independent protocol randomness, positive dimension, and the stated htheta condition. Before any adaptive messages are generated, the original decision experiment can be represented by independent paired inputs, fair ancillary bits, and public coins.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Bridge.AncillaryTranscript 5 declarations Independent fair reconstruction bits can be averaged one stage at a time, including when the next channel depends on the preceding messages.
Integrating ancillary bits through adaptive transcripts
Independent fair reconstruction bits can be averaged one stage at a time, including when the next channel depends on the preceding messages.
Flipping any one fair assignment preserves the entire independent bit law.
Formal statement
Proof (Lean source)
Assume the function f. Resampling a single independent fair bit leaves every nonnegative expectation unchanged.
Formal statement
Proof (Lean source)
Assume order no larger than the sample size, the function f, and measurability of f. Averaging independent ancillary assignments commutes with every adaptive prefix.
Formal statement
Proof (Lean source)
Assume the function f and measurability of f. The full transcript expectation averages the independent reconstruction bits.
Formal statement
Proof (Lean source)
Averaging the ancillary bits preserves decisions jointly with both independent coins.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Bridge.Identification 19 declarations Causal value identities and deterministic signed-input transcript preprocessing.
Causal bridge identification
Causal value identities and deterministic signed-input transcript preprocessing.
Fix the probability law P and the coordinate index. Conditional signed cell mean.
Definition (Lean source)
Assume the causal-model conditions for the data law. Interior arm means put the causal contrast in the declared cube.
Formal statement
Proof (Lean source)
The armwise maximum splits into the arm average and half the absolute contrast.
Formal statement
Proof (Lean source)
A finite event partitions into its two Boolean marks.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law. Fair randomization also holds after marginalizing either potential outcome.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law. Consistency in the model gives the corresponding almost-everywhere identity.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law. Marginalizing the potential outcome leaves a fair assignment in each cell.
Formal statement
Proof (Lean source)
Integrating a finite event's unit indicator recovers its real probability.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law. Signed cell means identify the causal contrast by fair assignment and consistency.
Formal statement
Proof (Lean source)
A signed cell indicator is the difference of its positive and negative atoms.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law and positive dimension. A sign-valued conditional mean determines both signed atom probabilities.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law and positive dimension. The observed signed marginal is the paired law identified by the causal contrast.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law. The observed outcome in each cell averages the two potential-outcome marginals.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law and dimension at least two. Uniform cells and randomization identify the outcome baseline with the mean arm average.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law and dimension at least two. The causal value equals the observed baseline plus half the signed contrast norm.
Formal statement
Proof (Lean source)
Assume the stated htheta condition and positive dimension. The symmetric arm means give contrast theta and average welfare one half.
Formal statement
Proof (Lean source)
Assume order no larger than the sample size. Deterministic preprocessing preserves every recursively constructed prefix law.
Formal statement
Proof (Lean source)
Fixed transcripts under signed preprocessing are exactly paired-input transcripts.
Formal statement
Proof (Lean source)
Assume independent and identically distributed participant records, independent protocol randomness, dimension at least two, and the stated htheta condition. Signed preprocessing pushes the full iid decision experiment to the paired one.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Bridge.Protocol 34 declarations Causal identification, symmetric-law certificates, and private experiment equivalence.
Ancillary protocol preprocessing
Causal identification, symmetric-law certificates, and private experiment equivalence.
Fix the parameter v and the binary value a. Reconstruct the original observation using an ancillary assignment bit.
Definition (Lean source)
For a protocol, participant index, and ancillary bit, the recovered-input map is measurable.
Formal statement
Proof (Lean source)
Fix the local protocol Q, the participant index, and the binary value a. Original stage kernel evaluated on a recovered ancillary assignment.
Definition (Lean source)
Fix the local protocol Q, the participant index, and the parameter w. Fair mixture of original-record rows at a paired input.
Definition (Lean source)
For a protocol and participant index, the ancillary fair mixture is jointly measurable.
Formal statement
Proof (Lean source)
Fix the local protocol Q and the participant index. Averaged paired-input kernel with the ancillary fair bit integrated out.
Definition (Lean source)
The average remains a Markov kernel.
Formal statement
Proof (Lean source)
Fix the local protocol Q. Averaged paired-input protocol, retaining the same seed and message spaces.
Definition (Lean source)
For a paired protocol and participant index, the signed-observation pullback map is measurable.
Formal statement
Proof (Lean source)
Fix the local protocol K and the participant index. Pulled-back original-record kernel.
Definition (Lean source)
Pullback Markov certificate.
Formal statement
Proof (Lean source)
Fix the local protocol K. Deterministic signed preprocessing in the reverse direction.
Definition (Lean source)
Assume the full participant record. Averaging the ancillary assignment preserves the all-history privacy inequality.
Formal statement
Proof (Lean source)
Assume the stated privacy condition for the protocol. Averaging the ancillary assignment preserves history independence.
Formal statement
Proof (Lean source)
Assume the full participant record. Signed deterministic preprocessing preserves the all-history privacy inequality.
Formal statement
Proof (Lean source)
Assume the stated privacy condition for the protocol. Signed deterministic preprocessing preserves history independence.
Formal statement
Proof (Lean source)
Both directions of the ancillary-bit construction preserve the two protocol classes.
Formal statement
Proof (Lean source)
Recovering an observation gives its specified paired input back.
Formal statement
Proof (Lean source)
The observed outcome sign is reconstructed from the signed observation and assignment.
Formal statement
Proof (Lean source)
Assume the stated htheta condition. The recovered original-record atom has exactly half its paired-input mass. [](.
Formal statement
Proof (Lean source)
Every observed atom is reconstructed from its signed input and assignment.
Formal statement
Proof (Lean source)
Assume the stated htheta condition and positive dimension. Original-record singleton probabilities factor into paired mass and a fair bit.
Formal statement
Proof (Lean source)
Assume the stated htheta condition and positive dimension. At every history and seed, integrating the original row equals integrating its ancillary-bit average against the paired law. This is the one-stage experiment identity.
Formal statement
Proof (Lean source)
Assume the stated htheta condition and positive dimension. Integrating out the next iid participant gives the same message measure in both experiments, with no restriction on the history or public seed.
Formal statement
Proof (Lean source)
Assume order no larger than the sample size and the function hxy. An adaptive prefix uses only records from participants already queried.
Formal statement
Proof (Lean source)
Assume one plus the stage index no larger than the sample size. Changing the next participant cannot change the preceding adaptive history law.
Formal statement
Proof (Lean source)
Averaging the ancillary assignment at a next step commutes with extending any previous history law, including an adaptive law.
Formal statement
Proof (Lean source)
Assume one plus the stage index no larger than the sample size. The next adaptive prefix with the ancillary bit averaged is exactly the fair mixture of the two original-record prefixes, retaining the common past.
Formal statement
Proof (Lean source)
Assume the stated htheta condition, positive dimension, and the function f. Integrating any nonnegative observed-record function first integrates the parameter-independent ancillary assignment bit.
Formal statement
Proof (Lean source)
Assume the stated htheta condition, positive dimension, and measurability of f. Ancillary reconstruction applies to arbitrary measurable measure-valued rows, not merely to an event in a stage kernel.
Formal statement
Proof (Lean source)
Assume the stated htheta condition and positive dimension. The original observed law is exactly the paired law followed by independent fair reconstruction.
Formal statement
Proof (Lean source)
Assume the stated htheta condition and positive dimension. Fresh iid input can be integrated before or after extending any adaptive history law; the two experiments give the same history-message joint measure.
Formal statement
Proof (Lean source)
Assume the stated htheta condition, positive dimension, and measurability of f. The same transition equality survives measurable transcript processing, including retention of histories and appending the next message.
Formal statement
Proof (Lean source)
Assume the stated htheta condition, positive dimension, and one plus the stage index no larger than the sample size. Averaging a fresh participant's iid observed input gives precisely the paired next-prefix transition while leaving the previously queried records fixed.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Calibration.Assembly 3 declarations Apply the arbitrary-column dependence bound to the combined pilot and evaluation rows, then add the squared average bias to obtain the finite hybrid MSE bound.
Finite polynomial calibration assembly
Apply the arbitrary-column dependence bound to the combined pilot and evaluation rows, then add the squared average bias to obtain the finite hybrid MSE bound.
Assume independent and identically distributed participant records, the causal-model conditions for the data law, a privacy budget in the interval from zero to one, dimension at least two, positive block size, a block no larger than the sample, and the stated hvar condition. The dependence lemma controls the average hybrid variance on the combined rows.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, independent and identically distributed participant records, the causal-model conditions for the data law, an admissible sample size, dimension, and privacy budget, positive block size, the stated l condition, the stated d condition, the stated hm d condition, and a block no larger than the sample. Combined-row variance and the calibrated bias give the roadmap's final hybrid MSE.
Formal statement
Proof (Lean source)
Bounded mean concentration, Chebyshev approximation, iid sampling, causal-model validity, allowed resources, and positive block size within the sample imply both the global-polynomial and hybrid finite calibration bounds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Calibration.Average 8 declarations Linearity, finite averaging of the column bias bounds, and the bias--variance identity used in the last step of finite polynomial calibration.
Averaged hybrid bias and mean squared error
Linearity, finite averaging of the column bias bounds, and the bias--variance identity used in the last step of finite polynomial calibration.
Expectation commutes with the finite average of hybrid column statistics.
Formal statement
Proof (Lean source)
Assume positive dimension and the stated hbias condition. Uniform column bias bounds persist under averaging, without column independence.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, the stated l condition, the stated d condition, and the stated dm condition. The specified hybrid estimator inherits the calibrated column bias bound.
Formal statement
Proof (Lean source)
Centered hybrid squared error equals variance plus squared bias. the integrability condition.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, the stated l condition, the stated d condition, and the stated dm condition. Squaring the calibrated average bias gives its exact contribution to the MSE.
Formal statement
Proof (Lean source)
Assume the stated hvar condition and the stated hbias condition. Finite second moments allow separate bias and variance bounds to be added. the variance, integrability, and bias bounds.
Formal statement
Proof (Lean source)
Assume positive dimension and the stated l condition. On the hybrid resource domain, the column-variance exponential is absorbed by dimension.
Formal statement
Proof (Lean source)
Assume positive dimension and the stated l condition. The roadmap's averaged-variance envelope is at most 3200 times sigma squared over L.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Calibration.Combined 7 declarations The independent two-block experiment is a split iid vector block.
Combining the pilot and evaluation rows
The independent two-block experiment is a split iid vector block. Hybrid statistics depend only on their own columns in this combined experiment.
Fix the function z. Split a combined vector block into its pilot and evaluation halves.
Splitting iid rows gives exactly the independent pilot/evaluation law.
Formal statement
Proof (Lean source)
Hybrid means can be evaluated in the combined-row experiment.
Formal statement
Proof (Lean source)
Hybrid variances can be evaluated in the combined-row experiment.
Formal statement
Proof (Lean source)
Fix the privacy budget, the natural-number parameter D, the coordinate index, and the function w. The hybrid rule applied to a single combined scaled column.
Definition (Lean source)
Each split hybrid statistic is an own-column statistic of the combined block.
Formal statement
Proof (Lean source)
The combined hybrid rule is measurable on real scaled columns.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Calibration.Global 12 declarations Finite original-record private value frontiers: Helpers/Calibration/Global.
Helpers/Calibration/Global
Finite original-record private value frontiers: Helpers/Calibration/Global.
Fix the privacy budget and the amplitude, the natural-number parameter D, the coordinate index, and the function z. Scaled explicit polynomial, lifted through distinct-person moments.
Definition (Lean source)
Fix the dimension and the block size and the privacy budget. Squared-noise scale for one evaluation block.
Definition (Lean source)
The explicit truncated Chebyshev approximation has no coefficients above its degree.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, the stated ha condition, dimension at least two, and the stated dm condition. Moment unbiasedness evaluates the finite polynomial at the true scaled contrast.
Formal statement
Proof (Lean source)
Assume the Cai–Low Chebyshev approximation theorem, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, the stated even condition, polynomial degree at least two, and the stated dm condition. On the global radius one half, the cited approximation controls the bias.
Formal statement
Proof (Lean source)
Finite Cauchy--Schwarz controls a sum of possibly dependent statistics.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, the stated hm d condition, and the stated hv condition. Half-radius rescaling converts the private moment bound to a common geometric bound.
Formal statement
Proof (Lean source)
Assume the Cai–Low Chebyshev approximation theorem, the stated even condition, polynomial degree at least two, and the stated hv condition. The cited coefficient bound has a convenient squared exponential form.
Formal statement
Proof (Lean source)
Assume the Cai–Low Chebyshev approximation theorem, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, the stated even condition, polynomial degree at least two, and the stated hm d condition. A finite polynomial second moment uses no independence between moment degrees.
Formal statement
Proof (Lean source)
Assume dimension at least two and the stated degree condition. The degree restriction converts the geometric second-moment bound to the paper's exponent.
Formal statement
Proof (Lean source)
Assume the Cai–Low Chebyshev approximation theorem, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, the stated even condition, polynomial degree at least two, the stated hm d condition, and the stated degree condition. The global polynomial's second moment is at most one quarter of the calibrated exponent.
Formal statement
Proof (Lean source)
Assume the Cai–Low Chebyshev approximation theorem, the bounded-mean concentration inequality, independent and identically distributed participant records, the causal-model conditions for the data law, an admissible sample size, dimension, and privacy budget, positive block size, a block no larger than the sample, the stated even condition, polynomial degree at least two, the stated hm d condition, and the stated degree condition. Global-radius calibration from the explicit approximation and bounded-mean gates.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Calibration.Hybrid 16 declarations Independent pilot/evaluation blocks, unbiased evaluation means, and exact three-branch identities for hybrid bias and centered squared error.
Helpers/Calibration/Hybrid
Independent pilot/evaluation blocks, unbiased evaluation means, and exact three-branch identities for hybrid bias and centered squared error. The C7 variance reduction, inside-window bias and second moment (C5/C8), and degree calibration (C2) are proved. Pilot tails (C4) and nonnegative inside-window bias and variance assembly are proved. Outside-window estimates remain open.
Independence factors a product of a pilot statistic and an evaluation statistic.
Formal statement
Proof (Lean source)
Assume the stated t condition. The central, positive, and negative pilot events partition all outcomes, including ties.
Formal statement
Proof (Lean source)
The implemented hybrid is exactly its three disjoint pilot branches.
Formal statement
Proof (Lean source)
Assume the stated t condition. Exact pilot branch probabilities sum to one under the finite block law.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, and the stated dm condition. Independence and moment unbiasedness give the exact signed hybrid bias identity (C3).
Formal statement
Proof (Lean source)
Squaring the hybrid error preserves the three disjoint pilot branches.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and positive block size. Reversing an unbiased evaluation mean adds exactly four squared contrasts to its error.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and positive block size. The exact centered-error identity conditions on the three pilot branches (C7 precursor).
Formal statement
Proof (Lean source)
A pilot branch indicator has expectation between zero and one.
Formal statement
Proof (Lean source)
Centering at any fixed target can only increase the hybrid second moment.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and positive block size. The exact branch identity and evaluation variance yield the roadmap's bound (C7).
Formal statement
Proof (Lean source)
Assume the stated l condition and the stated d condition. The stipulated even degree obeys both sides of the roadmap's window (C2).
Formal statement
Proof (Lean source)
Assume the Cai–Low Chebyshev approximation theorem, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, the stated l condition, the stated d condition, the stated dm condition, and the stated hx condition. Inside the pilot window, the approximation error has the explicit C5 rate.
Formal statement
Proof (Lean source)
Assume the Cai–Low Chebyshev approximation theorem, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, the stated l condition, the stated d condition, the stated hm d condition, and the stated hx condition. Within the approximation window, C1 gives the calibrated second moment (C8).
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, the stated l condition, the stated d condition, the stated dm condition, the stated hx condition, and the stated hwindow condition. C3, C4 and C5 assemble the hybrid bias bound for nonnegative inside-window contrasts.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, the stated l condition, the stated d condition, the stated hm d condition, the stated hx condition, and the stated hwindow condition. C4, C7 and C8 assemble the hybrid variance bound for nonnegative inside contrasts.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Calibration.HybridBasics 11 declarations Independent pilot/evaluation blocks, column means and their finite variance bounds.
Hybrid block basics
Independent pilot/evaluation blocks, column means and their finite variance bounds.
Fix the privacy budget, the coordinate index, and the function z. Mean of one scaled column.
Definition (Lean source)
Fix the probability law P, the privacy budget, and the block size. Independent pilot/evaluation blocks.
Definition (Lean source)
Fix the privacy budget, the natural-number parameter D, the coordinate index, and the function z. Centered pilot/evaluation hybrid column statistic.
Definition (Lean source)
Fix the probability law P, the privacy budget, and the function f. Hybrid expectation.
Fix the probability law P, the privacy budget, and the function f. Hybrid variance.
Definition (Lean source)
The threshold includes zero, so the sign-zero convention is never used outside it.
Formal statement
Proof (Lean source)
Assume a positive privacy budget, dimension at least two, and positive block size. Allowed positive resources give a strictly positive pilot threshold.
Formal statement
Proof (Lean source)
The independent two-block experiment is a probability measure.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and positive block size. The evaluation column mean is unbiased for the causal contrast.
Formal statement
Proof (Lean source)
Finite block variance is the second moment minus the squared mean.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and positive block size. The iid column mean has variance bounded by the declared noise variance.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Calibration.Outside 15 declarations Polynomial growth and Gaussian pilot suppression for steps C6 and C9 of finite calibration.
Outside-window hybrid calibration
Polynomial growth and Gaussian pilot suppression for steps C6 and C9 of finite calibration. Bias and variance assembly for all causal contrasts, inside and outside the window, using reflection for negative contrasts. Combined-column MSE and the final finite-calibration theorem are assembled in Calibration.Assembly.
Assume the stated hy condition. The logarithmic growth of an outside-window parameter is at most half its square.
Formal statement
Proof (Lean source)
Assume the Cai–Low Chebyshev approximation theorem, the stated even condition, polynomial degree at least two, and the stated hy condition. The finite coefficient envelope bounds the polynomial beyond its approximation window.
Formal statement
Proof (Lean source)
Assume the stated l condition, the stated hy condition, and the stated d condition. At the calibrated degree, the outside pilot tail dominates polynomial growth (C6).
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, the stated l condition, and the stated hx condition. The actual outside-window pilot tail has the normalized exponent used in C6.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, the stated l condition, the stated d condition, the stated dm condition, and the stated hx condition. Pilot suppression times unbiased polynomial growth gives the first outside C6 bound.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, the stated l condition, and the stated hx condition. The outside pilot tail also suppresses the first and second contrast powers in C6.
Formal statement
Proof (Lean source)
Assume the stated l condition. The exponentially small C6 residual is at most the reciprocal log dimension.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, the stated l condition, the stated d condition, the stated dm condition, and the stated hx condition. C3, C4 and C6 give the hybrid bias bound outside the window for nonnegative contrasts.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, the stated l condition, the stated d condition, the stated dm condition, and the stated hx condition. The inside and outside C6 cases cover every nonnegative contrast, including the boundary.
Formal statement
Proof (Lean source)
Assume the stated l condition, the stated hy condition, and the stated d condition. Gaussian pilot suppression dominates the squared polynomial growth in C9.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, the stated l condition, the stated d condition, the stated hm d condition, and the stated hx condition. C1 and the actual pilot tail yield the outside-window weighted second moment (C9).
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, the stated l condition, the stated d condition, the stated hm d condition, and the stated hx condition. C4, C7 and C9 assemble the outside-window variance bound for nonnegative contrasts.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, the stated l condition, the stated d condition, the stated hm d condition, and the stated hx condition. C8 and C9 cover all nonnegative contrasts, including the window boundary.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, the stated l condition, the stated d condition, and the stated dm condition. Reflection extends the C3--C6 bias assembly to both signs of every causal contrast.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, the stated l condition, the stated d condition, and the stated hm d condition. Reflection extends the C4/C7--C9 variance assembly to both signs of every causal contrast.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Calibration.PilotTails 11 declarations Hoeffding bounds for actual scaled vector-message column means, including the wrong-sign and central-window pilot events in the hybrid calibration roadmap (C4/C6).
Pilot concentration
Hoeffding bounds for actual scaled vector-message column means, including the wrong-sign and central-window pilot events in the hybrid calibration roadmap (C4/C6).
Assume a positive privacy budget and dimension at least two. Positive privacy and dimension give a positive noise scale.
Formal statement
Proof (Lean source)
A pilot column has independent rows under the product release law.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, and the stated hu condition. The Hoeffding gate applies to the actual pilot column, with the paper's variance scale.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, and the stated hx condition. The wrong-sign pilot branch has the one-sided C4 tail, including threshold ties.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, and the stated hx condition. Outside the approximation radius, the central pilot event has the C6 tail.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, and the stated hx condition. The wrong-sign exponent separates into a Gaussian contrast factor and exp(-8L).
Formal statement
Proof (Lean source)
Assume the stated hs condition. The elementary Gaussian first-moment envelope used in C4.
Formal statement
Proof (Lean source)
Assume the stated hs condition. The elementary Gaussian second-moment envelope used in C4.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, and the stated hx condition. Both contrast-weighted wrong-sign bounds in C4 hold for the actual pilot.
Formal statement
Proof (Lean source)
The indicator expectation equals the probability of the pilot event.
Formal statement
Proof (Lean source)
Assume the stated l condition. At log dimension at least one, the C4 residual is bounded by inverse root dimension.
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Calibration.Radius 3 declarations Scaled approximation and finite second-moment bounds for the evaluation polynomial.
Calibration at an arbitrary positive radius
Scaled approximation and finite second-moment bounds for the evaluation polynomial. The radius is unrestricted relative to the causal parameter cube.
Assume the Cai–Low Chebyshev approximation theorem, the causal-model conditions for the data law, a positive privacy budget, the stated ha condition, dimension at least two, the stated even condition, polynomial degree at least two, the stated dm condition, and the stated hx condition. The cited approximation scales to every positive window containing the contrast (C5).
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, the stated ha condition, dimension at least two, positive block size, the stated hm d condition, and the stated hv condition. Rescaled moment degrees share one geometric bound, without degree independence.
Formal statement
Proof (Lean source)
Assume the Cai–Low Chebyshev approximation theorem, the causal-model conditions for the data law, a positive privacy budget, the stated ha condition, dimension at least two, positive block size, the stated even condition, polynomial degree at least two, and the stated hm d condition. Arbitrary-radius counterpart of C1, with the sharper coefficient factor exp(5D).
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Calibration.Reflection 17 declarations The explicit Chebyshev approximation is even.
Reflection of hybrid column statistics
The explicit Chebyshev approximation is even. Reflecting the bits in both blocks therefore preserves the hybrid column statistic, including threshold ties. The affine row integral identifies the reflected vector law, its iid block product, and the independent two-block law; hybrid means and variances are invariant.
Only even Chebyshev orders occur in the explicit approximation.
Formal statement
Proof (Lean source)
Negating the input multiplies each monomial coefficient by its parity sign.
Formal statement
Proof (Lean source)
The parity-weighted coefficients of the even approximation are unchanged.
Formal statement
Proof (Lean source)
Every distinct-person product acquires the sign of its degree under reflection.
Formal statement
Proof (Lean source)
Reflecting every released bit negates every scaled entry.
Formal statement
Proof (Lean source)
The pilot and evaluation means change sign under bit reflection.
Formal statement
Proof (Lean source)
Parity of the coefficients cancels parity of the reflected private moments.
Formal statement
Proof (Lean source)
Simultaneous reflection preserves both hybrid branches and threshold ties.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law and dimension at least two. Averaging an original-record vector row has an affine integral determined by the contrasts.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, the causal-model conditions for the second law, dimension at least two, and the stated hx condition. Negating all contrasts reflects every released vector bit in a one-row experiment.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, the causal-model conditions for the second law, dimension at least two, and the stated hx condition. The reflected vector-message pushforward is the law with opposite contrasts.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, the causal-model conditions for the second law, dimension at least two, and the stated hx condition. Reflection commutes with the iid product of participant rows.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, the causal-model conditions for the second law, dimension at least two, and the stated hx condition. Reflecting both independent blocks gives the hybrid law with opposite contrasts.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, the causal-model conditions for the second law, dimension at least two, and the stated hx condition. The hybrid mean is unchanged by reversing the entire contrast vector.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, the causal-model conditions for the second law, dimension at least two, and the stated hx condition. The hybrid variance is unchanged by reversing the entire contrast vector.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law. Reversing a causal contrast vector preserves the symmetric construction's parameter cube.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law and dimension at least two. The symmetric law built from the reversed contrast has exactly that contrast.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.CitedGates 11 declarations Finite original-record private value frontiers: Helpers/CitedGates.
Helpers/CitedGates
Finite original-record private value frontiers: Helpers/CitedGates.
Fix the local protocol. Best uniform polynomial error for the absolute-value function.
Definition (Lean source)
Fix the natural-number parameter D. Explicit truncated first-kind Chebyshev absolute-value approximation.
Vákár and Ong (2018), Theorem 10 and proof, pp. 19–20; Definition 1 p. 8, finite-reference reduction p. 18. Handle: VakarOng2018SFinite, arXiv:1810.01837v2. Logical gate: jointly measurable density for finite dominated kernels.
Definition (Lean source)
Hoeffding (1963), Theorem 2, equal-range specialization, printed p. 16. Handle: Hoeffding1963Bounded, DOI 10.1080/01621459.1963.10500830. Logical gate: upper, lower and hence two-sided bounded mean tails.
Definition (Lean source)
Cai and Low (2011), Lemma 2, equations (24), (27), (28), p. 13, D=2K. Handle: CaiLow2011Nonsmooth, arXiv:1105.3039. Logical approximation gate.
Definition (Lean source)
Cai and Low (2011), Lemma 1, p. 10. Handle: CaiLow2011Nonsmooth, arXiv:1105.3039. Symmetric moment-matched probability measures with exact gap.
Definition (Lean source)
Cai and Low (2011), Section 3.1, p. 8, Bernstein constant paragraph; Bernstein (1913), pp. 1–2 and 55–56. Handle: CaiLow2011Nonsmooth, arXiv:1105.3039. Positive even-degree absolute approximation limit.
Definition (Lean source)
Every pointwise-dominated pair of finite kernels on a standard Borel target admits a jointly measurable Radon--Nikodym density representing each kernel measure.
Formal statement
Proof (Lean source)
Hoeffding's inequality for finite independent bounded real-valued families establishes the bounded-mean concentration gate.
Formal statement
Proof (Lean source)
The Cai--Low symmetric moment-matched prior gate follows from the extremal absolute-value approximation duality construction.
Formal statement
Proof (Lean source)
The Cai--Low Chebyshev absolute-value approximation gate follows from the public half-degree truncation bounds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Contraction.CanonicalDensity 18 declarations This module constructs transcript densities from fixed-record row densities and the explicit affine masses of iid observed-record vectors.
Canonical finite-sum transcript densities
This module constructs transcript densities from fixed-record row densities and the explicit affine masses of iid observed-record vectors. The resulting density represents the conditional transcript law and is polynomial of degree at most the sample size in each parameter coordinate.
Fix the function theta and the observed participant record. The explicit affine mass of one observed record under the symmetric experiment.
Fix the function theta and the function o. The explicit iid mass of a complete observed-record vector.
Definition (Lean source)
Fix the function f and the function w. The finite sum of fixed-record transcript-row densities weighted by iid affine masses.
Definition (Lean source)
Assume the stated htheta condition. An observed-record affine mass is nonnegative throughout the parameter cube. [](.
Formal statement
Proof (Lean source)
Assume the stated htheta condition. The product mass of an iid observed-record vector is nonnegative on the cube. [](.
Formal statement
Proof (Lean source)
A finite sum of jointly measurable row densities with affine weights is measurable when the row-density family is measurable.
Formal statement
Proof (Lean source)
Assume the stated htheta condition and positive dimension. The explicit affine mass equals the observed symmetric-law singleton probability.
Formal statement
Proof (Lean source)
Assume positive dimension. Every fixed-record transcript row is dominated by the zero-contrast transcript law.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels and the stated absolute-continuity property. The kernel RN gate admits a jointly measurable everywhere-nonnegative real density version.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels and positive dimension. The RN gate supplies nonnegative densities for all fixed-record transcript rows at once.
Formal statement
Proof (Lean source)
Assume the stated htheta condition and positive dimension. The extended-real iid affine mass is the product-law singleton mass on the cube.
Formal statement
Proof (Lean source)
Assume the stated htheta condition and positive dimension. The conditional transcript law is the finite affine mixture of fixed-record rows.
Formal statement
Proof (Lean source)
Assume the function hf and the stated htheta condition. Nonnegative fixed-row densities give a nonnegative canonical transcript density.
Formal statement
Proof (Lean source)
Assume measurability of f, the function hf0, the function hrep, the stated htheta condition, and positive dimension. The canonical finite-sum density represents the conditional transcript law.
Formal statement
Proof (Lean source)
Updating one coordinate writes each observed-record mass as an affine function. [](.
Formal statement
Proof (Lean source)
Every iid observed-vector mass has degree at most the sample size in one coordinate. [](.
Formal statement
Proof (Lean source)
A canonical finite-sum transcript density has degree at most the sample size coordinatewise. [](.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels and positive dimension. The RN gate yields a canonical measurable, nonnegative, coordinate-polynomial density version.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Contraction.CanonicalIdentification 9 declarations Countably many density identities identify the entire coordinate polynomial outside one reference-null set.
Simultaneous coordinate identification of transcript densities
Countably many density identities identify the entire coordinate polynomial outside one reference-null set. Thus the canonical finite-sum version and repaired stage product have the same derivatives, including at boundary parameters.
Assume the stated hx condition and the stated heq condition. Equality at an injective sequence identifies measurable families of real polynomials outside one null set, simultaneously at every real argument.
Formal statement
Proof (Lean source)
A coordinate section of a finite affine stage product is an actual real polynomial, also outside the parameter cube. [](.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated htheta condition, measurability of p, the protocol transcript, the protocol transcript, measurability of f, the stated hf0 condition, and the stated hprod rep condition. Simultaneous coordinate equality of the canonical density and the repaired stage product follows from their density representations. The exceptional set is independent of the coordinate argument, so derivatives may be compared there.
Formal statement
Proof (Lean source)
Assume the protocol transcript. All orders of coordinate differentiation preserve the simultaneous canonical-to-product identity. No differentiation of a parameter-dependent null set is used.
Formal statement
Proof (Lean source)
Assume the stated hpos condition. The elementary score formula for a finite stage family uses zero scores past the transcript horizon.
Formal statement
Proof (Lean source)
Assume the stated hpos condition and the stated heq condition. The canonical density has the exact factorial-times-density-times-elementary score identity almost everywhere, simultaneously in the derivative order.
Formal statement
Proof (Lean source)
Assume measurability of p, the stated hp0 condition, the stated hrep condition, the stated hpos condition, and the stated heq condition. The canonical derivative L1 integral is exactly the score first moment under the original parameter-specific transcript law. This identifies the measure needed for the adaptive martingale bound.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, positive dimension, a nonnegative privacy budget, and sequential local privacy of the protocol. The RN gate gives canonical finite-sum densities and repaired rows whose coordinate sections agree simultaneously outside one reference-null set. This certifies the identification needed before applying the martingale score bound.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, sequential local privacy of the protocol, sample size at least two, dimension at least two, and a privacy budget in the interval from zero to one. Full polynomial-density derivative certificate with the RN gate threaded.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Contraction.CanonicalTaylor 5 declarations The finite original-record representation has integrable coordinate coefficients.
Taylor remainders of the canonical transcript density
The finite original-record representation has integrable coordinate coefficients. Its derivative certificate therefore supplies the exact coordinate L1 Taylor remainder needed before moment cancellation and coordinate telescoping.
Assume measurability of f, the function hf0, and the function hrow. Each nonnegative fixed-record RN density is integrable because its represented transcript law is a probability measure.
Formal statement
Proof (Lean source)
Assume measurability of f, the function hf0, and the function hrow. The canonical density's polynomial coefficients are finite linear combinations of integrable fixed-record row densities.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, sequential local privacy of the protocol, and an admissible sample size, dimension, and privacy budget. The explicitly constructed canonical density has the same adaptive martingale derivative certificate as the existing density version. This retains the finite original-record polynomial as the source of every derivative.
Formal statement
Proof (Lean source)
Assume a nonnegative privacy budget, measurability of f, the function hf0, the function hrow, the stated hcert condition, the stated htheta condition, the stated hk condition, order no larger than the sample size, amplitude between zero and one half, and the stated hu condition. The canonical density certificate controls each coordinate Taylor remainder uniformly in the other coordinates, transcript seed, and signed amplitude.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, sequential local privacy of the protocol, and an admissible sample size, dimension, and privacy budget. The RN gate supplies a full density certificate together with the exact L1 Taylor remainder required by the moment-mixture argument.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Contraction.Density 17 declarations Finite original-record private value frontiers: Helpers/Contraction/Density.
Helpers/Contraction/Density
Finite original-record private value frontiers: Helpers/Contraction/Density.
Fix the dimension and the privacy budget. Coordinate privacy derivative scale.
Definition (Lean source)
Fix the dimension and the probability law nu. Product prior, independent of the public seed.
Fix the local protocol Q, the function theta, and the public seed. Fixed-seed transcript law after integrating iid observed records.
Definition (Lean source)
Fix the local protocol Q and the public seed. Reference transcript law under the zero vector.
Definition (Lean source)
Fix the sampling scheme S, the local protocol Q, and the probability law nu. Mixture seed/transcript law induced by a product prior.
Definition (Lean source)
Fix the amplitude and the probability law nu. Support and probability requirements of an amplitude prior.
Definition (Lean source)
Fix the order and the probability law nu0 and the probability law nu1. Moment equality below the cancellation degree.
Definition (Lean source)
Fix the function p, the function theta, the public seed, the protocol transcript, the coordinate index, and the order. Coordinate derivative of a proposed density version.
Definition (Lean source)
Fix the local protocol Q, the privacy budget, and the function p. Full density version, polynomiality and derivative assertions.
Definition (Lean source)
Fix the function theta. Clipping extends cube-indexed probability experiments to the whole parameter space.
Coordinatewise parameter clipping is measurable.
Formal statement
Proof (Lean source)
Clipped parameters belong to the declared cube. [](.
Formal statement
Proof (Lean source)
Assume the stated htheta condition. Clipping fixes all parameters of the declared experiment. [](.
Formal statement
Proof (Lean source)
Assume the stated htheta condition and positive dimension. Integrating fixed-input probability transcript laws preserves total mass.
Formal statement
Proof (Lean source)
Finite input summation makes the clipped transcript experiment jointly measurable when the record dimension is positive.
Formal statement
Proof (Lean source)
Assume positive dimension. Full support of the zero-contrast iid input law dominates every transcript experiment. [](.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, sequential local privacy of the protocol, sample size at least two, dimension at least two, and a privacy budget in the interval from zero to one. Density polynomial existence with its version identities, conditional on the RN gate.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Contraction.Derivative 23 declarations Finite original-record private value frontiers: Helpers/Contraction/Derivative.
Helpers/Contraction/Derivative
Finite original-record private value frontiers: Helpers/Contraction/Derivative.
Fix the function xi. Higher-order elementary-symmetric score recursion.
Definition (Lean source)
The zeroth elementary score is one at every sample size.
Formal statement
Proof (Lean source)
Assume the stated h condition. No subset of a prefix has cardinality greater than that prefix.
Formal statement
Proof (Lean source)
Assume the stated hb condition and the stated hxi condition. The bounded-score subset expansion has its deterministic binomial bound.
Formal statement
Proof (Lean source)
The recursion is the exact coefficient expansion of a finite product of affine factors.
Formal statement
Proof (Lean source)
Assume the stated hpos condition. A coordinate shift factors each positive affine stage density into its base density times one plus the shift times its conditional score. [](.
Formal statement
Proof (Lean source)
Assume the stated hpos condition. The explicit stage-density product has the elementary-score coefficient expansion at every parameter with positive stage densities.
Formal statement
Proof (Lean source)
Differentiation at zero extracts a finite polynomial coefficient with the factorial required by the density derivative bound.
Formal statement
Proof (Lean source)
Assume the stated hpos condition. Repeated coordinate differentiation of the explicit affine product is exactly factorial times the base product times the elementary conditional score.
Formal statement
Proof (Lean source)
Assume the stated hpos condition. The product-score identity in the original coordinate, including boundary parameters where the polynomial defines the derivative.
Formal statement
Proof (Lean source)
Elementary scores depend measurably only on the preceding increments when all increments before the cutoff are measurable.
Formal statement
Proof (Lean source)
Assume measurability of xi, the stated hb condition, and the stated hbound condition. Bounded score products have finite moments of every natural order.
Formal statement
Proof (Lean source)
Assume the stated hm condition, measurability of f, the stated hg condition, the stated hfg condition, and the stated hmean condition. Conditional mean zero kills a bounded, past-measurable cross term.
Formal statement
Proof (Lean source)
Assume measurability of xi, the stated hb condition, the stated hbound condition, and the stated hcross condition. Cross-term cancellation and bounded increments give the score second-moment recursion.
Formal statement
Proof (Lean source)
Assume measurability of xi, the stated hb condition, the stated hbound condition, and the stated hcross condition. The martingale score recursion yields the binomial second-moment bound.
Formal statement
Proof (Lean source)
An adapted score prefix is measurable with respect to its own past when the filtration is monotone and each increment is adapted.
Formal statement
Proof (Lean source)
Assume the stated f condition, the stated hle condition, measurability of adapt, the stated hb condition, the stated hbound condition, and the stated hmean condition. Bounded adapted martingale increments cancel every elementary-score cross term.
Formal statement
Proof (Lean source)
Assume the stated f condition, the stated hle condition, measurability of adapt, the stated hb condition, the stated hbound condition, and the stated hmean condition. The binomial bound holds for adaptive martingale scores, without independence.
Formal statement
Proof (Lean source)
Assume the stated f condition, the stated hle condition, measurability of adapt, the stated hb condition, the stated hbound condition, and the stated hmean condition. Cauchy–Schwarz converts the adaptive binomial second moment into the needed L1 bound.
Formal statement
Proof (Lean source)
Assume measurability of p, the stated hp0 condition, the stated hc condition, and the stated d condition. The density-times-score identity changes the derivative L1 integral into a factorial times the score first moment under the parameter-specific law.
Formal statement
Proof (Lean source)
Assume the stated hpos condition, measurability of p, the stated probability-measure property, the stated f condition, the stated hle condition, measurability of adapt, the stated hb condition, the stated hbound condition, and the stated hmean condition. The explicit affine stage product satisfies the sharp derivative L1 bound whenever its conditional scores are bounded martingale increments under its own density-weighted transcript law. This is the change-of-measure assembly used after identifying the stage product with the protocol density.
Formal statement
Proof (Lean source)
Assume the stated hk condition. Every derivative above the degree bound of a finite coefficient polynomial vanishes.
Formal statement
Proof (Lean source)
Assume the function hpoly and the stated hk condition. Coordinate polynomiality forces transcript-density derivatives above the sample size to vanish.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Contraction.ExactCancellation 13 declarations Expanding the finite iid input probabilities into coordinate monomials shows that matching moments above the sample degree identify the prior predictive input law.
Exact cancellation of finite iid experiments
Expanding the finite iid input probabilities into coordinate monomials shows that matching moments above the sample degree identify the prior predictive input law. Applying the same sequential decision kernel preserves this equality.
Grouping repeated coordinates turns a sample monomial into a product of powers. [](.
Formal statement
Proof (Lean source)
Assume the stated hnk condition and the stated hmom condition. Product priors with matching moments give identical sample monomial means.
Formal statement
Proof (Lean source)
Assume the stated ha condition and the stated hnu condition. Supported sample monomials are integrable without an extra moment assumption.
Formal statement
Proof (Lean source)
Assume the stated ha condition, the stated hnu0 condition, the stated hnu1 condition, the stated hnk condition, and the stated hmom condition. The affine sample likelihood has the same mean under moment-matched product priors.
Formal statement
Proof (Lean source)
Assume the stated htheta condition. The observed symmetric-law atom is affine in its cell contrast. [](.
Formal statement
Proof (Lean source)
Assume the stated ha condition, the stated hnu0 condition, the stated hnu1 condition, the stated hnk condition, and the stated hmom condition. Moment matching identifies the mean real mass of each iid input vector.
Formal statement
Proof (Lean source)
Assume positive dimension and the stated htheta condition. The affine iid mass is nonnegative and at most one on the parameter cube.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated ha condition, and the stated hnu condition. The affine iid mass is integrable under each supported product prior.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated ha condition, and the stated hnu condition. The clipped iid input mixture's atom equals the integral of its affine mass.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated ha condition, the stated hnu0 condition, the stated hnu1 condition, the stated hnk condition, and the stated hmom condition. Matching moments through the sample degree identify the entire finite input mixture.
Formal statement
Proof (Lean source)
Assume measurability of rows and measurability of f. Mapping the output of a measurable mixture commutes with mixing its rows.
Formal statement
Proof (Lean source)
Integrate the independent public seed and analyst coin after fixing the iid input vector.
Formal statement
Proof (Lean source)
Assume independent and identically distributed participant records, independent protocol randomness, positive dimension, the stated ha condition, the stated hnu0 condition, the stated hnu1 condition, the stated hnk condition, and the stated hmom condition. Exact input cancellation survives arbitrary sequential channels and independent seeds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Contraction.FiniteDensity 5 declarations Measurability, domination and real-valued density versions for finite input experiments.
Finite-mixture density helpers
Measurability, domination and real-valued density versions for finite input experiments.
Finite atomic laws depend measurably on their real weights when each atom's weight is measurable in the parameter.
Formal statement
Proof (Lean source)
The symmetric finite full-data construction is measurable in its parameter.
Formal statement
Proof (Lean source)
Assume positive dimension. At zero contrast every observed record has strictly positive mass.
Formal statement
Proof (Lean source)
Assume measurability of rows and the stated hpos condition. A mixture with positive mass on every finite input dominates every other mixture of the same rows, regardless of the output space.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels and the stated absolute-continuity property. The cited kernel RN gate supplies jointly measurable real densities for dominated Markov kernels; finiteness of each row permits conversion from extended densities.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Contraction.HistoryScore 15 declarations Fresh-input message kernels and the structural product density identify the actual history-message law.
Transcript-history martingale scores
Fresh-input message kernels and the structural product density identify the actual history-message law. Repaired row scores are adapted bounded martingale differences, giving the binomial elementary-score first-moment bound.
Assume measurability of x, measurability of y, the stated hlaw condition, measurability of s, the stated hb condition, and the stated hzero condition. A bounded score centered in each conditional message law is centered given history under any transcript law with the corresponding history-message marginal.
Formal statement
Proof (Lean source)
Fix the local protocol Q, the function theta, and the participant index. The conditional message kernel obtained by integrating a fresh paired input.
Definition (Lean source)
Assume the stated htheta condition and positive dimension. The fresh-input message kernels have unit mass on the parameter cube.
Formal statement
Proof (Lean source)
Assume the stated htheta condition, measurability of f, the stated hf0 condition, and the Markov kernel hrow. Repaired row densities represent the fresh-input message kernel.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated htheta condition, measurability of f, the stated hf0 condition, the Markov kernel hrow, the stated href condition, and the stated hprod condition. Structural iteration of the conditional message densities identifies the parameter-specific chain with the original-record transcript experiment.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated htheta condition, and the Markov kernel hchain. The actual transcript law has the fresh-input history-message marginal, including on adaptive histories in arbitrary standard-Borel message spaces.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated htheta condition, a nonnegative privacy budget, measurability of f, the stated hbound condition, the stated hpriv condition, the Markov kernel hrow, and the Markov kernel hchain. The repaired coordinate score has zero conditional expectation given the actual original-record transcript history.
Formal statement
Proof (Lean source)
Fix the local protocol Q and the natural-number parameter v. Transcript information available by a stage, held constant after the horizon.
Definition (Lean source)
Every history sigma-algebra is contained in the full transcript sigma-algebra.
Formal statement
Proof (Lean source)
Transcript histories form an increasing family of sub-sigma-algebras.
Formal statement
Proof (Lean source)
Fix the local protocol Q, the function theta, the public seed, the function f, the coordinate index, the natural-number parameter v, and the protocol transcript. The conditional coordinate scores are extended by zero after the horizon.
Definition (Lean source)
Each stage score is measurable once its message has been observed when the repaired row densities are measurable.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated htheta condition, a nonnegative privacy budget, the stated hbound condition, and the stated hpriv condition. The sharp privacy envelope bounds all scores, including their zero extension.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated htheta condition, a nonnegative privacy budget, measurability of f, the stated hbound condition, the stated hpriv condition, the Markov kernel hrow, and the Markov kernel hchain. The extended scores are martingale differences for transcript history.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated htheta condition, a nonnegative privacy budget, measurability of f, the stated hbound condition, the stated hpriv condition, the Markov kernel hrow, and the Markov kernel hchain. Transcript martingale certification gives the binomial first-moment bound for the elementary score polynomial under the actual experiment law.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Contraction.JointSeed 8 declarations The sampling atoms identify the joint seed/transcript law with the fixed-seed experiment integrated against the same independent public-seed law.
Public-seed disintegration of supported transcript mixtures
The sampling atoms identify the joint seed/transcript law with the fixed-seed experiment integrated against the same independent public-seed law. Supported product priors can then be integrated before the public seed.
Appending the public seed to the clipped conditional experiment is jointly measurable when the record dimension is positive.
Formal statement
Proof (Lean source)
Assume independent and identically distributed participant records, independent protocol randomness, positive dimension, and the stated htheta condition. The sampling assumptions give the common-seed representation at every cube parameter.
Formal statement
Proof (Lean source)
Assume measurability of rows. Jointly measurable measure rows remain measurable after integrating one independent index.
Formal statement
Proof (Lean source)
Assume measurability of rows. Independent mixing indices commute for jointly measurable measure rows.
Formal statement
Proof (Lean source)
Assume independent and identically distributed participant records, independent protocol randomness, positive dimension, the stated ha condition, and the stated hnu condition. Supported product priors mix conditionally before the independent public seed.
Formal statement
Proof (Lean source)
Assume measurability of rows, the stated probability-measure property, measurability of p, the stated hnonneg condition, and the stated hdensity condition. A probability mixture has the prior-averaged real density against its common reference. This is the arbitrary-parameter version of the scalar-prior mixture likelihood identity.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated hp condition, the stated ha condition, and the stated hnu condition. The supported fixed-seed mixture is represented by the average of the given density version.
Formal statement
Proof (Lean source)
Assume independent and identically distributed participant records, independent protocol randomness, positive dimension, the stated hp condition, the stated ha condition, and the stated hnu condition. Joint seed/transcript mixtures use the same seed law and the prior-integrated conditional density, including arbitrary public seeds of law-zero mass.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Contraction.Mixture 7 declarations Finite original-record private value frontiers: Helpers/Contraction/Mixture.
Helpers/Contraction/Mixture
Finite original-record private value frontiers: Helpers/Contraction/Mixture.
Assume measurability of p, measurability of q, the stated hp0 condition, the stated hq0 condition, the stated hmu condition, and the stated hnu condition. Probability densities against a common reference obey the half-L1 TV bound.
Formal statement
Proof (Lean source)
Assume measurability of m, the stated probability-measure property, and the set hE. Real event masses of measurable probability mixtures are averages of row masses.
Formal statement
Proof (Lean source)
Assume measurability of m0, measurability of m1, the stated probability-measure property, the stated probability-measure property, and the stated b condition. A uniform rowwise TV bound survives mixing with the same independent seed law.
Formal statement
Proof (Lean source)
Assume measurability of f. Applying a measurable transcript map cannot increase TV.
Formal statement
Proof (Lean source)
Assume the stated hp condition, the stated ha condition, and the stated hnu condition. The supported conditional mixture has a measurable, nonnegative real density.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated hp condition, the stated ha condition, the stated hnu0 condition, and the stated hnu1 condition. Fixed-seed supported transcript mixtures obey their density L1 bound.
Formal statement
Proof (Lean source)
Adaptive higher-order transcript contraction holds for arbitrary public seeds and randomized tests when the measurable-kernel Radon–Nikodym property, iid sampling, independent randomness, sequential ε-local privacy, and the admissible parameter regime hold.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Contraction.MixtureProbability 6 declarations Clipped measurable experiment versions agree with the original sampling scheme on the parameter cube.
Probability laws for supported transcript mixtures
Clipped measurable experiment versions agree with the original sampling scheme on the parameter cube. Supported product priors therefore induce probability mixtures, to which the bounded-statistic total-variation inequality applies.
Finite iid input laws vary measurably with their atom probabilities when the one-sample laws vary measurably and each such law is finite.
Formal statement
Proof (Lean source)
Clipping gives a globally measurable canonical decision experiment when the record dimension is positive.
Formal statement
Proof (Lean source)
Assume independent and identically distributed participant records, independent protocol randomness, positive dimension, and the stated htheta condition. The sampling hypotheses identify decision laws with their clipped versions on the cube.
Formal statement
Proof (Lean source)
Assume the stated ha condition and the stated hnu condition. A supported coordinate prior places its entire product mass in the parameter cube.
Formal statement
Proof (Lean source)
Assume independent and identically distributed participant records, independent protocol randomness, positive dimension, the stated ha condition, and the stated hnu condition. Every supported mixture is a probability law, even for a sampling scheme specified only through its iid and independent-randomness properties.
Formal statement
Proof (Lean source)
Assume independent and identically distributed participant records, independent protocol randomness, positive dimension, the stated ha condition, the stated hnu0 condition, the stated hnu1 condition, measurability of f, and the protocol transcript. Arbitrary Borel randomized transcript statistics obey the mixture TV bound.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Contraction.PriorAverage 6 declarations The canonical finite-row representation justifies Fubini for a coordinate replacement averaged over any probability law supported on the parameter cube.
Averaging coordinate replacements
The canonical finite-row representation justifies Fubini for a coordinate replacement averaged over any probability law supported on the parameter cube. The exact single-coordinate L1 cost is preserved by this averaging.
Assume the stated htheta condition, the stated ha condition, and the stated hu condition. Replacing a cube coordinate by a supported amplitude stays in the cube.
Formal statement
Proof (Lean source)
Assume positive dimension and the stated htheta condition. An iid affine input mass lies between zero and one on the cube.
Formal statement
Proof (Lean source)
Assume positive dimension, the function hpi, the stated ha condition, and the stated hnu condition. Supported coordinate-averaged affine masses are integrable over any probability law on the remaining contrasts.
Formal statement
Proof (Lean source)
Assume the stated f condition and the stated b condition. Probability averaging preserves a uniform L1 bound.
Formal statement
Proof (Lean source)
Assume a nonnegative privacy budget, positive dimension, measurability of f, the function hf0, the function hrow, the stated hcert condition, the function hpi, amplitude between zero and one half, the stated hnu0 condition, the stated hnu1 condition, the stated hk condition, order no larger than the sample size, and the stated hmom condition. Integrating the remaining contrasts under any cube-supported probability law preserves the exact single-coordinate matched-prior contraction cost.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, sequential local privacy of the protocol, and an admissible sample size, dimension, and privacy budget. The RN gate supplies a canonical certificate whose coordinate contraction is already averaged over every supported remaining-coordinate prior.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Contraction.PriorCoordinate 3 declarations Testing a finite polynomial family against the sign of its prior density difference reduces its L1 contraction to scalar moment cancellation.
Single-coordinate matched-prior integration
Testing a finite polynomial family against the sign of its prior density difference reduces its L1 contraction to scalar moment cancellation. All integration exchanges are finite coefficient sums.
Assume the stated hc condition, nonnegative amplitude, a nonnegative bias bound, the stated hnu0 condition, the stated hnu1 condition, the stated hk condition, the stated hmom condition, and the stated hderiv condition. Matched supported priors contract an integrable finite polynomial density family by twice the uniform coordinate Taylor remainder radius.
Formal statement
Proof (Lean source)
Assume a nonnegative privacy budget, measurability of f, the function hf0, the function hrow, the stated hcert condition, the stated htheta condition, amplitude between zero and one half, the stated hnu0 condition, the stated hnu1 condition, the stated hk condition, order no larger than the sample size, and the stated hmom condition. A single coordinate replacement between moment-matched priors has the exact L1 cost, uniformly over the other contrasts and every public seed.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, sequential local privacy of the protocol, and an admissible sample size, dimension, and privacy budget. The RN construction provides one canonical density certificate and all single-coordinate matched-prior L1 bounds needed for product-prior telescoping.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Contraction.PriorTelescoping 13 declarations Intervening product priors replace coordinates one at a time.
Product-prior coordinate telescoping
Intervening product priors replace coordinates one at a time. Independent coordinate replacement identifies each adjacent density difference with the averaged coordinate difference, so the exact L1 costs add over the dimension.
Replacing a coordinate by an independent draw updates its product-law factor.
Formal statement
Proof (Lean source)
Assume the probability law hg. Fubini turns an independent coordinate replacement into an updated product integral.
Formal statement
Proof (Lean source)
Fix the probability law nu0 and the probability law nu1, the natural-number parameter v, and the coordinate index. The first v coordinates use the second prior and all others use the first.
Assume the stated hnu0 condition and the stated hnu1 condition. All intervening coordinate laws remain supported probability measures.
Formal statement
Proof (Lean source)
Assume the stated ha condition, the stated hnu0 condition, and the stated hnu1 condition. Intervening product laws give full mass to the parameter cube.
Formal statement
Proof (Lean source)
Assume the stated hv condition. The next hybrid law changes exactly the next coordinate.
Formal statement
Proof (Lean source)
Assume the stated hv condition. Resampling the next coordinate from the first prior leaves the current hybrid law unchanged.
Formal statement
Proof (Lean source)
Assume positive dimension and the function hpi. A cube-supported probability law integrates every affine sample mass.
Formal statement
Proof (Lean source)
Assume positive dimension and the function hpi. Canonical densities are integrable in the prior parameter at every transcript.
Formal statement
Proof (Lean source)
Assume positive dimension, measurability of f, the function hf0, the function hrow, and the function hpi. The finite-row representation makes each prior-averaged density integrable in the transcript.
Formal statement
Proof (Lean source)
Assume the stated h condition and the stated hstep condition. The L1 triangle inequality adds the costs along a finite chain of densities.
Formal statement
Proof (Lean source)
Assume a nonnegative privacy budget, positive dimension, measurability of f, the function hf0, the function hrow, the stated hcert condition, amplitude between zero and one half, the stated hnu0 condition, the stated hnu1 condition, the stated hk condition, order no larger than the sample size, and the stated hmom condition. Coordinate replacement and the exact averaged-coordinate bound telescope to an L1 bound for the two full product-prior densities at each fixed seed.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, sequential local privacy of the protocol, and an admissible sample size, dimension, and privacy budget. The RN gate supplies a canonical density certificate with the full product-prior L1 contraction bound at every seed.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Contraction.StageDensity 11 declarations Uniform finite averages dominate each input row.
Stagewise reference densities
Uniform finite averages dominate each input row. Applying the measurable kernel Radon–Nikodym gate to these stage references gives jointly measurable nonnegative real densities, at every history and seed, for the ancillary-averaged protocol.
Fix the Markov kernel K. Uniform averaging of finitely many probability kernels at a common parameter.
Definition (Lean source)
Assume the Markov kernel hK. A uniform average of a nonempty finite family of Markov kernels is Markov.
Formal statement
Proof (Lean source)
Every row is dominated by the uniform finite average, with no privacy premise.
Formal statement
Proof (Lean source)
Assume the Markov kernel hK, measurability of f, the stated hf0 condition, and the stated hrep condition. Finite row densities have average one almost everywhere under their reference.
Formal statement
Proof (Lean source)
Assume measurability of f, measurability of g, the stated hg0 condition, the stated hc condition, and the set hpriv. An all-event privacy inequality transfers to any measurable density versions.
Formal statement
Proof (Lean source)
Assume the stated privacy condition for the protocol, measurability of f, the stated hf0 condition, the stated hrep condition, a privacy factor at least one, and the stated hpriv condition. A common measurable null-set repair makes normalization and privacy pointwise, without changing any represented row at any parameter.
Formal statement
Proof (Lean source)
Fix the local protocol Q and the participant index. Stage reference rows are the uniform average of all paired-input rows, with the ancillary assignment already integrated out.
Definition (Lean source)
Assume positive dimension. Each stage reference is a probability kernel, including at null histories.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels and positive dimension. The measurable RN gate gives nonnegative stage densities jointly in input, seed, history and message. The reference is the uniform input average, rather than a whole-transcript RN witness.
Formal statement
Proof (Lean source)
Assume the stated hc condition, the stated hsum condition, and the stated hpriv condition. Uniform normalization and pairwise privacy bound each row away from zero and above by the privacy factor.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, positive dimension, a nonnegative privacy budget, and sequential local privacy of the protocol. Repaired stage densities jointly represent every private paired-input row and satisfy exact uniform normalization and privacy at every message, history and seed.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Contraction.StageIdentification 7 declarations At each fixed public seed, ancillary reconstruction identifies the paired adaptive experiment with the original-record experiment.
Original-record identification of stage products
At each fixed public seed, ancillary reconstruction identifies the paired adaptive experiment with the original-record experiment. Consequently the structural stage product represents the transcript law relative to its zero-contrast reference.
Assume the stated htheta condition and positive dimension. Integrating the independent reconstruction bits identifies the full transcript law at every fixed seed, including seeds of public-law measure zero.
Formal statement
Proof (Lean source)
Assume positive dimension, measurability of f, the stated hf0 condition, the stated hsum condition, and the function hrep. The uniform stage chain is the actual zero-contrast reference experiment.
Formal statement
Proof (Lean source)
Assume the stated htheta condition, positive dimension, measurability of f, the stated hf0 condition, the stated hsum condition, and the function hrep. The explicit affine stage product represents the original-record transcript law with the exact reference measure used by the derivative certificate.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, positive dimension, a nonnegative privacy budget, and sequential local privacy of the protocol. Repaired protocol rows give the original experiment an explicit stage-product RN density, while retaining the row normalization and privacy needed by scores.
Formal statement
Proof (Lean source)
The affine product of the repaired rows is jointly measurable in the parameter, public seed, and complete adaptive transcript when every repaired row is measurable.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated htheta condition, a nonnegative privacy budget, the stated hbound condition, and the stated hpriv condition. Every score of the actual adaptive transcript has the sharp deterministic privacy bound, with a strictly positive denominator at all histories.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated htheta condition, measurability of p, the protocol transcript, the stated hp rep condition, measurability of f, the stated hf0 condition, the stated hsum condition, and the function hrep. Any nonnegative measurable density certificate agrees almost everywhere with the explicit product. This applies to the existing canonical finite-sum version without selecting another whole-transcript Radon–Nikodym witness.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Contraction.StageProduct 11 declarations A structural prefix construction carries row-level Radon–Nikodym densities through adaptive history extension.
Sequential products of stage densities
A structural prefix construction carries row-level Radon–Nikodym densities through adaptive history extension. The density is an explicit product of the stage factors.
Assume the density or prior under consideration, measurability of p, the function f, measurability of f, and the stated hrow condition. Weighting the preceding history and the conditional next-message law multiplies their densities, including for kernels depending on the whole history.
Formal statement
Proof (Lean source)
Assume measurability of g, the density or prior under consideration, and measurability of p. A density which is measurable on the target space commutes with pushforward when pulled back along the history-extension map.
Formal statement
Proof (Lean source)
Fix the function f, the order, and order no larger than the sample size. The prefix density is constructed structurally by multiplying the next factor by the density of the preceding prefix.
Definition (Lean source)
The prefix product formed from a stage-density family is measurable when each stage density is measurable and the prefix length does not exceed the horizon.
Formal statement
Proof (Lean source)
Assume the function f and one plus the stage index no larger than the sample size. Appending a message exposes exactly the preceding product and the new factor.
Formal statement
Proof (Lean source)
Assume the Markov kernel hK, the Markov kernel hL, the function f, measurability of f, the stated hrow condition, and order no larger than the sample size. Iterating the row density identities gives an explicit density for every finite prefix of the adaptive experiment. No transcript RN witness is chosen.
Formal statement
Proof (Lean source)
Assume the function f and order no larger than the sample size. The structural prefix construction is the finite product of the densities evaluated at their own stage message and preceding history.
Formal statement
Proof (Lean source)
Fix the local protocol Q and the public seed. The uniform next-message kernels generate a fixed-seed reference chain.
Definition (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, positive dimension, a nonnegative privacy budget, and sequential local privacy of the protocol. Repaired stage rows yield explicit product densities for every fixed paired input transcript, relative to the same uniform reference chain.
Formal statement
Proof (Lean source)
Assume the stated htheta condition, positive dimension, measurability of f, the stated hf0 condition, and the function hrep. The density of a paired iid transcript factors into the affine conditional message densities at its actual adaptive histories.
Formal statement
Proof (Lean source)
Assume positive dimension, measurability of f, the stated hf0 condition, the stated hsum condition, and the function hrep. Exact uniform normalization identifies the reference chain as the zero-contrast iid paired experiment, at every seed.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Contraction.StageScore 13 declarations The repaired finite row densities give positive affine stage mixtures.
Conditional stage scores
The repaired finite row densities give positive affine stage mixtures. Their coordinate scores have the sharp privacy bound and zero mean under the parameter-specific conditional message law.
Fix the function theta and the amplitude. The affine paired-input probability weights.
Definition (Lean source)
Fix the function theta and the function f. The parameter-specific stage density relative to the uniform row average.
Definition (Lean source)
Fix the function f and the coordinate index. The coordinate slope of the affine conditional density.
Definition (Lean source)
Assume the stated htheta condition. Cube parameters give nonnegative conditional input weights. [](.
Formal statement
Proof (Lean source)
Assume positive dimension. The affine input weights sum to one, even outside the cube. [](.
Formal statement
Proof (Lean source)
Splitting the two signs exposes the affine coordinate coefficients. [](.
Formal statement
Proof (Lean source)
Assume positive dimension and the stated hsum condition. Exact row normalization makes the zero-contrast conditional density one.
Formal statement
Proof (Lean source)
Replacing one parameter coordinate changes a stage density by its exact slope. [](.
Formal statement
Proof (Lean source)
Assume the stated hw condition, the stated hsum condition, the stated hf condition, a privacy factor at least one, and the stated hpriv condition. A convex mixture of private rows inherits their minimum, and every row difference is bounded by the privacy excess times that same minimum.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated htheta condition, the stated hf condition, a nonnegative privacy budget, and the stated hpriv condition. The sharp coordinate score bound follows from privacy and convex weighting, without losing a factor from the lower bound on each input weight.
Formal statement
Proof (Lean source)
Assume measurability of f, the stated hf0 condition, and the stated probability-measure property. Every normalized probability-row density has real integral one.
Formal statement
Proof (Lean source)
Assume measurability of f, the stated hf0 condition, the stated hb condition, the stated hbound condition, the stated probability-measure property, and the stated hpos condition. Under the parameter-specific conditional law, dividing the zero-integral coordinate slope by its positive density preserves zero mean.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, positive dimension, a nonnegative privacy budget, and sequential local privacy of the protocol. The RN gate supplies actual jointly measurable protocol-row versions whose conditional coordinate scores satisfy both martingale prerequisites, at every history and seed (including reference-null histories).
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Contraction.StageTransition 5 declarations The affine mixtures of repaired stage rows represent the actual next-message laws of the symmetric iid experiment, at every history and public seed.
Conditional message density identification
The affine mixtures of repaired stage rows represent the actual next-message laws of the symmetric iid experiment, at every history and public seed.
Assume the stated hw condition, measurability of f, the stated hf0 condition, measurability of rows, and the stated hrep condition. Mixing finitely many nonnegative row densities commutes with taking the message law, with the original finite input weights retained.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated htheta condition, measurability of f, the stated hf0 condition, and the Markov kernel hrep. The affine paired mixture is the conditional next-message density for the original-record experiment after the ancillary bit is integrated out.
Formal statement
Proof (Lean source)
Assume positive dimension. The zero-contrast next-message law is exactly the uniform row reference, including at histories that have zero transcript probability.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated htheta condition, and the stated hbound condition. A convex stage mixture inherits the deterministic positive bounds on all its rows. These bounds make every finite transcript product integrable.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, positive dimension, a nonnegative privacy budget, and sequential local privacy of the protocol. The repaired jointly measurable stage densities simultaneously represent the actual original-record next-message law and give bounded zero-mean coordinate scores under that law. This identifies the measures needed by the transcript martingale argument, rather than an abstract density-weighted proxy.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Contraction.TaylorRemainder 8 declarations Taylor expansion at zero works on either side of zero with the exact factorial constant.
Exact Taylor cancellation for the contraction argument
Taylor expansion at zero works on either side of zero with the exact factorial constant. Matching moments cancel its finite polynomial; only the remainders contribute to a difference of supported prior means.
Assume the stated hf condition and the stated hu condition. On a nondegenerate interval, the Taylor polynomial of a globally smooth function uses its ordinary derivatives, including at an endpoint.
Formal statement
Proof (Lean source)
Assume the stated hk condition, the stated hf condition, nonnegative amplitude, the stated hu condition, a nonnegative bias bound, and the stated hderiv condition. A uniform kth derivative bound gives the exact Taylor remainder bound at zero, for positive and negative coordinates alike.
Formal statement
Proof (Lean source)
Assume the stated hnu condition and the stated hf condition. Compactly supported probability priors integrate every continuous scalar coordinate function; no extra moment hypothesis is needed.
Formal statement
Proof (Lean source)
Assume the stated hnu0 condition, the stated hnu1 condition, and the stated hmom condition. Matching moments cancel any finite Taylor polynomial of degree below k.
Formal statement
Proof (Lean source)
Assume nonnegative amplitude, a nonnegative bias bound, the stated hnu0 condition, the stated hnu1 condition, the stated hk condition, the stated hmom condition, the stated hf condition, and the stated hderiv condition. A matched pair of supported priors differs only through Taylor remainders. The exact derivative bound yields twice the single-prior remainder radius.
Formal statement
Proof (Lean source)
Assume the stated hc condition. Derivatives of a finite polynomial density family are integrable whenever its coefficients are integrable.
Formal statement
Proof (Lean source)
Assume the stated hc condition. Coefficientwise integration commutes with every coordinate derivative of an integrable finite polynomial density family.
Formal statement
Proof (Lean source)
Assume the stated hc condition, the stated hk condition, nonnegative amplitude, the stated hu condition, a nonnegative bias bound, and the stated hderiv condition. A finite polynomial family with a uniform kth-derivative L1 bound has the exact coordinate Taylor remainder bound in L1. Testing against the sign of the remainder reduces the assertion to scalar Taylor's theorem, avoiding any parameter-dependent exceptional sets.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Decision 13 declarations Finite original-record private value frontiers: Helpers/Decision.
Helpers/Decision
Finite original-record private value frontiers: Helpers/Decision.
Fix the local protocol Q. Measurable decisions using only transcript, seed and analyst randomizer.
Definition (Lean source)
Fix the local protocol Q and the real parameter lower and the real parameter upper. Connected, ordered, closed interval decisions in a fixed range.
Definition (Lean source)
Fix the probability law L, the estimator T, and the real parameter v. Extended nonnegative squared-error expectation; infinite risks stay infinite.
Definition (Lean source)
Fix the probability law L and the interval procedure I. Expected connected interval length.
Definition (Lean source)
Fix the probability law L, the interval procedure I, and the real parameter v. Coverage of a deterministic population target.
Definition (Lean source)
Fix the probability law M, the probability law target, the local protocol laws, the protocol-class label, and the privacy budget. Generic decision value over a law class and a population target.
Definition (Lean source)
Fix the probability law M, the probability law target, the local protocol laws, the protocol-class label, and the privacy budget and the real parameter lower and the real parameter upper. Generic globally honest connected-interval value.
Definition (Lean source)
Fix the sampling scheme S, the protocol-class label, and the privacy budget. Mechanism-optimal scalar causal risk.
Definition (Lean source)
Fix the sampling scheme S, the protocol-class label, and the privacy budget. Globally 0.90-honest connected causal interval length.
Definition (Lean source)
Fix the local protocol Q. Finite alphabet certificate for attaining protocols.
Definition (Lean source)
Fix the local protocol Q and the estimator T. A decision is transcript-only when the public and analyst coins do not alter it.
Definition (Lean source)
Fix the sampling scheme S and the privacy budget and the public seed and the stated h condition and the constant C0. A concrete NI protocol and decisions attaining both upper orders.
Definition (Lean source)
NI optimization is over a smaller protocol class.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.DecisionCompletion 3 declarations Finite atomic sampling weights extend the canonical experiment to all population measures.
A measurable completion of the iid decision experiment
Finite atomic sampling weights extend the canonical experiment to all population measures. On probability laws this extension is exactly the iid experiment.
Fix the local protocol Q and the probability law P. Atomic iid weights followed by the fixed protocol and its independent coins.
Definition (Lean source)
For every protocol, the completed finite atomic decision law is measurable even off the probability model.
Formal statement
Proof (Lean source)
On probability populations, atomic sampling is the canonical iid experiment.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.DecisionSampling 6 declarations Probability, measurability and independent analyst-coin factorization of causal decision laws.
Sampling and analyst randomness
Probability, measurability and independent analyst-coin factorization of causal decision laws.
The finite causal value is measurable in the population law.
Formal statement
Proof (Lean source)
A sampling scheme whose law is measurable induces a measurable decision experiment.
Formal statement
Proof (Lean source)
Assume independent and identically distributed participant records, independent protocol randomness, and the causal-model conditions for the data law. The two sampling conditions identify the input law, including both independent coins.
Formal statement
Proof (Lean source)
Assume independent and identically distributed participant records, independent protocol randomness, and the causal-model conditions for the data law. Every causal decision row is a probability law under the stated sampling scheme.
Formal statement
Proof (Lean source)
Assume the set hE, the set hF, and the set hG. Rectangle probabilities separate the independent analyst coin from the transcript experiment.
Formal statement
Proof (Lean source)
Assume independent and identically distributed participant records, independent protocol randomness, and the causal-model conditions for the data law. The analyst coin remains independent after any sequential transcript is generated.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Frontier.BaselineCalibration 11 declarations The first block releases randomized-response outcomes.
Binary baseline calibration
The first block releases randomized-response outcomes. Its estimate is unbiased, and independence of different people gives the baseline squared-error bound.
Every attaining row is a probability kernel, including the constant branch.
Formal statement
Proof (Lean source)
Assume the stated hn condition and the stated hi condition. A baseline row releases a sign with the randomized-response conditional mean.
Formal statement
Proof (Lean source)
The observed outcome sign has mean twice the baseline minus one.
Formal statement
Proof (Lean source)
Assume the stated hn condition and the stated hi condition. Averaging original records gives the baseline row's unconditional mean.
Formal statement
Proof (Lean source)
Averaging any attaining row over a probability input law preserves mass one.
Formal statement
Proof (Lean source)
Assume the stated hn condition, the stated hg condition, and the stated hbase condition. Distinct baseline rows have additive variances and the prescribed total mean.
Formal statement
Proof (Lean source)
The baseline block lies in the declared participant horizon.
Formal statement
Proof (Lean source)
The transcript's natural-number sum is exactly its in-horizon baseline block.
Formal statement
Proof (Lean source)
Assume the stated hn3 condition and a privacy budget in the interval from zero to one. The actual binary baseline estimate has the roadmap's finite-block MSE.
Formal statement
Proof (Lean source)
The baseline block contains at least one third of the people.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget and the stated hn condition. Equation (11)'s binary counterpart: baseline MSE is at most twelve over t.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Frontier.BlockSampling 5 declarations Selecting distinct vector-release rows recovers the iid vector experiment used by the finite moment calibration.
Vector blocks extracted from the attaining transcript
Selecting distinct vector-release rows recovers the iid vector experiment used by the finite moment calibration.
Assume the stated hn condition and the stated hi condition. A vector-release row has exactly the signed-vector marginal.
Formal statement
Proof (Lean source)
Assume the stated hn condition and the stated hi condition. Averaging inputs preserves the vector marginal of every vector-release row.
Formal statement
Proof (Lean source)
Assume the stated hn condition, the stated hg condition, and the stated hvec condition. Selecting distinct vector-release rows yields independent vector messages.
Formal statement
Proof (Lean source)
Assume the stated hn condition, the stated hstart condition, and the stated hend condition. Any in-horizon contiguous vector block has the calibrated iid block law.
Formal statement
Proof (Lean source)
Assume the stated hn condition, the stated hstart condition, and the stated hend condition. Expectations of extracted vector-block statistics equal their calibration expectations.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Frontier.CausalPriorDecision 5 declarations Supported symmetric-law priors retain the transcript contraction bound after passing to law space.
Causal product priors in the measurable decision experiment
Supported symmetric-law priors retain the transcript contraction bound after passing to law space. The measurable completion lets the separated-mixture reduction apply to every sampling scheme satisfying iid and independent coins.
The finite causal model is a Borel set of population laws.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated ha condition, and the stated hnu condition. Supported parameter priors push forward into the unchanged causal class.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated ha condition, and the stated hnu condition. The completed law-space decision marginal equals the parameter transcript mixture.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, sequential local privacy of the protocol, an admissible sample size, dimension, and privacy budget, the stated hnu0 condition, the stated hnu1 condition, and the stated hmatch condition. Prescribed amplitude and matching degree make the causal law-space transcript mixtures at most one hundredth apart, including orders beyond the sample size.
Formal statement
Proof (Lean source)
Assume independent and identically distributed participant records, independent protocol randomness, the stated support condition, the stated support condition, strict separation of the two target values, the stated concentration near the target value, the stated concentration near the target value, and the probability law hTV. Law-space separated priors give the stated causal risk and honest interval bounds for every iid scheme with independent public and analyst randomness.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Frontier.ContractionCalibration 8 declarations The binomial and privacy bounds turn the adaptive contraction coefficient into its resource-normalized geometric form, as in equation (15) of the proof.
Geometric calibration of adaptive contraction
The binomial and privacy bounds turn the adaptive contraction coefficient into its resource-normalized geometric form, as in equation (15) of the proof.
Assume the stated hk condition. The exponential-series bound gives the classical exponential upper bound on a binomial coefficient.
Formal statement
Proof (Lean source)
Assume the stated hk condition. Taking square roots gives the factor appearing in the higher-order adaptive first-moment bound.
Formal statement
Proof (Lean source)
Assume positive dimension and a privacy budget in the interval from zero to one. Pure local privacy on the stated budget range bounds the coordinate score scale by epsilon divided by dimension.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated hk condition, a privacy budget in the interval from zero to one, and nonnegative amplitude. Equation (15): the binomial contraction coefficient is bounded by a geometric power of the resource-normalized amplitude.
Formal statement
Proof (Lean source)
Assume the stated hz condition, the stated hw condition, the stated hk condition, a nonnegative bias bound, the stated hround condition, the stated hsq condition, and the stated hbudget condition. A rounded matching order turns a squared geometric coefficient bound into exponential decay in the resource logarithm.
Formal statement
Proof (Lean source)
Assume the stated hz condition. The logarithm in the nondense branch has the exponential budget needed for the fixed amplitude one hundredth.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget. At the prescribed public amplitude and matching order, the geometric coefficient has exponentially small base in each resource branch.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget. The exact prescribed amplitude and rounded matching order make equation (15)'s geometric transcript bound at most one hundredth, in both branches.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Frontier.ConverseResources 8 declarations The prescribed amplitude and rounded moment degree yield separation at the square-root frontier rate, in both resource branches including saturation.
Converse resource calibration
The prescribed amplitude and rounded moment degree yield separation at the square-root frontier rate, in both resource branches including saturation.
Assume the stated hx condition. Rounding the even approximation degree costs at most a factor thirty-four.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget. The public amplitude is positive and remains inside the paired parameter cube.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget. The chosen approximation degree is a positive even number, before adding one to obtain the matching order in the contraction theorem.
Formal statement
Proof (Lean source)
Assume the stated hx condition, the stated hr0 condition, the stated hr1 condition, and the stated hrx condition. A normalized rate factor cancels the reciprocal resource scale in the rounded degree.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget. The prescribed amplitude divided by the approximation degree dominates one thirty-four-hundredth of the square-root frontier rate.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget. In either resource branch, the positive even approximation degree is at most thirty-four times the logarithmic dimension, uniformly in sample size and privacy.
Formal statement
Proof (Lean source)
Squared logarithmic dimension divided by dimension vanishes, giving a universal cutoff for concentration of the prescribed product priors.
Proof (Lean source)
Assume the stated hb condition. Once the dimension exceeds a constant depending only on the universal approximation constant, the prior escape bound is at most one hundredth, uniformly over every allowed resource tuple.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Frontier.GlobalResources 6 declarations The selected even degree has the roadmap's rounding bounds and fits in the finite evaluation block.
Intermediate global-polynomial resources
The selected even degree has the roadmap's rounding bounds and fits in the finite evaluation block. Its exponential variance and approximation error are compared with the nonsaturated intermediate rate.
Assume dimension at least two. The noise logarithm is at least one.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget, the stated hn condition, the stated l condition, the stated hdense condition, and the stated hf condition. Intermediate resources that avoid the fallback select the global branch and an even degree between half and all of the unrounded budget.
Formal statement
Proof (Lean source)
Assume a positive privacy budget. The vector noise is at least the dimension squared divided by block size, since the randomized-response signal is below one.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget, the stated hn condition, the stated d condition, and the stated degree condition. The selected global degree fits its distinct-person moments in the block. An undersized block would make the noise logarithm at least the dimension logarithm, contradicting the nonfallback degree budget.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget and the protocol-class label. Below saturation, the elementary parametric comparison absorbs baseline noise without imposing any new estimator assumptions.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget, the stated hn condition, the stated l condition, the stated hdense condition, the protocol-class label, the stated degree condition, and the stated lower condition. The global polynomial variance and approximation bias have intermediate rate order. This uses the rounded degree, the eighty-fold noise comparison, and the established exponential dimension bound.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Frontier.Lower 15 declarations Finite original-record private value frontiers: Helpers/Frontier/Lower.
Helpers/Frontier/Lower
Finite original-record private value frontiers: Helpers/Frontier/Lower.
The paper's indexed infimum agrees with the library's best uniform error.
Formal statement
Proof (Lean source)
Increasing the degree enlarges the candidate space and decreases the best error.
Formal statement
Proof (Lean source)
Assume the Bernstein absolute-approximation limit. Positive universal absolute-approximation scale, including each finite even degree.
Formal statement
Proof (Lean source)
Assume the stated hxi condition and the stated ha condition. Positive scaling transports a unit-interval probability to the amplitude interval.
Formal statement
Proof (Lean source)
Pushforward scaling multiplies the q-th raw moment by the q-th power of the scale.
Formal statement
Proof (Lean source)
Assume nonnegative amplitude. Positive pushforward scaling multiplies the absolute moment by the scale.
Formal statement
Proof (Lean source)
Assume the Cai–Low moment-duality theorem, the stated privacy condition for the protocol, the stated even condition, and the stated ha condition. Scaled symmetric duality priors retain exact moment matching and target separation.
Formal statement
Proof (Lean source)
Assume the Cai–Low moment-duality theorem and the Bernstein absolute-approximation limit. The scaled dual priors have separated half-norm means and both targets concentrate within one eighth of their actual mean gap. The escape bound is uniform in amplitude, as required before choosing the dimension cutoff.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated ha condition, and the stated hnu condition. Mapping a supported coordinate prior to symmetric causal laws shifts its half-norm mean by the common baseline one half.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated ha condition, and the stated hnu condition. A common baseline shift preserves target-neighborhood escape probabilities when the coordinate prior is pushed to full-data causal laws.
Formal statement
Proof (Lean source)
Assume the Cai–Low moment-duality theorem and the Bernstein absolute-approximation limit. Moment-dual coordinate priors produce a positive gap between actual welfare means and the same quantitative escape bound on causal law space.
Formal statement
Proof (Lean source)
Assume the Cai–Low moment-duality theorem and the Bernstein absolute-approximation limit. At the prescribed resource amplitude and moment order, causal law-space priors have a frontier-sized welfare gap and escape probability at most one hundredth above a universal dimension cutoff.
Formal statement
Proof (Lean source)
Assume polynomial degree at least two, dimension no larger than the polynomial degree, and an admissible sample size, dimension, and privacy budget. Below any fixed dimension cutoff, the frontier is controlled by the two-point rate.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, polynomial degree at least two, dimension no larger than the polynomial degree, an admissible sample size, dimension, and privacy budget, independent and identically distributed participant records, independent protocol randomness, and sequential local privacy of the protocol. A fixed dimension cutoff gives both per-decision frontier converses with one constant.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, the Cai–Low moment-duality theorem, and the Bernstein absolute-approximation limit. Per-protocol and per-decision causal lower bounds, including connected honest intervals.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Frontier.NormCalibration 16 declarations The structural moment computation agrees with the calibrated polynomial statistic.
Squared-error calibration of the concrete norm statistics
The structural moment computation agrees with the calibrated polynomial statistic. Finite averaging and the bias--variance identity give its global polynomial MSE. Selecting the actual evaluation and disjoint pilot rows transfers all three norm calibrations to the attaining transcript.
The executable structural moment recursion computes the calibrated statistic exactly.
Formal statement
Proof (Lean source)
Centered finite-block error splits into variance and squared bias.
Formal statement
Proof (Lean source)
Assume positive dimension and the stated hbias condition. Column bias bounds persist under finite averaging without independent columns.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, independent and identically distributed participant records, the causal-model conditions for the data law, an admissible sample size, dimension, and privacy budget, positive block size, a block no larger than the sample, the stated even condition, polynomial degree at least two, the stated hm d condition, and the stated degree condition. The roadmap's global polynomial MSE applies to the actual recursive computation.
Formal statement
Proof (Lean source)
Assume positive dimension. Cauchy--Schwarz bounds a squared finite average by the average squared error.
Formal statement
Proof (Lean source)
Absolute value is a contraction in squared error at every true column mean.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and positive block size. The roadmap's absolute evaluation means have signed-norm MSE at most sigma squared.
Formal statement
Proof (Lean source)
Assume the stated hb condition. On the global branch the concrete transcript norm is exactly the calibrated recursive average.
Formal statement
Proof (Lean source)
Assume the stated hb condition. On the absolute-mean branch the concrete transcript norm is the calibrated mean statistic.
Formal statement
Proof (Lean source)
Assume the stated hn condition. The disjoint pilot and evaluation extracts have the independent hybrid expectation.
Formal statement
Proof (Lean source)
Assume the stated hn condition, the stated hb condition, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and the stated hm condition. The actual absolute-mean transcript branch inherits its calibrated norm MSE.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, the stated hn condition, the stated hb condition, independent and identically distributed participant records, the causal-model conditions for the data law, an admissible sample size, dimension, and privacy budget, the stated hm condition, the stated even condition, the stated d condition, the stated hm d condition, and the stated degree condition. The actual global-polynomial transcript branch inherits its calibrated norm MSE.
Formal statement
Proof (Lean source)
Assume the stated hb condition. On the hybrid branch the transcript computation is the calibrated pilot rule.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, the stated hn condition, the stated hb condition, independent and identically distributed participant records, the causal-model conditions for the data law, an admissible sample size, dimension, and privacy budget, the stated hm condition, the stated l condition, the stated d condition, and the stated hm d condition. The actual hybrid transcript branch inherits its finite calibrated norm MSE.
Formal statement
Proof (Lean source)
Assume the stated hn condition, the causal-model conditions for the data law, and dimension at least two. Projection and the signed causal bridge reduce value error to baseline and norm errors.
Formal statement
Proof (Lean source)
Assume the stated hn condition, the causal-model conditions for the data law, and dimension at least two. Finite-product value risk is controlled by the two actual component MSEs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Frontier.ProductPriorConcentration 5 declarations Mean, variance and escape bounds for the half absolute-norm target under independent amplitude-supported coordinates.
Product-prior target concentration
Mean, variance and escape bounds for the half absolute-norm target under independent amplitude-supported coordinates. The causal symmetric target is this statistic plus one half; the paired TV target is this statistic itself.
Assume the stated hnu condition. An amplitude-supported scalar absolute value is square integrable.
Formal statement
Proof (Lean source)
Assume positive dimension and the stated hnu condition. The half-norm prior mean is one half of the scalar absolute moment.
Formal statement
Proof (Lean source)
Assume positive dimension and the stated hnu condition. Independence of prior coordinates bounds the half-norm variance by the paper's amplitude-squared over four times the dimension.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated hnu condition, and the stated ht condition. Chebyshev's inequality controls escape from the scalar absolute-moment center under the coordinate product prior.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated hnu condition, and the stated hgap condition. At radius one eighth of a positive target gap, the escape probability is at most sixteen times amplitude squared divided by dimension and gap squared.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Frontier.Resources 8 declarations The deterministic third split and randomized-response signal bound control the vector noise.
Resource comparisons for the frontier fallback
The deterministic third split and randomized-response signal bound control the vector noise. Comparing its logarithm with the rate logarithm certifies the insufficient-degree fallback without any sampling moment assumptions.
Assume the stated hn condition. The third split used by the frontier has at least one fifth of the people.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget and the stated hn condition. The evaluation-block noise obeys the upper half of equation (11).
Formal statement
Proof (Lean source)
Assume the stated l condition, the stated hz condition, the stated hs0 condition, and the stated hs condition. A noise inflation of at most eighty inflates the rate logarithm by at most six.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget, the stated hn condition, the stated hbranch condition, and the stated hfallback condition. The insufficient-degree branch keeps the intermediate rate uniformly positive.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget, the stated l condition, and the stated hbranch condition. In the intermediate branch a bounded logarithmic dimension bounds the rate away from zero.
Formal statement
Proof (Lean source)
Assume the stated hb condition. Reading the branch selector exposes the fallback's two resource inequalities.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget, the stated hn condition, the stated l condition, and the stated hdense condition. Dense resources select exactly the calibrated hybrid degree and fit its moments in the evaluation block, as in the upper-bound roadmap.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget, the stated hn condition, and the stated hdense condition. The calibrated hybrid MSE and binary baseline noise have dense rate order.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Frontier.Sampling 4 declarations The concrete noninteractive transcript law factors into participant row laws.
Independent message rows in the attaining experiment
The concrete noninteractive transcript law factors into participant row laws. Averaging the iid inputs preserves this product structure, allowing the finite vector-block moment calculations to apply to the actual private transcript.
For fixed records the concrete transcript consists of independent message rows.
Formal statement
Proof (Lean source)
Averaging independent input records preserves the product of private row laws.
Formal statement
Proof (Lean source)
Assume independent and identically distributed participant records, independent protocol randomness, and the causal-model conditions for the data law. The actual sampling decision law has the independent averaged message-row marginal.
Formal statement
Proof (Lean source)
Assume independent and identically distributed participant records, independent protocol randomness, and the causal-model conditions for the data law. The risk of the actual transcript-only frontier estimate is a finite product-law integral.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Frontier.Upper 37 declarations Finite original-record private value frontiers: Helpers/Frontier/Upper.
Helpers/Frontier/Upper
Finite original-record private value frontiers: Helpers/Frontier/Upper.
Explicit fallback and polynomial branches of the attaining construction.
Definition (Lean source)
Equality of the explicit frontier-construction branches is decidable.
Definition (Lean source)
Resource-selected design including converse amplitude and matching degree.
Definition (Lean source)
Fix the sample size and the dimension and the privacy budget. Fixed public-resource choices: the first applicable branch is used, with the constants and rounding rules of the frozen construction. In the n=2 branch the block and polynomial entries are unused by the constant estimator.
Definition (Lean source)
Fix the dimension. Combined binary/vector message alphabet.
Fix the sample size and the dimension, the privacy budget, the participant index, the observed participant record, and the parameter z. Original-input participant-specific finite atom channel.
Definition (Lean source)
Fix the sample size and the dimension, the privacy budget, and the participant index. Finite participant channel ignoring histories.
Definition (Lean source)
Fix the sample size and the dimension, the privacy budget, and the participant index. Participant stage with ignored histories.
Definition (Lean source)
Binary randomized-response masses are nonnegative.
Formal statement
Proof (Lean source)
The two binary response probabilities sum to one.
Formal statement
Proof (Lean source)
The binary outcome channel is a probability kernel.
Formal statement
Proof (Lean source)
Stage Markov certificate.
Formal statement
Proof (Lean source)
Fix the sample size and the dimension and the privacy budget. Explicit noninteractive original-record attaining protocol.
Definition (Lean source)
Fix the protocol transcript and the participant index. Safe extraction from a finite transcript, returning a fixed unused message past the horizon.
Definition (Lean source)
Fix the sample size and the dimension, the privacy budget, the natural-number parameter offset, and the protocol transcript. Scaled vector block extracted from a transcript.
Definition (Lean source)
Fix the privacy budget and the amplitude, the natural-number parameter D, the coordinate index, and the function z. Finite polynomial computation using the prescribed elementary-symmetric recursion.
Definition (Lean source)
Fix the sample size and the dimension, the privacy budget, and the protocol transcript. Raw norm estimate from the chosen pilot/evaluation branch.
Definition (Lean source)
Fix the sample size and the dimension, the privacy budget, and the protocol transcript. Fresh-person randomized-response estimate of the baseline.
Definition (Lean source)
Fix the sample size and the dimension, the privacy budget, and the protocol decision. Projected causal estimator using only private messages.
Definition (Lean source)
Measurability of the concrete finite transcript estimate.
Formal statement
Proof (Lean source)
Fix the sample size and the dimension and the privacy budget. Attaining Borel estimator packaged without any unproved definitional payload.
Definition (Lean source)
Fix the sample size and the dimension and the privacy budget. The fixed honesty radius prescribed for every branch, including n=2.
Definition (Lean source)
Fix the sample size and the dimension, the privacy budget, and the protocol decision. Lower endpoint with the prescribed fixed honesty radius.
Definition (Lean source)
Fix the sample size and the dimension, the privacy budget, and the protocol decision. Upper endpoint of the concrete connected interval.
Definition (Lean source)
Endpoint regularity and range certificate for the actual interval.
Formal statement
Proof (Lean source)
Fix the sample size and the dimension and the privacy budget. The resource-selected closed connected interval.
Definition (Lean source)
Fix the sample size and the dimension. Data of the fixed constructive and converse handle. Kernel normalization, Borel decisions and interval range are typing obligations; privacy, moment identities, risk and global honesty are proved later rather than defining membership. The prior maps are applied to the symmetric moment-duality measures at degree k-1.
Definition (Lean source)
Fix the sample size and the dimension and the privacy budget. The fixed original-input construction for the public tuple (n,d,ε): singleton seed, binary baseline and two disjoint sign-vector blocks, transcript-only clipped estimate, fixed-radius connected interval, and scaled coordinate product priors. Selection is deterministic in public resources, by the ordered branches of frontierResources; there is no optimization over designs. Admissibility, calibration, risk and coverage are subsequent construction obligations, not assumed performance fields of this mathematical object.
Definition (Lean source)
Assume a nonnegative privacy budget. The binary outcome response obeys the same extreme-sign ratio as the vector release.
Formal statement
Proof (Lean source)
Assume a nonnegative privacy budget. Each branch of the combined finite message channel satisfies the atomwise privacy bound.
Formal statement
Proof (Lean source)
Assume a nonnegative privacy budget. Summing the finite atom inequalities proves privacy for every message event.
Formal statement
Proof (Lean source)
Assume a nonnegative privacy budget. The entire resource-selected original-input procedure is noninteractive and pure private.
Formal statement
Proof (Lean source)
Clipping the endpoints can only shorten the fixed-radius interval.
Formal statement
Proof (Lean source)
Integrating the deterministic length bound requires only that the decision law be a probability.
Formal statement
Proof (Lean source)
The interval radius has exactly the prescribed square-root rate, for all resource tuples.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law and positive dimension. The causal target lies in the interval's fixed output domain.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget, the stated hv condition, and the estimator hRisk. Markov's inequality converts the finite MSE bound into ninety-percent coverage.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Frontier.UpperCalibration 14 declarations Projection bounds the loss without moment calibration in the saturated regime.
Bounded-loss branches of the concrete frontier construction
Projection bounds the loss without moment calibration in the saturated regime. The two-participant constant procedure also satisfies the prescribed risk rate. Resource comparisons also close the insufficient-degree fallback and both bounded-logarithmic-dimension branches. The dense absolute-mean and hybrid proofs combine the actual transcript component MSEs. The intermediate global-polynomial proof uses the selected degree and finite-block resource comparisons.
Every branch of the concrete estimate lies in the causal target domain.
Formal statement
Proof (Lean source)
Assume the stated hv condition. Projection bounds squared risk uniformly, under any probability decision law.
Formal statement
Proof (Lean source)
Assume the stated hv condition. The two-participant constant estimate has worst-case squared risk at most 1/16.
Formal statement
Proof (Lean source)
Assume the stated allowed condition. With two participants the elementary lower comparison keeps the rate above 1/2.
Formal statement
Proof (Lean source)
Assume the stated allowed condition and the stated hv condition. The constant branch attains the same universal upper-risk constant.
Formal statement
Proof (Lean source)
Assume the protocol-class label and the stated hv condition. At saturation, projection alone attains the prescribed upper-risk bound.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget, the stated hb condition, and the stated hv condition. The insufficient-degree fallback satisfies the fixed final risk constant.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget, the stated l condition, the stated hbranch condition, and the stated hv condition. In bounded logarithmic dimension the intermediate branch needs only projection.
Formal statement
Proof (Lean source)
Assume the stated allowed condition. The two-participant interval is the full target domain, as prescribed by the roadmap.
Formal statement
Proof (Lean source)
Assume the stated hn condition and the stated l condition. Small logarithmic dimension selects the absolute evaluation means.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget, the stated hn condition, the stated l condition, and the stated hdense condition. The dense small-dimension comparison absorbs baseline and vector noise, with the constant stated in the constructive proof roadmap.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget, the stated hn condition, the stated l condition, the stated hdense condition, independent and identically distributed participant records, independent protocol randomness, and the causal-model conditions for the data law. The concrete absolute-mean branch attains the dense small-dimension risk bound by combining its calibrated norm MSE with the binary baseline MSE.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, an admissible sample size, dimension, and privacy budget, the stated hn condition, the stated l condition, the stated hdense condition, independent and identically distributed participant records, independent protocol randomness, and the causal-model conditions for the data law. The dense hybrid branch combines actual component calibration with the resource comparisons, using the same public design as the roadmap.
Formal statement
Proof (Lean source)
Assume the Cai–Low Chebyshev approximation theorem and the bounded-mean concentration inequality. Upper orders attained by the explicit original-input construction.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.MomentDependence.AffineCovariance 7 declarations Exact covariance and variance calculations for affine functions of a single private row.
Affine column covariance
Exact covariance and variance calculations for affine functions of a single private row. These give the degree-zero and one-row cases of the finite Walsh covariance argument.
Fix the probability law P, the privacy budget, and the function f and the function g. Covariance on the finite message block.
Definition (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, and dimension at least two. The private block mean of an affine coordinate is its affine contrast.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, and dimension at least two. Centered affine coordinates have the exact scaled-coordinate variance.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and the stated hjj condition. Distinct affine coordinates have covariance coming solely from their nonzero means.
Formal statement
Proof (Lean source)
Assume the stated hb condition. A nonzero scaled sign supports affine interpolation of any one-row column statistic.
Formal statement
Proof (Lean source)
On an empty block every column statistic is constant.
Formal statement
Proof (Lean source)
A constant statistic has zero covariance with every finite block statistic.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.MomentDependence.CenteredProducts 9 declarations Independence of participant rows diagonalizes the centered product moments, both within one column and between distinct columns.
Centered finite column products
Independence of participant rows diagonalizes the centered product moments, both within one column and between distinct columns. These are the finite Walsh calculations used by the column covariance proof.
Fix the probability law P, the privacy budget, the coordinate index, and the function z. The centered scaled sign in a single released row.
Definition (Lean source)
Fix the probability law P, the privacy budget, the coordinate index, the finite index set J, and the function z. A product of centered entries indexed by a participant subset.
Definition (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, and dimension at least two. Centering removes the one-row mean.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, and dimension at least two. The centered one-row second moment is its exact variance.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and the stated hjj condition. Distinct centered row coordinates have the negative product of contrasts as their moment.
Formal statement
Proof (Lean source)
Products over iid rows factor into their centered one-row moments.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and the stated jk condition. Unequal participant subsets have zero mixed moment, even across different columns.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, and dimension at least two. Equal-subset within-column moments are powers of the coordinate variance.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and the stated hjj condition. Equal-subset cross-column moments are powers of the exact one-row covariance.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.MomentDependence.Counting 5 declarations Inclusion probabilities and a finite union bound control squared private moments.
Finite subset-overlap counting
Inclusion probabilities and a finite union bound control squared private moments.
Assume positive block size, the stated hkm condition, and the stated hv condition. The inclusion probability of a specified subset is bounded by the paper's sampling-without-replacement factor, including the empty subset.
Formal statement
Proof (Lean source)
Assume the stated hm condition, the stated hkm condition, the stated hs condition, and the stated hk condition. A specified subset is contained in at most the inclusion-factor fraction of all uniformly weighted subsets of the required size.
Formal statement
Proof (Lean source)
Assume nonnegative amplitude and a nonnegative bias bound. The term for an exact intersection is dominated by the sum of all included subsets; this is the finite union bound with nonnegative moment weights.
Formal statement
Proof (Lean source)
Assume the stated hm condition, the stated hkm condition, the stated js condition, the stated j condition, nonnegative amplitude, and a nonnegative bias bound. Summing the union bound over a uniform subset and applying the binomial expansion gives the second-moment row bound.
Formal statement
Proof (Lean source)
Assume the stated hm condition, the stated hkm condition, nonnegative amplitude, and a nonnegative bias bound. Averaging the row bound twice cancels both subset-count normalizers.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.MomentDependence.Covariance 6 declarations Finite original-record private value frontiers: Helpers/MomentDependence/Covariance.
Helpers/MomentDependence/Covariance
Finite original-record private value frontiers: Helpers/MomentDependence/Covariance.
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and the stated hjj condition. Affine statistics of distinct coordinates attain the one-row correlation bound exactly.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and the stated hjj condition. The full arbitrary-column covariance inequality for a block containing one participant.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, and dimension at least two. A dimension bound on the exact cross-column correlation coefficient.
Formal statement
Proof (Lean source)
Assume positive dimension and the function hcov. Summing diagonal variances and bounded cross-column covariances gives the paper's factor-two bound for the average. This step does not assume independent columns.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a privacy budget in the interval from zero to one, dimension at least two, and measurability of g. The remaining finite Walsh-basis calculation controls arbitrary column statistics. This is the dependence step in the paper's private-moment proof roadmap.
Formal statement
Proof (Lean source)
For iid sampling, a causal population law, privacy in the calibrated range, at least two cells, and a positive block size bounded by the sample size, the vector channel satisfies privacy, its moment identities, and both column-dependence bounds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.MomentDependence.Moments 28 declarations Finite original-record private value frontiers: Helpers/MomentDependence/Moments.
Helpers/MomentDependence/Moments
Finite original-record private value frontiers: Helpers/MomentDependence/Moments.
Fix the probability law P, the privacy budget, and the function f. Expectations on finite message blocks.
Definition (Lean source)
Fix the probability law P, the privacy budget, and the function f. Variance on finite message blocks.
Definition (Lean source)
Fix the privacy budget, the function g, the coordinate index, and the function z. Own-column statistics.
Squaring a scaled sign removes all dependence on the released bit.
Formal statement
Proof (Lean source)
The second scaled-message moment is the squared noise scale.
Proof (Lean source)
Assume the stated hjj condition. Uniform signs have zero mixed second moment in distinct coordinates.
Formal statement
Proof (Lean source)
Global sign reversal cancels every product of three signs, including repeated indices.
Formal statement
Proof (Lean source)
Assume the stated hjj condition. Cancellation of both the uniform and affine parts of a channel's cross moment.
Formal statement
Proof (Lean source)
Assume the stated hjj condition. A channel row has zero cross-coordinate sign expectation for every original record.
Formal statement
Proof (Lean source)
Assume the stated hjj condition. Averaging channel rows preserves the zero cross-coordinate expectation.
Formal statement
Proof (Lean source)
Assume the stated hjj condition. The independent row law transfers the channel cross moment to scaled block messages.
Formal statement
Proof (Lean source)
Products using distinct participant rows factor under the independent block law.
Formal statement
Proof (Lean source)
Assume the stated hkm condition. Averaging distinct-row products gives the corresponding power of the one-row mean.
Formal statement
Proof (Lean source)
A selected participant has the common one-row mean.
Formal statement
Proof (Lean source)
A channel row biases precisely the coordinate named by its original input.
Formal statement
Proof (Lean source)
Averaging the original-input rows expresses a coordinate bias as a signed cell integral.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, and dimension at least two. The signed causal bridge identifies the scaled one-row coordinate mean. The causal input mean is supplied by the proved signedCellMean_eq_contrast.
Formal statement
Proof (Lean source)
The degree-zero distinct-person statistic is identically one.
Formal statement
Proof (Lean source)
The degree-one statistic is the average of the scaled participant messages.
Formal statement
Proof (Lean source)
Assume the stated hii condition. Independent distinct rows factor their common-coordinate cross moment.
Formal statement
Proof (Lean source)
The squared column sum separates the diagonal noise terms from distinct-row means.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and positive block size. The squared first private moment has the exact iid mean-square formula.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and positive block size. The exact first-moment formula implies the declared degree-one second-moment bound.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, and dimension at least two. The product of two subset statistics factors into its one-row moments.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, and dimension at least two. Shared participant rows contribute squared noise and unshared rows contribute contrast powers.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, and dimension at least two. The squared private moment is the normalized finite sum over subset overlaps.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, positive block size, and the stated hkm condition. The exact overlap expansion and finite inclusion bound give the second moment for every degree, without dividing by the cell contrast.
Formal statement
Proof (Lean source)
Assume independent and identically distributed participant records, the causal-model conditions for the data law, a privacy budget in the interval from zero to one, dimension at least two, positive block size, and a block no larger than the sample. First, second, cross and distinct-person power moments of the vector channel.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.MomentDependence.WalshExpansion 11 declarations Completeness of the tilted Boolean product basis and exact expansions of column statistics.
Finite Walsh expansion
Completeness of the tilted Boolean product basis and exact expansions of column statistics.
Fix the probability law P, the privacy budget, the coordinate index, the finite index set J, and the function x. The tilted Walsh product as a function of one Boolean column.
Definition (Lean source)
Pulling a Boolean Walsh function back to released rows gives the column basis.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, and dimension at least two. Orthogonality detects every coefficient, so the Boolean product functions are independent.
Formal statement
Proof (Lean source)
Fix the probability law P, the causal-model conditions for the data law, the privacy budget, a positive privacy budget, dimension at least two, and the coordinate index. Counting Boolean configurations makes the independent product family a full basis.
Definition (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, and dimension at least two. Every statistic of one column has a finite tilted Walsh expansion.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, and dimension at least two. Only the empty Walsh subset contributes to a column mean.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, and dimension at least two. Centering deletes precisely the empty-subset coefficient in the finite expansion.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, and dimension at least two. All off-diagonal subset terms vanish in the product of two finite expansions.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and the function hf. Parseval's identity expresses each centered column variance as a finite sum of squares.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, the stated hjj condition, the function hf, and the function hf'. Cross-column covariance is the diagonal coefficient sum weighted by row-correlation powers.
Formal statement
Proof (Lean source)
Assume the stated hc condition and the stated hr condition. Cauchy–Schwarz bounds the diagonal expansion after the constant coefficient is removed.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.MomentDependence.WalshMoments 12 declarations Exact orthogonality and cross-column moments for the finite product basis.
Tilted Walsh moments
Exact orthogonality and cross-column moments for the finite product basis.
Fix the probability law P, the privacy budget, the coordinate index, the finite index set J, and the function z. Standardized tilted sign product basis within a column.
Definition (Lean source)
The integral block variance agrees with Mathlib's variance on this finite space.
Formal statement
Proof (Lean source)
The covariance diagonal is exactly the block variance.
Formal statement
Proof (Lean source)
Finite covariance expansion of the average, with no independence between columns.
Formal statement
Proof (Lean source)
Assume a positive privacy budget and positive dimension. The signed-vector scale exceeds the number of cells.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, and dimension at least two. The variance of a scaled sign is strictly positive throughout the causal cube.
Formal statement
Proof (Lean source)
Normalized products are centered column products divided by their scale power.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and the stated jk condition. Unequal Walsh subsets have zero mixed moment in any pair of columns.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, and dimension at least two. Every Walsh product has unit second moment, including the empty subset.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and the stated j condition. Nonempty Walsh products are centered.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, and dimension at least two. The finite within-column product family is orthonormal.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and the stated hjj condition. Equal-subset cross-column Walsh moments are powers of the exact row correlation.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.PairedDecisionCompletion 10 declarations Finite atomic sampling weights extend the canonical experiment to all input measures.
A measurable completion of the paired decision experiment
Finite atomic sampling weights extend the canonical experiment to all input measures. On probability laws this extension is exactly the iid experiment.
Fix the local protocol Q and the probability law P. Atomic iid weights followed by the fixed protocol and its independent coins.
Definition (Lean source)
For every paired protocol, the completed finite atomic decision law is measurable even off the probability model.
Formal statement
Proof (Lean source)
On probability inputs, atomic sampling is the canonical iid experiment.
Formal statement
Proof (Lean source)
A measurable experiment commutes with pushing its parameter prior forward.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated ha condition, and the stated hnu condition. The measurable law-space completion has precisely the original product-prior seed/transcript mixture on the supported paired cube.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, sequential local privacy of the protocol, an admissible sample size, dimension, and privacy budget, the stated hnu0 condition, the stated hnu1 condition, and the stated hmatch condition. The exact one-hundredth contraction bound now applies to the measurable law-space experiment required by the separated-decision reduction.
Formal statement
Proof (Lean source)
Assume dimension at least two and the stated hp condition. Paired cube laws retain the independent analyst randomizer in the completed experiment.
Formal statement
Proof (Lean source)
Assume positive dimension. The paired family is Borel, as can be checked through its finite atomic masses.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated ha condition, and the stated hnu condition. Supported coordinate priors push forward to probability laws in the paired model.
Formal statement
Proof (Lean source)
Assume dimension at least two, the stated support condition, the stated support condition, strict separation of the two target values, the stated concentration near the target value, the stated concentration near the target value, and the stated total-variation bound. The generic testing and connectedness reductions apply to completed paired experiments and yield bounds on the canonical paired decision risks.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.PairedProductPrior 13 declarations Signed preprocessing identifies the paired product-prior transcript experiment with the causal symmetric experiment.
Paired product-prior experiments
Signed preprocessing identifies the paired product-prior transcript experiment with the causal symmetric experiment. Moment duality, target concentration and adaptive contraction then supply the three ingredients for the paired converse.
The paired finite law depends measurably on its contrast coordinates.
Formal statement
Proof (Lean source)
The finite total-variation target is measurable on the space of input laws.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated ha condition, and the stated hnu condition. Pushing the product prior to paired laws preserves its scalar TV center.
Formal statement
Proof (Lean source)
Escape probabilities transfer to law-space priors with the same radius and center.
Formal statement
Proof (Lean source)
Assume dimension at least two, the stated ha condition, and the stated hnu condition. Averaging signed preprocessing over a supported product prior preserves the joint public-seed and transcript law, including sequential histories.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, sequential local privacy of the protocol, an admissible sample size, dimension, and privacy budget, amplitude between zero and one half, the stated hnu0 condition, the stated hnu1 condition, the stated hk condition, and the stated hmatch condition. Arbitrary paired sequential protocols obey the same higher-order product-prior contraction and exact above-sample moment cancellation as the causal experiment.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, sequential local privacy of the protocol, an admissible sample size, dimension, and privacy budget, amplitude between zero and one half, the stated hnu0 condition, the stated hnu1 condition, the stated hk condition, and the stated hmatch condition. The paired adaptive contraction has the geometric resource form of equation (15), for every matching order. Orders beyond the sample size use exact mixture cancellation rather than an artificial binomial estimate.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, sequential local privacy of the protocol, an admissible sample size, dimension, and privacy budget, the stated hnu0 condition, the stated hnu1 condition, and the stated hmatch condition. At the prescribed frontier amplitude and matching degree, every paired sequential protocol has product-prior transcript TV at most one hundredth. Matching beyond the sample horizon uses exact cancellation.
Formal statement
Proof (Lean source)
Assume positive dimension, the stated ha condition, and the stated hnu condition. The paired TV prior center is half the scalar absolute moment.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, the Cai–Low moment-duality theorem, and the Bernstein absolute-approximation limit. The dual product priors simultaneously separate and concentrate the paired TV target and contract its private transcript experiment. This leaves the public amplitude, degree and dimension-cutoff calculations to the frontier assembly.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, the Cai–Low moment-duality theorem, and the Bernstein absolute-approximation limit. At the exact public resource choices, dual priors have a positive paired TV center gap at least a universal multiple of the square-root rate. Their concentration and transcript-contraction bounds retain the explicit degree, so subsequent dimension-cutoff calculations use the same priors.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, the Cai–Low moment-duality theorem, and the Bernstein absolute-approximation limit. The prescribed paired priors simultaneously achieve the frontier gap, matching moments, adaptive transcript contraction and escape probability at most one hundredth above one universal dimension cutoff.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, the Cai–Low moment-duality theorem, and the Bernstein absolute-approximation limit. The prescribed concentrated priors, pushed to paired input laws, have the same center gap and the strict real escape bounds used by the decision reduction. The underlying scalar priors are retained for transcript contraction.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.PairedTV 8 declarations Normalization, singleton masses and the half-L1 formula for the paired family.
Finite paired total variation
Normalization, singleton masses and the half-L1 formula for the paired family.
Fix the dimension. All probability laws on the finite paired alphabet.
Definition (Lean source)
Fix the dimension. The closed paired contrast family.
Definition (Lean source)
Fix the probability law p. Scalar total variation from the public uniform law on the paired alphabet.
Definition (Lean source)
Assume positive dimension. Probability membership of every paired law.
Formal statement
Proof (Lean source)
Assume the stated hw condition. Singleton masses of a nonnegative finite atomic law.
Formal statement
Proof (Lean source)
A finite probability experiment attains its half-L1 distance on positive atoms.
Formal statement
Proof (Lean source)
Assume positive dimension. Finite-sum TV agrees with the measure-theoretic testing distance.
Formal statement
Proof (Lean source)
Assume the stated theta condition and positive dimension. The paired target is one half of the signed norm.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.PairedTwoPoint 4 declarations Direct squared-risk and honest-length reductions on the paired model, including all dimensions below a fixed universal cutoff.
Paired two-point converse
Direct squared-risk and honest-length reductions on the paired model, including all dimensions below a fixed universal cutoff.
Assume measurable Radon–Nikodym densities for dominated kernels, sequential local privacy of the protocol, an admissible sample size, dimension, and privacy budget, and amplitude between zero and one half. Constant paired parameters inherit the arbitrary-channel contraction through signed preprocessing of the original records.
Formal statement
Proof (Lean source)
Assume amplitude between zero and one half, dimension at least two, and the stated total-variation bound. The two point-prior reduction is applied on the symmetric submodel, so the interval premise asks for honesty only on paired laws.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, an admissible sample size, dimension, and privacy budget, and sequential local privacy of the protocol. The paired two-point experiment gives both per-decision inverse-information bounds for every sequential channel and independent public seed.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, polynomial degree at least two, dimension no larger than the polynomial degree, an admissible sample size, dimension, and privacy budget, and sequential local privacy of the protocol. Below a fixed dimension cutoff the two-point bounds control the full paired frontier, with the same universal cutoff factor for risk and honest length.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.PrivateMoments 5 declarations Finite original-record private value frontiers: Helpers/PrivateMoments.
Helpers/PrivateMoments
Finite original-record private value frontiers: Helpers/PrivateMoments.
Fix the function W, the order, and the coordinate index. Distinct-person unbiased power statistic including degree zero.
Fix the function w. Structural elementary-symmetric recursion, avoiding subset enumeration.
Definition (Lean source)
Assume the stated hx condition. Splitting subsets according to whether they contain the new participant.
Formal statement
Proof (Lean source)
The structural recursion enumerates products over subsets of a finite range.
Formal statement
Proof (Lean source)
Recursion agrees with the private moment subset formula.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.Protocol 22 declarations Finite original-record private value frontiers: Helpers/Protocol.
Helpers/Protocol
Finite original-record private value frontiers: Helpers/Protocol.
Fix the sample size and the parameter α. All law-independent choices of a one-message sequential protocol.
Definition (Lean source)
Fix the local protocol Q and the participant index. History immediately preceding a participant.
Definition (Lean source)
Fix the local protocol Q. Complete dependent transcript.
Definition (Lean source)
Fix the local protocol Q and the privacy budget. Pure privacy for every input pair, seed, history and measurable output event.
Definition (Lean source)
Fix the local protocol Q. Constancy in all message histories.
Definition (Lean source)
Fix the local protocol Q and the privacy budget. The declared sequential class.
Definition (Lean source)
Fix the local protocol Q and the privacy budget. The declared noninteractive class.
Definition (Lean source)
Fix the protocol-class label, the local protocol Q, and the privacy budget. Select one of the two protocol classes.
Definition (Lean source)
NI protocols are sequential protocols.
Formal statement
Proof (Lean source)
Analyst's uniform randomizer law.
Fix the sample size and the dimension. Scheme for the joint input, public seed and analyst randomizer.
Definition (Lean source)
Fix the sampling scheme S. On the declared causal model and standard-Borel public-seed spaces, the records marginal is the n-fold observed product law.
Definition (Lean source)
Fix the sampling scheme S. On the declared causal model and standard-Borel public-seed spaces, the seed and analyst randomizer form a product independent of the record vector.
Definition (Lean source)
Fix the sample size and the dimension. Canonical iid scheme, displaying non-vacuity of the sampling atoms.
Definition (Lean source)
Canonical iid certificate.
Formal statement
Proof (Lean source)
Canonical independent-randomness certificate.
Formal statement
Proof (Lean source)
Fix the local protocol Q, the function o, and the public seed. Conditional transcript law for fixed records and seed.
Definition (Lean source)
Fix the local protocol Q. Private decision observation space.
Definition (Lean source)
Fix the sampling scheme S, the local protocol Q, and the probability law P. Joint transcript, seed and analyst randomizer law induced by any sampling scheme.
Definition (Lean source)
Fix the local protocol Q and the probability law p. Canonical decision law for an arbitrary input alphabet.
Definition (Lean source)
Fix the sampling scheme S, the local protocol Q, and the probability law P. Joint seed/transcript marginal.
Definition (Lean source)
Fix the local protocol Q and the probability law p. Canonical joint seed/transcript law on an arbitrary alphabet.
Definition (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.RateAlgebra 22 declarations Finite original-record private value frontiers: Helpers/RateAlgebra.
Helpers/RateAlgebra
Finite original-record private value frontiers: Helpers/RateAlgebra.
Fix the function f and the function g. Eventual comparison of two real numerical sequences by fixed positive constants.
Definition (Lean source)
All numerical resource conclusions carried by rho.
Definition (Lean source)
Assume dimension at least two. The logarithmic dimension is positive on the declared dimension domain.
Formal statement
Proof (Lean source)
Assume dimension at least two, the stated ht condition, and the stated hbranch condition. In the nondense branch, the rate saturates exactly at the paper's threshold.
Formal statement
Proof (Lean source)
Assume dimension at least two. The logarithmic dimension lies between one and the dimension itself.
Formal statement
Proof (Lean source)
Assume dimension at least two, the stated ht condition, and the stated hbranch condition. All three elementary resource comparisons hold in the dense branch.
Formal statement
Proof (Lean source)
Assume the stated hv condition. The logarithmic derivative factor in the weighted resource comparison is nonnegative.
Proof (Lean source)
Assume the stated ha condition. The squared weighted logarithm increases with the positive resource variable.
Formal statement
Proof (Lean source)
Assume the stated hz condition. For z at least one, the squared shifted logarithm is at most four times z.
Proof (Lean source)
Assume the stated hx condition. Squaring commutes with truncation at one for a nonnegative argument.
Proof (Lean source)
Assume dimension at least two. The dimension times its logarithmic dimension is at least the exponential constant.
Proof (Lean source)
Assume dimension at least two. The shifted logarithm at resource t = d is at least half the logarithmic dimension.
Formal statement
Proof (Lean source)
Assume dimension at least two, the stated ht condition, and the stated hbranch condition. All three elementary resource comparisons hold in the nondense branch.
Formal statement
Proof (Lean source)
Elementary global rate comparisons used for small dimensions.
Formal statement
Proof (Lean source)
Assume dimension at least two and the stated ht condition. The rate is at most one at every positive allowed resource.
Formal statement
Proof (Lean source)
Assume the stated h condition. The elementary comparisons characterize parametric order even for oscillating resources.
Formal statement
Proof (Lean source)
Assume the stated ht condition. Diverging resources turn an eventual bound on the minimum into bounded dimension.
Formal statement
Proof (Lean source)
Assume the stated h condition and the stated ht condition. Along diverging resources, parametric order holds exactly for bounded dimensions.
Formal statement
Proof (Lean source)
The logarithmic dimension diverges with the number of cells.
Assume the stated ha condition, the stated hu condition, the stated l condition, the stated hb condition, and the stated ha l condition. At resources comparable to squared dimension, the shifted logarithm is comparable with the logarithm of the logarithmic dimension.
Formal statement
Proof (Lean source)
Assume the stated ha condition and the stated hab assumption. The numerical rate at resources comparable to squared dimension has the squared log-log over log order, uniformly once the dimension is large enough.
Formal statement
Proof (Lean source)
Fix the function risk and the function length. Resource conclusions transferred to actual finite minimax values.
Definition (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.RateConsistency 6 declarations Logarithmic comparisons and the consistency criterion for arbitrary resource sequences.
Numerical consistency of the private value rate
Logarithmic comparisons and the consistency criterion for arbitrary resource sequences.
Assume the stated l condition and the stated hx condition. The shifted logarithm lies between the unshifted logarithm and its logarithmic correction.
Formal statement
Proof (Lean source)
Assume dimension at least two, the stated ht condition, and the stated hr condition. Off saturation the desired logarithmic ratio is bounded by the square root of the rate.
Formal statement
Proof (Lean source)
Assume dimension at least two and the stated ht condition. Both branches are bounded by the logarithmic ratio, its correction, and a dense remainder.
Formal statement
Proof (Lean source)
The logarithmic correction vanishes with dimension.
Proof (Lean source)
Assume the stated h condition. The paper's exact consistency criterion holds for arbitrary, possibly oscillating resources.
Formal statement
Proof (Lean source)
Pure numerical branch, consistency, parametric boundary and elbow assertions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.SeparatedMixtures 11 declarations Finite original-record private value frontiers: Helpers/SeparatedMixtures.
Helpers/SeparatedMixtures
Finite original-record private value frontiers: Helpers/SeparatedMixtures.
Fix the local protocol Q. Reattach an independent uniform analyst coin to a seed/transcript pair.
Definition (Lean source)
The reattachment channel is Markov, including for arbitrary public seeds.
Formal statement
Proof (Lean source)
The reconstruction kernel is exactly the declared product with the analyst coin.
Formal statement
Proof (Lean source)
Assume measurability of laws, the stated probability-measure property, the product-law representation, and the stated support condition. Supported rowwise coin independence also holds for a predictive mixture.
Formal statement
Proof (Lean source)
Assume measurability of laws, the stated probability-measure property, the product-law representation, the stated support condition, and the stated support condition. Appending independent analyst randomness cannot increase predictive total variation.
Formal statement
Proof (Lean source)
Assume the stated hsupport condition. A supported prior averages no more risk than the supremum on its support.
Formal statement
Proof (Lean source)
Assume the stated probability-measure property, the stated support condition, the stated support condition, measurability of target, measurability of laws, strict separation of the two target values, the stated concentration near the target value, the stated concentration near the target value, and the stated total-variation bound. The exact paper risk constant follows from classification at the midpoint. Rows outside the model are completed to probability rows without changing either prior.
Formal statement
Proof (Lean source)
Assume measurability of laws, the stated probability-measure property, the stated support condition, measurability of target, the stated concentration near the target value, and uniform ninety-percent coverage. Integrating global coverage loses at most the prior's target escape probability.
Formal statement
Proof (Lean source)
Assume the stated probability-measure property, the stated support condition, the stated support condition, measurability of target, measurability of laws, strict separation of the two target values, the stated concentration near the target value, the stated concentration near the target value, the stated total-variation bound, and uniform ninety-percent coverage. Two concentrated target neighborhoods force the paper's connected-interval length bound.
Formal statement
Proof (Lean source)
Assume the product-law representation, the stated probability-measure property, the stated support condition, the stated support condition, measurability of target, measurability of laws, strict separation of the two target values, the stated concentration near the target value, the stated concentration near the target value, and the stated total-variation bound. Generic concentrated-prior squared-risk and connected honest-length lower bounds.
Formal statement
Proof (Lean source)
Under iid sampling and independent randomization, two priors with causal support, probability decision mixtures, separated target centers, small escape probabilities, and nearby transcript mixtures, the causal experiment obeys squared-risk and connected honest-length lower bounds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.SymmetricLaw 11 declarations Finite Bernoulli sums establish normalization and the ancillary assignment law.
Symmetric causal law certificates
Finite Bernoulli sums establish normalization and the ancillary assignment law.
Assume the stated htheta condition. Every weight in the symmetric construction is nonnegative on the parameter cube. [](.
Formal statement
Proof (Lean source)
Assume the stated hw condition. Real probabilities of finite atomic events are sums of the nonnegative weights.
Formal statement
Proof (Lean source)
Assume the stated htheta condition. Event probabilities in the symmetric construction have their explicit Bernoulli expansion. [](.
Formal statement
Proof (Lean source)
Assume the stated htheta condition and positive dimension. Summing the Bernoulli potentials and consistent outcome gives unit total mass.
Formal statement
Proof (Lean source)
Assume the stated htheta condition. A fair assignment is ancillary to the signed input under the symmetric law. [](.
Formal statement
Proof (Lean source)
Assume the stated htheta condition. Each public cell has mass one over the dimension. [](.
Formal statement
Proof (Lean source)
Assume the stated htheta condition. The cellwise potential marginals are the two declared Bernoulli arm means. [](.
Formal statement
Proof (Lean source)
Assume the stated htheta condition. Independent fair assignment remains fair conditional on both potential outcomes. [](.
Formal statement
Proof (Lean source)
Assume the stated htheta condition and positive dimension. All symmetric-law mass is supported on consistent records.
Formal statement
Proof (Lean source)
Assume the stated htheta condition and positive dimension. The symmetric construction has the specified arm means in every nonempty cell.
Formal statement
Proof (Lean source)
Assume the stated htheta condition and positive dimension. Cube parameters give the interior means required by the causal model.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.TVCalibration 11 declarations The paired releases omit the baseline block.
Calibration of the paired transcript norm
The paired releases omit the baseline block. Shifting them into the common norm computation preserves the evaluation block law and its absolute-mean calibration.
Assume the causal-model conditions for the data law, positive dimension, and the stated hend condition. Either shifted norm block selects the corresponding active paired participants.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, positive dimension, and the stated hend condition. Expectations of shifted evaluation statistics are their iid calibration expectations.
Formal statement
Proof (Lean source)
Assume the stated hb condition, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and the stated hm condition. The paired absolute evaluation means inherit the finite signed-norm MSE.
Formal statement
Proof (Lean source)
Assume the stated hn condition, the causal-model conditions for the data law, dimension at least two, and the protocol decision. Projecting the norm statistic divided by two costs one quarter of its MSE.
Formal statement
Proof (Lean source)
Assume the stated hn condition, the stated hb condition, the causal-model conditions for the data law, a positive privacy budget, dimension at least two, and the stated hm condition. Projecting the norm statistic divided by two costs one quarter of its MSE.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget, the stated hn condition, the stated l condition, the stated hdense condition, and the stated hp condition. The dense bounded-logarithmic branch attains the paired TV risk rate on every law in the paired family, with the specified common upper constant.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, the stated hn condition, the stated hb condition, independent and identically distributed participant records, the causal-model conditions for the data law, an admissible sample size, dimension, and privacy budget, the stated hm condition, the stated even condition, the stated d condition, the stated hm d condition, and the stated degree condition. The shifted paired evaluation block inherits the global polynomial MSE, including its finite-degree variance and approximation terms.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, an admissible sample size, dimension, and privacy budget, the stated hn condition, the stated l condition, the stated hdense condition, the protocol-class label, the stated hf condition, independent and identically distributed participant records, and the causal-model conditions for the data law. The concrete paired global-polynomial branch attains the finite-resource risk rate after projection, using the same selected degree as the causal norm.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law and positive dimension. The two shifted paired blocks have the calibrated independent hybrid expectation.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, the stated hb condition, independent and identically distributed participant records, the causal-model conditions for the data law, an admissible sample size, dimension, and privacy budget, the stated hm condition, the stated l condition, the stated d condition, and the stated hm d condition. The paired hybrid statistic inherits the finite pilot/evaluation norm calibration.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, an admissible sample size, dimension, and privacy budget, the stated hn condition, the stated l condition, the stated hdense condition, independent and identically distributed participant records, and the causal-model conditions for the data law. Projection of the paired hybrid norm attains the dense large-dimension TV rate.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.TVModel 22 declarations Finite original-record private value frontiers: Helpers/TVModel.
Helpers/TVModel
Finite original-record private value frontiers: Helpers/TVModel.
Fix the protocol-class label, the probability law M, the sample size, and the privacy budget. Paired-input pure-local minimax squared-error value, with canonical iid sampling.
Definition (Lean source)
Fix the protocol-class label, the probability law M, the sample size, and the privacy budget. Globally honest TV interval value on the specified model, interval range [0,1].
Definition (Lean source)
Fix the sample size and the dimension and the privacy budget and the public seed and the stated h condition and the constant C0. Paired finite sign-vector protocol and attaining transcript-only decisions in [0,1/4].
Definition (Lean source)
Fix the sample size and the dimension, the privacy budget, and the participant index. Paired-input signed-vector channel, with constant unused releases.
Definition (Lean source)
Fix the sample size and the dimension, the privacy budget, and the participant index. Paired participant stage ignoring seed and histories.
Definition (Lean source)
Markov certificate of the concrete paired participant channel.
Formal statement
Proof (Lean source)
Fix the sample size and the dimension and the privacy budget. Resource-selected finite sign-vector NI protocol for the paired model.
Definition (Lean source)
Assume a nonnegative privacy budget and the set hE. Active paired rows are signed-vector rows after a deterministic record embedding; unused participants release the same constant for every input.
Formal statement
Proof (Lean source)
Assume a nonnegative privacy budget. The resource-selected paired sign-vector protocol is noninteractive and pure private at every history, including constant unused releases.
Formal statement
Proof (Lean source)
Fix the sample size and the dimension, the privacy budget, and the protocol transcript. Embed paired vector messages in the common private polynomial computation.
Definition (Lean source)
Fix the sample size and the dimension, the privacy budget, and the protocol decision. Explicit projected TV polynomial decision, using no baseline block.
Definition (Lean source)
Borel measurability of the concrete paired polynomial decision.
Formal statement
Proof (Lean source)
Fix the sample size and the dimension and the privacy budget. The measurable transcript-only paired estimator.
Definition (Lean source)
Fix the sample size and the dimension, the privacy budget and the constant C0, and the protocol decision. Lower endpoint in the sharper paired interval range.
Definition (Lean source)
Fix the sample size and the dimension, the privacy budget and the constant C0, and the protocol decision. Upper endpoint in the sharper paired interval range.
Definition (Lean source)
Regularity, order and range certificate for the concrete paired interval.
Formal statement
Proof (Lean source)
Fix the sample size and the dimension and the privacy budget and the constant C0. Actual paired globally honest closed connected interval.
Definition (Lean source)
Fix the sample size and the dimension and the privacy budget and the constant C0. Concrete attainment by the resource-selected sign-vector polynomial decisions.
Definition (Lean source)
Assume the stated hv condition. The two-participant fallback has squared error at most one sixty-fourth throughout the paired target range.
Formal statement
Proof (Lean source)
Clipping the paired interval to its target range can only shorten it.
Formal statement
Proof (Lean source)
Assume the stated c0 condition. Integrating the deterministic paired length bound yields the square-root rate.
Formal statement
Proof (Lean source)
Assume an admissible sample size, dimension, and privacy budget, the stated c0 condition, the stated hv condition, and the estimator hRisk. Markov's inequality converts the finite MSE bound into ninety-percent coverage.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.TVSampling 6 declarations The finite paired sign-vector transcript factors into averaged participant rows.
Independent rows in the paired attaining experiment
The finite paired sign-vector transcript factors into averaged participant rows. Its transcript-only squared risk is the corresponding finite product integral.
For fixed records the concrete transcript consists of independent message rows.
Formal statement
Proof (Lean source)
Averaging independent input records preserves the product of private row laws.
Formal statement
Proof (Lean source)
The actual sampling decision law has the independent averaged message-row marginal.
Formal statement
Proof (Lean source)
The risk of the actual transcript-only frontier estimate is a finite product-law integral.
Formal statement
Proof (Lean source)
Assume the stated hi condition, the causal-model conditions for the data law, and positive dimension. An active paired row, averaged over the causal signed marginal, is exactly the vector-message law used by the moment calibration.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law, positive dimension, the stated hg condition, and the stated hactive condition. Distinct active participants in the paired protocol provide exactly the iid vector block experiment, so all finite moment calibrations apply to their messages.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.TVUpper 7 declarations Projection closes the bounded-loss branches; the calibrated iid norm blocks close the remaining branches of the explicit paired polynomial procedure.
Uniform risk of the paired attaining estimator
Projection closes the bounded-loss branches; the calibrated iid norm blocks close the remaining branches of the explicit paired polynomial procedure.
Every input probability law induces a probability decision law.
Formal statement
Proof (Lean source)
The paired projection keeps all estimates in the sharper target interval.
Formal statement
Proof (Lean source)
Assume the stated hv condition. The paired projection gives a uniform one-sixteenth squared-risk bound.
Formal statement
Proof (Lean source)
Assume dimension at least two and the stated hp condition. The paired target ranges over zero to one quarter on the parameter cube.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, an admissible sample size, dimension, and privacy budget, and the stated hp condition. All finite-resource branches of the explicit paired estimator attain the common upper-risk constant, using the calibrated polynomial blocks.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, and an admissible sample size, dimension, and privacy budget. The explicit sign-vector procedure has finite global coverage and the square-root expected-length rate on the full paired family.
Formal statement
Proof (Lean source)
Assume the bounded-mean concentration inequality, the Cai–Low Chebyshev approximation theorem, and an admissible sample size, dimension, and privacy budget. The concrete paired procedure supplies the existential finite sign-vector attainment witness with the same universal constant.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.TranscriptPreprocessing 3 declarations Joint measurability of finite sequential transcript laws and their decision observations.
Measurable transcript laws
Joint measurability of finite sequential transcript laws and their decision observations.
When the prefix length does not exceed the sample size, prefix laws are measurable in the fixed participant inputs and public seed.
Formal statement
Proof (Lean source)
For every protocol, fixed transcript laws are jointly measurable in the records and public seed.
Formal statement
Proof (Lean source)
For every protocol, appending the seed and analyst randomizer gives jointly measurable decision rows.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.TwoCell 8 declarations Admissible attaining decisions bound both minimax values.
Two-cell calibration assembly
Admissible attaining decisions bound both minimax values. The saturated experiment uses a fixed message, the midpoint estimate, and the whole causal target interval.
Assume the stated attain condition. One noninteractive attaining procedure gives upper bounds in either protocol class.
Formal statement
Proof (Lean source)
Assume the stated hr condition, the stated hh condition, the stated c condition, and the stated attain condition. Increasing a nonnegative comparison constant preserves attained upper bounds.
Formal statement
Proof (Lean source)
Fix the sample size and the dimension. Fixed-message original-record protocol for the saturated branch.
Definition (Lean source)
Assume a nonnegative privacy budget. A fixed message satisfies privacy at every history and seed.
Formal statement
Proof (Lean source)
Fix the sample size and the dimension. Midpoint estimate, independent of all coins.
Definition (Lean source)
Fix the sample size and the dimension. Full causal target interval, independent of all coins.
Definition (Lean source)
Assume the stated hv condition. The saturated procedure has risk at most one sixteenth and perfect coverage.
Formal statement
Proof (Lean source)
Assume the stated allowed condition, independent and identically distributed participant records, independent protocol randomness, and the stated ht condition. Saturation of both two-cell rates is attained by fixed messages and the full interval.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.TwoCellAttainment 3 declarations This assembly separates the binary/vector sampling calculation from the already proved projection, Markov coverage, and interval length arguments.
Two-cell attainment from component estimates
This assembly separates the binary/vector sampling calculation from the already proved projection, Markov coverage, and interval length arguments. Component bounds are proof inputs here, not extra assumptions on the paper theorem.
Fix the sampling scheme S and the privacy budget. The binary baseline and two vector-coordinate estimates required by the roadmap. Existence of this certificate remains a proof obligation in the calibration theorem.
Definition (Lean source)
Assume the stated b condition, the stated hx0 condition, and the stated hx1 condition. Combining transcript-only components preserves the transcript-only property.
Formal statement
Proof (Lean source)
Assume the stated allowed condition, independent and identically distributed participant records, independent protocol randomness, the stated ht condition, and the stated components condition. Component MSEs give both unsaturated upper orders with the roadmap's constant 1000.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.TwoCellComponents 18 declarations Independent participant rows yield the binary baseline MSE, and extraction of the remaining vector rows transfers the existing coordinate mean and variance calculation.
MSEs for the half-block protocol
Independent participant rows yield the binary baseline MSE, and extraction of the remaining vector rows transfers the existing coordinate mean and variance calculation. These estimates provide the two-cell attainment certificate.
Every attaining row is a probability kernel, in the binary or vector branch.
Formal statement
Proof (Lean source)
Assume the stated hi condition. A baseline row releases a sign with the randomized-response conditional mean.
Formal statement
Proof (Lean source)
Assume the stated hi condition. Averaging original records gives the baseline row's unconditional mean.
Formal statement
Proof (Lean source)
Averaging any attaining row over a probability input law preserves mass one.
Formal statement
Proof (Lean source)
Assume the stated hg condition and the stated hbase condition. Distinct baseline rows have additive variances and the prescribed total mean.
Formal statement
Proof (Lean source)
Fix the sample size and the dimension, the privacy budget, and the protocol transcript. First-half binary randomized-response estimate of the baseline.
Definition (Lean source)
Assume sample size at least two and a privacy budget in the interval from zero to one. The actual binary baseline estimate has the roadmap's finite-block MSE.
Formal statement
Proof (Lean source)
Assume the stated hi condition. A vector-release row has exactly the signed-vector marginal.
Formal statement
Proof (Lean source)
Assume the stated hi condition. Averaging inputs preserves the vector marginal of every vector-release row.
Formal statement
Proof (Lean source)
Assume the stated hg condition and the stated hvec condition. Selecting distinct vector-release rows yields independent vector messages.
Formal statement
Proof (Lean source)
Fix the sample size and the dimension, the privacy budget, and the protocol transcript. The remaining vector rows, indexed without unused messages.
Definition (Lean source)
The remaining people have the calibrated iid vector-block law.
Formal statement
Proof (Lean source)
Fix the sample size and the dimension, the privacy budget, the coordinate index, and the protocol transcript. Each estimated contrast uses the mean of the last block's scaled coordinate.
Definition (Lean source)
Assume the stated allowed condition and the causal-model conditions for the data law. The two vector coordinates have the exact finite-block MSE order in the roadmap.
Formal statement
Proof (Lean source)
Fix the sample size and the dimension, the privacy budget, and the function f. Lift any finite transcript statistic to a Borel transcript-only decision.
Definition (Lean source)
The lifted decision uses only the finite transcript.
Formal statement
Proof (Lean source)
Assume independent and identically distributed participant records, independent protocol randomness, and the causal-model conditions for the data law. Sampling MSEs of finite transcript statistics equal their product-law MSEs.
Formal statement
Proof (Lean source)
Assume the stated allowed condition, independent and identically distributed participant records, and independent protocol randomness. The explicit binary/vector half-block construction supplies all three MSEs.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.TwoCellError 11 declarations Projection and the absolute-value inequality turn the baseline and two coordinate mean-square errors into the two-cell value error.
Two-cell error assembly
Projection and the absolute-value inequality turn the baseline and two coordinate mean-square errors into the two-cell value error. This argument does not require independence between the coordinate estimates.
Fix the constant B and the real parameter x0 and the real parameter x1. The projected two-cell transcript estimate specified in the calibration proof.
Assume the stated hv condition. Projection onto the causal target interval cannot increase squared error.
Formal statement
Proof (Lean source)
Assume the stated hv condition. The two absolute contrast errors cost at most one quarter of their squared errors in the value MSE, after combining with the baseline error.
Formal statement
Proof (Lean source)
Assume measurability of b, measurability of x0, measurability of x1, and the stated hv condition. Integrating the pointwise assembly gives a bound from the three component MSEs.
Formal statement
Proof (Lean source)
Assume the causal-model conditions for the data law. The bridge identifies the two-cell target used in the error calculation.
Formal statement
Proof (Lean source)
Assume a privacy budget in the interval from zero to one. On the allowed privacy domain the randomized-response signal is at least ε/4.
Formal statement
Proof (Lean source)
Assume sample size at least two. The deterministic half split supplies the two lower block-size bounds.
Formal statement
Proof (Lean source)
Assume the stated allowed condition. The block MSE bounds yield the roadmap's finite numerical constant 88.
Formal statement
Proof (Lean source)
If the baseline and two contrast statistics are measurable, their two-cell projection is measurable.
Formal statement
Proof (Lean source)
Fix the local protocol Q and the estimator B and the estimator x0 and the estimator x1. Combine three transcript-only statistics into the projected two-cell estimate.
Definition (Lean source)
Assume the stated allowed condition, the causal-model conditions for the data law, the stated b condition, the stated hx0 condition, and the stated hx1 condition. Component binary/vector MSE bounds assemble into the uniform two-cell risk bound. The component estimates can be dependent: only their marginal MSEs enter.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.TwoCellInterval 7 declarations The calibration roadmap uses radius √(10000/t) around the projected value estimate.
Two-cell finite honest intervals
The calibration roadmap uses radius √(10000/t) around the projected value estimate. Markov's inequality applied to the assembled 88/t MSE gives global ninety-percent coverage, and clipping gives length at most 200/√t.
Fix the sample size and the privacy budget. The deterministic radius in the two-cell calibration roadmap.
Definition (Lean source)
Projection keeps the two-cell estimate inside the causal target domain.
Formal statement
Proof (Lean source)
Fix the privacy budget, the local protocol Q, and the estimator B and the estimator x0 and the estimator x1. The clipped interval around the projected two-cell value estimate.
Definition (Lean source)
Assume the stated allowed condition. The roadmap's radius is exactly 100 divided by the private square-root sample size.
Formal statement
Proof (Lean source)
Clipping bounds the interval length pointwise by twice the radius.
Formal statement
Proof (Lean source)
Assume the stated allowed condition. The finite expected length has the asserted 200/√t bound.
Formal statement
Proof (Lean source)
Assume the stated allowed condition, the stated hv condition, and the estimator hRisk. The assembled MSE implies finite global ninety-percent coverage by Markov's inequality.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.TwoCellProtocol 11 declarations The two-cell construction assigns the first half of people to binary outcome releases and the remaining people to signed-vector releases.
Half-block binary/vector protocol
The two-cell construction assigns the first half of people to binary outcome releases and the remaining people to signed-vector releases. All rows are total, private, and independent of histories; their sampling transcript has product law.
Fix the sample size and the dimension, the privacy budget, the participant index, the observed participant record, and the parameter z. Original-input participant-specific finite atom channel.
Definition (Lean source)
Fix the sample size and the dimension, the privacy budget, and the participant index. Finite participant channel ignoring histories.
Definition (Lean source)
Fix the sample size and the dimension, the privacy budget, and the participant index. Participant stage with ignored histories.
Definition (Lean source)
Stage Markov certificate.
Formal statement
Proof (Lean source)
Fix the sample size and the dimension and the privacy budget. Explicit noninteractive original-record attaining protocol.
Definition (Lean source)
Assume a nonnegative privacy budget. Each branch of the combined finite message channel satisfies the atomwise privacy bound.
Formal statement
Proof (Lean source)
Assume a nonnegative privacy budget. Summing the finite atom inequalities proves privacy for every message event.
Formal statement
Proof (Lean source)
Assume a nonnegative privacy budget. The entire resource-selected original-input procedure is noninteractive and pure private.
Formal statement
Proof (Lean source)
For fixed records the concrete transcript consists of independent message rows.
Formal statement
Proof (Lean source)
Averaging independent input records preserves the product of private row laws.
Formal statement
Proof (Lean source)
Assume independent and identically distributed participant records, independent protocol randomness, and the causal-model conditions for the data law. The actual sampling decision law has the independent averaged message-row marginal.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.TwoPoint 11 declarations Finite original-record private value frontiers: Helpers/TwoPoint.
Helpers/TwoPoint
Finite original-record private value frontiers: Helpers/TwoPoint.
A degenerate coordinate prior fixes the entire parameter vector.
Formal statement
Proof (Lean source)
A point coordinate prior gives the corresponding unmixed experiment.
Formal statement
Proof (Lean source)
Finite population measures are separated by their measurable atom masses.
Definition (Lean source)
A law prior at a single population has no mixing effect.
Formal statement
Proof (Lean source)
Assume positive dimension. The constant contrast has its absolute value as its averaged signed norm.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, independent and identically distributed participant records, independent protocol randomness, sequential local privacy of the protocol, an admissible sample size, dimension, and privacy budget, and amplitude between zero and one half. The first moment-matching contraction controls the two constant-contrast experiments.
Formal statement
Proof (Lean source)
Assume independent and identically distributed participant records, independent protocol randomness, amplitude between zero and one half, positive dimension, and the stated total-variation bound. Point priors turn transcript closeness into both per-decision lower bounds.
Formal statement
Proof (Lean source)
Assume the stated hs condition. Squaring the truncated reciprocal gives the truncated inverse information.
Proof (Lean source)
Assume the stated hn condition and a positive privacy budget. The roadmap's amplitude obeys its support, privacy, and rate calibration requirements.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, an admissible sample size, dimension, and privacy budget, independent and identically distributed participant records, independent protocol randomness, and sequential local privacy of the protocol. The two-point converse holds before taking either minimax infimum.
Formal statement
Proof (Lean source)
Assuming measurable kernel Radon--Nikodym derivatives, universal private two-point alternatives give lower bounds for both minimax decision values.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.ValueSequences 5 declarations Positive uniform rate comparisons transfer consistency, parametric comparability, and the growing-dimension elbow to risk and honest length.
Transfer of numerical rates to value sequences
Positive uniform rate comparisons transfer consistency, parametric comparability, and the growing-dimension elbow to risk and honest length.
Eventual comparison by positive constants is symmetric.
Formal statement
Proof (Lean source)
Assume the stated hfg condition and the stated hgh condition. Eventual comparison by positive constants is transitive.
Formal statement
Proof (Lean source)
Assume the stated hf condition and the stated hg condition. Nonnegative comparable sequences vanish together.
Formal statement
Proof (Lean source)
Assume the stated hf condition. A nonnegative sequence and its square root vanish together.
Formal statement
Proof (Lean source)
Assume the stated hc condition, the stated hc c condition, and the function hBounds. Risk and honest length inherit every numerical resource conclusion from uniform positive comparisons with the rate and its square root.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.Helpers.VectorChannel 29 declarations Finite original-record private value frontiers: Helpers/VectorChannel.
Helpers/VectorChannel
Finite original-record private value frontiers: Helpers/VectorChannel.
Fix the sample size and the block size. Standing admissibility of a signed-message block in the n-person experiment.
Definition (Lean source)
Fix the sample size. Block sizes in the standing paper domain, with both bounds carried by the type.
Definition (Lean source)
Fix the privacy budget. Local noise parameter.
Definition (Lean source)
Fix the dimension and the privacy budget. Scaled sign noise.
Definition (Lean source)
Fix the privacy budget, the observed participant record, and the function z. Signed-vector atom weight.
Fix the dimension and the privacy budget. Explicit finite signed-vector channel.
Flipping one coordinate pairs the positive and negative signs.
Proof (Lean source)
Signed-vector masses are nonnegative for every real privacy parameter.
Formal statement
Proof (Lean source)
Uniform signs cancel the perturbation in the mass sum.
Formal statement
Proof (Lean source)
Markov certificate for the finite vector channel.
Formal statement
Proof (Lean source)
Fix the sample size and the dimension, the privacy budget, and the participant index. Constant-history vector stage.
Stagewise Markov certificate after ignoring seed and history.
Formal statement
Proof (Lean source)
Fix the sample size and the dimension and the privacy budget. Original-input vector protocol with a singleton public seed.
Definition (Lean source)
Fix the probability law P and the privacy budget. One signed-vector message law.
Definition (Lean source)
Fix the probability law P, the privacy budget, and the block size. Independent m-row vector-message law.
Definition (Lean source)
Fix the privacy budget, the function z, the participant index, and the coordinate index. Scaled message matrix.
Fix the privacy budget and the observed participant record. Direct product sampler: distinguished coordinate has mean δS; others are fair.
A finite atomic law assigns the declared nonnegative mass to each singleton.
Formal statement
Proof (Lean source)
The sampler's coordinate weights multiply to the vector-channel mass.
Formal statement
Proof (Lean source)
The finite channel is the stated total product sampler.
Formal statement
Proof (Lean source)
The tanh parametrization gives the exact randomized-response odds.
Formal statement
Proof (Lean source)
Assume a nonnegative privacy budget. The local sign bias is nonnegative and strictly below one.
Formal statement
Proof (Lean source)
The two extreme sign weights have exactly the pure-privacy ratio.
Formal statement
Proof (Lean source)
Assume a nonnegative privacy budget. Every vector atom satisfies the full original-input privacy bound.
Formal statement
Proof (Lean source)
Assume a nonnegative privacy budget and the set hE. Summing the atom bounds proves privacy for every measurable message event.
Formal statement
Proof (Lean source)
Assume a nonnegative privacy budget. The fixed signed-vector mechanism is noninteractive and pure private.
Formal statement
Proof (Lean source)
One release is a probability law whenever the original record law is.
Formal statement
Proof (Lean source)
Independent rows of the signed-vector mechanism form a probability law.
Formal statement
Proof (Lean source)
Fix the dimension and the privacy budget. Binary outcome randomized response.
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.TFullSimplexTvConverse 1 declarations Finite original-record private value frontiers: TFullSimplexTvConverse.
TFullSimplexTvConverse
Finite original-record private value frontiers: TFullSimplexTvConverse.
Under the Bernstein absolute-approximation limit, the full simplex obeys the private minimax-risk and globally honest connected-length lower bounds.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.TPairedUniformTvFrontier 5 declarations Finite original-record private value frontiers: TPairedUniformTvFrontier.
TPairedUniformTvFrontier
Finite original-record private value frontiers: TPairedUniformTvFrontier.
Assume measurable Radon–Nikodym densities for dominated kernels, the Cai–Low moment-duality theorem, and the Bernstein absolute-approximation limit. Per-decision paired converse for reuse under model inclusion.
Formal statement
Proof (Lean source)
Assume measurable Radon–Nikodym densities for dominated kernels, the Cai–Low moment-duality theorem, and the Bernstein absolute-approximation limit. The paired per-decision converse survives both minimax infima.
Formal statement
Proof (Lean source)
Assume the stated attain condition. Finite paired attainment bounds both private decision values; the same interval endpoints also define a legal interval in the larger range [0,1].
Formal statement
Proof (Lean source)
Paired NI optimization is over a smaller protocol class than SI optimization.
Formal statement
Proof (Lean source)
Given the Bernstein absolute-approximation limit, the paired experiment satisfies the complete TV frontier, finite sign-vector attainment, and resource conclusions.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.TSignedCausalBridge 1 declarations Causal identification, symmetric realization, and two-way private experiment equivalence.
Signed causal experiment bridge
Causal identification, symmetric realization, and two-way private experiment equivalence.
For a scheme with iid participants and independent randomization and at least two cells, the signed construction proves causal identification, symmetric-law realization, and two-way private experiment equivalence.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.TTwoCellCalibration 1 declarations Finite original-record private value frontiers: TTwoCellCalibration.
TTwoCellCalibration
Finite original-record private value frontiers: TTwoCellCalibration.
The two-cell model has universal finite private risk bounds, globally honest length bounds, and explicit attainment.
Formal statement
Proof (Lean source)
CausalSmith.Stat.STAT_LdpOptvalueUniformFrontier_Research.TUniformPrivateValueFrontiers 5 declarations Finite original-record private value frontiers: TUniformPrivateValueFrontiers.
TUniformPrivateValueFrontiers
Finite original-record private value frontiers: TUniformPrivateValueFrontiers.
Assume measurable Radon–Nikodym densities for dominated kernels, the Cai–Low moment-duality theorem, and the Bernstein absolute-approximation limit. Per-decision sequential lower bounds survive both minimax infima.
Formal statement
Proof (Lean source)
Assume the stated hc condition, the stated c condition, the stated hr condition, the stated r assumption and the function H, the stated rlo condition, the stated rhi condition, the stated hlo condition, and the stated hhi condition. Separate risk and honest-length bounds imply their square-root comparison.
Formal statement
Proof (Lean source)
Assume the stated hc condition, the stated c condition, the stated hr condition, the stated a assumption and the constant B, the stated ba condition, the stated blo condition, and the stated ahi condition. Nested finite positive values with common rate bounds have bounded ratios.
Formal statement
Proof (Lean source)
Fix the sampling scheme S and the privacy budget and the constant C0. Every finite causal upper bound is attained by the resource-selected explicit protocol.
Definition (Lean source)
Given the Bernstein absolute-approximation limit, the causal experiment satisfies the complete finite-resource frontier, explicit attainment, NI/SI and risk/length comparisons, saturation, consistency, private-parametric boundary, and growing-dimension elbow.