CoarseSampling.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Independent heterogeneous coarse threshold samples

Every child has its own fixed true cost and an independent uniform label in 1,...,B. The child estimates are absent from this probability space: they enter only the pathwise reconstruction proved separately.

theorem OAI.EditApproximation.coarse_sum_labels line 19
def OAI.EditApproximation.coarseThresholdSample line 34
theorem OAI.EditApproximation.coarseThresholdSample_large line 37
theorem OAI.EditApproximation.coarseThresholdSample_moments line 51
Source documentation
The mean, centered range and variance proxy are established for each fixed cost, including the deterministic range above the threshold scale.
```
theorem coarseThresholdSample_moments {B : ℕ} [NeZero B]
    [MeasurableSpace (Fin B)] [MeasurableSingletonClass (Fin B)]
    (scale value : ℝ) (hscale : 0 < scale) (hvalue : 0 ≤ value) :
    (0 ≤ value - uniformMean (coarseThresholdSample (B := B) scale value) ∧
…
```
Mentions: OAI.EditApproximation.uniformMean, OAI.EditApproximation.coarseThresholdSample

theorem OAI.EditApproximation.coarse_product_threshold_concentration_positive line 98

Source documentation

Actual product-uniform child labels satisfy the manuscript's coarse Bernstein tail bound for every fixed heterogeneous true-cost list.

theorem coarse_product_threshold_concentration_positive {B : ℕ} [NeZero B]
    [MeasurableSpace (Fin B)] [MeasurableSingletonClass (Fin B)]
    (value : Fin B → ℝ) (scale allowance Q lam : ℝ)
    (hvalue : ∀ i, 0 ≤ value i) (hu : 0 < scale) (ha : 0 < allowance)
    (hQ : Q * scale = allowance) (hscale : scale ≤ allowance / 2)
    (hlam : 0 ≤ lam) (hlamone : lam ≤ 1)
    (hV : 0 < ∑ i, value i)
    (bernstein : FiniteBernsteinInput (Measure.pi fun _ : Fin B =>
      (PMF.uniformOfFintype (Fin B)).toMeasure)) :
    (Measure.pi fun _ : Fin B => (PMF.uniformOfFintype (Fin B)).toMeasure).real
      {draws | lam * (∑ i, value i) + allowance <
        |(∑ i, coarseThresholdSample scale (value i) (draws i)) - ∑ i, value i|} ≤
…

Mentions: OAI.EditApproximation.FiniteBernsteinInput, OAI.EditApproximation.coarseThresholdSample

theorem OAI.EditApproximation.coarse_product_threshold_concentration line 157

Source documentation

The same exact product-uniform law, including zero total true cost.

theorem coarse_product_threshold_concentration {B : ℕ} [NeZero B]
    [MeasurableSpace (Fin B)] [MeasurableSingletonClass (Fin B)]
    (value : Fin B → ℝ) (scale allowance Q lam : ℝ)
    (hvalue : ∀ i, 0 ≤ value i) (hu : 0 < scale) (ha : 0 < allowance)
    (hQ : Q * scale = allowance) (hscale : scale ≤ allowance / 2)
    (hlam : 0 ≤ lam) (hlamone : lam ≤ 1)
    (bernstein : FiniteBernsteinInput (Measure.pi fun _ : Fin B =>
      (PMF.uniformOfFintype (Fin B)).toMeasure)) :
    (Measure.pi fun _ : Fin B => (PMF.uniformOfFintype (Fin B)).toMeasure).real
      {draws | lam * (∑ i, value i) + allowance <
        |(∑ i, coarseThresholdSample scale (value i) (draws i)) - ∑ i, value i|} ≤
      2 * Real.exp (-lam * Q / 12) := by
…

Mentions: OAI.EditApproximation.FiniteBernsteinInput, OAI.EditApproximation.coarseThresholdSample