CandidatePredictions.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Final ideal predictions are members of their pre-map detector families

The coefficient parameter is obtained from the completed retained weights. Reindexing identifies its earlier ledger with the literal candidate prefix. Finite-frontier evaluation agrees with the final tree evaluation. Thus the chosen prediction is one of the limits for which the detector was selected before the current candidate map and before any current-level weights.

def OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefixParameter line 32
Source documentation
The final retained parameter transported to the exact pre-map prefix.
```
def candidatePrefixParameter (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) :
    Prediction.coefficientSet
      ((context D A U k).historyParent (candidatePrefix D A U k v)) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.Prediction.coefficientSet, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefix
def OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefixPrediction line 41
Source documentation
This is a member of the prediction family fixed before the map at v.
```
def candidatePrefixPrediction (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) : D.K :=
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower
def OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePredictionLimit line 52
Source documentation
The same point expressed through the final actual ideal-cutoff evaluator.
```
def candidatePredictionLimit (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) : D.K :=
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefixPrediction_eq line 58
Source documentation
Both descriptions choose the limit of literally the same evaluated sequence.
```
theorem candidatePrefixPrediction_eq (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) :
    candidatePrefixPrediction D A U k v = candidatePredictionLimit D A U k v := by
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefixPrediction, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePredictionLimit
theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePredictionLimit_mem_detectorSet line 93
Source documentation
The actual final prediction belongs to the compact set fixed before v.
```
theorem candidatePredictionLimit_mem_detectorSet (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) :
    (candidatePredictionLimit D A U k v : X) ∈
      (context D A U k).detectorSet (candidatePrefix D A U k v) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePredictionLimit, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.context, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePrefix

theorem OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePredictionLimit_tendsto line 109

Source documentation

The resulting point is an actual weak limit of the final ideal cutoffs.

theorem candidatePredictionLimit_tendsto (k : ℕ)
    (v : (tower D A U).toOrderedTree.Node (k + 1)) :
    Tendsto (fun j => toWeakSpace ℝ X
      ((tower D A U).toEvaluation.evaluate (k + 1)
        ((tower D A U).toEvaluation.idealCutoff (k + 1) A.x
          (terminalSequence D.closed D.convex D.T D.nonexpansive A.x j) v) : X))
      (U : Filter ℕ)
      (𝓝 (toWeakSpace ℝ X (candidatePredictionLimit D A U k v : X))) :=
…

Mentions: OAI.ReflexiveFixedPoints.AnchoredCandidateContext.tower, OAI.ReflexiveFixedPoints.terminalSequence, OAI.ReflexiveFixedPoints.AnchoredCandidateContext.candidatePredictionLimit