TreeCovering.lean`

32 declarations, 0 contain sorry, 0 declared as axioms

Covering a probability tree by iterative reductions

Recovery keeps the original and retained path histories distinct, even when their labels agree. All draws are retained in the accumulating union.

theorem OAI.LeanBlast.SecondKahnKalai.exists_zero_prefix_positive_suffix line 25
Source documentation
A nondecreasing finite list of capacities has a zero prefix followed by strictly positive capacities. The empty positive suffix is permitted.
```
theorem exists_zero_prefix_positive_suffix (m : ℕ → ℕ) (d : ℕ)
    (hmono : MonotoneOn m (Set.Iio d)) :
    ∃ k, k ≤ d ∧ (∀ i, i < k → m i = 0) ∧
      (∀ i, i < d - k → 0 < m (i + k)) := by
…
```
theorem OAI.LeanBlast.SecondKahnKalai.capacityReserve_div_sampling_le line 49
theorem OAI.LeanBlast.SecondKahnKalai.sampling_budget_le line 59
def OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.Recovers line 72
Source documentation
Each path of a retained tree recovers a path of the original tree after the already collected coordinates are added.
```
def Recovers {d e : ℕ} (T : ProbabilityTree X d) (S : ProbabilityTree X e)
    (W : Finset X) : Prop :=
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree
theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.Recovers.refl line 76
theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.Recovers.mono line 80
theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.Recovers.trans line 87
Source documentation
Recovery composes through the union of the independent draws.
```
theorem Recovers.trans {d e f : ℕ}
    {T : ProbabilityTree X d} {S : ProbabilityTree X e} {U : ProbabilityTree X f}
    {W V : Finset X} (hTS : Recovers T S W) (hSU : Recovers S U V) :
    Recovers T U (W ∪ V) := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.Recovers
theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.Recovers.coveredBy line 99
Source documentation
A covered retained path yields a covered original path.
```
theorem Recovers.coveredBy {d e : ℕ} {T : ProbabilityTree X d} {S : ProbabilityTree X e}
    {W V : Finset X} (h : Recovers T S W) (hS : S.CoveredBy V) :
    T.CoveredBy (W ∪ V) := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.Recovers
theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.Recovers.coveredBy_of_depth_zero line 107
Source documentation
When no levels remain, recovery is already a covering certificate.
```
theorem Recovers.coveredBy_of_depth_zero {d : ℕ} {T : ProbabilityTree X d}
    {S : ProbabilityTree X 0} {W : Finset X} (h : Recovers T S W) : T.CoveredBy W := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.Recovers
theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.Recovers.coveredBy_of_depth_eq_zero line 113
theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.Recovers.of_pathUnion_eq line 122
Source documentation
Removing empty initial labels preserves recovery without adding any coordinates. The path lifting premise is supplied by deterministic prefix removal.
```
theorem Recovers.of_pathUnion_eq {d e : ℕ}
    {T : ProbabilityTree X d} {S : ProbabilityTree X e}
    (h : ∀ q : S.Path, ∃ p : T.Path, T.pathUnion p = S.pathUnion q) :
    Recovers T S ∅ := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.Recovers
theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.HasSpread.mono line 131
Source documentation
Increasing each nonnegative level spread parameter preserves spread.
```
theorem HasSpread.mono {d : ℕ} {T : ProbabilityTree X d} {a b : ℕ → ℝ}
    (hT : T.HasSpread a) (ha : ∀ i, i < d → 0 ≤ a i)
    (hab : ∀ i, i < d → a i ≤ b i) : T.HasSpread b := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree
theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.coveredBy_probability_one line 144
structure OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState line 157
Source documentation
The actual retained tree, its spread budget, and recovery to the fixed original tree. Only positive-capacity levels are stored.
```
structure CoverState {k : ℕ} (original : ProbabilityTree X k) (σ : ℝ) where
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree
def OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState.initial line 173
def OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState.rank line 190
theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState.rank_eq_zero_iff line 193
theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState.coveredBy_of_rank_zero line 200
def OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState.accumulate line 205
Source documentation
Every draw is retained even when the reduction attempt fails.
```
def accumulate (state : CoverState original σ) (W : Finset X) : CoverState original σ :=
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState
theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState.accumulate_rank line 210
def OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState.Advances line 213
def OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState.step line 219
Source documentation
Choose a strict improvement when one exists; otherwise keep the tree. Existence of improvements will be supplied by the actual good-tree reduction.
```
def step (state : CoverState original σ) (W : Finset X) : CoverState original σ :=
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState
theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState.step_seen line 222
theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState.step_rank_le line 229
theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState.step_rank_lt_of_exists line 236
theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState.biUnion_fin_succ line 242
theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState.run_seen line 254
Source documentation
The recorded set is exactly the union of all draws, including failures.
```
theorem run_seen (n : ℕ) (state : CoverState original σ) (draws : Fin n → Finset X) :
    (adaptiveRun step n state draws).seen = state.seen ∪ Finset.univ.biUnion draws := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState, OAI.LeanBlast.SecondKahnKalai.adaptiveRun, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState.step

theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState.prob_covered_of_advance_probability line 263

Source documentation

The finite adaptive theorem transfers actual strict advances to covering. The good-tree probability estimate supplies the premise in the final theorem.

theorem prob_covered_of_advance_probability [Fintype X] (μ : FiniteLaw (Finset X))
    (hprogress : ∀ state : CoverState original σ, state.rank ≠ 0 →
      (3 / 4 : ℝ) ≤ μ.prob (fun W => ∃ next, state.Advances W next))
    (s : ℕ) (state : CoverState original σ) (hrank : state.rank ≤ s) :
    (2 / 3 : ℝ) ≤ (μ.iid (4 * s)).prob
      (fun draws => original.CoveredBy (state.seen ∪ Finset.univ.biUnion draws)) := by
…

Mentions: OAI.LeanBlast.SecondKahnKalai.FiniteLaw, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState

theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState.exists_advance_of_halved line 282
Source documentation
A halved tree, after its zero prefix is removed, is a strict improvement of the current positive-capacity tree.
```
theorem exists_advance_of_halved (state : CoverState original σ) (W : Finset X)
    (hdepth : state.depth ≠ 0) (U : ProbabilityTree X state.depth)
    (hdisjoint : U.IsDisjoint)
    (hcapacity : U.HasCapacities (fun i => state.capacity i / 2))
    (hspread : U.HasSpread (fun i => capacityReserve σ (state.capacity i / 2)))
    (hrecovery : Recovers state.tree U W) :
    ∃ next, state.Advances W next := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree, OAI.LeanBlast.SecondKahnKalai.capacityReserve, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.Recovers
theorem OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState.exists_advance_of_good line 332
Source documentation
A good draw produces an actual strict advance: construct the pruned tree, preserve the reserve budget, and delete exactly its zero-capacity prefix.
```
theorem exists_advance_of_good (state : CoverState original σ) (W : Finset X)
    (hσ : 0 < σ) {ρ : ℝ} (hρ : 0 < ρ) (hrank : state.rank ≠ 0)
    (hgood : Good ρ state.capacity W state.tree) :
    ∃ next, state.Advances W next := by
…
```
Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState, OAI.LeanBlast.SecondKahnKalai.Good

theorem OAI.LeanBlast.SecondKahnKalai.tree_covering_of_progress line 356

Source documentation

The finite random experiment and final parameter comparison. The next theorem supplies this private lemma's progress estimate from actual reduction.

private theorem tree_covering_of_progress {X : Type} [Fintype X] [DecidableEq X]
    {k : ℕ} (T : ProbabilityTree X k) (hk : 0 < k) (hdis : T.IsDisjoint)
    (m : ℕ → ℕ) (hcap : T.HasCapacities m) (hpos : ∀ i, i < k → 0 < m i)
    (hgrowth : ∀ i, i + 1 < k → 16 * m i ≤ m (i + 1))
    (σ : ℝ) (hσ : 0 < σ) (hspread : T.HasSpread (fun _ => σ))
    (hprogress : Real.exp 50 * (4 * σ) < 1 →
      ∀ state : ProbabilityTree.CoverState T σ, state.rank ≠ 0 →
        (3 / 4 : ℝ) ≤ bernoulliProbability (Real.exp 50 * (4 * σ))
          (fun W => ∃ next, state.Advances W next)) :
    (2 / 3 : ℝ) ≤ bernoulliProbability
      (min 1 (16 * Real.exp 50 * σ * (1 + Real.logb 2 (m (k - 1) : ℝ)))) T.CoveredBy := by
…

Mentions: OAI.LeanBlast.SecondKahnKalai.ProbabilityTree, OAI.LeanBlast.SecondKahnKalai.ProbabilityTree.CoverState, OAI.LeanBlast.SecondKahnKalai.bernoulliProbability

theorem OAI.LeanBlast.SecondKahnKalai.tree_covering line 407