PredictionOutputs.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Actual evaluated prediction outputs and their compact detector sets

At a candidate one level below a completed cutoff, the parent residual inputs are formed from the earlier candidate labels. The parent maps and the prior tree evaluation are then applied in the stated order. Compactness chooses weak limits of these already evaluated outputs. Uniform coefficient estimates give norm continuity of their image without weak continuity of a nonlinear map.

theorem OAI.ReflexiveFixedPoints.Prediction.exists_weakLimit line 29

Source documentation

Actual existence of a weak ultrafilter limit in a weakly compact set.

theorem exists_weakLimit {J : Type*} {K : Set X} (hK : WeaklyCompact K)
    (q : J → K) (U : Ultrafilter J) :
    ∃ z : K, Tendsto (fun j => toWeakSpace ℝ X (q j : X)) (U : Filter J)
      (𝓝 (toWeakSpace ℝ X (z : X))) := by
…

Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact

def OAI.ReflexiveFixedPoints.Prediction.chosenWeakLimit line 47
Source documentation
A chosen actual limit, obtained from compactness rather than a limit-existence field.
```
def chosenWeakLimit {J : Type*} {K : Set X} (hK : WeaklyCompact K)
    (q : J → K) (U : Ultrafilter J) : K :=
…
```
Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact
theorem OAI.ReflexiveFixedPoints.Prediction.tendsto_chosenWeakLimit line 51
def OAI.ReflexiveFixedPoints.Prediction.residualInput line 65
Source documentation
The common point receives all unassigned mass in each parent group.
```
def residualInput (b : K) (theta : coefficientSet parent) (p : T.Node k) : K :=
…
```
Mentions: OAI.ReflexiveFixedPoints.Prediction.coefficientSet
theorem OAI.ReflexiveFixedPoints.Prediction.residualInput_val line 70
def OAI.ReflexiveFixedPoints.Prediction.evaluatedPrediction line 76
Source documentation
Apply the parent maps once, then the actual evaluation strictly above the cutoff.
```
def evaluatedPrediction (b : K) (theta : coefficientSet parent) : K :=
…
```
Mentions: OAI.ReflexiveFixedPoints.Prediction.coefficientSet

theorem OAI.ReflexiveFixedPoints.Prediction.evaluatedPrediction_norm_sub_le line 80

Source documentation

Uniform coefficient control of the actual nonlinear root evaluation.

theorem evaluatedPrediction_norm_sub_le
    (hdiam : ∀ a b : K, ‖(a : X) - (b : X)‖ ≤ 1)
    (b : K) (theta eta : coefficientSet parent) :
    ‖(evaluatedPrediction E k parent y b theta : X) -
      evaluatedPrediction E k parent y b eta‖ ≤
        ∑ i, |theta.val i - eta.val i| := by
…

Mentions: OAI.ReflexiveFixedPoints.Prediction.coefficientSet, OAI.ReflexiveFixedPoints.Prediction.evaluatedPrediction

def OAI.ReflexiveFixedPoints.Prediction.predictionWeakLimit line 104
Source documentation
The actual weak limit of already evaluated prediction outputs.
```
def predictionWeakLimit (hK : WeaklyCompact K) (b : ℕ → K) (U : Ultrafilter ℕ)
    (theta : coefficientSet parent) : K :=
…
```
Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact, OAI.ReflexiveFixedPoints.Prediction.coefficientSet
theorem OAI.ReflexiveFixedPoints.Prediction.tendsto_predictionWeakLimit line 108

theorem OAI.ReflexiveFixedPoints.Prediction.predictionWeakLimit_norm_sub_le line 117

Source documentation

The chosen weak limits satisfy the same uniform sum-norm coefficient estimate.

theorem predictionWeakLimit_norm_sub_le (hK : WeaklyCompact K)
    (hdiam : ∀ a b : K, ‖(a : X) - (b : X)‖ ≤ 1)
    (b : ℕ → K) (U : Ultrafilter ℕ) (theta eta : coefficientSet parent) :
    ‖(predictionWeakLimit E k parent y hK b U theta : X) -
      predictionWeakLimit E k parent y hK b U eta‖ ≤
        ∑ i, |theta.val i - eta.val i| :=
…

Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact, OAI.ReflexiveFixedPoints.Prediction.coefficientSet, OAI.ReflexiveFixedPoints.Prediction.predictionWeakLimit

theorem OAI.ReflexiveFixedPoints.Prediction.continuous_predictionWeakLimit_val line 129
Source documentation
Norm continuity in the original ambient norm, after choosing the weak limits.
```
theorem continuous_predictionWeakLimit_val (hK : WeaklyCompact K)
    (hdiam : ∀ a b : K, ‖(a : X) - (b : X)‖ ≤ 1)
    (b : ℕ → K) (U : Ultrafilter ℕ) :
    Continuous (fun theta => (predictionWeakLimit E k parent y hK b U theta : X)) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact, OAI.ReflexiveFixedPoints.Prediction.predictionWeakLimit
theorem OAI.ReflexiveFixedPoints.Prediction.continuous_predictionWeakLimit line 137
Source documentation
The limit map is also continuous into the literal norm subtype.
```
theorem continuous_predictionWeakLimit (hK : WeaklyCompact K)
    (hdiam : ∀ a b : K, ‖(a : X) - (b : X)‖ ≤ 1)
    (b : ℕ → K) (U : Ultrafilter ℕ) :
    Continuous (predictionWeakLimit E k parent y hK b U) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact, OAI.ReflexiveFixedPoints.Prediction.predictionWeakLimit

theorem OAI.ReflexiveFixedPoints.Prediction.isCompact_predictionWeakLimit_range line 145

Source documentation

The image of the actual prediction limits is norm compact.

theorem isCompact_predictionWeakLimit_range (hK : WeaklyCompact K)
    (hdiam : ∀ a b : K, ‖(a : X) - (b : X)‖ ≤ 1)
    (b : ℕ → K) (U : Ultrafilter ℕ) :
    IsCompact (Set.range (fun theta =>
      (predictionWeakLimit E k parent y hK b U theta : X))) := by
…

Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact, OAI.ReflexiveFixedPoints.Prediction.predictionWeakLimit

def OAI.ReflexiveFixedPoints.Prediction.detectorSet line 156
Source documentation
The first k + 1 test points and every possible actual prediction limit. The sequence is supplied before the candidate map; density is only used later.
```
def detectorSet (hK : WeaklyCompact K) (b : ℕ → K) (U : Ultrafilter ℕ)
    (densePoints : ℕ → K) : Set X :=
…
```
Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact
theorem OAI.ReflexiveFixedPoints.Prediction.detectorSet_nonempty line 162
Source documentation
A test point witnesses nonemptiness before any current candidate is chosen.
```
theorem detectorSet_nonempty (hK : WeaklyCompact K) (b : ℕ → K)
    (U : Ultrafilter ℕ) (densePoints : ℕ → K) :
    (detectorSet E k parent y hK b U densePoints).Nonempty := by
…
```
Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact, OAI.ReflexiveFixedPoints.Prediction.detectorSet
theorem OAI.ReflexiveFixedPoints.Prediction.detectorSet_subset line 169
Source documentation
Both parts of the detector set consist of actual points of K.
```
theorem detectorSet_subset (hK : WeaklyCompact K) (b : ℕ → K)
    (U : Ultrafilter ℕ) (densePoints : ℕ → K) :
    detectorSet E k parent y hK b U densePoints ⊆ K := by
…
```
Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact, OAI.ReflexiveFixedPoints.Prediction.detectorSet
theorem OAI.ReflexiveFixedPoints.Prediction.mem_detectorSet_prefix line 177
theorem OAI.ReflexiveFixedPoints.Prediction.mem_detectorSet_predictionWeakLimit line 182
theorem OAI.ReflexiveFixedPoints.Prediction.isCompact_detectorSet line 189
Source documentation
This compactness is in the original norm topology, as required by the detector lemma.
```
theorem isCompact_detectorSet (hK : WeaklyCompact K)
    (hdiam : ∀ a b : K, ‖(a : X) - (b : X)‖ ≤ 1)
    (b : ℕ → K) (U : Ultrafilter ℕ) (densePoints : ℕ → K) :
    IsCompact (detectorSet E k parent y hK b U densePoints) :=
…
```
Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact, OAI.ReflexiveFixedPoints.Prediction.detectorSet