PointwiseWeakApproximation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous approximation in the pointwise weak topology

A convex family of weak-valued maps can approximate each point in its closure in norm at any prescribed finite family of arguments. The finite family is handled as one vector in the finite product normed space. Consequently the chosen approximating map is the same at every argument.

No completeness, reflexivity, or nontriviality assumption is required here.

def OAI.ReflexiveFixedPoints.finiteNormEvaluation line 34
Source documentation
The underlying normed tuple at a prescribed family of arguments. This is a linear map, without a claim of weak-to-norm continuity.
```
def finiteNormEvaluation (a : ι → α) :
    (α → WeakSpace ℝ X) →ₗ[ℝ] (ι → X) :=
…
```
theorem OAI.ReflexiveFixedPoints.finiteNormEvaluation_apply line 39
theorem OAI.ReflexiveFixedPoints.continuous_finite_weak_evaluation line 47
Source documentation
Finite evaluation is continuous when its target has the weak topology of the finite product normed space.
```
theorem continuous_finite_weak_evaluation (a : ι → α) :
    Continuous (fun f : α → WeakSpace ℝ X =>
      toWeakSpace ℝ (ι → X) (finiteNormEvaluation a f)) := by
…
```
Mentions: OAI.ReflexiveFixedPoints.finiteNormEvaluation

theorem OAI.ReflexiveFixedPoints.exists_mem_norm_approx_of_mem_pointwiseWeak_closure line 72

Source documentation

One member of a convex family approximates a point of its pointwise weak closure simultaneously in norm at every argument in a finite indexed family. The index type is allowed to be empty, and arguments may repeat.

theorem exists_mem_norm_approx_of_mem_pointwiseWeak_closure
    {s : Set (α → WeakSpace ℝ X)} (hs : Convex ℝ s)
    {f : α → WeakSpace ℝ X} (hf : f ∈ closure s)
    (a : ι → α) {ε : ℝ} (hε : 0 < ε) :
    ∃ g ∈ s, ∀ i,
      ‖(toWeakSpace ℝ X).symm (g (a i)) -
        (toWeakSpace ℝ X).symm (f (a i))‖ < ε := by
…

theorem OAI.ReflexiveFixedPoints.exists_mem_norm_approx_finset_of_mem_pointwiseWeak_closure line 99

Source documentation

Finset form of simultaneous norm approximation from pointwise weak closure. In particular, separate choices at different arguments are not used.

theorem exists_mem_norm_approx_finset_of_mem_pointwiseWeak_closure
    {s : Set (α → WeakSpace ℝ X)} (hs : Convex ℝ s)
    {f : α → WeakSpace ℝ X} (hf : f ∈ closure s)
    (t : Finset α) {ε : ℝ} (hε : 0 < ε) :
    ∃ g ∈ s, ∀ x ∈ t,
      ‖(toWeakSpace ℝ X).symm (g x) -
        (toWeakSpace ℝ X).symm (f x)‖ < ε := by
…

theorem OAI.ReflexiveFixedPoints.mem_closure_of_finite_dist_approx line 115
Source documentation
Simultaneous approximation on every finite set of arguments implies membership in the product-topology closure. This uses only the codomain's pseudometric, so it applies directly to maps taking values in a norm subtype.
```
theorem mem_closure_of_finite_dist_approx
    {Y : Type u} [PseudoMetricSpace Y]
    {B : Set (α → Y)} {f : α → Y}
    (h : ∀ (s : Finset α) (ε : ℝ), 0 < ε →
      ∃ g ∈ B, ∀ a ∈ s, dist (g a) (f a) < ε) :
    f ∈ closure B := by
…
```