CandidateThreshold.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Candidate thresholds chosen before maps

A single integer simultaneously supplies the detector defect scale and all already fixed ancestor displacement bounds.

theorem OAI.ReflexiveFixedPoints.exists_candidate_threshold line 20
Source documentation
The threshold depends only on the current positive budget, detector scale, and the sum of the displacement constants of the fixed ancestors.
```
theorem exists_candidate_threshold {C δ e : ℝ}
    (hδ : 0 < δ) (he : 0 < e) :
    ∃ m : ℕ, 1 ≤ m ∧ 1 / (m : ℝ) < δ ∧ C / (m : ℝ) ≤ e := by
…
```

theorem OAI.ReflexiveFixedPoints.candidate_ancestor_displacement line 39

Source documentation

Summing the actual fixed-ancestor displacement estimates preserves their common approximate-fixed-point defect factor.

theorem candidate_ancestor_displacement {A X : Type*} [Fintype A]
    [NormedAddCommGroup X] (G : A → X) (c : A → ℝ) (y : X)
    {defect e : ℝ} {m : ℕ}
    (hc : ∀ a, 0 ≤ c a)
    (hG : ∀ a, ‖G a - y‖ ≤ c a * defect)
    (hdefect : defect ≤ 1 / (m : ℝ))
    (hscale : (∑ a, c a) / (m : ℝ) ≤ e) :
    (∑ a, ‖G a - y‖) ≤ e := by
…