Concentration.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Coarse threshold concentration from the published scalar input

The quantitative Bernstein bound used in Section 3 does not require independence of estimated child values. The random variables to which Bernstein is applied are fixed true-cost threshold contributions, conditional on ancestor thresholds.

theorem OAI.EditApproximation.coarse_bernstein_exponent line 21

Source documentation

Numerical exponent estimate for the coarse estimator's choice of deviation. The proof also covers the two regimes in the manuscript at once.

theorem coarse_bernstein_exponent {lam V allowance scale Q : ℝ}
    (hlam : 0 ≤ lam) (hlamone : lam ≤ 1) (hV : 0 ≤ V)
    (ha : 0 < allowance) (hu : 0 < scale) (hQ : Q * scale = allowance) :
    lam * Q / 12 ≤ (lam * V + allowance / 2) ^ 2 /
      (2 * scale * V + (2 / 3 : ℝ) * scale * (lam * V + allowance / 2)) := by
…

theorem OAI.EditApproximation.coarse_threshold_concentration line 51

Source documentation

Coarse threshold concentration, conditional only on the ancestor data. Its hypotheses specify the centered true-cost random variables, their moment proxy, and the threshold estimator's small bias.

theorem coarse_threshold_concentration {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) [IsProbabilityMeasure μ]
    (bernstein : FiniteBernsteinInput μ)
    {n : ℕ} (X : Fin n → Ω → ℝ) (estimator : Ω → ℝ)
    (mean V lam allowance scale Q : ℝ)
    (hlam : 0 ≤ lam) (hlamone : lam ≤ 1) (hV : 0 < V)
    (ha : 0 < allowance) (hu : 0 < scale) (hQ : Q * scale = allowance)
    (hscale : scale ≤ allowance / 2)
    (hindep : iIndepFun X μ) (hmeas : ∀ i, Measurable (X i))
    (hint : ∀ i, Integrable (X i) μ)
    (hmean : ∀ i, (∫ ω, X i ω ∂μ) = 0)
    (hbound : ∀ i, ∀ᵐ ω ∂μ, |X i ω| ≤ scale)
…

Mentions: OAI.EditApproximation.FiniteBernsteinInput