OAI/Probability/MatroidSecretary/Residual/ResidualTailExact.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The effective numerical tail in source eq:residual-tail, including its strict final inequality and its validity already at the threshold group size.

  1. lemma OAI.MatroidProphet.SourceProof.residual_exponent_coefficient line 10
  2. theorem OAI.MatroidProphet.SourceProof.residual_tail_exact line 20

    Source documentation

    Exact effective exponential bound at the smallest analyzed group size.

    theorem residual_tail_exact (N : ℝ) (hN : densityThreshold ≤ N) :
    Real.exp ((1000 * Real.log densityThreshold / densityThreshold -
      residualDelta * Real.log 2) * N) ≤
        Real.exp (-((2 : ℝ)^73) * Real.log 2) ∧
      Real.exp (-((2 : ℝ)^73) * Real.log 2) < residualDelta := by
…

    Mentions: OAI.MatroidProphet.densityThreshold, OAI.MatroidProphet.residualDelta