PrefixPredictionReindex.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Reindexing a finite prediction history

Equivalent finite candidate labels give the same residual inputs, actual nonlinear predictions, and chosen weak limits. The coefficient domain is transported in both directions, so the full detector sets also agree. These identities connect a recorded finite prefix to the final ledger without changing any map or passing a weak limit through a nonlinear operation.

theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.coefficientSum_pullCoeff line 29

Source documentation

Every parent-group mass is preserved under a finite equivalence of candidate labels.

theorem coefficientSum_pullCoeff {P I J : Type*}
    [Fintype P] [DecidableEq P] [Fintype I] [Fintype J]
    {parentI : I → P} {parentJ : J → P} (e : I ≃ J)
    (hp : ∀ i, parentJ (e i) = parentI i) (theta : J → ℝ) (p : P) :
    Prediction.coefficientSum parentI (fun i => theta (e i)) p =
      Prediction.coefficientSum parentJ theta p := by
…

Mentions: OAI.ReflexiveFixedPoints.Prediction.coefficientSum

def OAI.ReflexiveFixedPoints.Prediction.Prefix.pullCoeff line 40
Source documentation
Pull back an admissible coefficient function along the candidate-label equivalence.
```
def pullCoeff (e : I ≃ J) (hp : ∀ i, parentJ (e i) = parentI i)
    (theta : Prediction.coefficientSet parentJ) : Prediction.coefficientSet parentI :=
…
```
Mentions: OAI.ReflexiveFixedPoints.Prediction.coefficientSet
theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.pullCoeff_apply line 47
def OAI.ReflexiveFixedPoints.Prediction.Prefix.pullCoeffEquiv line 53
Source documentation
Reindexing is an equivalence of the entire admissible coefficient domains.
```
def pullCoeffEquiv (e : I ≃ J) (hp : ∀ i, parentJ (e i) = parentI i) :
    Prediction.coefficientSet parentJ ≃ Prediction.coefficientSet parentI where
…
```
Mentions: OAI.ReflexiveFixedPoints.Prediction.coefficientSet
theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.pullCoeffEquiv_apply line 66

theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.residualPoint_pullCoeff line 72

Source documentation

The ambient residual finite sum is unchanged by reindexing every candidate.

theorem residualPoint_pullCoeff (e : I ≃ J)
    (hp : ∀ i, parentJ (e i) = parentI i)
    (yI : I → X) (yJ : J → X) (hy : ∀ i, yJ (e i) = yI i)
    (b : X) (theta : Prediction.coefficientSet parentJ) (p : P) :
    Prediction.residualPoint parentI yI b (pullCoeff e hp theta).val p =
      Prediction.residualPoint parentJ yJ b theta.val p := by
…

Mentions: OAI.ReflexiveFixedPoints.Prediction.coefficientSet, OAI.ReflexiveFixedPoints.Prediction.residualPoint, OAI.ReflexiveFixedPoints.Prediction.Prefix.pullCoeff

theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.residualInput_pullCoeff line 99
Source documentation
The residual inputs agree as elements of the actual norm subtype.
```
theorem residualInput_pullCoeff (b : K) (theta : Prediction.coefficientSet parentJ) (p : P) :
    residualInput hconvex parentI yI b (pullCoeff e hp theta) p =
      residualInput hconvex parentJ yJ b theta p := by
…
```
Mentions: OAI.ReflexiveFixedPoints.Prediction.coefficientSet, OAI.ReflexiveFixedPoints.Prediction.Prefix.residualInput, OAI.ReflexiveFixedPoints.Prediction.Prefix.pullCoeff
theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.evaluatedPrediction_pullCoeff line 107
Source documentation
Nonlinear maps receive exactly equal inputs; no linearity is required.
```
theorem evaluatedPrediction_pullCoeff (b : K) (theta : Prediction.coefficientSet parentJ) :
    evaluatedPrediction hconvex maps evaluate parentI yI b (pullCoeff e hp theta) =
      evaluatedPrediction hconvex maps evaluate parentJ yJ b theta := by
…
```
Mentions: OAI.ReflexiveFixedPoints.Prediction.coefficientSet, OAI.ReflexiveFixedPoints.Prediction.Prefix.evaluatedPrediction, OAI.ReflexiveFixedPoints.Prediction.Prefix.pullCoeff
theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.predictionWeakLimit_pullCoeff line 117
Source documentation
Equality of the actual sequences preserves the exact compactness-selected weak limit.
```
theorem predictionWeakLimit_pullCoeff (hK : WeaklyCompact K) (b : ℕ → K)
    (U : Ultrafilter ℕ) (theta : Prediction.coefficientSet parentJ) :
    predictionWeakLimit hconvex maps evaluate parentI yI hK b U (pullCoeff e hp theta) =
      predictionWeakLimit hconvex maps evaluate parentJ yJ hK b U theta := by
…
```
Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact, OAI.ReflexiveFixedPoints.Prediction.coefficientSet, OAI.ReflexiveFixedPoints.Prediction.Prefix.predictionWeakLimit, OAI.ReflexiveFixedPoints.Prediction.Prefix.pullCoeff

theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.predictionWeakLimit_range_reindex line 127

Source documentation

Reindexing preserves the full prediction image, not merely a selected parameter.

theorem predictionWeakLimit_range_reindex (hK : WeaklyCompact K) (b : ℕ → K)
    (U : Ultrafilter ℕ) :
    Set.range (fun theta =>
      (predictionWeakLimit hconvex maps evaluate parentI yI hK b U theta : X)) =
    Set.range (fun theta =>
      (predictionWeakLimit hconvex maps evaluate parentJ yJ hK b U theta : X)) := by
…

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

theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.detectorSet_reindex line 146

Source documentation

The complete pre-map detector set is identical after a finite history reindexing.

theorem detectorSet_reindex (hK : WeaklyCompact K) (b : ℕ → K)
    (U : Ultrafilter ℕ) (densePoints : ℕ → K) (densePrefixLength : ℕ) :
    detectorSet hconvex maps evaluate parentI yI hK b U densePoints densePrefixLength =
      detectorSet hconvex maps evaluate parentJ yJ hK b U densePoints densePrefixLength := by
…

Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact, OAI.ReflexiveFixedPoints.Prediction.Prefix.detectorSet