TreeTolerance.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Tolerances from the actual budgets on the tree

At every positive depth, take the minimum of all budgets at that level and all earlier positive levels, capped by one. The cap makes the construction work for arbitrary positive budgets. When those budgets are at most one, the cumulative minimum at every positive depth is attained by an actual node, so the cap does not change the prescribed finite minimum.

The tolerance is the cumulative minimum multiplied by the dyadic coefficient 2^(-(k+1)). Its value at depth zero is exactly one half. Every finite tail is bounded by every actual budget at its initial or an earlier depth.

theorem OAI.ReflexiveFixedPoints.OrderedTree.budgetLevel_nonempty line 30
Source documentation
Every positive level has at least one actual node.
```
theorem budgetLevel_nonempty (k : ℕ) :
    (Finset.univ : Finset (T.Node (k + 1))).Nonempty :=
…
```
def OAI.ReflexiveFixedPoints.OrderedTree.levelMinimum line 35
Source documentation
The minimum of all actual budgets at positive depth k+1.
```
def levelMinimum (k : ℕ) : ℝ :=
…
```
theorem OAI.ReflexiveFixedPoints.OrderedTree.levelMinimum_le line 38
theorem OAI.ReflexiveFixedPoints.OrderedTree.le_levelMinimum_iff line 42
theorem OAI.ReflexiveFixedPoints.OrderedTree.levelMinimum_pos line 46
theorem OAI.ReflexiveFixedPoints.OrderedTree.levelMinimum_attained line 52
def OAI.ReflexiveFixedPoints.OrderedTree.cumulativeMinimum line 59
Source documentation
The actual cumulative minimum, with the initial cap equal to one.
```
def cumulativeMinimum : ℕ → ℝ
  | 0 => 1
  | k + 1 => min (cumulativeMinimum k) (T.levelMinimum e k)
```
theorem OAI.ReflexiveFixedPoints.OrderedTree.cumulativeMinimum_zero line 63
theorem OAI.ReflexiveFixedPoints.OrderedTree.cumulativeMinimum_succ line 65
theorem OAI.ReflexiveFixedPoints.OrderedTree.cumulativeMinimum_pos line 69
theorem OAI.ReflexiveFixedPoints.OrderedTree.cumulativeMinimum_antitone line 76
theorem OAI.ReflexiveFixedPoints.OrderedTree.cumulativeMinimum_le_one line 81
theorem OAI.ReflexiveFixedPoints.OrderedTree.cumulativeMinimum_le_budget line 84
theorem OAI.ReflexiveFixedPoints.OrderedTree.le_cumulativeMinimum_iff line 94
Source documentation
Exact lower-bound characterization of the finite minimum: it includes every budget through depth k, without choosing a branch of the tree.
```
theorem le_cumulativeMinimum_iff (k : ℕ) (a : ℝ) :
    a ≤ T.cumulativeMinimum e k ↔
      a ≤ 1 ∧ ∀ i < k, ∀ v : T.Node (i + 1), a ≤ e ⟨i, v⟩ := by
…
```
theorem OAI.ReflexiveFixedPoints.OrderedTree.cumulativeMinimum_attained line 117
Source documentation
When actual budgets are at most one, the positive-depth minimum is attained by an actual node. Together with cumulativeMinimum_le_budget, this identifies it with the uncapped minimum of the finite collection.
```
theorem cumulativeMinimum_attained (he : ∀ v, e v ≤ 1) (k : ℕ) :
    ∃ i < k + 1, ∃ v : T.Node (i + 1),
      T.cumulativeMinimum e (k + 1) = e ⟨i, v⟩ := by
…
```
def OAI.ReflexiveFixedPoints.OrderedTree.tolerance line 136
Source documentation
The dyadic tolerance obtained from the actual cumulative budgets.
```
def tolerance (k : ℕ) : ℝ := (1 / 2 : ℝ) ^ (k + 1) * T.cumulativeMinimum e k
```
theorem OAI.ReflexiveFixedPoints.OrderedTree.tolerance_zero line 138
theorem OAI.ReflexiveFixedPoints.OrderedTree.tolerance_pos line 141
theorem OAI.ReflexiveFixedPoints.OrderedTree.tolerance_le_dyadic line 144
theorem OAI.ReflexiveFixedPoints.OrderedTree.tolerance_le_one line 150

theorem OAI.ReflexiveFixedPoints.OrderedTree.tolerance_tail_le_dyadic line 155

Source documentation

The stronger dyadic finite-tail estimate. The empty tail is included.

theorem tolerance_tail_le_dyadic (he : ∀ v, 0 < e v)
    (k N : ℕ) (hkN : k ≤ N) :
    (∑ d ∈ Finset.Ico k N, T.tolerance e d) ≤
      (1 / 2 : ℝ) ^ k * T.cumulativeMinimum e k := by
…

theorem OAI.ReflexiveFixedPoints.OrderedTree.tolerance_tail_le_dyadic_budget line 165

Source documentation

A tail starting at depth k is bounded by the dyadic coefficient times the budget of any actual node at positive depth at most k.

theorem tolerance_tail_le_dyadic_budget (he : ∀ v, 0 < e v)
    {i k N : ℕ} (hik : i + 1 ≤ k) (hkN : k ≤ N) (v : T.Node (i + 1)) :
    (∑ d ∈ Finset.Ico k N, T.tolerance e d) ≤ (1 / 2 : ℝ) ^ k * e ⟨i, v⟩ := by
…

theorem OAI.ReflexiveFixedPoints.OrderedTree.tolerance_tail_le_budget line 173

Source documentation

The unweighted node-budget bound used by the switching construction.

theorem tolerance_tail_le_budget (he : ∀ v, 0 < e v)
    {i k N : ℕ} (hik : i + 1 ≤ k) (hkN : k ≤ N) (v : T.Node (i + 1)) :
    (∑ d ∈ Finset.Ico k N, T.tolerance e d) ≤ e ⟨i, v⟩ := by
…