Closed discs inside the closed unit disc

For a, c ∈ K, the closed subdisc D(a, |c|) of the closed unit disc Spa (K⟨T⟩, K⟨T⟩°) is the rational subset

D(a, |c|) = {v : v(T - a) ≤ v(c) ≠ 0} = R({T - a, c} / c).

These are the basic rational subdomains of the closed unit disc. This file locates the classical points, the points η_{b,r} and the rank-two points η_{r±} relative to them. Over a complete nonarchimedean field K:

• a classical point x_b lies in D(a, |c|) exactly when ‖b - a‖ ≤ ‖c‖ and c ≠ 0, whatever point of Spa (K, K°) it is built from. Every point of Spa (K, K°) compares elements of K by their norms (TauCeti.ValuationSpectrum.vle_iff_norm_le_of_mem_spa), and so does every point of the closed polydisc on constants (TauCeti.ValuationSpectrum.closedPolydisc_vle_weightedC_iff);
• the point η_{b,r} lies in D(a, |c|) exactly when ‖b - a‖ ≤ ‖c‖ and r ≤ ‖c‖;
• about the origin, η_{r⁻} lies in D(0, |c|) exactly when r ≤ ‖c‖, while η_{r⁺} does exactly when r < ‖c‖. At ‖c‖ = r the disc contains η_r and η_{r⁻} but not η_{r⁺}, although η_{r⁺} is a specialization of η_r: the rank-two point η_{r⁺} lies outside the closed disc of radius r. The same holds about every centre: η_{b,r⁻} lies in D(a, |c|) exactly when ‖b - a‖ ≤ ‖c‖ and r ≤ ‖c‖, and η_{b,r⁺} exactly when ‖b - a‖ ≤ ‖c‖ and r < ‖c‖.

The points η_{b,r} also determine the discs themselves. For ‖a‖ ≤ 1 and 0 < ‖c‖ ≤ 1, D(a, |c|) ⊆ D(b, |d|) exactly when ‖a - b‖ ≤ ‖d‖ and ‖c‖ ≤ ‖d‖, and two such discs are equal exactly when their radii agree and each centre lies in the other disc. If max ‖c‖ ‖d‖ < ‖a - b‖, the discs D(a, |c|) and D(b, |d|) are disjoint.

Main definitions

• TauCeti.ValuationSpectrum.closedSubdisc: the rational subset D(a, |c|) of the closed unit disc.

Main results

• TauCeti.ValuationSpectrum.closedSubdisc_eq_rationalSubset, TauCeti.ValuationSpectrum.isOpen_closedSubdisc, TauCeti.ValuationSpectrum.closedSubdisc_mem_spaRationalFamily and TauCeti.ValuationSpectrum.isCompact_closedSubdisc: D(a, |c|) is the rational subset R({T - a, c} / c), hence open and, when T - a and c generate an open ideal (for instance when c is a unit), a member of the rational family and quasi-compact.
• TauCeti.ValuationSpectrum.closedSubdisc_zero_one: D(0, 1) is the whole closed unit disc, and TauCeti.ValuationSpectrum.closedSubdisc_zero_right: D(a, |0|) is empty.
• TauCeti.ValuationSpectrum.closure_closedSubdisc_subset_closedSubdisc: strictly enlarging a radius contains the closure of the smaller disc.
• TauCeti.ValuationSpectrum.isClosed_iInter_closedSubdisc: an intersection of discs is closed when every disc contains a member of the family with strictly smaller radius.
• TauCeti.ValuationSpectrum.isClosed_iInter_closedSubdisc_of_no_common_point: a decreasing sequence with no common point in K has closed intersection in the adic unit disc.
• TauCeti.ValuationSpectrum.classicalPoint_mem_closedSubdisc_iff, TauCeti.ValuationSpectrum.gaussPoint_mem_closedSubdisc_iff, TauCeti.ValuationSpectrum.discPoint_mem_closedSubdisc_iff, TauCeti.ValuationSpectrum.gaussPointBelow_mem_closedSubdisc_zero_iff and TauCeti.ValuationSpectrum.gaussPointAbove_mem_closedSubdisc_zero_iff, TauCeti.ValuationSpectrum.discPointBelow_mem_closedSubdisc_iff and TauCeti.ValuationSpectrum.discPointAbove_mem_closedSubdisc_iff: which points of the closed unit disc lie in D(a, |c|).
• TauCeti.ValuationSpectrum.closedSubdisc_subset_closedSubdisc_iff, TauCeti.ValuationSpectrum.closedSubdisc_eq_closedSubdisc_iff and TauCeti.ValuationSpectrum.disjoint_closedSubdisc: inclusion, equality and disjointness of discs.
• TauCeti.ValuationSpectrum.exists_closedSubdisc_inter_closedSubdisc_eq: the intersection of two discs is a disc, possibly the empty disc D(a, |0|).
• TauCeti.ValuationSpectrum.valuation_weightedX_sub_weightedC_of_mem_closedSubdisc: a point of D(a, |c|) takes the value of the constant a - b on T - b for every b outside the disc.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Example 7.57.
• S. Bosch, U. Güntzer, R. Remmert, Non-Archimedean Analysis, §7.2, for rational subdomains of affinoid spaces.
• P. Scholze, Perfectoid spaces, Publ. Math. IHÉS 116 (2012), Example 2.20, for the points of type (5).

The discs as rational subsets

noncomputable def TauCeti.ValuationSpectrum.closedSubdisc {K : Type u_1} [CommRing K] [TopologicalSpace K] [NonarchimedeanRing K] (a c : K) : Set ↑(closedPolydisc 1 K)

The closed subdisc D(a, |c|) of the closed unit disc: the rational subset {v : v(T - a) ≤ v(c) ≠ 0}. For a nonarchimedean normed field K, ‖a‖ ≤ 1 and 0 < ‖c‖ ≤ 1, this is the closed disc of radius ‖c‖ about a.

@[simp]

theorem TauCeti.ValuationSpectrum.mem_closedSubdisc {K : Type u_1} [CommRing K] [TopologicalSpace K] [NonarchimedeanRing K] (a c : K) (v : ↑(closedPolydisc 1 K)) : v ∈ closedSubdisc a c ↔ Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a ≤ᵥ (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) c ∧ ¬(Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) c ≤ᵥ 0

Membership in D(a, |c|) is the defining valuation inequality and nonvanishing.

theorem TauCeti.ValuationSpectrum.isOpen_closedSubdisc {K : Type u_1} [CommRing K] [TopologicalSpace K] [NonarchimedeanRing K] (a c : K) : IsOpen (closedSubdisc a c)

Each disc D(a, |c|) is open in the closed unit disc.

theorem TauCeti.ValuationSpectrum.closedSubdisc_eq_rationalSubset {K : Type u_1} [CommRing K] [TopologicalSpace K] [NonarchimedeanRing K] (a c : K) : closedSubdisc a c = Subtype.val ⁻¹' rationalSubset (Huber.powerBoundedSubring ↥(Huber.weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)) {Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a, (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) c} ((Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) c)

D(a, |c|) is the rational subset R({T - a, c} / c). Including the denominator among the numerators makes the admissibility of the presentation explicit when c is a unit.

theorem TauCeti.ValuationSpectrum.closedSubdisc_mem_spaRationalFamily {K : Type u_1} [CommRing K] [TopologicalSpace K] [NonarchimedeanRing K] (a c : K) (hT : IsOpen ↑(Ideal.span {Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a, (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) c})) : ⇑(Homeomorph.setCongr ⋯).symm ⁻¹' closedSubdisc a c ∈ spaRationalFamily (Huber.powerBoundedSubring ↥(Huber.weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯))

D(a, |c|) belongs to the rational family of Spa (K⟨T⟩, K⟨T⟩°) when the numerators T - a and c of R({T - a, c} / c) generate an open ideal, for instance when c is a unit.

theorem TauCeti.ValuationSpectrum.isCompact_closedSubdisc {K : Type u_1} [CommRing K] [TopologicalSpace K] [NonarchimedeanRing K] [Huber.IsHuberRing K] (a c : K) (hT : IsOpen ↑(Ideal.span {Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a, (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) c})) : IsCompact (closedSubdisc a c)

D(a, |c|) is quasi-compact over a Huber ring when T - a and c generate an open ideal, for instance when c is a unit.

@[simp]

theorem TauCeti.ValuationSpectrum.closedSubdisc_zero_one {K : Type u_1} [CommRing K] [TopologicalSpace K] [NonarchimedeanRing K] : closedSubdisc 0 1 = Set.univ

D(0, 1) is the whole closed unit disc: the variable is power-bounded, so every point of the disc has v(T) ≤ 1.

@[simp]

theorem TauCeti.ValuationSpectrum.closedSubdisc_zero_right {K : Type u_1} [CommRing K] [TopologicalSpace K] [NonarchimedeanRing K] (a : K) : closedSubdisc a 0 = ∅

D(a, |0|) is empty: no point has v(0) ≠ 0.

Discs over a normed field

theorem TauCeti.ValuationSpectrum.closedSubdisc_eq_setOf_vle {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] (a : K) {c : K} (hc : c ≠ 0) : closedSubdisc a c = {v : ↑(closedPolydisc 1 K) | Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a ≤ᵥ (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) c}

A disc D(a, |c|) of nonzero radius is cut out by its defining inequality v(T - a) ≤ v(c) alone: the nonvanishing condition v(c) ≠ 0 is automatic.

theorem TauCeti.ValuationSpectrum.closedSubdisc_subset_closedSubdisc {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {a b c d : K} (hab : ‖a - b‖ ≤ ‖d‖) (hcd : ‖c‖ ≤ ‖d‖) : closedSubdisc a c ⊆ closedSubdisc b d

Nested discs: D(a, |c|) ⊆ D(b, |d|) whenever ‖a - b‖ ≤ ‖d‖ and ‖c‖ ≤ ‖d‖.

theorem TauCeti.ValuationSpectrum.closure_closedSubdisc_subset_closedSubdisc {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {a c d : K} (hcd : ‖c‖ < ‖d‖) : closure (closedSubdisc a c) ⊆ closedSubdisc a d

Strict enlargement of the radius contains the closure of a closed subdisc.

theorem TauCeti.ValuationSpectrum.isClosed_iInter_closedSubdisc {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {ι : Sort u_2} (a c : ι → K) (hrefine : ∀ (i : ι), ∃ (j : ι), ‖a j - a i‖ ≤ ‖c i‖ ∧ ‖c j‖ < ‖c i‖) : IsClosed (⋂ (i : ι), closedSubdisc (a i) (c i))

An intersection of discs is closed if each disc contains a disc of the family with strictly smaller radius. The centres may vary, and the family need not be a sequence.

theorem TauCeti.ValuationSpectrum.isClosed_iInter_closedSubdisc_of_no_common_point {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] (a c : ℕ → K) (hac : ∀ (n : ℕ), ‖a (n + 1) - a n‖ ≤ ‖c n‖) (hcc : ∀ (n : ℕ), ‖c (n + 1)‖ ≤ ‖c n‖) (hempty : ∀ (b : K), ∃ (n : ℕ), ‖c n‖ < ‖b - a n‖) : IsClosed (⋂ (n : ℕ), closedSubdisc (a n) (c n))

A decreasing sequence of discs with no common point in the ground field has closed intersection in the adic unit disc. Its adic intersection need not be empty.

theorem TauCeti.ValuationSpectrum.closedSubdisc_eq_univ {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {a c : K} (ha : ‖a‖ ≤ 1) (hc : 1 ≤ ‖c‖) : closedSubdisc a c = Set.univ

A disc whose radius parameter has norm at least one, about a centre in the closed unit disc, is the whole closed unit disc.

theorem TauCeti.ValuationSpectrum.disjoint_closedSubdisc {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {a b c d : K} (h : max ‖c‖ ‖d‖ < ‖a - b‖) : Disjoint (closedSubdisc a c) (closedSubdisc b d)

Far-apart discs are disjoint: if max ‖c‖ ‖d‖ < ‖a - b‖, no point lies in both D(a, |c|) and D(b, |d|), since at such a point a - b = (T - b) - (T - a) would be dominated by c or d.

theorem TauCeti.ValuationSpectrum.exists_closedSubdisc_inter_closedSubdisc_eq {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] (a b c d : K) : ∃ (e : K) (r : K), closedSubdisc a c ∩ closedSubdisc b d = closedSubdisc e r

The intersection of two discs is a disc: either one of D(a, |c|) and D(b, |d|) contains the other, or they are disjoint and their intersection is the empty disc D(a, |0|).

theorem TauCeti.ValuationSpectrum.valuation_weightedX_sub_weightedC_of_mem_closedSubdisc {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {x : ↑(closedPolydisc 1 K)} {a c : K} (hx : x ∈ closedSubdisc a c) {b : K} (hb : ‖c‖ < ‖b - a‖) : (↑x).valuation (Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) b) = (↑x).valuation ((Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) (a - b))

A point of D(a, |c|) takes the value of the constant a - b on T - b for every b outside the disc: there T - b = (T - a) + (a - b) with x(T - a) ≤ x(c) < x(a - b).

theorem TauCeti.ValuationSpectrum.classicalPoint_mem_closedSubdisc_iff {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] [CompleteSpace K] (x : ↑(spa (Huber.powerBoundedSubring K))) (b : Fin 1 → K) (hb : ∀ (i : Fin 1), Huber.IsPowerBounded (b i)) (a c : K) : classicalPoint x b hb ∈ closedSubdisc a c ↔ ‖b 0 - a‖ ≤ ‖c‖ ∧ c ≠ 0

A classical point x_b lies in D(a, |c|) exactly when ‖b - a‖ ≤ ‖c‖ and c ≠ 0, whichever point x of Spa (K, K°) it is built from.

The points of the disc in D(a, |c|)

theorem TauCeti.ValuationSpectrum.gaussPoint_mem_closedSubdisc_iff {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {r : ℝ} (hr₀ : 0 < r) (hr₁ : r ≤ 1) (a c : K) : gaussPoint hr₀ hr₁ ∈ closedSubdisc a c ↔ ‖a‖ ≤ ‖c‖ ∧ r ≤ ‖c‖

The Gauss point η_r lies in D(a, |c|) exactly when ‖a‖ ≤ ‖c‖ and r ≤ ‖c‖, since its Gauss norm of T - a is max r ‖a‖.

theorem TauCeti.ValuationSpectrum.gaussPointBelow_mem_closedSubdisc_zero_iff {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {r : ℝ} (hr₀ : 0 < r) (hr₁ : r ≤ 1) (c : K) : gaussPointBelow hr₀ hr₁ ∈ closedSubdisc 0 c ↔ r ≤ ‖c‖

η_{r⁻} lies in D(0, |c|) exactly when r ≤ ‖c‖. At ‖c‖ = r the constant c is strictly larger than T just below radius r.

theorem TauCeti.ValuationSpectrum.gaussPointAbove_mem_closedSubdisc_zero_iff {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {r : ℝ} (hr₀ : 0 < r) (hr₁ : r < 1) (c : K) : gaussPointAbove hr₀ hr₁ ∈ closedSubdisc 0 c ↔ r < ‖c‖

η_{r⁺} lies in D(0, |c|) exactly when r < ‖c‖. At ‖c‖ = r the variable T is strictly larger than c just above radius r, so the disc of radius r contains η_r and η_{r⁻} but not η_{r⁺}.

theorem TauCeti.ValuationSpectrum.discPoint_mem_closedSubdisc_iff {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {r : ℝ} [CompleteSpace K] (b : K) (hb : ‖b‖ ≤ 1) (hr₀ : 0 < r) (hr₁ : r ≤ 1) (a c : K) : discPoint b hb hr₀ hr₁ ∈ closedSubdisc a c ↔ ‖b - a‖ ≤ ‖c‖ ∧ r ≤ ‖c‖

The point η_{b,r} lies in D(a, |c|) exactly when ‖b - a‖ ≤ ‖c‖ and r ≤ ‖c‖. Translating by b turns T - a into T - (a - b), whose Gauss norm of radius r is max r ‖a - b‖.

theorem TauCeti.ValuationSpectrum.closedSubdisc_subset_closedSubdisc_iff {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] [CompleteSpace K] {a c : K} (ha : ‖a‖ ≤ 1) (hc₀ : c ≠ 0) (hc₁ : ‖c‖ ≤ 1) (b d : K) : closedSubdisc a c ⊆ closedSubdisc b d ↔ ‖a - b‖ ≤ ‖d‖ ∧ ‖c‖ ≤ ‖d‖

Inclusion of discs: for ‖a‖ ≤ 1 and 0 < ‖c‖ ≤ 1, D(a, |c|) ⊆ D(b, |d|) exactly when ‖a - b‖ ≤ ‖d‖ and ‖c‖ ≤ ‖d‖. The point η_{a,‖c‖} of D(a, |c|) witnesses the forward direction.

theorem TauCeti.ValuationSpectrum.closedSubdisc_eq_closedSubdisc_iff {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] [CompleteSpace K] {a b c d : K} (ha : ‖a‖ ≤ 1) (hb : ‖b‖ ≤ 1) (hc₀ : c ≠ 0) (hc₁ : ‖c‖ ≤ 1) (hd₀ : d ≠ 0) (hd₁ : ‖d‖ ≤ 1) : closedSubdisc a c = closedSubdisc b d ↔ ‖c‖ = ‖d‖ ∧ ‖a - b‖ ≤ ‖c‖

Equality of discs: for centres in the closed unit disc and radius parameters of norm in (0, 1], D(a, |c|) = D(b, |d|) exactly when ‖c‖ = ‖d‖ and ‖a - b‖ ≤ ‖c‖.

theorem TauCeti.ValuationSpectrum.discPointAbove_mem_closedSubdisc_iff {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {r : ℝ} [CompleteSpace K] (b : K) (hb : ‖b‖ ≤ 1) (hr₀ : 0 < r) (hr₁ : r < 1) (a c : K) : discPointAbove b hb hr₀ hr₁ ∈ closedSubdisc a c ↔ ‖b - a‖ ≤ ‖c‖ ∧ r < ‖c‖

The point η_{b,r⁺} lies in D(a, |c|) exactly when ‖b - a‖ ≤ ‖c‖ and r < ‖c‖. On T - a it takes the value of the constant a - b when r < ‖a - b‖, and otherwise a value just above the constants of norm r.

theorem TauCeti.ValuationSpectrum.discPointBelow_mem_closedSubdisc_iff {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {r : ℝ} [CompleteSpace K] (b : K) (hb : ‖b‖ ≤ 1) (hr₀ : 0 < r) (hr₁ : r ≤ 1) (a c : K) : discPointBelow b hb hr₀ hr₁ ∈ closedSubdisc a c ↔ ‖b - a‖ ≤ ‖c‖ ∧ r ≤ ‖c‖

The point η_{b,r⁻} lies in D(a, |c|) exactly when ‖b - a‖ ≤ ‖c‖ and r ≤ ‖c‖, as for η_{b,r}. On T - a it takes the value of the constant a - b when r ≤ ‖a - b‖, and otherwise a value just below the constants of norm r.

theorem TauCeti.ValuationSpectrum.valuation_weightedX_sub_weightedC_lt_of_one_lt {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] (x : ↑(closedPolydisc 1 K)) {b b' : K} (hb : ‖b‖ ≤ 1) (hb' : 1 < ‖b'‖) : (↑x).valuation (Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) b) < (↑x).valuation (Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) b')

For b in the unit disc and b' off it, x(T - b) ≤ x(1) < x(b') = x(T - b').

theorem TauCeti.ValuationSpectrum.exists_forall_mem_closedSubdisc {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {x : ↑(closedPolydisc 1 K)} (hmin : ¬∃ (a₀ : K), ∀ (b : K), Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a₀ ≤ᵥ Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) b) : ∃ (a : ℕ → K) (c : ℕ → K), (∀ (n : ℕ), ‖a n‖ ≤ 1) ∧ (∀ (n : ℕ), c n ≠ 0) ∧ (∀ (n : ℕ), ‖c n‖ ≤ 1) ∧ (∀ (n : ℕ), ‖a (n + 1) - a n‖ ≤ ‖c n‖) ∧ (∀ (n : ℕ), ‖c (n + 1)‖ ≤ ‖c n‖) ∧ (∀ (b : K), ∃ (n : ℕ), ‖c n‖ < ‖b - a n‖) ∧ ∀ (n : ℕ), x ∈ closedSubdisc (a n) (c n)

A point on which b ↦ x(T - b) attains no minimum lies in a decreasing sequence of discs with no common point. Every value x(T - b) is the value x(e) of a constant, and the norms ‖e‖ for ‖b‖ ≤ 1 have an infimum which is not attained, since an e attaining it would make b a minimum. The discs D(b, |e|) along a sequence of norms decreasing to this infimum work.