Finite-coordinate truncations in l-one

These are the common finite truncations used in the coherent limit-stage argument. They converge to the original vector and never increase pairwise distance.

noncomputable def ScottishBook155.lpTruncation {ι : Type u} (s : Finset ι) (f : ↥(lp (fun (x : ι) => ℝ) 1)) : ↥(lp (fun (x : ι) => ℝ) 1)

Keep exactly the coordinates in a finite set.

Equations

• ScottishBook155.lpTruncation s f = ∑ i ∈ s, lp.single 1 i (↑f i)

theorem ScottishBook155.lpTruncation_apply {ι : Type u} (s : Finset ι) (f : ↥(lp (fun (x : ι) => ℝ) 1)) (i : ι) : ↑(lpTruncation s f) i = if i ∈ s then ↑f i else 0

theorem ScottishBook155.lpTruncation_zero {ι : Type u} (s : Finset ι) : lpTruncation s 0 = 0

theorem ScottishBook155.lpTruncation_add {ι : Type u} (s : Finset ι) (f g : ↥(lp (fun (x : ι) => ℝ) 1)) : lpTruncation s (f + g) = lpTruncation s f + lpTruncation s g

theorem ScottishBook155.lpTruncation_smul {ι : Type u} (s : Finset ι) (c : ℝ) (f : ↥(lp (fun (x : ι) => ℝ) 1)) : lpTruncation s (c • f) = c • lpTruncation s f

theorem ScottishBook155.lpTruncation_sub {ι : Type u} (s : Finset ι) (f g : ↥(lp (fun (x : ι) => ℝ) 1)) : lpTruncation s (f - g) = lpTruncation s f - lpTruncation s g

theorem ScottishBook155.norm_lpTruncation_le {ι : Type u} (s : Finset ι) (f : ↥(lp (fun (x : ι) => ℝ) 1)) : ‖lpTruncation s f‖ ≤ ‖f‖

Finite-coordinate truncation is contractive in the l-one norm.

theorem ScottishBook155.dist_lpTruncation_le {ι : Type u} (s : Finset ι) (f g : ↥(lp (fun (x : ι) => ℝ) 1)) : dist (lpTruncation s f) (lpTruncation s g) ≤ dist f g

theorem ScottishBook155.lpTruncation_tendsto {ι : Type u} (f : ↥(lp (fun (x : ι) => ℝ) 1)) : Filter.Tendsto (fun (s : Finset ι) => lpTruncation s f) Filter.atTop (nhds f)

Finite truncations converge along the directed set of finite subsets.

noncomputable def ScottishBook155.lpSetTruncation {ι : Type u} (A : Set ι) (f : ↥(lp (fun (x : ι) => ℝ) 1)) : ↥(lp (fun (x : ι) => ℝ) 1)

Restrict an l-one vector to an arbitrary set of coordinates.

Equations

• ScottishBook155.lpSetTruncation A f = ⟨A.indicator ↑f, ⋯⟩

@[simp]

theorem ScottishBook155.lpSetTruncation_apply {ι : Type u} (A : Set ι) (f : ↥(lp (fun (x : ι) => ℝ) 1)) (i : ι) : ↑(lpSetTruncation A f) i = A.indicator (↑f) i

@[reducible, inline]

abbrev ScottishBook155.L1ExtensionSpace (M : Type u_2) (ι : Type u) : Type (max u u_2)

The l-one sum of a normed space and an l-one coordinate space.

Equations

• ScottishBook155.L1ExtensionSpace M ι = WithLp 1 (M × ↥(lp (fun (x : ι) => ℝ) 1))

noncomputable def ScottishBook155.l1ExtensionTruncation {M : Type u_1} {ι : Type u} (s : Finset ι) (x : L1ExtensionSpace M ι) : L1ExtensionSpace M ι

Leave the first summand fixed and truncate the l-one coordinates.

Equations

• ScottishBook155.l1ExtensionTruncation s x = WithLp.toLp 1 (WithLp.fst x, ScottishBook155.lpTruncation s (WithLp.snd x))

noncomputable def ScottishBook155.l1ExtensionSetTruncation {M : Type u_1} {ι : Type u} (A : Set ι) (x : L1ExtensionSpace M ι) : L1ExtensionSpace M ι

Leave the first summand fixed and restrict the l-one tail to an arbitrary set of coordinates.

Equations

• ScottishBook155.l1ExtensionSetTruncation A x = WithLp.toLp 1 (WithLp.fst x, ScottishBook155.lpSetTruncation A (WithLp.snd x))

@[simp]

theorem ScottishBook155.l1ExtensionSetTruncation_fst {M : Type u_1} {ι : Type u} (A : Set ι) (x : L1ExtensionSpace M ι) : WithLp.fst (l1ExtensionSetTruncation A x) = WithLp.fst x

@[simp]

theorem ScottishBook155.l1ExtensionSetTruncation_snd {M : Type u_1} {ι : Type u} (A : Set ι) (x : L1ExtensionSpace M ι) : WithLp.snd (l1ExtensionSetTruncation A x) = lpSetTruncation A (WithLp.snd x)

@[simp]

theorem ScottishBook155.l1ExtensionTruncation_fst {M : Type u_1} {ι : Type u} (s : Finset ι) (x : L1ExtensionSpace M ι) : WithLp.fst (l1ExtensionTruncation s x) = WithLp.fst x

@[simp]

theorem ScottishBook155.l1ExtensionTruncation_snd {M : Type u_1} {ι : Type u} (s : Finset ι) (x : L1ExtensionSpace M ι) : WithLp.snd (l1ExtensionTruncation s x) = lpTruncation s (WithLp.snd x)

theorem ScottishBook155.l1ExtensionTruncation_zero {M : Type u_1} [NormedAddCommGroup M] {ι : Type u} (s : Finset ι) : l1ExtensionTruncation s 0 = 0

theorem ScottishBook155.l1ExtensionTruncation_add {M : Type u_1} [NormedAddCommGroup M] {ι : Type u} (s : Finset ι) (x y : L1ExtensionSpace M ι) : l1ExtensionTruncation s (x + y) = l1ExtensionTruncation s x + l1ExtensionTruncation s y

theorem ScottishBook155.l1ExtensionTruncation_smul {M : Type u_1} [NormedAddCommGroup M] [NormedSpace ℝ M] {ι : Type u} (s : Finset ι) (c : ℝ) (x : L1ExtensionSpace M ι) : l1ExtensionTruncation s (c • x) = c • l1ExtensionTruncation s x

theorem ScottishBook155.dist_l1ExtensionTruncation_le {M : Type u_1} [NormedAddCommGroup M] {ι : Type u} (s : Finset ι) (x y : L1ExtensionSpace M ι) : dist (l1ExtensionTruncation s x) (l1ExtensionTruncation s y) ≤ dist x y

A common coordinate truncation never increases the distance of two points.

theorem ScottishBook155.l1ExtensionTruncation_tendsto {M : Type u_1} [NormedAddCommGroup M] {ι : Type u} (x : L1ExtensionSpace M ι) : Filter.Tendsto (fun (s : Finset ι) => l1ExtensionTruncation s x) Filter.atTop (nhds x)

Product truncations converge while keeping the first summand fixed.

theorem ScottishBook155.l1ExtensionTruncation_common {M : Type u_1} [NormedAddCommGroup M] {ι : Type u} (x y : L1ExtensionSpace M ι) : Filter.Tendsto (fun (s : Finset ι) => l1ExtensionTruncation s x) Filter.atTop (nhds x) ∧ Filter.Tendsto (fun (s : Finset ι) => l1ExtensionTruncation s y) Filter.atTop (nhds y) ∧ ∀ (s : Finset ι), dist (l1ExtensionTruncation s x) (l1ExtensionTruncation s y) ≤ dist x y

The same directed family of finite sets simultaneously approximates a pair, with its distance controlled at every stage.

theorem ScottishBook155.preservesUpTo_of_l1ExtensionTruncations {M : Type u_1} [NormedAddCommGroup M] {ι : Type u} {N : Type u_2} [MetricSpace N] {V : L1ExtensionSpace M ι → N} {r : ℝ} (hV : Continuous V) (hfinite : ∀ (s : Finset ι) (x y : L1ExtensionSpace M ι), dist (l1ExtensionTruncation s x) (l1ExtensionTruncation s y) ≤ r → dist (V (l1ExtensionTruncation s x)) (V (l1ExtensionTruncation s y)) = dist (l1ExtensionTruncation s x) (l1ExtensionTruncation s y)) : PreservesUpTo r V

If a continuous map preserves the distances of every common finite truncation, then it preserves the corresponding distance in the full l-one sum.

theorem ScottishBook155.eq_of_eventually_l1ExtensionSetTruncation_eq {M : Type u_1} {ι : Type u} {A : Type u_2} {l : Filter A} [l.NeBot] (sets : A → Set ι) (hcover : ∀ (i : ι), ∀ᶠ (a : A) in l, i ∈ sets a) {x y : L1ExtensionSpace M ι} (hxy : ∀ᶠ (a : A) in l, l1ExtensionSetTruncation (sets a) x = l1ExtensionSetTruncation (sets a) y) : x = y

Prefix restrictions which eventually contain every coordinate jointly separate the l-one sum.