ThresholdMoments.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Discrete threshold moments

The initial estimator samples an integer uniformly from 1, …, B. The finite count below proves its rounding bias exactly; no continuous threshold distribution is substituted for the executable sampler.

theorem OAI.EditApproximation.threshold_count line 17

theorem OAI.EditApproximation.threshold_sum line 44

Source documentation

Exact discrete first moment below the scale; dividing the sum by B gives scale * floor(B * value / scale) / B.

theorem threshold_sum (B : ℕ) (scale value : ℝ)
    (hB : 0 < B) (hscale : 0 < scale) (hvalue : 0 ≤ value) (hupper : value < scale) :
    (∑ r ∈ Icc 1 B, thresholdContribution (scale * r / B) scale value) =
      (⌊(B : ℝ) * value / scale⌋₊ : ℝ) * scale := by
…

Mentions: OAI.EditApproximation.thresholdContribution

theorem OAI.EditApproximation.threshold_bias line 58

Source documentation

Bias bound used in the coarse estimator: the discrete mean is below the true argument by at most one grid unit.

theorem threshold_bias (B : ℕ) (scale value : ℝ)
    (hB : 0 < B) (hscale : 0 < scale) (hvalue : 0 ≤ value) (hupper : value < scale) :
    0 ≤ value - (∑ r ∈ Icc 1 B,
      thresholdContribution (scale * r / B) scale value) / B ∧
    value - (∑ r ∈ Icc 1 B,
      thresholdContribution (scale * r / B) scale value) / B ≤ scale / B := by
…

Mentions: OAI.EditApproximation.thresholdContribution

theorem OAI.EditApproximation.uniform_centered_square_identity line 81

theorem OAI.EditApproximation.threshold_variance_bound line 105

Source documentation

The centered second moment of the actual finite threshold sampler is at most scale * value, as used in the Bernstein variance proxy.

theorem threshold_variance_bound (B : ℕ) (scale value : ℝ)
    (hB : 0 < B) (hscale : 0 < scale) (hvalue : 0 ≤ value) (hupper : value < scale) :
    (∑ r ∈ Icc 1 B,
      (thresholdContribution (scale * r / B) scale value -
        (∑ s ∈ Icc 1 B, thresholdContribution (scale * s / B) scale value) / B) ^ 2) / B ≤
      scale * value := by
…

Mentions: OAI.EditApproximation.thresholdContribution