ResidualTailEvent.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Effective tail for the actual deterministic residual-family bad event, with every outside mask and the parity fixed, but without conditioning on listing.

theorem OAI.MatroidProphet.SourceProof.residualBad_tail_exact line 16

Source documentation

Exact effective union bound for an arbitrary deterministic residual family.

theorem residualBad_tail_exact (q : α → ℝ)
    (hq0 : ∀ e, 0 ≤ q e) (hqhalf : ∀ e, q e ≤ 1 / 2)
    (V : Finset α) (F : Finset (Finset α)) (hF : ∀ R ∈ F, R ⊆ V)
    (hcard : (F.card : ℝ) ≤ Real.exp
      (1000 * Real.log densityThreshold / densityThreshold * V.card))
    (hn : densityThreshold ≤ (V.card : ℝ)) :
    bitsExpectation q V (residualBadIndicator F (residualDelta * V.card)) ≤
      Real.exp (-((2 : ℝ)^73) * Real.log 2) := by
…

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

theorem OAI.MatroidProphet.SourceProof.focalResidualBad_tail_exact line 40

Source documentation

The source's conditional bad event for the actual focal residual family. The fixed data contain H, parity, and all outside coordinates; only the focal D,C,T coordinates are integrated. Empty discovery outcomes are retained.

theorem focalResidualBad_tail_exact {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (d : MainMasks n) (s : Fin n → Option ℤ)
    (i : ℤ) (ε : Fin 2)
    (hn : densityThreshold ≤ ((trueGroup M d s i).card : ℝ)) :
    tripleMaskExpectation (fun _ => (1 : ℝ)/4) (fun _ => thinningRate)
      (fun _ => thinningRate) (trueGroup M d s i)
      (fun A B _C => residualBadIndicator (focalResidualFamily M hE (2^100) d s i ε)
        (residualDelta * (trueGroup M d s i).card) (A ∪ B)) ≤
        Real.exp (-((2 : ℝ)^73) * Real.log 2) ∧
      Real.exp (-((2 : ℝ)^73) * Real.log 2) < residualDelta := by
…

Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.densityThreshold, OAI.MatroidProphet.tripleMaskExpectation, OAI.MatroidProphet.thinningRate, OAI.MatroidProphet.residualBadIndicator, OAI.MatroidProphet.residualDelta