OAI/Analysis/Nonexpansive/PrefixPredictionOutputs.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Prediction families from a finite constructed frontier

The evaluator is the actual evaluator of an already constructed finite frontier. Its uniform sensitivity is a proved helper premise. No future infinite tree is needed to form the coefficient family or its detector set.

  1. def OAI.ReflexiveFixedPoints.Prediction.Prefix.residualInput line 30

    Source documentation

    The finite frontier's residual parent input, before any current map is chosen.

    def residualInput (b : K) (theta : Prediction.coefficientSet parent) (p : P) : K :=
…

    Mentions: OAI.ReflexiveFixedPoints.Prediction.coefficientSet

  2. theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.residualInput_val line 35
  3. def OAI.ReflexiveFixedPoints.Prediction.Prefix.evaluatedPrediction line 41

    Source documentation

    The actual prediction evaluates the current frontier maps on its residual inputs.

    def evaluatedPrediction (b : K) (theta : Prediction.coefficientSet parent) : K :=
…

    Mentions: OAI.ReflexiveFixedPoints.Prediction.coefficientSet

  4. theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.evaluatedPrediction_norm_sub_le line 45

    Source documentation

    Actual norm sensitivity of the finite evaluator gives a uniform coefficient estimate.

    theorem evaluatedPrediction_norm_sub_le
    (hmaps : ∀ p, LipschitzWith 1 (maps p))
    (hevaluate : ∀ H H' (ε : ℝ),
      (∀ p, ‖(H p : X) - (H' p : X)‖ ≤ ε) →
        ‖(evaluate H : X) - (evaluate H' : X)‖ ≤ ε)
    (hdiam : ∀ a b : K, ‖(a : X) - (b : X)‖ ≤ 1)
    (b : K) (theta eta : Prediction.coefficientSet parent) :
    ‖(evaluatedPrediction hconvex maps evaluate parent y b theta : X) -
      evaluatedPrediction hconvex maps evaluate parent y b eta‖ ≤
        ∑ i, |theta.val i - eta.val i| := by
…

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

  5. def OAI.ReflexiveFixedPoints.Prediction.Prefix.predictionWeakLimit line 74

    Source documentation

    Compactness chooses limits of the already evaluated finite-frontier outputs.

    def predictionWeakLimit (hK : WeaklyCompact K) (b : ℕ → K) (U : Ultrafilter ℕ)
    (theta : Prediction.coefficientSet parent) : K :=
…

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

  6. theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.tendsto_predictionWeakLimit line 79
  7. theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.predictionWeakLimit_norm_sub_le line 90

    Source documentation

    The selected weak limits preserve the finite coefficient estimate.

    theorem predictionWeakLimit_norm_sub_le
    (hmaps : ∀ p, LipschitzWith 1 (maps p))
    (hevaluate : ∀ H H' (ε : ℝ),
      (∀ p, ‖(H p : X) - (H' p : X)‖ ≤ ε) →
        ‖(evaluate H : X) - (evaluate H' : X)‖ ≤ ε)
    (hK : WeaklyCompact K)
    (hdiam : ∀ a b : K, ‖(a : X) - (b : X)‖ ≤ 1)
    (b : ℕ → K) (U : Ultrafilter ℕ) (theta eta : Prediction.coefficientSet parent) :
    ‖(predictionWeakLimit hconvex maps evaluate parent y hK b U theta : X) -
      predictionWeakLimit hconvex maps evaluate parent y hK b U eta‖ ≤
        ∑ i, |theta.val i - eta.val i| :=
…

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

  8. theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.continuous_predictionWeakLimit_val line 108

    Source documentation

    Continuity of the chosen limit family in the original ambient norm.

    theorem continuous_predictionWeakLimit_val
    (hmaps : ∀ p, LipschitzWith 1 (maps p))
    (hevaluate : ∀ H H' (ε : ℝ),
      (∀ p, ‖(H p : X) - (H' p : X)‖ ≤ ε) →
        ‖(evaluate H : X) - (evaluate H' : X)‖ ≤ ε)
    (hK : WeaklyCompact K)
    (hdiam : ∀ a b : K, ‖(a : X) - (b : X)‖ ≤ 1)
    (b : ℕ → K) (U : Ultrafilter ℕ) :
    Continuous (fun theta =>
      (predictionWeakLimit hconvex maps evaluate parent y hK b U theta : X)) :=
…

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

  9. theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.continuous_predictionWeakLimit line 123

    Source documentation

    Continuity also holds for the literal norm subtype.

    theorem continuous_predictionWeakLimit
    (hmaps : ∀ p, LipschitzWith 1 (maps p))
    (hevaluate : ∀ H H' (ε : ℝ),
      (∀ p, ‖(H p : X) - (H' p : X)‖ ≤ ε) →
        ‖(evaluate H : X) - (evaluate H' : X)‖ ≤ ε)
    (hK : WeaklyCompact K)
    (hdiam : ∀ a b : K, ‖(a : X) - (b : X)‖ ≤ 1)
    (b : ℕ → K) (U : Ultrafilter ℕ) :
    Continuous (predictionWeakLimit hconvex maps evaluate parent y hK b U) :=
…

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

  10. theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.isCompact_predictionWeakLimit_range line 137

    Source documentation

    The finite-prefix prediction image is norm compact.

    theorem isCompact_predictionWeakLimit_range
    (hmaps : ∀ p, LipschitzWith 1 (maps p))
    (hevaluate : ∀ H H' (ε : ℝ),
      (∀ p, ‖(H p : X) - (H' p : X)‖ ≤ ε) →
        ‖(evaluate H : X) - (evaluate H' : X)‖ ≤ ε)
    (hK : WeaklyCompact K)
    (hdiam : ∀ a b : K, ‖(a : X) - (b : X)‖ ≤ 1)
    (b : ℕ → K) (U : Ultrafilter ℕ) :
    IsCompact (Set.range (fun theta =>
      (predictionWeakLimit hconvex maps evaluate parent y hK b U theta : X))) := by
…

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

  11. def OAI.ReflexiveFixedPoints.Prediction.Prefix.detectorSet line 153

    Source documentation

    The prescribed finite test prefix and all possible evaluated prediction limits.

    def detectorSet (hK : WeaklyCompact K) (b : ℕ → K) (U : Ultrafilter ℕ)
    (densePoints : ℕ → K) (densePrefixLength : ℕ) : Set X :=
…

    Mentions: OAI.ReflexiveFixedPoints.WeaklyCompact

  12. theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.detectorSet_nonempty line 160

    Source documentation

    Nonemptiness follows from the zero parameter even if the test prefix is empty.

    theorem detectorSet_nonempty (hK : WeaklyCompact K) (b : ℕ → K)
    (U : Ultrafilter ℕ) (densePoints : ℕ → K) (densePrefixLength : ℕ) :
    (detectorSet hconvex maps evaluate parent y hK b U densePoints densePrefixLength).Nonempty := by
…

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

  13. theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.detectorSet_subset line 168
  14. theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.mem_detectorSet_prefix line 176
  15. theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.mem_detectorSet_predictionWeakLimit line 183
  16. theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.isCompact_detectorSet line 191

    Source documentation

    Compactness in the original norm topology supplies exactly the compact-detector input.

    theorem isCompact_detectorSet
    (hmaps : ∀ p, LipschitzWith 1 (maps p))
    (hevaluate : ∀ H H' (ε : ℝ),
      (∀ p, ‖(H p : X) - (H' p : X)‖ ≤ ε) →
        ‖(evaluate H : X) - (evaluate H' : X)‖ ≤ ε)
    (hK : WeaklyCompact K)
    (hdiam : ∀ a b : K, ‖(a : X) - (b : X)‖ ≤ 1)
    (b : ℕ → K) (U : Ultrafilter ℕ)
    (densePoints : ℕ → K) (densePrefixLength : ℕ) :
    IsCompact (detectorSet hconvex maps evaluate parent y hK b U densePoints densePrefixLength) :=
…

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

  17. theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.evaluatedPrediction_congr_evaluate line 206

    Source documentation

    An exact evaluator correspondence preserves every actual prediction.

    theorem evaluatedPrediction_congr_evaluate {evaluate' : (P → K) → K}
    (heq : ∀ H, evaluate H = evaluate' H)
    (b : K) (theta : Prediction.coefficientSet parent) :
    evaluatedPrediction hconvex maps evaluate parent y b theta =
      evaluatedPrediction hconvex maps evaluate' parent y b theta :=
…

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

  18. theorem OAI.ReflexiveFixedPoints.Prediction.Prefix.predictionWeakLimit_congr_evaluate line 214

    Source documentation

    The chosen weak limits are preserved by equality of the actual evaluated sequences.

    theorem predictionWeakLimit_congr_evaluate {evaluate' : (P → K) → K}
    (heq : ∀ H, evaluate H = evaluate' H)
    (hK : WeaklyCompact K) (b : ℕ → K) (U : Ultrafilter ℕ)
    (theta : Prediction.coefficientSet parent) :
    predictionWeakLimit hconvex maps evaluate parent y hK b U theta =
      predictionWeakLimit hconvex maps evaluate' parent y hK b U theta := by
…

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