PredictionCompact.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Compact coefficient prediction families

The coefficient domain retains every earlier candidate label, including discarded ones. A parent group has total mass at most one; the remaining mass is assigned to the common terminal point. Weak limits are taken after evaluation. The coefficient estimate passes through weakly closed norm balls and yields norm continuity of the limit family.

def OAI.ReflexiveFixedPoints.Prediction.groupedCoefficient line 34
Source documentation
The coefficient of a candidate within one parent group.
```
def groupedCoefficient (parent : I → P) (theta : I → ℝ) (p : P) (i : I) : ℝ :=
…
```
def OAI.ReflexiveFixedPoints.Prediction.coefficientSum line 38
Source documentation
Total coefficient mass belonging to one parent.
```
def coefficientSum (parent : I → P) (theta : I → ℝ) (p : P) : ℝ :=
…
```
def OAI.ReflexiveFixedPoints.Prediction.coefficientSet line 42
Source documentation
All nonnegative earlier-candidate coefficients with parent-group mass at most one.
```
def coefficientSet (parent : I → P) : Set (I → ℝ) :=
…
```
theorem OAI.ReflexiveFixedPoints.Prediction.groupedCoefficient_self line 45
theorem OAI.ReflexiveFixedPoints.Prediction.groupedCoefficient_nonneg line 51
theorem OAI.ReflexiveFixedPoints.Prediction.coefficientSum_nonneg line 58
theorem OAI.ReflexiveFixedPoints.Prediction.coefficient_le_one line 63
theorem OAI.ReflexiveFixedPoints.Prediction.zero_mem_coefficientSet line 72
theorem OAI.ReflexiveFixedPoints.Prediction.coefficientSet_nonempty line 77
theorem OAI.ReflexiveFixedPoints.Prediction.continuous_coefficientSum line 81
theorem OAI.ReflexiveFixedPoints.Prediction.isClosed_coefficientSet line 92
theorem OAI.ReflexiveFixedPoints.Prediction.isCompact_coefficientSet line 100
Source documentation
Compactness uses a closed subset of the finite coefficient box, including the empty box.
```
theorem isCompact_coefficientSet (parent : I → P) :
    IsCompact (coefficientSet parent) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.Prediction.coefficientSet
def OAI.ReflexiveFixedPoints.Prediction.residualPoint line 109
Source documentation
The parent input predicted from earlier candidates and one common terminal point.
```
def residualPoint (parent : I → P) (y : I → X) (b : X) (theta : I → ℝ) (p : P) : X :=
…
```

theorem OAI.ReflexiveFixedPoints.Prediction.residualPoint_eq line 113

Source documentation

The residual point is an actual finite convex combination.

theorem residualPoint_eq {I P X : Type*} [Fintype I] [Fintype P] [DecidableEq P]
    [NormedAddCommGroup X] [NormedSpace ℝ X] (parent : I → P) (y : I → X) (b : X)
    (theta : I → ℝ) (p : P) :
    residualPoint parent y b theta p =
      (1 - coefficientSum parent theta p) • b +
        ∑ i, groupedCoefficient parent theta p i • y i := by
…

Mentions: OAI.ReflexiveFixedPoints.Prediction.residualPoint, OAI.ReflexiveFixedPoints.Prediction.coefficientSum, OAI.ReflexiveFixedPoints.Prediction.groupedCoefficient

theorem OAI.ReflexiveFixedPoints.Prediction.residualPoint_mem line 124
Source documentation
Nonnegative coefficients of mass at most one can be completed using the base point.
```
theorem residualPoint_mem (parent : I → P) {K : Set X} (hK : Convex ℝ K)
    (y : I → X) (hy : ∀ i, y i ∈ K) (b : X) (hb : b ∈ K)
    {theta : I → ℝ} (htheta : theta ∈ coefficientSet parent) (p : P) :
    residualPoint parent y b theta p ∈ K := by
…
```
Mentions: OAI.ReflexiveFixedPoints.Prediction.coefficientSet, OAI.ReflexiveFixedPoints.Prediction.residualPoint

theorem OAI.ReflexiveFixedPoints.Prediction.residualPoint_sub line 154

Source documentation

Subtracting predictions at two coefficient values cancels the base point exactly.

theorem residualPoint_sub {I P X : Type*} [Fintype I] [Fintype P] [DecidableEq P]
    [NormedAddCommGroup X] [NormedSpace ℝ X] (parent : I → P) (y : I → X) (b : X)
    (theta eta : I → ℝ) (p : P) :
    residualPoint parent y b theta p - residualPoint parent y b eta p =
      ∑ i, (groupedCoefficient parent theta p i -
        groupedCoefficient parent eta p i) • (y i - b) := by
…

Mentions: OAI.ReflexiveFixedPoints.Prediction.residualPoint, OAI.ReflexiveFixedPoints.Prediction.groupedCoefficient

theorem OAI.ReflexiveFixedPoints.Prediction.residualPoint_norm_sub_le line 164

Source documentation

Uniform sum-norm coefficient bound for one parent input.

theorem residualPoint_norm_sub_le (parent : I → P) {K : Set X}
    (hdiam : ∀ a ∈ K, ∀ b ∈ K, ‖a - b‖ ≤ 1)
    (y : I → X) (hy : ∀ i, y i ∈ K) (b : X) (hb : b ∈ K)
    (theta eta : I → ℝ) (p : P) :
    ‖residualPoint parent y b theta p - residualPoint parent y b eta p‖ ≤
      ∑ i, |theta i - eta i| := by
…

Mentions: OAI.ReflexiveFixedPoints.Prediction.residualPoint

theorem OAI.ReflexiveFixedPoints.Prediction.weaklyClosed_closedBallImage line 185
Source documentation
The closed norm ball, viewed in the weak topology, is closed.
```
theorem weaklyClosed_closedBallImage (r : ℝ) :
    IsClosed ((toWeakSpace ℝ X) '' Metric.closedBall (0 : X) r) := by
…
```

theorem OAI.ReflexiveFixedPoints.Prediction.norm_sub_le_of_weak_tendsto line 193

Source documentation

A uniform difference bound survives two weak limits along the same proper filter.

theorem norm_sub_le_of_weak_tendsto {F : Filter J} [F.NeBot]
    {a b : J → X} {za zb : X} {r : ℝ}
    (ha : Tendsto (fun j => toWeakSpace ℝ X (a j)) F (𝓝 (toWeakSpace ℝ X za)))
    (hb : Tendsto (fun j => toWeakSpace ℝ X (b j)) F (𝓝 (toWeakSpace ℝ X zb)))
    (hbound : ∀ j, ‖a j - b j‖ ≤ r) :
    ‖za - zb‖ ≤ r := by
…

theorem OAI.ReflexiveFixedPoints.Prediction.lipschitz_of_coefficient_bound line 214

Source documentation

In the default finite Pi metric, a sum-norm coefficient bound has constant card I.

theorem lipschitz_of_coefficient_bound {I X : Type*}
    [Fintype I] [NormedAddCommGroup X] [NormedSpace ℝ X]
    {S : Set (I → ℝ)} (f : S → X)
    (hf : ∀ theta eta, ‖f theta - f eta‖ ≤ ∑ i, |theta.val i - eta.val i|) :
    LipschitzWith (Fintype.card I : ℝ≥0) f := by
…

theorem OAI.ReflexiveFixedPoints.Prediction.continuous_of_coefficient_bound line 232

Source documentation

Continuity here has the norm topology on the target.

theorem continuous_of_coefficient_bound {S : Set (I → ℝ)} (f : S → X)
    (hf : ∀ theta eta, ‖f theta - f eta‖ ≤ ∑ i, |theta.val i - eta.val i|) :
    Continuous f :=
…

theorem OAI.ReflexiveFixedPoints.Prediction.weakLimit_coefficient_bound line 238

Source documentation

Weak convergence after evaluation preserves the coefficient bound.

theorem weakLimit_coefficient_bound {S : Set (I → ℝ)} {F : Filter J} [F.NeBot]
    (q : J → S → X) (z : S → X)
    (hz : ∀ theta, Tendsto (fun j => toWeakSpace ℝ X (q j theta)) F
      (𝓝 (toWeakSpace ℝ X (z theta))))
    (hq : ∀ j theta eta, ‖q j theta - q j eta‖ ≤ ∑ i, |theta.val i - eta.val i|)
    (theta eta : S) :
    ‖z theta - z eta‖ ≤ ∑ i, |theta.val i - eta.val i| :=
…

theorem OAI.ReflexiveFixedPoints.Prediction.continuous_weakLimit_of_coefficient_bound line 248

Source documentation

Uniform coefficient bounds give norm continuity of the already evaluated weak limits.

theorem continuous_weakLimit_of_coefficient_bound {S : Set (I → ℝ)}
    {F : Filter J} [F.NeBot] (q : J → S → X) (z : S → X)
    (hz : ∀ theta, Tendsto (fun j => toWeakSpace ℝ X (q j theta)) F
      (𝓝 (toWeakSpace ℝ X (z theta))))
    (hq : ∀ j theta eta, ‖q j theta - q j eta‖ ≤ ∑ i, |theta.val i - eta.val i|) :
    Continuous z :=
…

theorem OAI.ReflexiveFixedPoints.Prediction.isCompact_weakLimit_image line 257

Source documentation

Compactness of the coefficient space yields norm compactness of the weak-limit image.

theorem isCompact_weakLimit_image (parent : I → P) {F : Filter J} [F.NeBot]
    (q : J → coefficientSet parent → X) (z : coefficientSet parent → X)
    (hz : ∀ theta, Tendsto (fun j => toWeakSpace ℝ X (q j theta)) F
      (𝓝 (toWeakSpace ℝ X (z theta))))
    (hq : ∀ j theta eta, ‖q j theta - q j eta‖ ≤ ∑ i, |theta.val i - eta.val i|) :
    IsCompact (Set.range z) := by
…

Mentions: OAI.ReflexiveFixedPoints.Prediction.coefficientSet