OAI/Combinatorics/EditApproximation/Probability/BernsteinFinite.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite scalar Bernstein concentration for independent centered bounded real sums with a summed second-moment upper bound.

  1. theorem OAI.EditApproximation.bernstein_chernoff_exponent line 12
  2. theorem OAI.EditApproximation.finite_bernstein_upper line 30
  3. theorem OAI.EditApproximation.finiteBernsteinInput line 67

    Source documentation

    Two-sided Bernstein concentration for independent centered bounded sums.

    theorem finiteBernsteinInput {Ω : Type*} [MeasurableSpace Ω]
    (μ : Measure Ω) [IsProbabilityMeasure μ] : FiniteBernsteinInput μ := by
…

    Mentions: OAI.EditApproximation.FiniteBernsteinInput